Operators body can now be formulas

When cloning a theory, inlined operator definitions must be
expressions s.t. their substitution can be done in procedures
bodies.

src/ecCoreFol.ml

@@ -947,6 +947,14 @@ let f_xmul_simpl f1 f2 =
 let f_xmuli_simpl f1 f2 =
   f_xmul_simpl (f_N f1) f2
 
+(* -------------------------------------------------------------------- *)
+let f_none (ty : ty) : form =
+  f_op EcCoreLib.CI_Option.p_none [ty] (toption ty)
+
+let f_some ({ f_ty = ty } as f : form) : form =
+  let op = f_op EcCoreLib.CI_Option.p_some [ty] (tfun ty (toption ty)) in
+  f_app op [f] (toption ty)
+
 (* -------------------------------------------------------------------- *)
 let cost_map g cost =
   let calls =

src/ecCoreFol.mli

@@ -337,6 +337,10 @@ val f_int_mul   : form -> form -> form
 val f_int_pow   : form -> form -> form
 val f_int_edivz : form -> form -> form
 
+(* -------------------------------------------------------------------- *)
+val f_none : ty -> form
+val f_some : form -> form
+
 (* -------------------------------------------------------------------- *)
 val f_is_inf : form -> form
 val f_is_int : form -> form
@@ -466,7 +470,7 @@ type f_subst = private {
   fs_freshen  : bool; (* true means realloc local *)
   fs_loc      : form Mid.t;
   fs_esloc    : expr Mid.t;
-  fs_ty      : ty_subst;
+  fs_ty       : ty_subst;
   fs_mem      : EcIdent.t Mid.t;
   fs_memtype  : EcMemory.memtype option; (* Only substituted in Fcoe *)
   fs_mempred  : mem_pr Mid.t;  (* For predicates over memories,

src/ecDecl.ml

@@ -74,7 +74,7 @@ type operator_kind =
   | OB_nott of notation
 
 and opbody =
-  | OP_Plain  of EcTypes.expr * bool  (* nosmt? *)
+  | OP_Plain  of EcCoreFol.form * bool  (* nosmt? *)
   | OP_Constr of EcPath.path * int
   | OP_Record of EcPath.path
   | OP_Proj   of EcPath.path * int * int
@@ -294,8 +294,7 @@ let operator_as_prind (op : operator) =
   | _ -> assert false
 
 (* -------------------------------------------------------------------- *)
-let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, bd) lc =
-  let axbd = EcCoreFol.form_of_expr EcCoreFol.mhr bd in
+let axiomatized_op ?(nargs = 0) ?(nosmt = false) path (tparams, axbd) lc =
   let axbd, axpm =
     let bdpm = List.map fst tparams in
     let axpm = List.map EcIdent.fresh bdpm in

src/ecDecl.mli

@@ -49,7 +49,7 @@ type operator_kind =
   | OB_nott of notation
 
 and opbody =
-  | OP_Plain  of EcTypes.expr * bool (* nosmt? *)
+  | OP_Plain  of EcCoreFol.form * bool (* nosmt? *)
   | OP_Constr of EcPath.path * int
   | OP_Record of EcPath.path
   | OP_Proj   of EcPath.path * int * int
@@ -169,7 +169,7 @@ val axiomatized_op :
      ?nargs: int
   -> ?nosmt:bool
   -> EcPath.path
-  -> (ty_params * expr)
+  -> (ty_params * form)
   -> locality
   -> axiom
 

src/ecEnv.ml

@@ -2887,8 +2887,7 @@ module Op = struct
     let op = oget (by_path_opt p env) in
     let f  =
       match op.op_kind with
-      | OB_oper (Some (OP_Plain (e, _))) when force || not op.op_opaque ->
-          form_of_expr EcCoreFol.mhr e
+      | OB_oper (Some (OP_Plain (f, _)))
       | OB_pred (Some (PR_Plain f)) when force || not op.op_opaque ->
           f
       | _ -> raise NotReducible

src/ecFol.ml

@@ -54,7 +54,6 @@ let destr_rint f =
 
   | _ -> destr_error "destr_rint"
 
-
 (* -------------------------------------------------------------------- *)
 let fop_int_le     = f_op CI.CI_Int .p_int_le    [] (toarrow [tint ; tint ] tbool)
 let fop_int_lt     = f_op CI.CI_Int .p_int_lt    [] (toarrow [tint ; tint ] tbool)

src/ecHiGoal.ml

@@ -615,8 +615,8 @@ let process_delta ~und_delta ?target (s, o, p) tc =
         let op = EcEnv.Op.by_path (fst p) env in
 
         match op.EcDecl.op_kind with
-        | EcDecl.OB_oper (Some (EcDecl.OP_Plain (e, _))) ->
-            (snd p, op.EcDecl.op_tparams, form_of_expr EcFol.mhr e, args, Some (fst p))
+        | EcDecl.OB_oper (Some (EcDecl.OP_Plain (f, _))) ->
+            (snd p, op.EcDecl.op_tparams, f, args, Some (fst p))
         | EcDecl.OB_pred (Some (EcDecl.PR_Plain f)) ->
             (snd p, op.EcDecl.op_tparams, f, args, Some (fst p))
         | _ ->

src/ecInductive.ml

@@ -3,6 +3,7 @@ open EcUtils
 open EcSymbols
 open EcTypes
 open EcDecl
+open EcCoreFol
 
 module EP = EcPath
 module FL = EcCoreFol
@@ -163,7 +164,7 @@ let datatype_projectors (tpath, tparams, { tydt_ctors = ctors }) =
 
   let do1 i (cname, cty) =
     let thv = EcIdent.create "the" in
-    let the = e_local thv thety in
+    let the = f_local thv thety in
     let rty = ttuple cty in
 
     let do1 j (_, cty2) =
@@ -172,17 +173,17 @@ let datatype_projectors (tpath, tparams, { tydt_ctors = ctors }) =
           (fun ty -> (EcIdent.create (symbol_of_ty ty), ty))
           cty2 in
 
-      e_lam lvars
+      f_lambda
+        (List.map (fun (x, ty) -> (x, GTty ty)) lvars)
         (if   i = j
-         then e_some (e_tuple (List.map (curry e_local) lvars))
-         else e_none rty) in
+         then f_some (f_tuple (List.map (curry f_local) lvars))
+         else f_none rty) in
 
