let-expressions in the element language - #48
Merged
Merged
Conversation
Strong (definition-carrying) form: the body is typed under the definiens' value and its unfolding equation, so el-reflect makes the definiendum unfold judgementally inside the body — a definitional context entry with no new context former. Conservative: let a b ≐ ((λ (λ b)) a) ⋆; retained so a local definition reads and prints as one. Rules: el-let, el-let-beta, el-sub-let, el-let-cong.
Kernel: el-let-beta as an nf contraction (a let is always a redex, so normal forms and equation replay never meet one — no new finals or selectors), child indexing, item-level bidirectional rules (checking at T[↑ ∘ ↑] is fully general under the unfolding hypothesis); the proof fragment excludes let. Elaboration: surface form 'let x ≔ e in b' (annotated variant sugar for ascription), e-let / e-let-check propagating the ambient mode to the body, definiens always inferred; the unfolding hypothesis feeds E's existing HYPOTHESIS source, so the definition is transparent in the body with no new discharge mechanism.
Core: Let former (Syntax/Subst/Beta/Compute — always a redex, one fuel per contraction); kernel item-level bidirectional rules (body checked at T[↑ ∘ ↑] under the value and its unfolding equation); excluded from the proof fragment and the typed descent, per spec. Elaboration: surface 'let x ≔ e in b' (annotated definiens sugar for ascription), both-mode e-let/e-let-check; the body's surface indices are counted against the core two-binder context (the parser pushes a wildcard slot for the unfolding hypothesis, so x resolves to index 1); the hypothesis feeds the existing HYPOTHESIS discharge source, making the definition transparent inside the body. Printer renders the core form back as 'let x ≔ e in b' with the hypothesis entry anonymous. Tests: kernel + surface parser goldens, accepted-file and obligation- report goldens, an evaluation golden; src/nova/letExpr.nova exercises nested/annotated lets, inference position, and in-body transparency.
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
1 participant
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.
Adds
let-expressions to Nova, end to end: theory, kernel and elaboration specs, implementation, tests, and a corpus file.Closes #47
Theory (NovaFoundation.txt)
The strong (definition-carrying) form: in
let a b, the body is typed under two binders — the definiens' value and its unfolding equationPrf (☐₀ ≡ a[↑] ∈ A[↑])— soel-reflectmakes the definiendum unfold judgementally inside the body. This is a definitional context entry with no new context former: extensionally, a definition is a variable plus a Prf of its unfolding. Conservative (let a b ≐ ((λ (λ b)) a) ⋆); retained so a local definition reads and prints as one rather than as its λ-plumbing. Rules:el-let,el-let-beta(let a b ≜ b[id, a, ⋆]),el-sub-let,el-let-cong. No eta, no injectivity — it is not a type former.Kernel spec & implementation
A let is always a redex, so nf contracts every one and normal forms contain no let — equation replay, selectors, and the typed descent needed no extension. Additions: the nf contraction clause, child indexing (
let a b → 0, 1(2)), and item-level bidirectional rules — definiens inferred, body checked atT[↑ ∘ ↑]under the value and its unfolding equation (fully general, not an approximation: under the hypothesis(id, a, ⋆) ∘ (↑ ∘ ↑) ≐ id). The proof fragment excludes let.Elaboration spec & implementation
Surface form
let x ≔ e in b, withlet x : T ≔ e in bas parse-level sugar for an ascribed definiens. let is both-mode: the body elaborates in the ambient mode (e-let/e-let-check), so checking-only body forms need no ascription. The unfolding hypothesis is a Prf of an equality prop, so the equation store's existing HYPOTHESIS source reflectsx ≐ einto discharge automatically — the definition is transparent inside the body with no new mechanism. The body's surface indices are counted against the core two-binder context (the parser pushes a never-resolvable wildcard slot for the hypothesis, soxresolves to index 1). The printer renders core lets back aslet x ≔ e in b, the hypothesis entry anonymous:Tests & corpus
Five new goldens (kernel parse, surface parse, accepted file, obligation report, evaluation);
src/nova/letExpr.novaexercises nested and annotated lets, a let in inference position, in-body transparency (a⋆stated at the abbreviation paying a goal stated at the unfolding), and the outside view (a let is judgementally its unfolding). Suite: 132/132 tests, 26/26 corpus elaborations.