Rewrite Core language reference and add transforms doc#1084
Merged
Conversation
Rewrite LangDefDoc.lean as a proper language reference with 5 sections: Introduction, Lambda, Imperative, Strata Core, and Semantics. Add coverage for built-in types, operators, algebraic datatypes, functions, axioms, programs, denotational semantics, and KleeneStmt. Add TransformsDoc.lean documenting program transforms (procedure inlining, call/loop elimination, filtering, axiom removal), analysis modes, and the SMT analysis pipeline. Source changes: add missing docstrings to CmdExt, CallArg, Decl, Program, LSort, StepKleene, and StepKleeneStar. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Contributor
Author
|
@tautschnig We can document the GOTO transforms in the Transforms Doc., going forward. |
joscoh
reviewed
Apr 30, 2026
MikaelMayer
reviewed
May 1, 2026
Contributor
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
Well-structured rewrite of the language reference. The reorganization into five clear sections (Introduction, Lambda, Imperative, Strata Core, Semantics) is a significant improvement. The new docstrings on source types are accurate and useful. The denotational semantics section and the Strata Core section (expressions, types, operators, ADTs, functions, axioms, procedures, programs) are thorough additions.
A few minor items below.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
joscoh
reviewed
May 1, 2026
Unsafe destructors return an arbitrary value of the return type on the wrong constructor, not UB in the C sense. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The partial evaluator is not introduced in this document, so mentioning eval_denote_sound pulls in unexplained concepts. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
joscoh
previously approved these changes
May 1, 2026
MikaelMayer
reviewed
May 1, 2026
Contributor
|
🤖 Removed the empty "GOTO Analysis" section entirely. It can be added back when content is ready. |
MikaelMayer
reviewed
May 1, 2026
joscoh
approved these changes
May 4, 2026
MikaelMayer
approved these changes
May 4, 2026
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
4 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.
Summary
LangDefDoc.leanas a proper 5-section language reference: Introduction, Lambda (syntax + type system), Imperative (commands, statements, KleeneStmt, metadata), Strata Core (expressions, built-in types, built-in operators, type declarations, ADTs, functions, recursive functions, axioms, commands, procedures, programs), and Semantics (Lambda operational + denotational, command, statement, KleeneStmt).TransformsDoc.leandocumenting program transforms (strata transformCLI), analysis modes, and the SMT analysis pipeline.CmdExt,CallArg,Decl,Program,LSort,StepKleene, andStepKleeneStarin the source.Datatypes.md,RecursiveFunctions.md, andVerificationModes.mdpointing to the canonical Verso docs.