create TC univar

Author: strub

src/ecAst.ml

@@ -57,9 +57,11 @@ and ty_node =
   | Tfun    of ty * ty
 
 (* -------------------------------------------------------------------- *)
-and etyarg    = ty * tcwitness list
+and etyarg = ty * tcwitness list
 
 and tcwitness =
+  | TCIUni of EcUid.uid
+
   | TCIConcrete of {
       path: EcPath.path;
       etyargs: (ty * tcwitness list) list;
@@ -68,12 +70,11 @@ and tcwitness =
   | TCIAbstract of {
       support: [
         | `Var    of EcIdent.t
-        | `Univar of EcUid.uid
         | `Abs    of EcPath.path
       ];
       offset: int;
   }
-  
+
 (* -------------------------------------------------------------------- *)
 and ovariable = {
   ov_name : EcSymbols.symbol option;
@@ -374,6 +375,9 @@ let lp_fv = function
 (* -------------------------------------------------------------------- *)
 let rec tcw_fv (tcw : tcwitness) =
   match tcw with
+  | TCIUni _  ->
+    Mid.empty
+
   | TCIConcrete { etyargs } ->
     List.fold_left
       (fun fv (ty, tcws) -> fv_union fv (fv_union ty.ty_fv (tcws_fv tcws)))
@@ -398,6 +402,9 @@ let etyargs_fv (tyargs : etyarg list) =
 (* -------------------------------------------------------------------- *)
 let rec tcw_equal (tcw1 : tcwitness) (tcw2 : tcwitness) =
   match tcw1, tcw2 with
+  | TCIUni uid1, TCIUni uid2 ->
+    uid_equal uid1 uid2
+
   | TCIConcrete tcw1, TCIConcrete tcw2 ->
        EcPath.p_equal tcw1.path tcw2.path
     && List.all2 etyarg_equal tcw1.etyargs tcw2.etyargs
@@ -409,8 +416,6 @@ let rec tcw_equal (tcw1 : tcwitness) (tcw2 : tcwitness) =
       match support1, support2 with
       | `Var x1, `Var x2 ->
         EcIdent.id_equal x1 x2
-      | `Univar u1, `Univar u2 ->
-        uid_equal u1 u2
       | `Abs p1, `Abs p2 ->
         EcPath.p_equal p1 p2
       | _, _ -> false
@@ -426,6 +431,9 @@ and etyarg_equal ((ty1, tcws1) : etyarg) ((ty2, tcws2) : etyarg) =
 (* -------------------------------------------------------------------- *)
 let rec tcw_hash (tcw : tcwitness) =
   match tcw with
+  | TCIUni uid ->
+    Hashtbl.hash uid
+
   | TCIConcrete tcw ->
     Why3.Hashcons.combine_list
       etyarg_hash
@@ -435,9 +443,6 @@ let rec tcw_hash (tcw : tcwitness) =
   | TCIAbstract { support = `Var tyvar; offset } ->
     Why3.Hashcons.combine (EcIdent.id_hash tyvar) offset
 
-  | TCIAbstract { support = `Univar uni; offset } ->
-    Why3.Hashcons.combine (Hashtbl.hash uni) offset
-  
   | TCIAbstract { support = `Abs p; offset } ->
     Why3.Hashcons.combine (EcPath.p_hash p) offset
 

src/ecAst.mli

@@ -56,6 +56,8 @@ and ty_node =
 and etyarg = ty * tcwitness list
 
 and tcwitness =
+  | TCIUni of EcUid.uid
+
   | TCIConcrete of {
       path: EcPath.path;
       etyargs: (ty * tcwitness list) list;
@@ -64,7 +66,6 @@ and tcwitness =
   | TCIAbstract of {
       support: [
         | `Var    of EcIdent.t
-        | `Univar of EcUid.uid
         | `Abs    of EcPath.path
       ];
       offset: int;

src/ecCoreEqTest.ml

@@ -62,6 +62,9 @@ and for_etyargs env (tyargs1 : etyarg list) (tyargs2 : etyarg list) =
 
 and for_tcw env (tcw1 : tcwitness) (tcw2 : tcwitness) =
   match tcw1, tcw2 with
+  | TCIUni uid1, TCIUni uid2 ->
+    EcUid.uid_equal uid1 uid2
+
   | TCIConcrete tcw1, TCIConcrete tcw2 ->
        EcPath.p_equal tcw1.path tcw2.path
     && for_etyargs env tcw1.etyargs tcw2.etyargs
@@ -70,10 +73,6 @@ and for_tcw env (tcw1 : tcwitness) (tcw2 : tcwitness) =
     TCIAbstract { support = `Var v2; offset = o2 } ->
     EcIdent.id_equal v1 v2 && o1 = o2
 
-  | TCIAbstract { support = `Univar v1; offset = o1 },
-    TCIAbstract { support = `Univar v2; offset = o2 } ->
-    EcUid.uid_equal v1 v2 && o1 = o2
-
   | TCIAbstract { support = `Abs p1; offset = o1 },
     TCIAbstract { support = `Abs p2; offset = o2 } ->
     EcPath.p_equal p1 p2 && o1 = o2

src/ecCoreSubst.ml

@@ -17,7 +17,8 @@ type mod_extra = {
 (* -------------------------------------------------------------------- *)
 type f_subst = {
   fs_freshen : bool; (* true means freshen locals *)
-  fs_u       : etyarg Muid.t;
+  fs_u       : ty Muid.t;
+  fs_utc     : tcwitness Muid.t;
   fs_v       : etyarg Mid.t;
   fs_mod     : EcPath.mpath Mid.t;
   fs_modex   : mod_extra Mid.t;
@@ -47,22 +48,36 @@ let fv_Mid (type a)
 =
   Mid.fold (fun _ t s -> fv_union s (fv t)) m s
 
+(* -------------------------------------------------------------------- *)
+type unisubst = {
+  uvars   : ty Muid.t;
+  utcvars : tcwitness Muid.t;
+}
+
+(* -------------------------------------------------------------------- *)
+let unisubst0 : unisubst = {
+  uvars = Muid.empty; utcvars = Muid.empty;
+}
+
 (* -------------------------------------------------------------------- *)
 let f_subst_init
-      ?(freshen=false)
-      ?(tu=Muid.empty)
-      ?(tv=Mid.empty)
-      ?(esloc=Mid.empty)
-      () =
+  ?(freshen = false)
+  ?(tu      = unisubst0)
+  ?(tv      = Mid.empty)
+  ?(esloc   = Mid.empty)
+  ()
+=
 
   let fv = Mid.empty in
-  let fv = Muid.fold (fun _ t s -> fv_union s (etyarg_fv t)) tu fv in
+  let fv = Muid.fold (fun _ t s -> fv_union s (ty_fv t)) tu.uvars fv in
+  let fv = Muid.fold (fun _ t s -> fv_union s (tcw_fv t)) tu.utcvars fv in
   let fv = fv_Mid etyarg_fv tv fv in
   let fv = fv_Mid e_fv esloc fv in
 
   {
     fs_freshen  = freshen;
-    fs_u        = tu;
+    fs_u        = tu.uvars;
+    fs_utc      = tu.utcvars;
     fs_v        = tv;
     fs_mod      = Mid.empty;
     fs_modex    = Mid.empty;
@@ -166,7 +181,7 @@ let rec ty_subst (s : f_subst) (ty : ty) : ty =
 
   | Tunivar id ->
        Muid.find_opt id s.fs_u
-    |> Option.map (fun (ty, _) -> ty_subst s ty)
+    |> Option.map (ty_subst s)
     |> Option.value ~default:ty
 
   | Tvar id ->
@@ -190,7 +205,11 @@ let rec ty_subst (s : f_subst) (ty : ty) : ty =
 (* -------------------------------------------------------------------- *)
 and tcw_subst (s : f_subst) (tcw : tcwitness) : tcwitness =
   match tcw with
-  | TCIConcrete ({ etyargs = etyargs0 } as rtcw) ->
+  | TCIUni uid ->
+       Muid.find_opt uid s.fs_utc
+    |> Option.value ~default:tcw
+
+| TCIConcrete ({ etyargs = etyargs0 } as rtcw) ->
     let etyargs = List.Smart.map (etyarg_subst s) etyargs0 in
     if etyargs ==(*phy*) etyargs0 then
       tcw
@@ -201,11 +220,6 @@ and tcw_subst (s : f_subst) (tcw : tcwitness) : tcwitness =
     |> Option.map (fun (_, tcws) -> List.nth tcws offset)
     |> Option.value ~default:tcw
 
-  | TCIAbstract { support = `Univar uni; offset } ->
-       Muid.find_opt uni s.fs_u
-    |> Option.map (fun (_, tcws) -> List.nth tcws offset)
-    |> Option.value ~default:tcw
-
   | TCIAbstract { support = `Abs _ } ->
     tcw
 
@@ -768,13 +782,13 @@ end
 
 (* -------------------------------------------------------------------- *)
 module Tuni = struct
-  let subst (uidmap : etyarg Muid.t) : f_subst =
+  let subst (uidmap : unisubst) : f_subst =
     f_subst_init ~tu:uidmap ()
 
-  let subst1 ((id, t) : uid * etyarg) : f_subst =
-    subst (Muid.singleton id t)
+  let subst1 ((id, t) : uid * ty) : f_subst =
+    subst { unisubst0 with uvars = Muid.singleton id t }
 
-  let subst_dom (uidmap : etyarg Muid.t) (dom : dom) : dom =
+  let subst_dom (uidmap : unisubst) (dom : dom) : dom =
     List.map (ty_subst (subst uidmap)) dom
 
   let occurs (u : uid) : ty -> bool =

src/ecCoreSubst.mli

@@ -16,10 +16,15 @@ type tx = before:form -> after:form -> form
 type 'a tx_substitute = ?tx:tx -> 'a substitute
 type 'a subst_binder = f_subst -> 'a -> f_subst * 'a
 
+(* -------------------------------------------------------------------- *)
+type unisubst = {
+  uvars : ty Muid.t; utcvars : tcwitness Muid.t;
+}
+
 (* -------------------------------------------------------------------- *)
 val f_subst_init :
        ?freshen:bool
-    -> ?tu:etyarg Muid.t
+    -> ?tu:unisubst
     -> ?tv:etyarg Mid.t
     -> ?esloc:expr Mid.t
     -> unit
@@ -28,9 +33,9 @@ val f_subst_init :
 (* -------------------------------------------------------------------- *)
 module Tuni : sig
   val univars   : ty -> Suid.t
-  val subst1    : (uid * etyarg) -> f_subst
-  val subst     : etyarg Muid.t -> f_subst
-  val subst_dom : etyarg Muid.t -> dom -> dom
+  val subst1    : (uid * ty) -> f_subst
+  val subst     : unisubst -> f_subst
+  val subst_dom : unisubst -> dom -> dom
   val occurs    : uid -> ty -> bool
   val fv        : ty -> Suid.t
 end
@@ -63,7 +68,7 @@ module Fsubst : sig
 
   val f_subst_init :
        ?freshen:bool
-    -> ?tu:etyarg Muid.t
+    -> ?tu:unisubst
     -> ?tv:etyarg Mid.t
     -> ?esloc:expr Mid.t
     -> unit -> f_subst

src/ecHiNotations.ml

@@ -83,8 +83,8 @@ let trans_abbrev_r (env : env) (at : pabbrev located) =
   if not (EcUnify.UniEnv.closed ue) then
     nterror gloc env NTE_TyNotClosed;
 
-  let ts = Tuni.subst (EcUnify.UniEnv.close ue) in
-  let es = e_subst ts in
+  let ts      = Tuni.subst (EcUnify.UniEnv.close ue) in
+  let es      = e_subst ts in
   let body    = es body in
   let codom   = ty_subst ts codom in
   let xs      = List.map (snd_map (ty_subst ts)) xs in

src/ecHiPredicates.ml

@@ -2,7 +2,6 @@
 open EcUtils
 open EcSymbols
 open EcLocation
-open EcTypes
 open EcCoreSubst
 open EcParsetree
 open EcDecl
@@ -20,8 +19,8 @@ exception TransPredError of EcLocation.t * EcEnv.env * tperror
 let tperror loc env e = raise (TransPredError (loc, env, e))
 
 (* -------------------------------------------------------------------- *)
-let close_pr_body (uni : etyarg EcUid.Muid.t) (body : prbody) =
-  let fsubst = EcFol.Fsubst.f_subst_init ~tu:uni () in
+let close_pr_body (uidmap : unisubst) (body : prbody) =
+  let fsubst = EcFol.Fsubst.f_subst_init ~tu:uidmap () in
   let tsubst = ty_subst fsubst in
 
   match body with

src/ecMatching.mli

@@ -1,6 +1,5 @@
 (* -------------------------------------------------------------------- *)
 open EcMaps
-open EcUid
 open EcIdent
 open EcTypes
 open EcModules
@@ -196,7 +195,7 @@ val f_match :
   -> unienv * mevmap
   -> form
   -> form
-  -> unienv * (etyarg Muid.t) * mevmap
+  -> unienv * unisubst * mevmap
 
 (* -------------------------------------------------------------------- *)
 type ptnpos = private [`Select of int | `Sub of ptnpos] Mint.t

src/ecPrinting.ml

@@ -561,7 +561,7 @@ let pp_modtype1 (ppe : PPEnv.t) fmt mty =
 
 (* -------------------------------------------------------------------- *)
 let pp_local (ppe : PPEnv.t) fmt x =
-  Format.fprintf fmt "%s" (EcIdent.tostring x) (* (PPEnv.local_symb ppe x) *)
+  Format.fprintf fmt "%s" (PPEnv.local_symb ppe x)
 
 (* -------------------------------------------------------------------- *)
 let pp_local ?fv (ppe : PPEnv.t) fmt x =
@@ -947,6 +947,36 @@ let pp_opname fmt (nm, op) =
 
   in EcSymbols.pp_qsymbol fmt (nm, op)
 
+(* -------------------------------------------------------------------- *)
+let rec pp_etyarg (ppe : PPEnv.t) (fmt : Format.formatter) ((ty, tcws) : etyarg) =
+  Format.fprintf fmt "%a[%a]" (pp_type ppe) ty (pp_tcws ppe) tcws
+
+(* -------------------------------------------------------------------- *)
+and pp_etyargs (ppe : PPEnv.t) (fmt : Format.formatter) (etys : etyarg list) =
+    Format.fprintf fmt "%a" (pp_list ",@ " (pp_etyarg ppe)) etys
+
+(* -------------------------------------------------------------------- *)
+and pp_tcw (ppe : PPEnv.t) (fmt : Format.formatter) (tcw : tcwitness) =
+  match tcw with
+  | TCIUni uid ->
+    Format.fprintf fmt "%a" (pp_tyunivar ppe) uid
+
+  | TCIConcrete { path; etyargs } ->
+    Format.fprintf fmt "%a[%a]"
+      pp_qsymbol (EcPath.toqsymbol path)
+      (pp_etyargs ppe) etyargs
+
+  | TCIAbstract { support = `Var x; offset } ->
+    Format.fprintf fmt "%a.`%d" (pp_tyvar ppe) x (offset + 1)
+  
+  | TCIAbstract { support = `Abs path; offset } ->
+    Format.fprintf fmt "%a.`%d" (pp_tyname ppe) path (offset + 1)
+
+(* -------------------------------------------------------------------- *)
+and pp_tcws (ppe : PPEnv.t) (fmt : Format.formatter) (tcws : tcwitness list) =
+  Format.fprintf fmt "%a" (pp_list ",@ " (pp_tcw ppe)) tcws
+
+(* -------------------------------------------------------------------- *)
 let pp_opname_with_tvi
   (ppe : PPEnv.t)
   (fmt : Format.formatter)
@@ -958,8 +988,7 @@ let pp_opname_with_tvi
 
   | Some tvi ->
       Format.fprintf fmt "%a<:%a>"
-        pp_opname (nm, op)
-        (pp_list ",@ " (pp_type ppe)) (List.fst tvi)
+        pp_opname (nm, op) (pp_etyargs ppe) tvi
 
 (* -------------------------------------------------------------------- *)
 let pp_opapp

src/ecReduction.ml

@@ -676,6 +676,9 @@ let reduce_tc (env : EcEnv.env) (p : path) (tys : etyarg list) =
   let tcw = as_seq1 tcw in
 
   match tcw with
+  | TCIUni _ ->
+    None
+
   | TCIAbstract _ ->
     None