-
-    let body = e_match the (List.mapi do1 ctors) (toption rty) in
-    let body = e_lam [thv, thety] body in
+    let body = f_match the (List.mapi do1 ctors) (toption rty) in
+    let body = f_lambda [thv, GTty thety] body in
 
     let op = Some (OP_Plain (body, false)) in
-    let op = mk_op ~opaque:false tparams body.e_ty op `Global in (* FIXME *)
+    let op = mk_op ~opaque:false tparams body.f_ty op `Global in (* FIXME *)
 
     (cname, op) in
 

src/ecParser.mly

@@ -24,7 +24,7 @@
   let opdef_of_opbody ty b =
     match b with
     | None            -> PO_abstr ty
-    | Some (`Expr e ) -> PO_concr (ty, e)
+    | Some (`Form f ) -> PO_concr (ty, f)
     | Some (`Case bs) -> PO_case  (ty, bs)
     | Some (`Reft rt) -> PO_reft  (ty, rt)
 
@@ -1972,7 +1972,7 @@ operator:
       po_locality = locality; } }
 
 opbody:
-| e=expr   { `Expr e  }
+| f=form   { `Form f  }
 | bs=opbr+ { `Case bs }
 
 opax:
@@ -3785,14 +3785,14 @@ clone_override:
 
 | OP st=nosmt x=qoident tyvars=bracket(tident*)?
     p=ptybinding1* sty=ioption(prefix(COLON, loc(type_exp)))
-    mode=loc(opclmode) e=expr
+    mode=loc(opclmode) f=form
 
    { let ov = {
        opov_nosmt  = st;
        opov_tyvars = tyvars;
        opov_args   = List.flatten p;
        opov_retty  = odfl (mk_loc mode.pl_loc PTunivar) sty;
-       opov_body   = e;
+       opov_body   = f;
      } in
 
      (x, PTHO_Op (`BySyntax ov, unloc mode)) }

