Revert subtype theory + syntactic sugar for cloning it

The previous Subtype theory forces the definition of the type sT for
the subtype carrier, having multiple `sT` types when one has multiple
subtype instances. This commits reverts this (i.e. the subtype carrier
can be substituted by a user type) but add a command to carefully
clone it.

examples/ChaChaPoly/chacha_poly.ec

@@ -80,14 +80,17 @@ theory C.
 
   axiom gt0_max_counter : 0 < max_counter.
 
+  type counter.
+
   clone include Subtype with 
-    type T <- int,
-    op P <- fun (i:int) => 0 <= i < max_counter + 1
-    rename (* [type] "sT" as "counter" *) (* Gives error. *)
-           [op] "insubd" as "ofint"
-  proof *.
-  realize inhabited. exists 0. smt(gt0_max_counter). qed.
-  type counter = sT.
+    type sT <- counter,
+    type T  <- int,
+      op P  <- fun (i:int) => 0 <= i < max_counter + 1
+    rename [op] "insubd" as "ofint"
+    proof *.
+
+  realize inhabited.
+  proof. by exists 0; smt(gt0_max_counter). qed.
 
   clone FinType with 
     type t  = counter,
@@ -116,16 +119,20 @@ abstract theory GenBlock.
   op block_size : int.
   axiom ge0_block_size : 0 <= block_size.
 
+  type block.
+
   clone include Subtype with
-    type T <- bytes, 
-    op P <- fun (l:bytes) => size l = block_size
+    type sT <- block,
+    type  T <- bytes, 
+      op  P <- fun (l:bytes) => size l = block_size
     rename [op] "val" as "bytes_of_block"
   proof *.
+
   realize inhabited.
+  proof.
     exists (nseq block_size witness).
     smt(size_nseq ge0_block_size).
   qed.
-  type block = sT.
 
   op dblock =  dmap (dlist dbyte block_size) insubd.
 

examples/MEE-CBC/FunctionalSpec.ec

@@ -492,7 +492,6 @@ proof.
                       (size (pad _p (hmac_sha256 _mk _p)))
                       (nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)
                                    (size (pad _p (hmac_sha256 _mk _p)))).
-        smt().
       split=> //=.
       split; 1:by rewrite /mee_enc /= size_cbc_enc addzC.
       by rewrite take_size.

examples/ehoare/adversary.ec

@@ -74,7 +74,7 @@ proof.
     rewrite (eq_Ep _ _
        ((fun r => (inv p)%xr * (! test r)%xr) + (fun r => (1 + size log)%xr))).
     + move => x xx /=. rewrite of_realM; 1,2:smt(of_realM invr_ge0 ge0_mu). smt().
-    rewrite EpD EpC EpZ /=; 1: smt(invr_gt0 dr_mu_test of_realK).
+    rewrite EpD EpC EpZ /=; 1: smt(invr_gt0 dr_mu_test of_realdK).
     rewrite Ep_mu mu_not dr_ll /= -/p.
     rewrite !to_pos_pos; 1,2,3,4:smt(mu_bounded dr_mu_test size_ge0).
   by auto.

src/ecCommands.ml

@@ -411,6 +411,13 @@ let rec process_type (scope : EcScope.scope) (tyd : ptydecl located) =
 and process_types (scope : EcScope.scope) tyds =
   List.fold_left process_type scope tyds
 
+(* -------------------------------------------------------------------- *)
+and process_subtype (scope : EcScope.scope) (subtype : psubtype located) =
+  EcScope.check_state `InTop "subtype" scope;
+  let scope = EcScope.Ty.add_subtype scope subtype in
+  EcScope.notify scope `Info "added subtype: `%s'" (unloc subtype.pl_desc.pst_name);
+  scope
+
 (* -------------------------------------------------------------------- *)
 and process_typeclass (scope : EcScope.scope) (tcd : ptypeclass located) =
   EcScope.check_state `InTop "type class" scope;
@@ -743,6 +750,7 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
     match
       match g.pl_desc with
       | Gtype        t    -> `Fct   (fun scope -> process_types      scope  (List.map (mk_loc loc) t))
