subtype-include + add decl + start fixing stdlib

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

Hide file tree

Showing 5 changed files with 22 additions and 14 deletions.
diff --git a/src/ecParser.mly b/src/ecParser.mly
@@ -1648,7 +1648,7 @@ typedecl:
 (* -------------------------------------------------------------------- *)
 (* Subtypes                                                             *)
 subtype:
-| SUBTYPE name=lident AS cname=uident EQ LBRACE
+| SUBTYPE name=lident cname=prefix(AS, uident)? EQ LBRACE
     x=lident COLON carrier=loc(type_exp) PIPE pred=form
   RBRACE
   { { pst_name    = name;

diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
@@ -387,7 +387,7 @@ let rec pf_ident ?(raw = false) f =
 (* -------------------------------------------------------------------- *)
 type psubtype = {
   pst_name    : psymbol;
-  pst_cname   : psymbol;
+  pst_cname   : psymbol option;
   pst_carrier : pty;
   pst_pred    : (psymbol * pformula);
 }

diff --git a/src/ecScope.ml b/src/ecScope.ml
@@ -1956,6 +1956,14 @@ module Ty = struct
     let loced x = mk_loc _dummy x in
     let env = env scope in
 
+    let scope =
+      let decl = EcDecl.{
+        tyd_params  = [];
+        tyd_type    = `Abstract Sp.empty;
+        tyd_loca    = `Global; (* FIXME:SUBTYPE *)
+        tyd_resolve = true;
+      } in bind scope (unloc subtype.pst_name, decl) in
+
     let carrier =
       let ue = EcUnify.UniEnv.create None in
       transty tp_tydecl env ue subtype.pst_carrier in
@@ -1980,7 +1988,8 @@ module Ty = struct
     let evclone =
       { EcThCloning.evc_empty with
           evc_types = Msym.of_list [
-            "T", loced (`ByPath carrier, `Inline `Clear)
+            "T", loced (`ByPath 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)
@@ -1990,15 +1999,20 @@ module Ty = struct
             ev_global  =  [ (None, Some [`Include, "prove"]) ]
           } } in
 
-    let npath = EcPath.pqname (EcEnv.root env) (unloc subtype.pst_cname) in
+    let cname = Option.map unloc subtype.pst_cname in
+    let npath = ofold ((^~) EcPath.pqname) (EcEnv.root env) cname in
     let cpath = EcPath.fromqsymbol ([EcCoreLib.i_top], "Subtype") in
     let theory = EcEnv.Theory.by_path ~mode:`Abstract cpath env in
 
     let (proofs, scope) =
       EcTheoryReplay.replay Cloning.hooks
-        ~abstract:false ~local:`Global ~incl:false
+        ~abstract:false ~local:`Global ~incl:(Option.is_none cname)
         ~clears:Sp.empty ~renames:[] ~opath:cpath ~npath
-        evclone scope (EcPath.basename npath, theory.cth_items) in
+        evclone scope
+        (
+          Option.value ~default:(EcPath.basename cpath) cname,
+          theory.cth_items
+        ) in
 
     let proofs = Cloning.replay_proofs scope `Check proofs in
 

diff --git a/tests/subtype-clone-sugar.ec b/tests/subtype-clone-sugar.ec
@@ -1,7 +1,7 @@
 require import AllCore.
 require Subtype.
 
-subtype zmod3 as ZMod3 =
+subtype zmod3 =
   { x : int | 0 <= x < 3 }.
 
 realize inhabited. by exists 0. qed.
diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec
@@ -11,13 +11,7 @@ abstract theory ZModRing.
 const p : { int | 2 <= p } as ge2_p.
 
 (* -------------------------------------------------------------------- *)
-type zmod.
-
-clone Subtype as Sub with
-  type sT <- zmod,
-  type  T <- int,
-    op  P <- fun (x : int) => 0 <= x < p
-proof *.
+subtype zmod as Sub = { x : int | 0 <= x < p }.
 
 realize inhabited.
 proof. by exists 0; smt(ge2_p). qed.