Grammar coverage: cartouches, modifiers, subscripts, qualified names, legacy markup#14
Merged
Merged
Conversation
`type_synonym name = \<open>...\<close>` (cartouche-delimited inner syntax, as opposed to a "..." string) failed to parse: the type_synonym rule only allowed `ID | QUOTED_STRING` on the right of `=`, while every other inner-syntax position already routes through `embedded`, which accepts cartouches. Add `cartouche` to the alternatives. 43 AFP thy files use this form. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`private` and `qualified` are local-theory command modifiers. The
`local_theory` rule (block bodies of context/locale/instantiation) already
allowed them, but the top-level `theory` rule did not, so a bare
`qualified definition ...` / `private lemma ...` directly under
`theory ... begin` failed to parse. Mirror the optional
`("private" | "qualified")?` prefix onto the top-level goal/statement
alternatives.
328 AFP thy files use these modifiers (qualified is standard in HOL/Library
at the global theory level). Adds regression tests.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
TYPE_IDENT only matched plain/Greek type variables (`'a`, `'\<alpha>`), not subscripted ones (`'a\<^sub>h`), even though inner-syntax type positions already accept them. As a result `datatype`/`type_synonym`/ `typedecl` declarations whose type arguments or constructor names carry `\<^sub>` subscripts failed to parse (e.g. AFP's ADS_Construction: `datatype 'a\<^sub>h blindable\<^sub>h = ...`). Extend the TYPE_IDENT terminal with a `\<^sub>...` segment (ordered first in the repeat group so the empty-matching alternative doesn't pre-empt it). Also allow a bare TYPE_IDENT on the type_synonym RHS (`type_synonym 'a foo = 'a`). Adds regression tests. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The `name` terminal allowed at most one `\<^sub>X` segment per identifier and its standalone-subscript alternative had a stray backslash (so it never matched). Identifiers with multiple subscripts (`Seq\<^sub>p\<^sub>t\<^sub>i`, `lang\<^sub>M\<^sub>2\<^sub>L`) or a symbol after the subscript marker (`\<Delta>\<^sub>\<epsilon>`) therefore truncated mid-name, failing every command that names such an entity (definition, lemmas, abbreviation, interpretation, ...). Make the subscript segment repeatable (`?` -> `*`) and fix the standalone `\<^sub>` alternative so subscripts can chain into following Greek/symbol glyphs. 142 AFP files use multi-subscript command names; 773 use a subscript-then-symbol identifier somewhere. Adds regression tests. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`sort` only allowed a bare ID or quoted string, so a qualified class name (`heap.rep`) in an arity failed: `instance unit :: heap.rep ..`. Add the existing LONG_IDENT terminal (dotted identifier) as a sort alternative, which also covers qualified classes anywhere a sort is accepted. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Three independent gaps found by statement-level localization: - `(in -)` local-theory target (global scope) on definition/abbreviation/ etc. — the target rule only allowed `(in name)`. ~94 AFP files. - datatype constructor discriminators: `datatype t = is_PUSH: PUSH | ...` — a constructor may carry a leading `discr:` name. Added the optional `(name ":")?` prefix to both constructor alternatives. - qualified fact names as attribute arguments: `[simplified bar.inject]`, `[OF foo.bar]` — the `arg` rule accepted ID but not LONG_IDENT, so a dotted fact reference inside `[...]` failed. Very common (~960 files use a dotted name inside an attribute bracket). Adds regression tests for each. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The `mode` rule only allowed the literal modes `input`/`output`/`ASCII`
inside parentheses, so a custom print mode — `abbreviation (latex) ...`,
`notation (do_notation) ...`, the modal-logic `(uniA_i)` modes — failed.
Add the general `"(" name ")"` form. ~104 AFP files use a custom print
mode on abbreviation/notation. Adds a regression test.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
`type_synonym error = String.literal` (and other `A.b` qualified type names) failed: the RHS allowed ID/TYPE_IDENT/QUOTED_STRING/cartouche but not LONG_IDENT. Add it. ~21 AFP files. Adds a regression test. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Pre-2016 Isabelle used {* ... *} (rather than cartouches) for document
text and ML/source bodies. Neither parsed: section/subsection/text/etc.
accepted only cartouche/string/ID, and the ML/setup/local_setup rule only
cartouche/name/string. Add a VERBATIM_TEXT terminal (/\{\*...\*\}/,
non-greedy) and wire it into doc_block and the ml rule. Deliberately NOT
added to the hot `embedded` rule (rare legacy method_setup bodies aren't
worth the Earley breadth). ~66 AFP files use {* — 22 in doc commands,
~56 in ML/ML_val/setup blocks. Adds regression tests.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
CI `ruff format --check` flagged the new test cases. No semantic change. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
christiankissig
added a commit
that referenced
this pull request
Jul 7, 2026
… legacy markup (#14) * Accept cartouche RHS in type_synonym declarations `type_synonym name = \<open>...\<close>` (cartouche-delimited inner syntax, as opposed to a "..." string) failed to parse: the type_synonym rule only allowed `ID | QUOTED_STRING` on the right of `=`, while every other inner-syntax position already routes through `embedded`, which accepts cartouches. Add `cartouche` to the alternatives. 43 AFP thy files use this form. Adds a regression test. * Accept private/qualified modifiers on top-level commands `private` and `qualified` are local-theory command modifiers. The `local_theory` rule (block bodies of context/locale/instantiation) already allowed them, but the top-level `theory` rule did not, so a bare `qualified definition ...` / `private lemma ...` directly under `theory ... begin` failed to parse. Mirror the optional `("private" | "qualified")?` prefix onto the top-level goal/statement alternatives. 328 AFP thy files use these modifiers (qualified is standard in HOL/Library at the global theory level). Adds regression tests. * Accept \<^sub> subscripts in type variables and typespec names TYPE_IDENT only matched plain/Greek type variables (`'a`, `'\<alpha>`), not subscripted ones (`'a\<^sub>h`), even though inner-syntax type positions already accept them. As a result `datatype`/`type_synonym`/ `typedecl` declarations whose type arguments or constructor names carry `\<^sub>` subscripts failed to parse (e.g. AFP's ADS_Construction: `datatype 'a\<^sub>h blindable\<^sub>h = ...`). Extend the TYPE_IDENT terminal with a `\<^sub>...` segment (ordered first in the repeat group so the empty-matching alternative doesn't pre-empt it). Also allow a bare TYPE_IDENT on the type_synonym RHS (`type_synonym 'a foo = 'a`). Adds regression tests. * Accept repeated and symbol subscripts in identifier names The `name` terminal allowed at most one `\<^sub>X` segment per identifier and its standalone-subscript alternative had a stray backslash (so it never matched). Identifiers with multiple subscripts (`Seq\<^sub>p\<^sub>t\<^sub>i`, `lang\<^sub>M\<^sub>2\<^sub>L`) or a symbol after the subscript marker (`\<Delta>\<^sub>\<epsilon>`) therefore truncated mid-name, failing every command that names such an entity (definition, lemmas, abbreviation, interpretation, ...). Make the subscript segment repeatable (`?` -> `*`) and fix the standalone `\<^sub>` alternative so subscripts can chain into following Greek/symbol glyphs. 142 AFP files use multi-subscript command names; 773 use a subscript-then-symbol identifier somewhere. Adds regression tests. * Accept qualified class names in sort/arity positions `sort` only allowed a bare ID or quoted string, so a qualified class name (`heap.rep`) in an arity failed: `instance unit :: heap.rep ..`. Add the existing LONG_IDENT terminal (dotted identifier) as a sort alternative, which also covers qualified classes anywhere a sort is accepted. Adds a regression test. * Accept (in -) target, ctor discriminators, qualified attribute args Three independent gaps found by statement-level localization: - `(in -)` local-theory target (global scope) on definition/abbreviation/ etc. — the target rule only allowed `(in name)`. ~94 AFP files. - datatype constructor discriminators: `datatype t = is_PUSH: PUSH | ...` — a constructor may carry a leading `discr:` name. Added the optional `(name ":")?` prefix to both constructor alternatives. - qualified fact names as attribute arguments: `[simplified bar.inject]`, `[OF foo.bar]` — the `arg` rule accepted ID but not LONG_IDENT, so a dotted fact reference inside `[...]` failed. Very common (~960 files use a dotted name inside an attribute bracket). Adds regression tests for each. * Accept custom print-mode names in mode annotations The `mode` rule only allowed the literal modes `input`/`output`/`ASCII` inside parentheses, so a custom print mode — `abbreviation (latex) ...`, `notation (do_notation) ...`, the modal-logic `(uniA_i)` modes — failed. Add the general `"(" name ")"` form. ~104 AFP files use a custom print mode on abbreviation/notation. Adds a regression test. * Accept qualified type names on the type_synonym RHS `type_synonym error = String.literal` (and other `A.b` qualified type names) failed: the RHS allowed ID/TYPE_IDENT/QUOTED_STRING/cartouche but not LONG_IDENT. Add it. ~21 AFP files. Adds a regression test. * Accept legacy {* ... *} verbatim markup in document and ML blocks Pre-2016 Isabelle used {* ... *} (rather than cartouches) for document text and ML/source bodies. Neither parsed: section/subsection/text/etc. accepted only cartouche/string/ID, and the ML/setup/local_setup rule only cartouche/name/string. Add a VERBATIM_TEXT terminal (/\{\*...\*\}/, non-greedy) and wire it into doc_block and the ml rule. Deliberately NOT added to the hot `embedded` rule (rare legacy method_setup bodies aren't worth the Earley breadth). ~66 AFP files use {* — 22 in doc commands, ~56 in ML/ML_val/setup blocks. Adds regression tests. * Apply ruff format to test additions CI `ruff format --check` flagged the new test cases. No semantic change. ---------
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.
Eleven focused grammar-coverage fixes (one per commit, each with a regression
test in
tests/test_parser.py). All target real constructs found by sweepingthe AFP 2026-06-01 corpus and localizing failures at the statement level.
Fixes
63e4fa4type_synonym(= \<open>int mpoly\<close>)7d5da0bprivate/qualifiedmodifiers on top-level commandsf30312b\<^sub>subscripts inTYPE_IDENT+ bare type-vartype_synonymRHSac4e7afnameterminal (was capped at one)a176417heap.rep) insort/arity (LONG_IDENT)2a2f14c(in -)global target; datatype ctor discriminators (is_PUSH: PUSH); qualified fact names as attribute args ([simplified bar.inject])bb41243abbreviation (latex))5b01c3ftype_synonymRHS (= String.literal)a00d27e{* ... *}verbatim markup in doc/ML blocks(Commits 4 and 6 each bundle closely-related sub-fixes; "files" columns are
corpus
grepestimates of how many files use the construct, not all fullyunblocked.)
Measured impact
Re-swept the same seeded 1200-file sample (
scripts/sweep_coverage.py,16-worker / 12s-timeout methodology) before and after:
12s-timeout-boundary noise driven by parallel-worker CPU contention, not the
grammar (verified: several "timeout" files parse in 4-6s single-threaded).
Notes
VERBATIM_TEXTis wired intodoc_blockand themlrule only, not thehot
embeddedrule, to avoid adding Earley breadth on the parser's busiestpath (parse speed is the project's known Grammar coverage: support ML/FFI, bare class, quoted sorts, (output), inductive_simps, datatype options #1 cost).
🤖 Generated with Claude Code