src/ecParsetree.ml

@@ -380,7 +380,7 @@ type ptyvardecls =
 
 type pop_def =
   | PO_abstr of pty
-  | PO_concr of pty * pexpr
+  | PO_concr of pty * pformula
   | PO_case  of pty * pop_branch list
   | PO_reft  of pty * (psymbol * pformula)
 
@@ -1197,7 +1197,7 @@ and op_override_def = {
   opov_tyvars : psymbol list option;
   opov_args   : ptybinding list;
   opov_retty  : pty;
-  opov_body   : pexpr;
+  opov_body   : pformula;
 }
 
 and pr_override_def = {

src/ecPrinting.ml

@@ -2262,21 +2262,22 @@ let pp_opdecl_op (ppe : PPEnv.t) fmt (basename, ts, ty, op) =
     | None ->
         Format.fprintf fmt ": %a" (pp_type ppe) ty
 
-    | Some (OP_Plain (e, _)) ->
+    | Some (OP_Plain (f, _)) ->
         let ((subppe, pp_vds), e, has_vds) =
           let (vds, e) =
-            match e.e_node with
-            | Equant (`ELambda, vds, e) -> (vds, e)
-            | _ -> ([], e) in
-          (pp_locbinds ppe ~fv:e.e_fv vds, e,
+            match f.f_node with
+            | Fquant (Llambda, vds, f) ->
+               (List.map (snd_map gty_as_ty) vds, f)
+            | _ -> ([], f) in
+          (pp_locbinds ppe ~fv:f.f_fv vds, e,
            match vds with [] -> false | _ -> true)
         in
           if has_vds then
             Format.fprintf fmt "%t :@ %a =@ %a" pp_vds
-              (pp_type ppe) e.e_ty (pp_expr subppe) e
+              (pp_type ppe) f.f_ty (pp_form subppe) f
           else
             Format.fprintf fmt ":@ %a =@ %a"
-              (pp_type ppe) e.e_ty (pp_expr subppe) e
+              (pp_type ppe) e.f_ty (pp_form subppe) f
     | Some (OP_Constr (indp, i)) ->
         Format.fprintf fmt
           ": %a =@ < %d-th constructor of %a >"

src/ecReduction.ml

@@ -2037,15 +2037,12 @@ let check_bindings exn tparams env s bd1 bd2 =
 
 let rec conv_oper env ob1 ob2 =
   match ob1, ob2 with
-  | OP_Plain(e1,_), OP_Plain(e2,_)  ->
-    Format.eprintf "[W]: ICI1@.";
-    conv_expr env EcSubst.empty e1 e2
-  | OP_Plain({e_node = Eop(p,tys)},_), _ ->
-    Format.eprintf "[W]: ICI2@.";
+  | OP_Plain(f1,_), OP_Plain(f2,_)  ->
+    error_body (is_conv (LDecl.init env []) f1 f2)
+  | OP_Plain({f_node = Fop(p,tys)},_), _ ->
     let ob1 = get_open_oper env p tys  in
     conv_oper env ob1 ob2
-  | _, OP_Plain({e_node = Eop(p,tys)}, _) ->
-    Format.eprintf "[W]: ICI3@.";
+  | _, OP_Plain({f_node = Fop(p,tys)}, _) ->
     let ob2 = get_open_oper env p tys in
     conv_oper env ob1 ob2
   | OP_Constr(p1,i1), OP_Constr(p2,i2) ->

src/ecScope.ml

@@ -1147,12 +1147,12 @@ module Op = struct
           let xs    = snd (TT.trans_binding eenv ue op.po_args) in
           (EcTypes.toarrow (List.map snd xs) codom, `Abstract, [])
 
-      | PO_concr (pty, pe) ->
+      | PO_concr (pty, pf) ->
           let codom   = TT.transty TT.tp_relax eenv ue pty in
           let env, xs = TT.trans_binding eenv ue op.po_args in
-          let body    = TT.transexpcast env `InOp ue codom pe in
-          let lam     = EcTypes.e_lam xs body in
-          (lam.EcTypes.e_ty, `Plain lam, [])
+          let body    = TT.trans_form env ue pf codom in
+          let lam     = f_lambda (List.map (fun (x, ty) -> (x, GTty ty)) xs) body in
+          (lam.f_ty, `Plain lam, [])
 
       | PO_case (pty, pbs) -> begin
           let name = { pl_loc = loc; pl_desc = unloc op.po_name } in
@@ -1189,13 +1189,13 @@ module Op = struct
 
     let uidmap  = EcUnify.UniEnv.close ue in
     let ts      = Tuni.subst uidmap in
-    let es      = e_subst { e_subst_id with es_ty = ts } in
+    let fs      = Fsubst.f_subst (Fsubst.f_subst_init ~sty:ts ()) in
     let ty      = ty_subst ts ty in
     let tparams = EcUnify.UniEnv.tparams ue in
     let body    =
       match body with
       | `Abstract -> None
-      | `Plain e  -> Some (OP_Plain (es e, nosmt))
+      | `Plain e  -> Some (OP_Plain (fs e, nosmt))
       | `Fix opfx ->
           Some (OP_Fix {
             opf_args     = opfx.EHI.mf_args;
@@ -1394,11 +1394,12 @@ module Op = struct
       (`Det, Sem.translate_e env ret) in
 
     let _, aout = Sem.translate_s env cont body.f_body in
