fix(subst): also bind expression-locals when substituting a form-local (#1056)

src/ecCoreSubst.ml

@@ -95,6 +95,10 @@ let bind_elocals (s : f_subst) (esloc : expr Mid.t) : f_subst =
 
 (* -------------------------------------------------------------------- *)
 let f_bind_local (s : f_subst) (x : ident) (t : form) : f_subst =
+  let s =
+    match EcCoreFol.expr_of_form t with
+    | e -> bind_elocal s x e
+    | exception EcCoreFol.CannotTranslate -> s in
   let fs_loc = Mid.add x t s.fs_loc in
   let fs_fv = fv_union (f_fv t) s.fs_fv in
   { s with fs_loc; fs_fv; }

src/ecSubst.ml

@@ -217,6 +217,10 @@ let fresh_elocals_opt (s : subst) (locals : (EcIdent.t option * ty) list) =
   List.fold_left_map fresh_elocal_opt s locals
 
 let add_flocal (s : subst) (x : EcIdent.t) (f : EcCoreFol.form) =
+  let s =
+    match EcCoreFol.expr_of_form f with
+    | e -> add_elocal s x e
+    | exception EcCoreFol.CannotTranslate -> s in
   { s with sb_flocal = Mid.add x f s.sb_flocal }
 
 let add_flocals (s : subst) (xs : EcIdent.t list) (fs : EcCoreFol.form list) =
@@ -1215,4 +1219,3 @@ let inv_rebind (inv : inv) (ms : memory list) : inv =
   | Inv_ts ts, [ml; mr] -> Inv_ts (ts_inv_rebind ts ml mr)
   | Inv_hs hs, [m] -> Inv_hs (hs_inv_rebind hs m)
   | _, _ -> assert false
-

tests/eager_call_instanciate.ec

@@ -0,0 +1,33 @@
+require import AllCore.
+
+section SC.
+module S = {
+  proc f(x:int) = { }
+
+  proc g (x:int) = { return x;}
+
+}.
+
+lemma eager_f_sample y : eager [
+  S.f(y);, S.g ~ S.g, S.f(y); :
+    ={x} ==> ={res} ].
+proof.
+eager proc; inline *; swap{1} 1; sim.
+qed.
+
+lemma eager_f_sample' z : eager [
+  S.f(z);, S.g ~ S.g, S.f(z); :
+    ={x} ==> ={res} ].
+proof.
+apply (eager_f_sample z).
+qed.
+
+end section SC.
+
+op b : bool.
+
+lemma toto : b.
+have /= h := eager_f_sample.
+have := h 1.
+admitted.
+