From c01afac0ab092af1cfb9493830ec8d21114032fb Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 10 Oct 2013 18:10:13 +0200 Subject: [PATCH] TypeClass: unification algorithm is now TC aware. --- src/ecCoreHiLogic.ml | 5 +- src/ecCoreHiPhl.ml | 7 +- src/ecEnv.ml | 13 ++- src/ecEnv.mli | 18 ++-- src/ecHiLogic.ml | 4 +- src/ecScope.ml | 11 +- src/ecThCloning.ml | 1 + src/ecTyping.ml | 4 +- src/ecUnify.ml | 233 +++++++++++++++++++++++++------------------ src/ecUnify.mli | 14 +-- src/ecUtils.ml | 2 + src/ecUtils.mli | 2 + 12 files changed, 184 insertions(+), 130 deletions(-) diff --git a/src/ecCoreHiLogic.ml b/src/ecCoreHiLogic.ml index b4ddedbbb5..ccf9dedc6f 100644 --- a/src/ecCoreHiLogic.ml +++ b/src/ecCoreHiLogic.ml @@ -13,6 +13,7 @@ open EcLogic open EcMetaProg module TT = EcTyping +module TC = EcTypeClass module Muid = EcUidgen.Muid @@ -47,7 +48,7 @@ let process_exp hyps e oty = let env = LDecl.toenv hyps in let ue = EcUnify.UniEnv.create (Some (LDecl.tohyps hyps).h_tvar) in let e = TT.transexpcast_opt env ue oty e in - EcTypes.e_uni (EcUnify.UniEnv.close ue) e + EcTypes.e_uni (EcUnify.UniEnv.close ue) e (* -------------------------------------------------------------------- *) type pterm_parg = @@ -170,7 +171,7 @@ let process_named_pterm _loc hyps (fp, tvi) = tyargs end; - let fs = EcUnify.UniEnv.freshen_ue ue typ tvi in + let fs = EcUnify.UniEnv.opentvi ue typ tvi in let ax = Fsubst.subst_tvar fs ax in (* FIXME: TC HOOK *) let typ = List.map (fun (a, _) -> EcIdent.Mid.find a fs) typ in diff --git a/src/ecCoreHiPhl.ml b/src/ecCoreHiPhl.ml index fbf61d5faf..976883cfa1 100644 --- a/src/ecCoreHiPhl.ml +++ b/src/ecCoreHiPhl.ml @@ -50,9 +50,10 @@ let process_phl_formula = process_phl_form tbool let process_prhl_formula = process_prhl_form tbool let process_prhl_stmt side g c = - let hyps,concl = get_goal g in - let es = EcCorePhl.t_as_equivS concl in - let mt = snd (if side then es.es_ml else es.es_mr) in + let (hyps, concl) = get_goal g in + + let es = EcCorePhl.t_as_equivS concl in + let mt = snd (if side then es.es_ml else es.es_mr) in let hyps = LDecl.push_active (mhr,mt) hyps in let env = LDecl.toenv hyps in let ue = EcUnify.UniEnv.create (Some (LDecl.tohyps hyps).EcBaseLogic.h_tvar) in diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 778223da09..df4fe1ebf7 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -17,6 +17,7 @@ module Msym = EcSymbols.Msym module Mp = EcPath.Mp module Sid = EcIdent.Sid module Mid = EcIdent.Mid +module TC = EcTypeClass (* -------------------------------------------------------------------- *) type 'a suspension = { @@ -1599,7 +1600,6 @@ end (* -------------------------------------------------------------------- *) module NormMp = struct - let rec norm_mpath_for_typing env p = let (ip, (i, args)) = ipath_of_mpath p in match Mod.by_ipath_r true ip env with @@ -2143,7 +2143,6 @@ end module TypeClass = struct type t = unit - let by_path_opt (p : EcPath.path) (env : env) = omap check_not_suspended @@ -2163,6 +2162,14 @@ module TypeClass = struct let env = { env with env_item = CTh_typeclass name :: env.env_item } in (* FIXME: TC HOOK *) env + + let graph (_env : env) = + (* FIXME: TC HOOK *) + TC.Graph.empty + + let tc_of_typename (_p : EcPath.path) (_env : env) = + (* FIXME: TC HOOK *) + Sp.empty end (* -------------------------------------------------------------------- *) @@ -2631,7 +2638,7 @@ module LDecl = struct | LD_hyp _ -> env | LD_abs_st us -> AbsStmt.bind x us env - let add_local x k h = + let add_local x k h = let nhyps = add_local x k (tohyps h) in let env = h.le_env in let nenv = add_local_env x k env in diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 218938ac5c..f342943510 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -196,14 +196,15 @@ end (* -------------------------------------------------------------------- *) module NormMp : sig + type use = { + us_pv : ty EcPath.Mx.t; + us_gl : EcIdent.Sid.t; + } + val norm_mpath : env -> mpath -> mpath val norm_xpath : env -> xpath -> xpath val norm_pvar : env -> EcTypes.prog_var -> EcTypes.prog_var val norm_form : env -> form -> form - type use = - { us_pv : ty EcPath.Mx.t; - us_gl : EcIdent.Sid.t; - } val mod_use : env -> mpath -> use val fun_use : env -> xpath -> use val norm_restr : env -> mod_restr -> use @@ -294,8 +295,11 @@ end module TypeClass : sig type t = unit - val add : path -> env -> env - val bind : symbol -> t -> env -> env + val add : path -> env -> env + val bind : symbol -> t -> env -> env + val graph : env -> EcTypeClass.graph + + val tc_of_typename : path -> env -> Sp.t end (* -------------------------------------------------------------------- *) @@ -337,7 +341,7 @@ module LDecl : sig type hyps - val init : env -> EcIdent.t list -> hyps + val init : env -> EcIdent.t list -> hyps val tohyps : hyps -> EcBaseLogic.hyps val toenv : hyps -> env diff --git a/src/ecHiLogic.ml b/src/ecHiLogic.ml index 6ad978d0d8..1e1462e2d0 100644 --- a/src/ecHiLogic.ml +++ b/src/ecHiLogic.ml @@ -764,7 +764,7 @@ let process_generalize l = let process_elimT loc (pf, qs) g = let noelim () = tacuerror "cannot recognize elimination principle" in - let (env, hyps, concl) = get_goal_e g in + let (hyps, concl) = get_goal g in let pf = process_form_opt hyps pf None in let (p, typs, ue, ax) = @@ -780,7 +780,7 @@ let process_elimT loc (pf, qs) g = in begin - try EcUnify.unify env ue (tfun pf.f_ty tbool) xpty + try EcUnify.unify (LDecl.toenv hyps) ue (tfun pf.f_ty tbool) xpty with EcUnify.UnificationFailure _ -> noelim () end; diff --git a/src/ecScope.ml b/src/ecScope.ml index 4330a061a1..d4483a5500 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -929,14 +929,15 @@ module Op = struct let tyop = EcDecl.mk_op tparams ty body in if op.po_kind = `Const then begin - let tue, ty, _ = EcUnify.UniEnv.freshen ue tparams None ty in - let tdom = EcUnify.UniEnv.fresh tue in - let tcom = EcUnify.UniEnv.fresh tue in - let tfun = EcTypes.tfun tdom tcom in + let tue = EcUnify.UniEnv.copy ue in + let ty, _ = EcUnify.UniEnv.openty tue tparams None ty in + let tdom = EcUnify.UniEnv.fresh tue in + let tcom = EcUnify.UniEnv.fresh tue in + let tfun = EcTypes.tfun tdom tcom in try EcUnify.unify (env scope) tue ty tfun; - let msg = "this operator type is (unifiable) to an function type" in + let msg = "this operator type is (unifiable) to a function type" in hierror ~loc "%s" msg with EcUnify.UnificationFailure _ -> () end; diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index a184eb1142..00be3e72cd 100644 --- a/src/ecThCloning.ml +++ b/src/ecThCloning.ml @@ -364,6 +364,7 @@ let clone (scenv : EcEnv.env) (thcl : theory_cloning) = let nargs = List.map2 (fun (_, tc) x -> (EcIdent.create (unloc x), tc)) otyd.tyd_params nargs in + (* FIXME: TC HOOK *) let ue = EcUnify.UniEnv.create (Some (List.map fst nargs)) in let ntyd = EcTyping.transty EcTyping.tp_tydecl scenv ue ntyd in diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 3dac3b9f2d..ccdf721224 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -500,9 +500,9 @@ let rec transty (tp : typolicy) (env : EcEnv.env) ue ty = and transtys tp (env : EcEnv.env) ue tys = List.map (transty tp env ue) tys -let transty_for_decl = +let transty_for_decl env ty = let ue = UE.create (Some []) in - fun env ty -> transty tp_nothing env ue ty + transty tp_nothing env ue ty (* -------------------------------------------------------------------- *) let transpattern1 env ue (p : EcParsetree.plpattern) = diff --git a/src/ecUnify.ml b/src/ecUnify.ml index f109868a56..2b338e1648 100644 --- a/src/ecUnify.ml +++ b/src/ecUnify.ml @@ -2,15 +2,21 @@ open EcMaps open EcUtils open EcUidgen +open EcSymbols open EcIdent open EcTypes open EcDecl +module Sp = EcPath.Sp +module TC = EcTypeClass + (* -------------------------------------------------------------------- *) exception UnificationFailure of ty * ty exception UninstanciateUni (* -------------------------------------------------------------------- *) +type pb = [ `TyUni of ty * ty | `TcCtt of ty * Sp.t ] + module UFArgs = struct module I = struct type t = uid @@ -20,33 +26,62 @@ module UFArgs = struct end module D = struct - type data = ty option - type effects = (ty * ty) list + type data = Sp.t * ty option + type effects = pb list let default : data = - None + (Sp.empty, None) - let isvoid (x : data) = (x = None) + let isvoid ((_, x) : data) = + (x = None) let noeffects : effects = [] let union d1 d2 = match d1, d2 with - | None, None -> (None, []) - | None, d -> (d , []) - | d, None -> (d , []) + | (tc1, None), (tc2, None) -> + ((Sp.union tc1 tc2, None), []) + + | (tc1, Some ty1), (tc2, Some ty2) -> + ((Sp.union tc1 tc2, Some ty1), [`TyUni (ty1, ty2)]) + + | (tc1, None ), (tc2, Some ty) + | (tc2, Some ty), (tc1, None ) -> + let tc = Sp.diff tc2 tc1 in + if Sp.is_empty tc + then ((Sp.union tc1 tc2, Some ty), []) + else ((Sp.union tc1 tc2, Some ty), [`TcCtt (ty, tc)]) - | Some ty1, Some ty2 -> (Some ty1, [ty1, ty2]) end end module UF = EcUFind.Make(UFArgs.I)(UFArgs.D) (* -------------------------------------------------------------------- *) -let unify_core (env : EcEnv.env) (uf : UF.t) t1 t2 = +type tvtc = TC.nodes + +let hastc env tvtc ty tc = + let tytc = + match ty.ty_node with + | Tvar x -> odfl Sp.empty (Mid.find_opt x tvtc) + | Tconstr (p, _) -> EcEnv.TypeClass.tc_of_typename p env + | _ -> Sp.empty + + and gr = EcEnv.TypeClass.graph env in + + Sp.for_all + (fun dst -> + let check = fun src -> TC.Graph.has_path ~src ~dst gr in + Sp.exists check tytc) + tc + +let unify_core (env : EcEnv.env) (tvtc : Sp.t Mid.t) (uf : UF.t) t1 t2 = let failure () = raise (UnificationFailure (t1, t2)) in - let ocheck uf i t = + let uf = ref uf in + let pb = let x = Queue.create () in Queue.push (`TyUni (t1, t2)) x; x in + + let ocheck i t = let map = Hint.create 0 in let rec doit t = @@ -54,7 +89,7 @@ let unify_core (env : EcEnv.env) (uf : UF.t) t1 t2 = | Tunivar i' when uid_equal i i' -> true | Tunivar i' when Hint.mem map i' -> false | Tunivar i' -> begin - match UF.data i' uf with + match snd (UF.data i' !uf) with | None -> Hint.add map i' (); false | Some t -> begin match doit t with @@ -68,61 +103,62 @@ let unify_core (env : EcEnv.env) (uf : UF.t) t1 t2 = doit t in - let rec unify uf pb = - let setvar i t = - if ocheck uf i t then failure (); - let (ti, effects) = UFArgs.D.union (UF.data i uf) (Some t) in - (UF.set i ti uf, effects) - in - - match pb with - | [] -> uf + let setvar i t = + if ocheck i t then failure (); + let (ti, effects) = UFArgs.D.union (UF.data i !uf) (Sp.empty, Some t) in + List.iter (Queue.push^~ pb) effects; + uf := UF.set i ti !uf + in - | (t1, t2) :: pb -> - let (uf, effects) = + let doit () = + while not (Queue.is_empty pb) do + match Queue.pop pb with + | `TyUni (t1, t2) -> begin match ty_equal t1 t2 with - | true -> (uf, UFArgs.D.noeffects) + | true -> () | false -> begin match t1.ty_node, t2.ty_node with - | Tunivar id1, Tunivar id2 -> - if not (uid_equal id1 id2) - then UF.union id1 id2 uf - else (uf, UFArgs.D.noeffects) + | Tunivar id1, Tunivar id2 -> begin + if not (uid_equal id1 id2) then + let effects = reffold (swap |- UF.union id1 id2) uf in + List.iter (Queue.push^~ pb) effects + end | Tunivar id, _ -> setvar id t2 | _, Tunivar id -> setvar id t1 | Ttuple lt1, Ttuple lt2 -> if List.length lt1 <> List.length lt2 then failure (); - (uf, List.combine lt1 lt2) + List.iter2 (fun t1 t2 -> Queue.push (`TyUni (t1, t2)) pb) lt1 lt2 | Tfun (t1, t2), Tfun (t1', t2') -> - (uf, [(t1, t1'); (t2, t2')]) + Queue.push (`TyUni (t1, t1')) pb; + Queue.push (`TyUni (t2, t2')) pb | Tconstr (p1, lt1), Tconstr (p2, lt2) when EcPath.p_equal p1 p2 -> if List.length lt1 <> List.length lt2 then failure (); - (uf, List.combine lt1 lt2) + List.iter2 (fun t1 t2 -> Queue.push (`TyUni (t1, t2)) pb) lt1 lt2 | Tconstr (p, lt), _ when EcEnv.Ty.defined p env -> - (uf, [EcEnv.Ty.unfold p lt env, t2]) + Queue.push (`TyUni (EcEnv.Ty.unfold p lt env, t2)) pb | _, Tconstr (p, lt) when EcEnv.Ty.defined p env -> - (uf, [t1, EcEnv.Ty.unfold p lt env]) + Queue.push (`TyUni (t1, EcEnv.Ty.unfold p lt env)) pb | Tglob mp1, Tglob mp2 -> let mp1 = EcEnv.NormMp.norm_tglob env mp1 in let mp2 = EcEnv.NormMp.norm_tglob env mp2 in - if not (ty_equal mp1 mp2) - then failure () - else (uf, UFArgs.D.noeffects) - - | _, _ -> raise (UnificationFailure (t1, t2)) + if not (ty_equal mp1 mp2) then failure () + + | _, _ -> failure () end - in - unify uf (effects @ pb) + end + | `TcCtt (ty, tc) -> + if not (hastc env tvtc ty tc) then failure () + done in - unify uf [t1, t2] + doit (); !uf (* -------------------------------------------------------------------- *) let close (uf : UF.t) = @@ -135,7 +171,7 @@ let close (uf : UF.t) = | Some t -> t | None -> begin let t = - match UF.data i uf with + match snd (UF.data i uf) with | None -> t | Some t -> doit t in @@ -158,8 +194,8 @@ let subst_of_uf (uf : UF.t) = (* -------------------------------------------------------------------- *) type unienv_r = { ue_uf : UF.t; - ue_tuni : Suid.t; ue_named : EcIdent.t Mstr.t; + ue_tvtc : Sp.t Mid.t; ue_decl : EcIdent.t list; ue_closed : bool; } @@ -191,11 +227,11 @@ module UniEnv = struct }; id end - let create vd = + let create (vd : EcIdent.t list option) = let ue = { ue_uf = UF.initial; - ue_tuni = Suid.empty; ue_named = Mstr.empty; + ue_tvtc = Mid.empty; ue_decl = []; ue_closed = false; } in @@ -212,58 +248,47 @@ module UniEnv = struct in ref ue - let fresh ue = + let fresh ?(tc = Sp.empty) ?ty ue = let uid = EcUidgen.unique () in - ue := { !ue with ue_tuni = Suid.add uid (!ue).ue_tuni; }; + ue := { !ue with ue_uf = UF.set uid (tc, ty) (!ue).ue_uf; }; tuni uid - let freshen_ue ue (params : ty_params) tvi = + let opentvi ue (params : ty_params) tvi = match tvi with | None -> List.fold_left - (* FIXME: TC HOOK *) - (fun s (v, _) -> Mid.add v (fresh ue) s) - Mid.empty params + (fun s (v, tc) -> Mid.add v (fresh ~tc ue) s) + Mid.empty params | Some (TVIunamed lt) -> List.fold_left2 - (* FIXME: TC HOOK *) - (fun s (v, _) t -> Mid.add v t s) Mid.empty - params lt + (fun s (v, tc) ty -> Mid.add v (fresh ~tc ~ty ue) s) + Mid.empty params lt - | Some (TVInamed l) -> - (* FIXME: TC HOOK *) - let for1 s (v, _) = + | Some (TVInamed lt) -> + let for1 s (v, tc) = let t = - try List.assoc (EcIdent.name v) l - with Not_found -> fresh ue + try fresh ~tc ~ty:(List.assoc (EcIdent.name v) lt) ue + with Not_found -> fresh ~tc ue in Mid.add v t s in List.fold_left for1 Mid.empty params - let subst_tv subst params = - (* FIXME: TC HOOK *) + let subst_tv subst params = List.map (fun (tv, _) -> subst (tvar tv)) params - let freshen ue params tvi ty = - let ue = copy ue in - let subst = Tvar.subst (freshen_ue ue params tvi) in - (ue, subst ty, subst_tv subst params) + let openty_r ue params tvi = + let subst = Tvar.subst (opentvi ue params tvi) in + (subst, subst_tv subst params) - let freshendom ue params tvi dom = - let ue = copy ue in - let subst = Tvar.subst (freshen_ue ue params tvi) in - (ue, List.map subst dom, subst_tv subst params) - - let freshensig ue params tvi (dom, codom) = - let ue = copy ue in - let subst = Tvar.subst (freshen_ue ue params tvi) in - (ue, (List.map subst dom, subst codom), subst_tv subst params) + let openty ue params tvi ty = + let (subst, tvs) = openty_r ue params tvi in + (subst ty, tvs) let rec repr (ue : unienv) (t : ty) : ty = match t.ty_node with - | Tunivar id -> odfl t (UF.data id (!ue).ue_uf) + | Tunivar id -> odfl t (snd (UF.data id (!ue).ue_uf)) | _ -> t let closed (ue : unienv) = @@ -276,42 +301,56 @@ module UniEnv = struct let assubst ue = subst_of_uf (!ue).ue_uf let tparams ue = - (* FIXME: TC HOOK *) - List.map (fun x -> (x, EcPath.Sp.empty)) (List.rev (!ue).ue_decl) + let fortv x = odfl Sp.empty (Mid.find_opt x (!ue).ue_tvtc) in + List.map (fun x -> (x, fortv x)) (List.rev (!ue).ue_decl) end (* -------------------------------------------------------------------- *) let unify env ue t1 t2 = - let uf = unify_core env (!ue).ue_uf t1 t2 in + let uf = unify_core env (!ue).ue_tvtc (!ue).ue_uf t1 t2 in ue := { !ue with ue_uf = uf; } (* -------------------------------------------------------------------- *) -let filter_tvi = function - | None -> fun _ -> true - - | Some (TVIunamed l) -> - let len = List.length l in - fun op -> List.length op.EcDecl.op_tparams = len - - | Some (TVInamed ls) -> fun op -> - List.for_all - (fun (s,_) -> - (* FIXME: TC HOOK *) - List.exists (fun (id, _) -> EcIdent.name id = s) - op.EcDecl.op_tparams) - ls - let tfun_expected ue psig = let tres = UniEnv.fresh ue in EcTypes.toarrow psig tres -let select_op pred tvi env name ue psig = - let fti = filter_tvi tvi in - let fop op = (pred || not (EcDecl.is_pred op)) && fti op in +let select_op ~preds tvi env name ue psig = + (* Filter operator based on given type variables instanciation *) + let filter_on_tvi = + let tvtc = (!ue).ue_tvtc in + + match tvi with + | None -> fun _ -> true + + | Some (TVIunamed lt) -> + let len = List.length lt in + fun op -> + let tparams = op.EcDecl.op_tparams in + (List.length tparams = len) + && (List.for_all2 + (fun (_, tc) ty -> hastc env tvtc ty tc) + tparams lt) + + | Some (TVInamed ls) -> fun op -> + let tparams = op.EcDecl.op_tparams in + let for1 (s, ty) = + match + try Some (List.find (fun (id, _) -> EcIdent.name id = s) tparams) + with Not_found -> None + with + | None -> false + | Some (_, tc) -> hastc env tvtc ty tc + in + List.for_all for1 ls + in + + let fop op = (preds || not (EcDecl.is_pred op)) && filter_on_tvi op in let ops = EcEnv.Op.all fop name env in let select (path, op) = - let (subue, top, tys) = - UniEnv.freshen ue op.EcDecl.op_tparams tvi (EcDecl.op_ty op) + let subue = UniEnv.copy ue in + let (top, tys) = + UniEnv.openty subue op.EcDecl.op_tparams tvi (EcDecl.op_ty op) in try let texpected = tfun_expected subue psig in diff --git a/src/ecUnify.mli b/src/ecUnify.mli index d3d5848463..9943bd8c51 100644 --- a/src/ecUnify.mli +++ b/src/ecUnify.mli @@ -20,11 +20,11 @@ module UniEnv : sig val create : EcIdent.t list option -> unienv val copy : unienv -> unienv (* constant time *) val restore : dst:unienv -> src:unienv -> unit (* constant time *) - val fresh : unienv -> ty + val fresh : ?tc:EcPath.Sp.t -> ?ty:ty -> unienv -> ty val getnamed : unienv -> symbol -> EcIdent.t val repr : unienv -> ty -> ty - val freshen_ue : unienv -> ty_params -> tvi -> ty EcIdent.Mid.t - val freshen : unienv -> ty_params -> tvi -> ty -> unienv * ty * ty list + val opentvi : unienv -> ty_params -> tvi -> ty EcIdent.Mid.t + val openty : unienv -> ty_params -> tvi -> ty -> ty * ty list val closed : unienv -> bool val close : unienv -> (uid -> ty option) val assubst : unienv -> (uid -> ty option) @@ -33,12 +33,8 @@ end val unify : EcEnv.env -> unienv -> ty -> ty -> unit -val filter_tvi : tvi -> EcDecl.operator -> bool - val tfun_expected : unienv -> EcTypes.ty list -> EcTypes.ty val select_op : - (* pred allowed *) bool -> - tvi -> EcEnv.env -> - EcSymbols.qsymbol -> unienv -> dom -> - ((EcPath.path * ty list) * ty * unienv) list + preds:bool -> tvi -> EcEnv.env -> qsymbol -> unienv + -> dom -> ((EcPath.path * ty list) * ty * unienv) list diff --git a/src/ecUtils.ml b/src/ecUtils.ml index e5a91b1a50..d7e98dd1b2 100644 --- a/src/ecUtils.ml +++ b/src/ecUtils.ml @@ -83,6 +83,8 @@ let snd_map (f : 'b -> 'c) ((x, y) : 'a * 'b) = let pair_equal tx ty (x1, y1) (x2, y2) = (tx x1 x2) && (ty y1 y2) +let swap (x, y) = (y, x) + (* -------------------------------------------------------------------- *) let opt_equal (f : 'a -> 'a -> bool) o1 o2 = match o1, o2 with diff --git a/src/ecUtils.mli b/src/ecUtils.mli index dce21592a4..41bb703698 100644 --- a/src/ecUtils.mli +++ b/src/ecUtils.mli @@ -56,6 +56,8 @@ val proj3_3 : 'a * 'b * 'c -> 'c val fst_map : ('a -> 'c) -> 'a * 'b -> 'c * 'b val snd_map : ('b -> 'c) -> 'a * 'b -> 'a * 'c +val swap: 'a * 'b -> 'b * 'a + (* -------------------------------------------------------------------- *) type 'a eq = 'a -> 'a -> bool type 'a cmp = 'a -> 'a -> int