smt: add [smt_inline] operator tag to δ/β-reduce at use sites

src/ecDecl.ml

@@ -144,7 +144,7 @@ type operator = {
   op_unfold   : int option;
 }
 
-and opopaque = { smt: bool; reduction: bool; }
+and opopaque = { smt: bool; reduction: bool; inline: bool; }
 
 (* -------------------------------------------------------------------- *)
 type axiom_kind = [`Axiom of (Ssym.t * bool) | `Lemma]
@@ -229,7 +229,7 @@ let mk_pred ?clinline ?unfold ~opaque tparams dom body lc =
   gen_op ?clinline ?unfold ~opaque tparams ty kind lc
 
 let optransparent : opopaque =
-  { smt = false; reduction = false; }
+  { smt = false; reduction = false; inline = false; }
 
 let mk_op ?clinline ?unfold ~opaque tparams ty body lc =
   let kind = OB_oper body in

src/ecDecl.mli

@@ -128,7 +128,7 @@ type operator = {
   op_unfold   : int option;
 }
 
-and opopaque = { smt: bool; reduction: bool; }
+and opopaque = { smt: bool; reduction: bool; inline: bool; }
 
 val op_ty        : operator -> ty
 val is_pred      : operator -> bool

src/ecHiPredicates.ml

@@ -83,7 +83,14 @@ let trans_preddecl_r (env : EcEnv.env) (pr : ppredicate located) =
 
   let dom     = Tuni.subst_dom uidmap dom in
 
-  EcDecl.mk_pred ~opaque:optransparent tparams dom body pr.pp_locality
+  let tags    = Ssym.of_list (List.map unloc pr.pp_tags) in
+  let opaque  = {
+    EcDecl.smt       = Ssym.mem "smt_opaque" tags;
+    EcDecl.reduction = Ssym.mem "opaque" tags;
+    EcDecl.inline    = Ssym.mem "smt_inline" tags;
+  } in
+
+  EcDecl.mk_pred ~opaque tparams dom body pr.pp_locality
 
 (* -------------------------------------------------------------------- *)
 let trans_preddecl (env : EcEnv.env) (pr : ppredicate located) =

src/ecParser.mly

@@ -1867,22 +1867,25 @@ exception_:
 (* -------------------------------------------------------------------- *)
 (* Predicate definitions                                                *)
 predicate:
-| locality=locality PRED x=oident
+| locality=locality PRED tags=bracket(ident*)? x=oident
    { { pp_name     = x;
        pp_tyvars   = None;
        pp_def      = PPabstr [];
+       pp_tags     = odfl [] tags;
        pp_locality = locality; } }
 
-| locality=locality PRED x=oident tyvars=tyvars_decl? COLON sty=pred_tydom
+| locality=locality PRED tags=bracket(ident*)? x=oident tyvars=tyvars_decl? COLON sty=pred_tydom
    { { pp_name     = x;
        pp_tyvars   = tyvars;
        pp_def      = PPabstr sty;
+       pp_tags     = odfl [] tags;
        pp_locality = locality; } }
 
-| locality=locality PRED x=oident tyvars=tyvars_decl? p=ptybindings? EQ f=form
+| locality=locality PRED tags=bracket(ident*)? x=oident tyvars=tyvars_decl? p=ptybindings? EQ f=form
    { { pp_name     = x;
        pp_tyvars   = tyvars;
        pp_def      = PPconcr (odfl [] p, f);
+       pp_tags     = odfl [] tags;
        pp_locality = locality; } }
 
 | locality=locality INDUCTIVE x=oident tyvars=tyvars_decl? p=ptybindings?
@@ -1891,6 +1894,7 @@ predicate:
    { { pp_name     = x;
        pp_tyvars   = tyvars;
        pp_def      = PPind (odfl [] p, b);
+       pp_tags     = [];
        pp_locality = locality; } }
 
 indpred_def:

src/ecParsetree.ml

@@ -508,6 +508,7 @@ type ppredicate = {
   pp_name   : psymbol;
   pp_tyvars : psymbol list option;
   pp_def    : ppred_def;
+  pp_tags   : psymbol list;
   pp_locality  : locality;
 }
 

src/ecScope.ml

@@ -1349,7 +1349,8 @@ module Op = struct
     let tags   = Sstr.of_list (List.map unloc op.po_tags) in
     let opaque = {
       smt       = Sstr.mem "smt_opaque" tags;
-      reduction = Sstr.mem "opaque" tags
+      reduction = Sstr.mem "opaque" tags;
+      inline    = Sstr.mem "smt_inline" tags;
     } in
     let unfold =
       match op.po_args with
