fix(subst): convert bound form-locals to expressions lazily

src/ecCoreSubst.ml

@@ -28,7 +28,10 @@ type f_subst = {
   fs_mod     : EcPath.mpath Mid.t;
   fs_modex   : mod_extra Mid.t;
   fs_loc     : form Mid.t;
-  fs_eloc    : expr Mid.t;
+  (* Expression-level view of [fs_loc] entries, converted on demand:
+     fix-reduction binds large data at every step and almost never
+     substitutes into expressions. [None] when not translatable. *)
+  fs_eloc    : expr option Lazy.t Mid.t;
   fs_mem     : EcIdent.t Mid.t;
   (* free variables in the codom of the substitution *)
   fs_fv      : int Mid.t;
@@ -53,6 +56,15 @@ let fv_Mid (type a)
 =
   Mid.fold (fun _ t s -> fv_union s (fv t)) m s
 
+(* -------------------------------------------------------------------- *)
+let eloc_of_expr (e : expr) : expr option Lazy.t =
+  Lazy.from_val (Some e)
+
+let eloc_of_form (f : form) : expr option Lazy.t =
+  lazy (
+    try  Some (EcCoreFol.expr_of_form f)
+    with EcCoreFol.CannotTranslate -> None)
+
 (* -------------------------------------------------------------------- *)
 let f_subst_init
       ?(freshen=false)
@@ -72,7 +84,7 @@ let f_subst_init
     fs_mod      = Mid.empty;
     fs_modex    = Mid.empty;
     fs_loc      = Mid.empty;
-    fs_eloc     = esloc;
+    fs_eloc     = Mid.map eloc_of_expr esloc;
     fs_mem      = Mid.empty;
     fs_fv       = fv;
   }
@@ -81,27 +93,24 @@ let f_subst_id = f_subst_init ()
 
 (* -------------------------------------------------------------------- *)
 let bind_elocal (s : f_subst) (x : ident) (e : expr) : f_subst =
-  let fs_eloc = Mid.add x e s.fs_eloc in
+  let fs_eloc = Mid.add x (eloc_of_expr e) s.fs_eloc in
   let fs_fv   = fv_union (e_fv e) s.fs_fv in
   { s with fs_eloc; fs_fv; }
 
 (* -------------------------------------------------------------------- *)
 let bind_elocals (s : f_subst) (esloc : expr Mid.t) : f_subst =
-  let merger (_ : ident) (oe1 : expr option) (oe2 : expr option) =
-    match oe2 with None -> oe1 | Some _ -> oe2 in
+  let merger (_ : ident) oe1 oe2 =
+    match oe2 with None -> oe1 | Some e -> Some (eloc_of_expr e) in
   let fs_eloc = Mid.merge merger s.fs_eloc esloc in
   let fs_fv = fv_Mid e_fv esloc s.fs_fv in
   { s with fs_eloc; fs_fv; }
 
 (* -------------------------------------------------------------------- *)
 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; }
+  let fs_loc  = Mid.add x t s.fs_loc in
+  let fs_eloc = Mid.add x (eloc_of_form t) s.fs_eloc in
+  let fs_fv   = fv_union (f_fv t) s.fs_fv in
+  { s with fs_loc; fs_eloc; fs_fv; }
 
 (* -------------------------------------------------------------------- *)
 let f_bind_mem (s : f_subst) (m1 : memory) (m2 : memory) : f_subst =
@@ -141,7 +150,7 @@ let f_bind_rename s xfrom xto ty =
   let xe = e_local xto ty in
   let s  = f_bind_local s xfrom xf in
   (* Free variable already added by f_bind_local *)
-  { s with fs_eloc = Mid.add xfrom xe s.fs_eloc; }
+  { s with fs_eloc = Mid.add xfrom (eloc_of_expr xe) s.fs_eloc; }
 
 (* ------------------------------------------------------------------ *)
 let f_rem_local (s : f_subst) (x : ident) : f_subst =
@@ -249,7 +258,7 @@ let elp_subst (s : f_subst) (lp : lpattern) : f_subst * lpattern =
 let rec e_subst (s : f_subst) (e : expr) : expr =
   match e.e_node with
   | Elocal id -> begin
