Grammar coverage: niche form gaps (datatype BNF annotations, nominal_datatype, method for-params, unbundle in-target)

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
@@ -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
@@ -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" | "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
+# 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

tests/test_parser.py

@@ -861,6 +861,58 @@
             "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,
+        ),
+        # -----------------------------------------------------------------------
+        # 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,
+        ),
+        # -----------------------------------------------------------------------
+        # 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,
+        ),
+        # -----------------------------------------------------------------------
+        # 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):