Skip to content

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

Merged
strub merged 1 commit into
mainfrom
slow-reduction
Sep 2, 2026
Merged

fix(subst): convert bound form-locals to expressions lazily#1106
strub merged 1 commit into
mainfrom
slow-reduction

Conversation

@strub

@strub strub commented Sep 2, 2026

Copy link
Copy Markdown
Member

Since 615d335 (#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.

Since 615d335 (#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.
@strub
strub requested a review from bgregoir September 2, 2026 16:00
@strub strub self-assigned this Sep 2, 2026
@strub
strub added this pull request to the merge queue Sep 2, 2026
Merged via the queue into main with commit 665d2d4 Sep 2, 2026
19 checks passed
@strub
strub deleted the slow-reduction branch September 2, 2026 19:03
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants