Open
Conversation
Implement a Lean 4 kernel typechecker using a DAG representation with BUBS (Bottom-Up Beta Substitution) for efficient reduction. The kernel operates on a mutable DAG rather than tree-based expressions, enabling in-place substitution and shared subterm reduction. 12 modules: doubly-linked list, DAG nodes with 10 pointer variants, BUBS upcopy with 12 parent cases, Expr/DAG conversion, universe level operations, WHNF via trail algorithm, definitional equality with lazy delta/proof irrelevance/eta, type inference, and checking for quotients and inductives.
Replace the closure-based NbE (Normalization by Evaluation) kernel with
a direct environment-based approach where types are Exprs throughout.
- Remove Value/Neutral/ValEnv/SusValue semantic domain (Datatypes.lean)
- Replace Eval.lean with Whnf.lean (WHNF via structural + delta reduction)
- Replace Equal.lean with DefEq.lean (staged definitional equality with
lazy delta reduction guided by ReducibilityHints)
- Rewrite Infer.lean to operate on Expr types instead of Values
- Simplify TypecheckM: remove NbE-specific state (evalCacheRef, equalCacheRef),
add whnf/defEq/infer caches as pure state
- Add proof irrelevance, eta expansion, structure eta, nat/string literal
expansion to isDefEq
- Flatten app spines and binder chains in infer/isDefEq to avoid deep recursion
Replace HashMap-based eqvCache with union-find EquivManager (ported from lean4lean) for congruence-aware structural equality caching. Add inferOnly mode that skips argument/let type-checking during inference, used for theorem value checking to handle sub-term type mismatches. Additional isDefEq improvements: - isDefEqUnitLike for non-recursive single-ctor zero-field types - isDefEqOffset for Nat.succ chain short-circuiting - tryUnfoldProjApp in lazy delta for projection-headed stuck terms - cheapProj=true in stage 1 defers full projection reduction to stage 2 - Failure cache on same-head optimization in lazyDeltaReduction - Fix ReducibilityHints.lt' to handle all cases correctly
Move checkStrictPositivity/checkCtorPositivity into the mutual block as monadic checkPositivity/checkCtorFields/checkNestedCtorFields, enabling whnf calls during positivity analysis. This matches lean4lean's checkPositivity and correctly handles nested inductives (e.g. an inductive appearing as a param of a previously-defined inductive). Split KernelTests.lean into Helpers, Unit, and Soundness submodules. Add targeted soundness tests for nested positivity: positive nesting via Wrap, double nesting, multi-field, multi-param, contravariant rejection, index-position rejection, non-inductive head, and unsafe outer. Add Lean.Elab.Term.Do.Code.action as an integration test case requiring whnf-based nested positivity.
- Rewrite lam/forallE/letE inference to iterate binder chains instead of recursing, preventing stack overflow on deeply nested terms - Add inductBlock/inductNames to RecursorVal to track the major inductive separately from rec.all, which can be empty in recursor-only Ixon blocks - Build InductiveBlockIndex to extract the correct major inductive from Ixon recursor types at conversion time - Fix validateRecursorRules to look up ctors from the major inductive directly instead of iterating rec.all - Fix isDefEq call in lazyDeltaReduction (was calling isDefEqCore) - Add regression tests for UInt64 isDefEq, recursor-only blocks, and deeply nested let chains
Switch all kernel caches from Std.HashMap to Std.TreeMap, replacing hash-based lookups with structural comparison (Expr.compare, Level.compare). Expr.compare is fully iterative using an explicit worklist stack, and Expr.beq/liftLooseBVars/instantiate/substLevels/hasLooseBVarsAbove now loop over binder chains to avoid stack overflow on deeply nested terms. Add pointer equality fast paths (ptrEq) for Level and Expr, and a pointer-address comparator (ptrCompare) for the def-eq failure cache.
| let depth := ctx.types.size | ||
| if idx < depth then | ||
| let arrayIdx := depth - 1 - idx | ||
| if h : arrayIdx < ctx.types.size then |
Member
There was a problem hiding this comment.
nit: there's no reason why use if statement here, since arrayIdx is always smaller than the context size
Member
There was a problem hiding this comment.
I think it's just to enable ctx.types[arrayIdx], without the exclamation mark, since h goes into context.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implement a Lean 4 kernel typechecker using a DAG representation with BUBS (Bottom-Up Beta Substitution) for efficient reduction. The kernel operates on a mutable DAG rather than tree-based expressions, enabling in-place substitution and shared subterm reduction.
12 modules: doubly-linked list, DAG nodes with 10 pointer variants, BUBS upcopy with 12 parent cases, Expr/DAG conversion, universe level operations, WHNF via trail algorithm, definitional equality with lazy delta/proof irrelevance/eta, type inference, and checking for quotients and inductives.