+      | Gsubtype     t    -> `Fct   (fun scope -> process_subtype    scope  (mk_loc loc t))
       | Gtypeclass   t    -> `Fct   (fun scope -> process_typeclass  scope  (mk_loc loc t))
       | Gtycinstance t    -> `Fct   (fun scope -> process_tycinst    scope  (mk_loc loc t))
       | Gmodule      m    -> `Fct   (fun scope -> process_module     scope  m)

src/ecCoreLib.ml

@@ -116,7 +116,7 @@ module CI_Xreal = struct
   let mk_Rpbar = fun x -> EcPath.pqname p_Rpbar x
 
   let p_realp   = mk_Rp "realp"
-  let p_of_real = mk_Rp "of_real"
+  let p_of_real = mk_Rp "of_reald"
 
   let p_xreal   = mk_Rpbar "xreal"
   let p_rp      = mk_Rpbar "rp"

src/ecLexer.mll

@@ -195,6 +195,7 @@
     "theory"      , THEORY     ;        (* KW: global *)
     "abstract"    , ABSTRACT   ;        (* KW: global *)
     "section"     , SECTION    ;        (* KW: global *)
+    "subtype"     , SUBTYPE    ;        (* KW: global *)
     "type"        , TYPE       ;        (* KW: global *)
     "class"       , CLASS      ;        (* KW: global *)
     "instance"    , INSTANCE   ;        (* KW: global *)

src/ecParser.mly

@@ -558,6 +558,7 @@
 %token SPLITWHILE
 %token STAR
 %token SUBST
+%token SUBTYPE
 %token SUFF
 %token SWAP
 %token SYMMETRY
@@ -1644,6 +1645,21 @@ typedecl:
 | locality=locality TYPE td=tyd_name EQ te=datatype_def
     { [mk_tydecl ~locality td (PTYD_Datatype te)] }
 
+(* -------------------------------------------------------------------- *)
+(* Subtypes                                                             *)
+subtype:
+| SUBTYPE name=lident cname=prefix(AS, uident)? EQ LBRACE
+    x=lident COLON carrier=loc(type_exp) PIPE pred=form
+  RBRACE rename=subtype_rename?
+  { { pst_name    = name;
+      pst_cname   = cname;
+      pst_carrier = carrier;
+      pst_pred    = (x, pred);
+      pst_rename  = rename; } }
+
+subtype_rename:
+| RENAME x=STRING COMMA y=STRING { (x, y) }
+
 (* -------------------------------------------------------------------- *)
 (* Type classes                                                         *)
 typeclass:
@@ -3763,6 +3779,7 @@ global_action:
 | mod_def_or_decl  { Gmodule      $1 }
 | sig_def          { Ginterface   $1 }
 | typedecl         { Gtype        $1 }
+| subtype          { Gsubtype     $1 }
 | typeclass        { Gtypeclass   $1 }
 | tycinstance      { Gtycinstance $1 }
 | operator         { Goperator    $1 }

src/ecParsetree.ml

@@ -384,6 +384,15 @@ let rec pf_ident ?(raw = false) f =
   | PFtuple [f] when not raw -> pf_ident ~raw f
   | _ -> None
 
+(* -------------------------------------------------------------------- *)
+type psubtype = {
+  pst_name    : psymbol;
+  pst_cname   : psymbol option;
+  pst_carrier : pty;
+  pst_pred    : (psymbol * pformula);
+  pst_rename  : (string * string) option;
+}
+
 (* -------------------------------------------------------------------- *)
 type ptyvardecls =
   (psymbol * pqsymbol list) list
@@ -1261,6 +1270,7 @@ type global_action =
   | Gabbrev      of pabbrev
   | Gaxiom       of paxiom
   | Gtype        of ptydecl list
+  | Gsubtype     of psubtype
   | Gtypeclass   of ptypeclass
   | Gtycinstance of ptycinstance
   | Gaddrw       of (is_local * pqsymbol * pqsymbol list)