allow non-named types in carrier + fix more stdlib

EasyCrypt · Jan 17, 2025 · e08adc2 · e08adc2
1 parent e768d09
commit e08adc2
Show file tree

Hide file tree

Showing 6 changed files with 42 additions and 34 deletions.
diff --git a/src/ecScope.ml b/src/ecScope.ml
@@ -1976,20 +1976,18 @@ module Ty = struct
       if not (EcUnify.UniEnv.closed ue) then
         hierror ~loc:(snd subtype.pst_pred).pl_loc 
           "the predicate contains free type variables";
-        f_lambda [(x, GTty carrier)] pred in
-
-    let carrier =
-      match carrier.ty_node with
-      | Tconstr (carrier, []) -> carrier
-      | _ ->
-        hierror ~loc:subtype.pst_carrier.pl_loc 
-          "the carrier must be a monomorphic named type" in
+      let uidmap = EcUnify.UniEnv.close ue in
+      let fs = Tuni.subst uidmap in
+      f_lambda [(x, GTty carrier)] (Fsubst.f_subst fs pred) in
 
     let evclone =
       { EcThCloning.evc_empty with
           evc_types = Msym.of_list [
-            "T", loced (`ByPath carrier, `Inline `Clear);
-            "sT", loced (`ByPath (EcPath.pqname (EcEnv.root env) (unloc subtype.pst_name)), `Inline `Clear);
+            "T", loced (`Direct carrier, `Inline `Clear);
+            "sT", loced (
+              `ByPath (EcPath.pqname (EcEnv.root env) (unloc subtype.pst_name)),
+              `Inline `Clear
+            );
           ];
           evc_ops = Msym.of_list [
             "P", loced (`Direct pred, `Inline `Clear)

diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml
@@ -53,6 +53,10 @@ type axclone = {
   axc_tac   : EcParsetree.ptactic_core option;
 }
 
+(* ------------------------------------------------------------------ *)
+type xty_override =
+  [ty_override_def genoverride | `Direct of EcAst.ty] * clmode
+
 (* ------------------------------------------------------------------ *)
 type xop_override =
   [op_override_def genoverride | `Direct of EcAst.form] * clmode
@@ -63,7 +67,7 @@ type xpr_override =
 
 (* ------------------------------------------------------------------ *)
 type evclone = {
-  evc_types    : (ty_override located) Msym.t;
+  evc_types    : (xty_override located) Msym.t;
   evc_ops      : (xop_override located) Msym.t;
   evc_preds    : (xpr_override located) Msym.t;
   evc_abbrevs  : (nt_override located) Msym.t;
@@ -280,7 +284,8 @@ end = struct
         (fun evc ->
           if Msym.mem x evc.evc_types then
             clone_error oc.oc_env (CE_DupOverride (OVK_Type, name));
-          { evc with evc_types = Msym.add x (mk_loc lc tyd) evc.evc_types })
+          { evc with evc_types =
+              Msym.add x (mk_loc lc tyd :> xty_override located) evc.evc_types })
         nm evc
 
     in (proofs, evc)

diff --git a/src/ecThCloning.mli b/src/ecThCloning.mli
@@ -39,17 +39,21 @@ exception CloneError of EcEnv.env * clone_error
 
 val clone_error : EcEnv.env -> clone_error -> 'a
 
+(* ------------------------------------------------------------------ *)
+type xty_override =
+  [ty_override_def genoverride | `Direct of EcAst.ty] * clmode
+
 (* ------------------------------------------------------------------ *)
 type xop_override =
-[ op_override_def genoverride | `Direct of EcAst.form ] * clmode
+  [op_override_def genoverride | `Direct of EcAst.form] * clmode
 
 (* ------------------------------------------------------------------ *)
 type xpr_override =
-  [ pr_override_def genoverride | `Direct of EcAst.form ] * clmode
+  [pr_override_def genoverride | `Direct of EcAst.form] * clmode
 
 (* -------------------------------------------------------------------- *)
 type evclone = {
-  evc_types    : (ty_override located) Msym.t;
+  evc_types    : (xty_override located) Msym.t;
   evc_ops      : (xop_override located) Msym.t;
   evc_preds    : (xpr_override located) Msym.t;
   evc_abbrevs  : (nt_override located) Msym.t;

diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml
@@ -366,6 +366,17 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
 
             | _ -> assert false
           end
+
+        | `Direct ty -> begin
+          assert (List.is_empty otyd.tyd_params);
+          let decl  =
+            { tyd_params  = [];
+              tyd_type    = `Concrete ty;
+              tyd_resolve = otyd.tyd_resolve && (mode = `Alias);
+              tyd_loca    = otyd.tyd_loca; }
+
+          in (decl, ty)
+    end
       in
 
       let subst, x =

diff --git a/theories/datatypes/Word.eca b/theories/datatypes/Word.eca
@@ -14,23 +14,16 @@ op wordw : t list = mkseq (fun _ => dchar) n.
 lemma size_wordw: size wordw = n.
 proof. by rewrite size_mkseq ler_maxr ?ge0_n. qed.
 
-type word.
-
-clone include Subtype with
-  type sT <- word,
-  type T  <- t list,
-    op P  <- fun w => size w = n
-  proof *.
+subtype word = { w : t list | size w = n }.
 
 realize inhabited.
-proof. by exists wordw; exact size_wordw. qed.
+proof. by exists wordw; exact: size_wordw. qed.
 
 (* default value chosen for backward compatibility *)
 op mkword x = odflt (insubd wordw) (insub x).
 op ofword = val.
 
 (* -------------------------------------------------------------------- *)
-
 lemma mkwordK : cancel ofword mkword.
 proof. smt(valK). qed.
 

diff --git a/theories/structure/Quotient.ec b/theories/structure/Quotient.ec
@@ -87,25 +87,22 @@ apply/(eqv_trans (canon x)); first by apply/eqv_canon.
 by rewrite eq &(eqv_refl).
 qed.
 
-type qT.
-
-clone import Subtype with
-  type sT <- qT,
-  type T  <- T,
-    op P  <- iscanon
-proof *.
+subtype qT as QSub = { x : T | iscanon x }.
 
 realize inhabited.
 proof. smt(canonK). qed.
-
+
+import QSub.
+
 clone include CoreQuotient with
   type T     <- T,
   type qT    <- qT,
-  op   pi    =  fun x => Subtype.insubd (canon x),
-  op   repr  =  fun x => Subtype.val x
+  op   pi    =  fun x => QSub.insubd (canon x),
+  op   repr  =  fun x => QSub.val x
 
   proof *.
 
+
 realize reprK. proof.
 by move=> q; rewrite /pi /repr /insubd canon_iscanon 1:valP valK.
 qed.