From 51def0313369442e5c291b955349ccb4f868539a Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 2 Sep 2026 17:48:59 +0200 Subject: [PATCH] fix(subst): convert bound form-locals to expressions lazily MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Since 615d33580 (#1056), `f_bind_local` / `add_flocal` eagerly translate every bound form to an expression so that expression-level locals inside program statements are substituted as well. Both fix-reduction paths (`EcReduction` ι match-fix, `EcCallbyValue.try_reduce_fixdef`) bind the constructor arguments through `f_bind_local` at every recursion step, so reducing a recursive operator over a large datum re-traverses and re-hashconses the whole remaining structure at each step: quadratic time plus heavy GC / weak-table churn. `size [0; ...; 4999] = 5000` took ~10s by `cbv delta`, `simplify delta` or `done`, and ~48s for 10000 elements. The expression-local maps (`fs_eloc`, `sb_elocal`) now hold `expr option Lazy.t`: the translation is suspended at bind time and forced, once per binding, on the first `Elocal` lookup in `e_subst` / `subst_expr`. `None` records the `CannotTranslate` case, preserving the semantics introduced by #1056. Also fix a regression from #1056 in `EcSubst.rename_flocal`: it asserted that no expression binding existed for the renamed local, but `add_flocal` now installs one, so the theory-replay compatibility check for inductive predicates with renamed constructor binders (e.g. `clone T with pred p <- q`) died with an anomaly. The entry is now overwritten, as `f_bind_rename` does. Regression test: `tests/clone_ind_rename_binders.ec`. The 5000-element example drops from 10.4s to 0.036s and scales linearly. `tests/eager_call_instanciate.ec`, `make unit` and `make stdlib` pass. --- src/ecCoreSubst.ml | 37 +++++++++++++++++++------------ src/ecSubst.ml | 26 +++++++++++----------- tests/clone_ind_rename_binders.ec | 17 ++++++++++++++ 3 files changed, 53 insertions(+), 27 deletions(-) create mode 100644 tests/clone_ind_rename_binders.ec diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml index 5df52665e..d8dbe7b78 100644 --- a/src/ecCoreSubst.ml +++ b/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 diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 1cbf0d5a6..4426911dc 100644 --- a/src/ecSubst.ml +++ b/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 -> diff --git a/tests/clone_ind_rename_binders.ec b/tests/clone_ind_rename_binders.ec new file mode 100644 index 000000000..ee55f68d4 --- /dev/null +++ b/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.