@@ -1383,7 +1384,7 @@ module Op = struct
               let axop  =
                 let nargs = List.sum (List.map (List.length -| fst) args) in
                   EcDecl.axiomatized_op ~nargs path (tyop.op_tparams, bd) lc in
-              let tyop  = { tyop with op_opaque = { reduction = true; smt = false; }} in
+              let tyop  = { tyop with op_opaque = { reduction = true; smt = false; inline = false; }} in
               let scope = bind scope (unloc op.po_name, tyop) in
               Ax.bind scope (unloc ax, axop)
 

src/ecSmt.ml

@@ -654,9 +654,36 @@ and trans_kpatterns env (ks : (kpattern * w3_known_op) list) (f : form) =
        ks)
 
 (* -------------------------------------------------------------------- *)
+(* Operators tagged `[smt_inline]` are δ/β-reduced at their use sites instead
+   of being emitted as a symbol plus a defining axiom. This keeps lambdas
+   occurring in their bodies monomorphic at the call's instantiation, which
+   avoids the polymorphic higher-order encoding (uni/t2tb bridges) that
+   weaker SMT solvers fail to navigate. *)
+and try_inline ((genv, _) : tenv * lenv) (fp : form) =
+  let hd, args =
+    match fp.f_node with
+    | Fapp (hd, args) -> (hd, args)
+    | _               -> (fp, []) in
+  match hd.f_node with
+  | Fop (p, tys) -> begin
+      match Op.by_path_opt p genv.te_env with
+      | Some op when op.op_opaque.inline -> begin
+          match op.op_kind with
+          | OB_oper (Some (OP_Plain _)) | OB_pred (Some (PR_Plain _)) ->
+              Some (f_app_simpl (Op.reduce ~mode:`Force genv.te_env p tys) args fp.f_ty)
+          | _ -> None
+        end
+      | _ -> None
+    end
+  | _ -> None
+
 and trans_form ((genv, lenv) as env : tenv * lenv) (fp : form) =
   try trans_kpatterns env genv.tk_known_w3 fp with CanNotTranslate ->
 
+  match try_inline env fp with
+  | Some fp -> trans_form env fp
+  | None ->
+
   match fp.f_node with
   | Fquant (qt, bds, body) ->
     begin

theories/prelude/Logic.ec

@@ -181,28 +181,28 @@ pred right_commutative (o:'a -> 'b -> 'a) =
 pred left_distributive (o1:'a -> 'b -> 'a) (o2:'a -> 'a -> 'a) =
   forall x y z, o1 (o2 x y) z = o2 (o1 x z) (o1 y z).
 
-pred right_loop (inv : 'b -> 'b) (o:'a -> 'b -> 'a) =
+pred [smt_inline] right_loop (inv : 'b -> 'b) (o:'a -> 'b -> 'a) =
   forall y, cancel (fun x, o x y) (fun x, o x (inv y)).
 
-pred rev_right_loop inv (o:'a -> 'b -> 'a) =
+pred [smt_inline] rev_right_loop inv (o:'a -> 'b -> 'a) =
   forall y, cancel (fun x, o x (inv y)) (fun x, o x y).
 
-pred left_loop inv (o:'a -> 'b -> 'b) =
+pred [smt_inline] left_loop inv (o:'a -> 'b -> 'b) =
   forall x, cancel (o x) (o (inv x)).
 
-pred rev_left_loop inv (o:'a -> 'b -> 'b) =
+pred [smt_inline] rev_left_loop inv (o:'a -> 'b -> 'b) =
   forall x, cancel (o (inv x)) (o x).
 
-pred right_loop_in p (inv : 'b -> 'b) (o:'a -> 'b -> 'a) =
+pred [smt_inline] right_loop_in p (inv : 'b -> 'b) (o:'a -> 'b -> 'a) =
   forall y, p y => cancel (fun x, o x y) (fun x, o x (inv y)).
 
-pred rev_right_loop_in p inv (o:'a -> 'b -> 'a) =
+pred [smt_inline] rev_right_loop_in p inv (o:'a -> 'b -> 'a) =
   forall y, p y => cancel (fun x, o x (inv y)) (fun x, o x y).
 
-pred left_loop_in p inv (o:'a -> 'b -> 'b) =
+pred [smt_inline] left_loop_in p inv (o:'a -> 'b -> 'b) =
   forall x, p x => cancel (o x) (o (inv x)).
 
-pred rev_left_loop_in p inv (o:'a -> 'b -> 'b) =
+pred [smt_inline] rev_left_loop_in p inv (o:'a -> 'b -> 'b) =
   forall x, p x => cancel (o (inv x)) (o x).
 
 pred left_id e (o:'a -> 'b -> 'b) =