Document Phase 1 imperative syntax in docs and editors#985
Merged
Conversation
Updates docs and editor highlighting for the imperative syntax that already parses (proc, observer, object, mutable array `[T]\!`, frame expressions). Wires #854 into the imperative-verification-plan as the tracking issue, adds concise Reference.md entries for the new declarations plus a Frame Expression section, lists the new statements in SyntaxGrammar.md with the parser/AST-only caveat, and teaches the emacs and vscode highlighters about the imperative keywords. Reference grammar entries are validated by gh_pages/scripts/ reference_grammar.py against Deduce.lark. Items in #969 covering syntax that has not been implemented yet (resource declarations, `emp`/`**`/`|->`, imperative statements, invariant/loop annotations, call labels) are deliberately not addressed here — they will follow once Phases 1d/1e/1h/1i land. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Splits the imperative documentation out of Reference.md into a new gh_pages/doc/ImperativeReference.md so the main reference doesn't grow entries for features that are parser-only today. Reference.md keeps a single pointer at the top; SyntaxGrammar.md's main statement list returns to the original ten entries with a paragraph linking to the experimental page. - gh_pages/doc/ImperativeReference.md: new page with Frame Expression, Object, Observer, Procedure, and a cross-link to the Type grammar for `[T]\!`. - gh_pages/doc/Reference.md: TOC pointer to the new page; previously inlined sections and TOC entries removed. - gh_pages/doc/SyntaxGrammar.md: restored to ten core statements plus a single paragraph pointing at the new page. - gh_pages/scripts/convert.py: register `ImperativeReference` in the html/title/description/deduce-code dicts so the site converter builds it and extracts its `.deduce^#` snippets. - gh_pages/scripts/reference_grammar.py: walk both Reference.md and ImperativeReference.md instead of only the former. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
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.
Summary
Addresses #969 (Phase 1j) for the imperative syntax that has actually
been implemented so far (proc, observer, object, mutable array
[T]!, frame expressions). Items covering syntax not yet parsed —resource declarations,
emp/**/|->, imperative statements,invariant/loop annotations, and call labels — are deliberately left
for future PRs that follow Phases 1d/1e/1h/1i.
The experimental imperative surface lives on its own page rather
than being interleaved into the main reference, so the alphabetized
Reference.md doesn't grow entries that say "parser-only, not
implemented yet."
docs/imperative-verification-plan.md: wires Implement imperative verification layer for controlled state and correctness proofs #854 in as thetracking issue (was "TBD").
gh_pages/doc/ImperativeReference.md(new): Frame Expression,Object, Observer, Procedure sections, plus a cross-link to the
existing
[T]!Type entry. Calls out the Phase 1 parser/AST-onlystatus and which forms need
--experimental-imperative. Hooksthe
object_examplesnippet into a{.deduce^file=...}block sothe site test actually validates it.
gh_pages/doc/Reference.md: a one-paragraph pointer near the topdirecting readers to the new page.
gh_pages/doc/SyntaxGrammar.md: a paragraph below the mainstatement list pointing at the new page; the numbered list is
back to its original ten core statements.
gh_pages/scripts/convert.py:ImperativeReferenceregisteredin the html/title/description/deduce-code dicts so the site
converter builds it and extracts its
.deduce^#snippets.gh_pages/scripts/reference_grammar.py: walks both Reference.mdand ImperativeReference.md instead of only the former, so the
new page's grammar fences are also enforced against
Deduce.lark.editor/emacs/deduce-mode.elandeditor/vscode/syntaxes/deduce.tmLanguage.json: highlightproc,observer,object,ghost,var,requires,ensures,reads,modifies,decreases,footprint, andnew.gh_pages/scripts/keywords.pyalready had the parser-levelkeywords from Gate imperative syntax behind experimental flag #971/Parse experimental mutable arrays and frame clauses #973/Parse proc declarations and specification clauses #977/Parse object declarations and reserve new allocation syntax #981/Parse observer declarations with read frames #983; no change needed there.
Test plan
python3.13 gh_pages/scripts/reference_grammar.py— passes(Checked 158 reference grammar rule(s) across both pages)
python3.13 gh_pages/scripts/keywords.py— passes silentlypython3.13 test-deduce.py --equiv— passespython3.13 test-deduce.py --site— passes; the newdoc_imperative-reference.pfentangled file contains theobject_examplesnippet and validatespython3.13 test-deduce.py --parser— passesmake static— ruff + mypy passemacs --batch -L editor/emacs ... ert-run-tests-batch-and-exit— 31/31 pass
Claude session — fallback UUID:
1552166f-f28b-4846-a53d-8e5ee710f6be🤖 Generated with Claude Code