From d38f705df01c8aac6bf0e973da8e79e397405aa3 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 20:22:56 +0100 Subject: [PATCH 1/3] Support Greek-letter type variables MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TYPE_IDENT only matched ASCII type variables (`'a`), so type variables written with Greek symbols (`'\`, `'\`) — common in the AFP — were rejected wherever type variables appear (type_synonym, datatype, typedef, …). Extend TYPE_IDENT to allow a `\` symbol after the apostrophe. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index f278373..aab0796 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -1573,7 +1573,7 @@ TERM_VAR: /\?[a-zA-Z](_?\d*[a-zA-Z]*)*\.?\d*/ TYPE_VAR: /'[a-zA-Z](_?\d*[a-zA-Z]*)*\.?\d*/ // Other predefined tokens -TYPE_IDENT: /\'[a-zA-Z](_?\d*[a-zA-Z_\']*)*/ +TYPE_IDENT: /\'(\\<[A-Za-z]+>|[a-zA-Z])(_?\d*[a-zA-Z_\']*)*/ SUBSCRIPT: "\\<^sub>" diff --git a/tests/test_parser.py b/tests/test_parser.py index b17f316..c411b33 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -811,6 +811,24 @@ "end", True, ), + # ----------------------------------------------------------------------- + # Greek type variables (e.g. '\) + # ----------------------------------------------------------------------- + ( + "type_synonym_greek_tvars", + "theory T imports Main begin\n" + "type_synonym ('\\, '\\) psubst = " + "\"'\\ \\ '\\\"\n" + "end", + True, + ), + ( + "datatype_greek_tvar", + "theory T imports Main begin\n" + "datatype '\\ wrap = Wrap '\\\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From 141c20e531e684c1b524ac7402292cba61ede192 Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 20:24:27 +0100 Subject: [PATCH 2/3] Support multiple superclasses in class declarations class_spec only allowed a single parent class name before the context elements, so `class c = foo + bar + linorder` (a chain of superclasses, common in algebraic-hierarchy entries) failed. Allow a `+`-separated list of parent class names, optionally followed by `+ `. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 3 +-- tests/test_parser.py | 17 +++++++++++++++++ 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index aab0796..6fcab6d 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/isabelle_parser/thy_grammar.lark @@ -2146,8 +2146,7 @@ definitions: "defines" definitions_item ("and" definitions_item)* class: "class" class_spec ("begin" local_theory "end")? -class_spec: name "=" ( (name opening? "+" context_elem+) - | (name opening?) +class_spec: name "=" ( (name ("+" name)* opening? ("+" context_elem+)?) | (opening? "+" context_elem+) | context_elem+ ) instantiation? diff --git a/tests/test_parser.py b/tests/test_parser.py index c411b33..090f9ce 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -829,6 +829,23 @@ "end", True, ), + # ----------------------------------------------------------------------- + # class with multiple superclasses + # ----------------------------------------------------------------------- + ( + "class_multiple_superclasses", + "theory T imports Main begin\n" + "class c = ordered_ab_semigroup_add + comm_monoid_add + linorder\n" + "end", + True, + ), + ( + "class_superclasses_then_assumes", + "theory T imports Main begin\n" + 'class c = foo + bar + assumes le: "x \\ x"\n' + "end", + True, + ), ], ) def test_parse(name, test_input, expected): From e1a7d8b3fad4ce378a938898b0af7e84f3c4e08e Mon Sep 17 00:00:00 2001 From: Christian Kissig Date: Tue, 2 Jun 2026 20:27:44 +0100 Subject: [PATCH 3/3] Support sort-annotated type variables in datatype declarations `datatype` used `generic_type` for its left-hand side, which treats type arguments as opaque types and rejects sort annotations like `datatype ('a::type) box = ...`. Switch to `typespec_sorts`, which is the correct shape for a type specification (`(tvar::sort, ...) name`) and already handles plain and Greek type variables. Verified against a corpus sample of real datatype declarations: 0 new regressions vs the previous grammar (one additional declaration now parses). Full unit suite green. Co-Authored-By: Claude Opus 4.8 (1M context) --- isabelle_parser/thy_grammar.lark | 2 +- tests/test_parser.py | 15 +++++++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 6fcab6d..d036a4c 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? generic_type "=" constructors +datatype: "datatype" spec_opts? typespec_sorts "=" constructors # 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 090f9ce..3c0ebf5 100644 --- a/tests/test_parser.py +++ b/tests/test_parser.py @@ -846,6 +846,21 @@ "end", True, ), + # ----------------------------------------------------------------------- + # datatype with sort-annotated type variables + # ----------------------------------------------------------------------- + ( + "datatype_sort_annotated_tvar", + "theory T imports Main begin\ndatatype ('a::type) box = Box 'a\nend", + True, + ), + ( + "datatype_multi_sort_annotated_tvars", + "theory T imports Main begin\n" + "datatype ('a::type, 'b::finite) pair = Pair 'a 'b\n" + "end", + True, + ), ], ) def test_parse(name, test_input, expected):