Grammar coverage: multiple superclasses, sort-annotated & Greek type variables

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>"
 
@@ -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?
 
@@ -2602,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

tests/test_parser.py

@@ -811,6 +811,56 @@
             "end",
             True,
         ),
+        # -----------------------------------------------------------------------
+        # Greek type variables (e.g. '\<alpha>)
+        # -----------------------------------------------------------------------
+        (
+            "type_synonym_greek_tvars",
+            "theory T imports Main begin\n"
+            "type_synonym ('\\<alpha>, '\\<beta>) psubst = "
+            "\"'\\<alpha> \\<Rightarrow> '\\<beta>\"\n"
+            "end",
+            True,
+        ),
+        (
+            "datatype_greek_tvar",
+            "theory T imports Main begin\n"
+            "datatype '\\<alpha> wrap = Wrap '\\<alpha>\n"
+            "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 \\<le> x"\n'
+            "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):