-    match Mid.find_opt id s.fs_eloc with
+    match obind Lazy.force (Mid.find_opt id s.fs_eloc) with
     | Some e' -> e'
     | None    -> e_local id (ty_subst s e.e_ty)
     end

src/ecSubst.ml

@@ -51,7 +51,7 @@ type subst = {
   sb_module   : EcPath.mpath Mid.t;
   sb_path     : EcPath.path Mp.t;
   sb_tyvar    : ty Mid.t;
-  sb_elocal   : expr Mid.t;
+  sb_elocal   : expr option Lazy.t Mid.t;
   sb_flocal   : EcCoreFol.form Mid.t;
   sb_fmem     : EcIdent.t Mid.t;
   sb_tydef    : (EcIdent.t list * ty) Mp.t;
@@ -262,7 +262,7 @@ let add_module (s : subst) (x : EcIdent.t) (m : EcPath.mpath) =
     { s with sb_module = Mid.change merger x s.sb_module }
 
 let add_elocal (s : subst) (x : EcIdent.t) (e : expr) =
-  { s with sb_elocal = Mid.add x e s.sb_elocal }
+  { s with sb_elocal = Mid.add x (Lazy.from_val (Some e)) s.sb_elocal }
 
 let add_elocals (s : subst) (xs : EcIdent.t list) (es : expr list) =
   List.fold_left2 add_elocal s xs es
@@ -285,12 +285,14 @@ let fresh_elocal_opt (s : subst) ((x, ty) : EcIdent.t option * ty) =
 let fresh_elocals_opt (s : subst) (locals : (EcIdent.t option * ty) list) =
   List.fold_left_map fresh_elocal_opt s locals
 
+(* Expression-level binding converted on demand (see
+   [EcCoreSubst.f_bind_local]); [None] when not translatable. *)
 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 e = lazy (
+    try  Some (EcCoreFol.expr_of_form f)
+    with EcCoreFol.CannotTranslate -> None) in
+  { s with sb_flocal = Mid.add x f s.sb_flocal;
+           sb_elocal = Mid.add x e s.sb_elocal; }
 
 let add_flocals (s : subst) (xs : EcIdent.t list) (fs : EcCoreFol.form list) =
   List.fold_left2 add_flocal s xs fs
@@ -317,9 +319,7 @@ let rename_flocal (s : subst) xfrom xto ty =
   let xf = EcCoreFol.f_local xto ty in
   let xe = EcTypes.e_local xto ty in
   let s  = add_flocal s xfrom xf in
-
-  let merger o = assert (o = None); Some xe in
-  { s with sb_elocal = Mid.change merger xfrom s.sb_elocal }
+  { s with sb_elocal = Mid.add xfrom (Lazy.from_val (Some xe)) s.sb_elocal }
 
 let add_memory (s : subst) (m : EcIdent.t) (target : EcIdent.t) =
   { s with sb_fmem = Mid.add m target s.sb_fmem }
@@ -402,9 +402,9 @@ let subst_expr_lpattern (s : subst) (lp : lpattern) =
 let rec subst_expr (s : subst) (e : expr) =
   match e.e_node with
   | Elocal id -> begin
-      match Mid.find id s.sb_elocal with
-      | aout -> aout
-      | exception Not_found -> e_local id (subst_ty s e.e_ty)
+      match obind Lazy.force (Mid.find_opt id s.sb_elocal) with
+      | Some aout -> aout
+      | None -> e_local id (subst_ty s e.e_ty)
     end
 
   | Evar pv ->

tests/clone_ind_rename_binders.ec

@@ -0,0 +1,17 @@
+(* Overriding a defined inductive predicate by a compatible one whose
+   constructor binders are named differently must not crash the
+   compatibility check (`EcSubst.rename_flocal`). *)
+require import AllCore.
+
+theory T.
+  inductive p (n : int) =
+  | C x of (n = 2 * x).
+end T.
+
+inductive q (n : int) =
+| C y of (n = 2 * y).
+
+clone T as U with pred p <- q.
+
+lemma foo (n : int) : q n => exists x, n = 2 * x.
+proof. by case=> x ->; exists x. qed.