pred -> op

examples/ChaChaPoly/chacha_poly.ec

@@ -85,7 +85,7 @@ theory C.
   clone include Subtype with 
     type sT <- counter,
     type T  <- int,
-    pred P  <- fun (i:int) => 0 <= i < max_counter + 1
+      op P  <- fun (i:int) => 0 <= i < max_counter + 1
     rename [op] "insubd" as "ofint"
     proof *.
 
@@ -124,7 +124,7 @@ abstract theory GenBlock.
   clone include Subtype with
     type sT <- block,
     type  T <- bytes, 
-    pred  P <- fun (l:bytes) => size l = block_size
+      op  P <- fun (l:bytes) => size l = block_size
     rename [op] "val" as "bytes_of_block"
   proof *.
 

src/ecScope.ml

@@ -1982,7 +1982,7 @@ module Ty = struct
           evc_types = Msym.of_list [
             "T", loced (`ByPath carrier, `Inline `Clear)
           ];
-          evc_preds = Msym.of_list [
+          evc_ops = Msym.of_list [
             "P", loced (`Direct pred, `Inline `Clear)
           ];
           evc_lemmas = {

src/ecThCloning.ml

@@ -54,20 +54,19 @@ type axclone = {
 }
 
 (* ------------------------------------------------------------------ *)
-type xty_override = ty_override
-type xop_override = op_override
-type xnt_override = nt_override
+type xop_override =
+  [op_override_def genoverride | `Direct of EcAst.form] * clmode
 
 (* ------------------------------------------------------------------ *)
 type xpr_override =
   [pr_override_def genoverride | `Direct of EcAst.form] * clmode
 
 (* ------------------------------------------------------------------ *)
 type evclone = {
-  evc_types    : (xty_override located) Msym.t;
+  evc_types    : (ty_override located) Msym.t;
   evc_ops      : (xop_override located) Msym.t;
   evc_preds    : (xpr_override located) Msym.t;
-  evc_abbrevs  : (xnt_override located) Msym.t;
+  evc_abbrevs  : (nt_override located) Msym.t;
   evc_modexprs : (me_override located) Msym.t;
   evc_modtypes : (mt_override located) Msym.t;
   evc_lemmas   : evlemma;
@@ -298,7 +297,8 @@ end = struct
         (fun evc ->
          if Msym.mem x evc.evc_ops then
            clone_error oc.oc_env (CE_DupOverride (OVK_Operator, name));
-         { evc with evc_ops = Msym.add x (mk_loc lc opd) evc.evc_ops })
+         { evc with evc_ops = 
+            Msym.add x (mk_loc lc opd :> xop_override located) evc.evc_ops })
         nm evc
 
     in (proofs, evc)

src/ecThCloning.mli

@@ -40,20 +40,19 @@ exception CloneError of EcEnv.env * clone_error
 val clone_error : EcEnv.env -> clone_error -> 'a
 
 (* ------------------------------------------------------------------ *)
-type xty_override = ty_override
-type xop_override = op_override
-type xnt_override = nt_override
+type xop_override =
+[ op_override_def genoverride | `Direct of EcAst.form ] * clmode
 
 (* ------------------------------------------------------------------ *)
 type xpr_override =
   [ pr_override_def genoverride | `Direct of EcAst.form ] * clmode
 
 (* -------------------------------------------------------------------- *)
 type evclone = {
-  evc_types    : (xty_override located) Msym.t;
+  evc_types    : (ty_override located) Msym.t;
   evc_ops      : (xop_override located) Msym.t;
   evc_preds    : (xpr_override located) Msym.t;
-  evc_abbrevs  : (xnt_override located) Msym.t;
+  evc_abbrevs  : (nt_override located) Msym.t;
   evc_modexprs : (me_override located) Msym.t;
   evc_modtypes : (mt_override located) Msym.t;
   evc_lemmas   : evlemma;

src/ecTheoryReplay.ml

@@ -495,6 +495,15 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) =
 
             | _ -> clone_error env (CE_UnkOverride(OVK_Operator, EcPath.toqsymbol p))
           end
+
+          | `Direct body ->
+            assert (List.is_empty refop.op_tparams);
+            let newop =
+              mk_op
+                ~opaque:optransparent ~clinline:(opmode <> `Alias)
+                [] body.f_ty (Some (OP_Plain body)) refop.op_loca in
+            (newop, body)
+
         in
           match opmode with
           | `Alias ->

theories/algebra/Poly.ec

@@ -28,7 +28,7 @@ type poly.
 clone include Subtype
   with type sT <- poly,
        type T <- prepoly,
-       pred P <- ispoly
+         op P <- ispoly
   rename "insub" as "to_poly"
   rename "val"   as "of_poly"
 proof *.

theories/algebra/ZModP.ec

@@ -16,7 +16,7 @@ type zmod.
 clone Subtype as Sub with
   type sT <- zmod,
   type  T <- int,
-  pred  P <- fun (x : int) => 0 <= x < p
+    op  P <- fun (x : int) => 0 <= x < p
 proof *.
 
 realize inhabited.

theories/datatypes/Word.eca

@@ -19,7 +19,7 @@ type word.
 clone include Subtype with
   type sT <- word,
   type T  <- t list,
-  pred P  <- fun w => size w = n
+    op P  <- fun w => size w = n
   proof *.
 
 realize inhabited.

theories/datatypes/Xreal.ec

@@ -67,7 +67,7 @@ type realp.
 clone include Subtype with
    type sT <- realp,
    type T  <- real,
-   pred P  <- fun x => 0.0 <= x
+     op P  <- fun x => 0.0 <= x
    rename "insubd" as "of_real"
    rename "val" as "to_real"
 proof *.

theories/structure/Quotient.ec

@@ -92,7 +92,7 @@ type qT.
 clone import Subtype with
   type sT <- qT,
   type T  <- T,
-  pred P  <- iscanon
+    op P  <- iscanon
 proof *.
 
 realize inhabited.

theories/structure/Subtype.eca

@@ -20,7 +20,8 @@ pragma +implicits.
 require import AllCore.
 
 type T, sT.
-pred P : T.
+
+op P : T -> bool.
 
 op insub : T  -> sT option.
 op val   : sT -> T.