TypeClass: unification algorithm is now TC aware.

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

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

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

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
 

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;
 

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;

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
 

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) =