From da90f34a5c1ceb014f6b554eb3fa200813acd4cf Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 21:45:38 +0100 Subject: [PATCH 1/4] Support BNF type-argument annotations in datatype datatype type arguments could be plain or sort-annotated type variables, but not the BNF annotations `dead 'a` (dead variable) or selector-style `name: 'a` (set-function name), e.g. `datatype ('s, dead 'p) t` / `datatype (dverts: 'a, darcs: 'b) graph`. Introduce a datatype-specific `dt_typespec` that allows these. Regression-checked against a corpus sample of real datatype declarations: 0 new regressions. Full unit suite green. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 10 +++++++++- tests/test_parser.py | 17 +++++++++++++++++ 2 files changed, 26 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index d036a4c..6b46ae6 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2601,7 +2601,15 @@ termination: "termination" term? proof_prove | "nominal_termination" ("(" name ")")? term? proof_prove # TODO generated from examples -datatype: "datatype" spec_opts? typespec_sorts "=" constructors +datatype: "datatype" spec_opts? dt_typespec "=" constructors + +# Type specification for datatype left-hand sides. Beyond plain and +# sort-annotated type variables it allows the BNF annotations `dead 'a` and +# selector-style `name: 'a`. +dt_typespec: dt_typeargs? name +dt_typeargs: dt_typearg + | "(" dt_typearg ("," dt_typearg)* ")" +dt_typearg: "dead"? (name ":")? TYPE_IDENT ("::" sort)? # Option block for spec commands, e.g. (plugins del: size), (nonexhaustive), # (transfer). The excluded apostrophe keeps this from matching a leading type diff --git a/tests/test_parser.py b/tests/test_parser.py index 3c0ebf5..b385624 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -861,6 +861,23 @@ "end", True, ), + # ----------------------------------------------------------------------- + # datatype BNF type-argument annotations (dead / selectors) + # ----------------------------------------------------------------------- + ( + "datatype_dead_tvars", + "theory T imports Main begin\n" + "datatype ('s, dead 'p, dead 'f) t = A 's\n" + "end", + True, + ), + ( + "datatype_selector_tvars", + "theory T imports Main begin\n" + "datatype (dverts: 'a, darcs: 'b) graph = G\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 9a521606db6388a2b227a123d5b31c7f85b885e3 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 21:46:49 +0100 Subject: [PATCH 2/4] Support the nominal_datatype command `nominal_datatype` (Nominal2 entries) has the same outer shape as `datatype`, so accept it through the same rule. Binder annotations in constructors remain out of scope, but plain nominal datatypes now parse. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 10 ++++++++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 6b46ae6..9935c05 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2601,7 +2601,7 @@ termination: "termination" term? proof_prove | "nominal_termination" ("(" name ")")? term? proof_prove # TODO generated from examples -datatype: "datatype" spec_opts? dt_typespec "=" constructors +datatype: ("datatype" | "nominal_datatype") spec_opts? dt_typespec "=" constructors # Type specification for datatype left-hand sides. Beyond plain and # sort-annotated type variables it allows the BNF annotations `dead 'a` and diff --git a/tests/test_parser.py b/tests/test_parser.py index b385624..7cc87b5 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -878,6 +878,16 @@ "end", True, ), + # ----------------------------------------------------------------------- + # nominal_datatype (same shape as datatype) + # ----------------------------------------------------------------------- + ( + "nominal_datatype", + "theory T imports Main begin\n" + "nominal_datatype pi = PiNil | Tau pi | Sum pi pi\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From c7d5420fa143e8ad9e9708ebfa500a8ab361485d Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 21:47:58 +0100 Subject: [PATCH 3/4] Support `for` parameters on the method command The `method` definition command can bind parameters, e.g. `method m for x :: "'a" and y = ...`. Allow an optional `for_fixes` clause between the method name and `=`. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 17 +++++++++++++++++ 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 9935c05..ad86b67 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1670,7 +1670,7 @@ statement: abbreviation | value | values -method_block: "method" name "=" instruction +method_block: "method" name for_fixes? "=" instruction instruction: single_instruction | single_instruction instruction_modifier diff --git a/tests/test_parser.py b/tests/test_parser.py index 7cc87b5..3abc09d 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -888,6 +888,23 @@ "end", True, ), + # ----------------------------------------------------------------------- + # method definition with `for` parameters + # ----------------------------------------------------------------------- + ( + "method_with_for_param", + "theory T imports Main begin\n" + 'method interval_split for x :: "nat" = (rule x)\n' + "end", + True, + ), + ( + "method_with_for_and", + "theory T imports Main begin\n" + 'method m for a :: "\'a" and b :: "\'b" = (simp)\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 08086d85a8e689653ab3a0a06a29c9213fe7e324 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 21:49:53 +0100 Subject: [PATCH 4/4] Support the (in target) qualifier on unbundle `unbundle` could only take a list of bundle names; the optional `(in target)` qualifier (e.g. `unbundle (in foo) no bar`) was rejected. Allow it before the bundle list. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 8 ++++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index ad86b67..10aae13 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2044,7 +2044,7 @@ includes: "includes" name* opening: "opening" name* -unbundle: "unbundle" name* +unbundle: "unbundle" ("(" "in" name ")")? name* # # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.4 diff --git a/tests/test_parser.py b/tests/test_parser.py index 3abc09d..19a3286 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -905,6 +905,14 @@ "end", True, ), + # ----------------------------------------------------------------------- + # unbundle with an (in target) qualifier + # ----------------------------------------------------------------------- + ( + "unbundle_in_target", + "theory T imports Main begin\nunbundle (in foo) no funcset_syntax\nend", + True, + ), ], ) def test_parse(name, test_input, expected):