-    let aout = e_lam (List.map2 (fun (_, ty) x -> (x, ty)) params ids) aout in
+    let aout = form_of_expr mhr aout in (* FIXME: translate to forms directly? *)
+    let aout = f_lambda (List.map2 (fun (_, ty) x -> (x, GTty ty)) params ids) aout in
 
     let opdecl = EcDecl.{
       op_tparams  = [];
-      op_ty       = aout.e_ty;
+      op_ty       = aout.f_ty;
       op_kind     = OB_oper (Some (OP_Plain (aout, false)));
       op_loca     = op.ppo_locality;
       op_opaque   = false;

src/ecSection.ml

@@ -434,7 +434,7 @@ let on_opdecl (cb : cb) (opdecl : operator) =
      match b with
      | OP_Constr _ | OP_Record _ | OP_Proj   _ -> assert false
      | OP_TC -> assert false
-     | OP_Plain  (e, _) -> on_expr cb e
+     | OP_Plain  (f, _) -> on_form cb f
      | OP_Fix    f ->
        let rec on_mpath_branches br =
          match br with
@@ -715,7 +715,7 @@ let tydecl_fv tyd =
 let op_body_fv body ty =
   let fv = ty_fv_and_tvar ty in
   match body with
-  | OP_Plain (e, _) -> EcIdent.fv_union fv (fv_and_tvar_e e)
+  | OP_Plain (f, _) -> EcIdent.fv_union fv (fv_and_tvar_f f)
   | OP_Constr _ | OP_Record _ | OP_Proj _ | OP_TC -> fv
   | OP_Fix opfix ->
     let fv =
@@ -902,8 +902,8 @@ let generalize_opdecl to_gen prefix (name, operator) =
           match body with
           | OP_Constr _ | OP_Record _ | OP_Proj _ -> assert false
           | OP_TC -> assert false (* ??? *)
-          | OP_Plain (e,nosmt) ->
-            OP_Plain (e_lam extra_a e, nosmt)
+          | OP_Plain (f,nosmt) ->
+            OP_Plain (f_lambda (List.map (fun (x, ty) -> (x, GTty ty)) extra_a) f, nosmt)
           | OP_Fix opfix ->
             let subst = EcSubst.add_opdef EcSubst.empty path tosubst in
             let nb_extra = List.length extra_a in

src/ecSmt.ml

@@ -1091,7 +1091,6 @@ and create_op ?(body = false) (genv : tenv) p =
     let decl =
       match body, op.op_kind with
       | true, OB_oper (Some (OP_Plain (body, false))) ->
-          let body = EcFol.form_of_expr EcFol.mhr body in
           let wparams, wbody = trans_body (genv, lenv) wdom wcodom body in
           WDecl.create_logic_decl [WDecl.make_ls_defn ls (wextra@wparams) wbody]
 
@@ -1449,8 +1448,8 @@ module Frequency = struct
     match EcEnv.Op.by_path_opt p env with
     | Some {op_kind = OB_pred (Some (PR_Plain f)) } ->
       r_union rs (f_ops unwanted_op f)
-    | Some {op_kind = OB_oper (Some (OP_Plain (e, false))) } ->
-      r_union rs (f_ops unwanted_op (form_of_expr mhr e))
+    | Some {op_kind = OB_oper (Some (OP_Plain (f, false))) } ->
+      r_union rs (f_ops unwanted_op f)
     | Some {op_kind = OB_oper (Some (OP_Fix ({ opf_nosmt = false } as e))) } ->
       let rec aux rs = function
         | OPB_Leaf (_, e) -> r_union rs (f_ops unwanted_op (form_of_expr mhr e))

src/ecSubst.ml

@@ -30,7 +30,7 @@ type subst = {
   sb_flocal   : EcCoreFol.form Mid.t;
   sb_fmem     : EcIdent.t Mid.t;
   sb_tydef    : (EcIdent.t list * ty) Mp.t;
-  sb_def      : (EcIdent.t list * [`Expr of expr | `Form of EcCoreFol.form]) Mp.t;
+  sb_def      : (EcIdent.t list * [`Op of  expr | `Pred of form]) Mp.t;
   sb_moddef   : EcPath.path Mp.t;
 }
 
@@ -100,7 +100,7 @@ let subst_mem (s : subst) (m : EcIdent.t) =
 (* -------------------------------------------------------------------- *)
 let get_opdef (s : subst) (p : EcPath.path) =
   match Mp.find_opt p s.sb_def with
-  | Some (ids, `Expr e) -> Some (ids, e) | _ -> None
+  | Some (ids, `Op f) -> Some (ids, f) | _ -> None
 
 (* -------------------------------------------------------------------- *)
 let has_opdef (s : subst) (p : EcPath.path) =
@@ -112,8 +112,8 @@ let get_def (s : subst) (p : EcPath.path) =
   | Some (ids, body) ->
      let body =
        match body with
-       | `Expr e -> form_of_expr mhr e
-       | `Form f -> f in
+       | `Op   e -> form_of_expr mhr e
+       | `Pred f -> f in
      Some (ids, body)
 
   | None -> None
@@ -257,13 +257,13 @@ let add_tydef (s : subst) p (ids, ty) =
   assert (Mp.find_opt p s.sb_tydef = None);
   { s with sb_tydef = Mp.add p (ids, ty) s.sb_tydef }
 
-let add_opdef (s : subst) p (ids, e) =
+let add_opdef (s : subst) p (ids, f) =
   assert (Mp.find_opt p s.sb_def = None);
-  { s with sb_def = Mp.add p (ids, (`Expr e)) s.sb_def }
+  { s with sb_def = Mp.add p (ids, (`Op f)) s.sb_def }
 
 let add_pddef (s : subst) p (ids, f) =
   assert (Mp.find_opt p s.sb_def = None);
-  { s with sb_def = Mp.add p (ids, `Form f) s.sb_def }
+  { s with sb_def = Mp.add p (ids, `Pred f) s.sb_def }
 
 let add_moddef (s : subst) ~(src : EcPath.path) ~(dst : EcPath.path) =
   assert (Mp.find_opt src s.sb_moddef = None);
@@ -962,7 +962,7 @@ and subst_notation (s : subst) (nott : notation) =
 and subst_op_body (s : subst) (bd : opbody) =
   match bd with
   | OP_Plain (body, nosmt) ->
-      OP_Plain (subst_expr s body, nosmt)
+      OP_Plain (subst_form s body, nosmt)
 
   | OP_Constr (p, i)  -> OP_Constr (subst_path s p, i)
   | OP_Record p       -> OP_Record (subst_path s p)