Grammar coverage: cartouches, modifiers, subscripts, qualified names, legacy markup

isabelle_parser/thy_grammar.lark

@@ -7,6 +7,9 @@
 QUOTED_STRING: "\"" /[\s\S]*?/ "\""
              | "`" /[\s\S]*?/ "`"
 
+// Legacy (pre-2016) verbatim document/source text: {* ... *}
+VERBATIM_TEXT: /\{\*[\s\S]*?\*\}/
+
 // Tokens for cartouche
 CARTOUCHE_OPEN: "\\<open>"
 CARTOUCHE_TEXT: /[^\\]+/
@@ -1574,7 +1577,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]+>|[a-zA-Z])(_?\d*[a-zA-Z_\']*)*/
+TYPE_IDENT: /\'(\\<[A-Za-z]+>|[a-zA-Z])(\\<\^sub>[a-zA-Z0-9_\']*|_?\d*[a-zA-Z_\']*)*/
 
 SUBSCRIPT: "\\<^sub>"
 
@@ -1594,8 +1597,8 @@ context: (   print_locale
            | print_locales
            | print_state )*
 
-theory: (   goal proof_prove
-          | statement
+theory: (   ("private" | "qualified")? goal proof_prove
+          | ("private" | "qualified")? statement
           | class_instance proof_prove
           | derive )*
 
@@ -1715,7 +1718,7 @@ name: QUOTED_STRING
     | /[+]+/
     | SYM_IDENT
     // | (ID | GREEK | SUBSCRIPT | "." | "_" | NAT | "'" | letter)+
-    | /(([a-zA-Z_][a-zA-Z_0-9\']*(\\<\^sub>[a-zA-Z0-9_]*)?)|(\\<((alpha)|(beta)|(gamma)|(delta)|(epsilon)|(zeta)|(eta)|(theta)|(iota)|(kappa)|(mu)|(nu)|(xi)|(pi)|(rho)|(sigma)|(tau)|(upsilon)|(phi)|(chi)|(psi)|(omega)|(Gamma)|(Delta)|(Theta)|(Lambda)|(Xi)|(Pi)|(Sigma)|(Upsilon)|(Phi)|(Psi)|(Omega))>)|(\\<\\^sub>)|([._'])|([0-9])|([a-zA-Z]+)|(\\?<[a-zA-Z]+>))+/
+    | /(([a-zA-Z_][a-zA-Z_0-9\']*(\\<\^sub>[a-zA-Z0-9_]*)*)|(\\<((alpha)|(beta)|(gamma)|(delta)|(epsilon)|(zeta)|(eta)|(theta)|(iota)|(kappa)|(mu)|(nu)|(xi)|(pi)|(rho)|(sigma)|(tau)|(upsilon)|(phi)|(chi)|(psi)|(omega)|(Gamma)|(Delta)|(Theta)|(Lambda)|(Xi)|(Pi)|(Sigma)|(Upsilon)|(Phi)|(Psi)|(Omega))>)|(\\<\^sub>)|([._'])|([0-9])|([a-zA-Z]+)|(\\?<[a-zA-Z]+>))+/
     | "\\<bottom>"
 
 par_name: "(" name ")"
@@ -1796,7 +1799,7 @@ typespec_sorts: typeargs_sorts? name
 # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 3.3.6
 #
 
-sort: ID | QUOTED_STRING
+sort: ID | LONG_IDENT | QUOTED_STRING
 
 sort_list_comma_sep: sort ("," sort)*
 
@@ -1879,6 +1882,7 @@ attribute: "OF" thms
 args: arg*
 
 arg: ID
+   | LONG_IDENT
    | cartouche
    | "False"
    | "for"
@@ -1945,7 +1949,7 @@ doc_block: (   "chapter"
              | "text"
              | "text_raw"
              | "txt"
-             | COMMENT_CARTOUCHE) ("(" "in" name ")")? (cartouche | QUOTED_STRING | ID)
+             | COMMENT_CARTOUCHE) ("(" "in" name ")")? (cartouche | QUOTED_STRING | VERBATIM_TEXT | ID)
 
 comment_block: COMMENT_CARTOUCHE cartouche
 
@@ -2030,7 +2034,7 @@ thy_bounds: name | ("(" name ("|" name)* ")")
 locale_theory_context: "context" comment_block? name opening? "begin" local_theory "end"
                      | "context" comment_block? includes? context_elem* "begin" local_theory "end"
 
-local_theory_target: "(" "in" name ")"
+local_theory_target: "(" "in" (name | "-") ")"
 
 #
 # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.3
@@ -2185,15 +2189,15 @@ spec: name ("\\<equiv>" | "==") term ("(" "unchecked" ")")?
 #
 
 ml : ( "ML" | "ml" | "ML_file" | "ML_val" | "ML_prf" | "ML_command"
-     | "SML_file" | "setup" | "local_setup" ) (name | cartouche | QUOTED_STRING)
+     | "SML_file" | "setup" | "local_setup" ) (name | cartouche | VERBATIM_TEXT | QUOTED_STRING)
 
 #
 # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.12.2
 #
 
 typedecl : "typedecl" typespec mixfix?
 
-type_synonym : "type_synonym" ("(" "in" name ")")? typespec "=" (ID | QUOTED_STRING) mixfix?
+type_synonym : "type_synonym" ("(" "in" name ")")? typespec "=" (ID | LONG_IDENT | TYPE_IDENT | QUOTED_STRING | cartouche) mixfix?
 
 #
 # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 5.13
@@ -2553,6 +2557,7 @@ mode: ID
     | "(" "input" ")"
     | "(" "output" ")"
     | "(" "ASCII" ")"
+    | "(" name ")"
 
 #
 # https://isabelle.in.tum.de/doc/isar-ref.pdf Section 8.5.2
@@ -2624,8 +2629,8 @@ generic_type : (type | ("(" type ("," type)*")")) name?
 
 constructors : constructor ("|" constructor)*
 
-constructor : comment_block? ID TYPE_IDENT mixfix? comment_block?
-            | comment_block? (   name
+constructor : comment_block? (name ":")? ID TYPE_IDENT mixfix? comment_block?
+            | comment_block? (name ":")? (   name
                                | cartouche
                                | ("(" (cartouche | (name ":" name) | (name ":" QUOTED_STRING)) ")") )+ mixfix? comment_block?
 

tests/test_parser.py

@@ -264,6 +264,40 @@
             "theory T imports Main begin\ntype_synonym 'a mylist = \"'a list\"\nend",
             True,
         ),
+        (
+            "type_synonym_cartouche",
+            "theory T imports Main begin\n"
+            "type_synonym int_poly = \\<open>int mpoly\\<close>\nend",
+            True,
+        ),
+        (
+            "type_synonym_subscripted_type_vars",
+            "theory T imports Main begin\n"
+            "type_synonym ('a\\<^sub>h, 'b\\<^sub>h) sum\\<^sub>h = "
+            "\"'a\\<^sub>h + 'b\\<^sub>h\"\nend",
+            True,
+        ),
+        (
+            "type_synonym_type_var_rhs",
+            "theory T imports Main begin\ntype_synonym 'a blindable = 'a\nend",
+            True,
+        ),
+        (
+            "type_synonym_qualified_rhs",
+            "theory T imports Main begin\ntype_synonym error = String.literal\nend",
+            True,
+        ),
+        (
+            "qualified_toplevel_definition",
+            "theory T imports Main begin\n"
+            'qualified definition bar :: nat where "bar = 0"\nend',
+            True,
+        ),
+        (
+            "private_toplevel_lemma",
+            'theory T imports Main begin\nprivate lemma l: "x = x" by simp\nend',
+            True,
+        ),
         # -----------------------------------------------------------------------
         # Constant declarations
         # -----------------------------------------------------------------------
@@ -609,6 +643,23 @@
             "end",
             True,
         ),
+        (
+            "instance_qualified_class_name",
+            "theory T imports Main begin\ninstance unit :: heap.rep ..\nend",
+            True,
+        ),
+        (
+            "definition_global_target_dash",
+            "theory T imports Main begin\n"
+            'definition (in -) foo :: nat where "foo = 0"\nend',
+            True,
+        ),
+        (
+            "inductive_cases_qualified_attribute_arg",
+            "theory T imports Main begin\n"
+            'inductive_cases fooCases[simplified bar.inject]: "P x"\nend',
+            True,
+        ),
         # -----------------------------------------------------------------------
         # abbreviation with an (output) print mode
         # -----------------------------------------------------------------------
@@ -619,6 +670,25 @@
             "end",
             True,
         ),
+        (
+            "abbreviation_custom_print_mode",
+            "theory T imports Main begin\n"
+            'abbreviation (latex) foo where "foo = x"\n'
+            "end",
+            True,
+        ),
+        (
+            "legacy_verbatim_doc_markup",
+            "theory T imports Main begin\n"
+            "subsubsection {* Monotonicity *}\n"
+            "text {* some legacy text *}\nend",
+            True,
+        ),
+        (
+            "legacy_verbatim_ml_block",
+            "theory T imports Main begin\nML {* val x = 1; fun f y = y + x *}\nend",
+            True,
+        ),
         # -----------------------------------------------------------------------
         # inductive_simps command
         # -----------------------------------------------------------------------
@@ -830,6 +900,22 @@
             True,
         ),
         # -----------------------------------------------------------------------
+        # identifiers with repeated / symbol subscripts in name position
+        # -----------------------------------------------------------------------
+        (
+            "definition_repeated_subscript_name",
+            "theory T imports Main begin\n"
+            "definition lang\\<^sub>M\\<^sub>2\\<^sub>L :: nat where "
+            '"lang\\<^sub>M\\<^sub>2\\<^sub>L = 0"\nend',
+            True,
+        ),
+        (
+            "lemmas_greek_symbol_subscript_name",
+            "theory T imports Main begin\n"
+            "lemmas \\<Delta>\\<^sub>\\<epsilon>_cong = foo\nend",
+            True,
+        ),
+        # -----------------------------------------------------------------------
         # class with multiple superclasses
         # -----------------------------------------------------------------------
         (
@@ -854,13 +940,26 @@
             "theory T imports Main begin\ndatatype ('a::type) box = Box 'a\nend",
             True,
         ),
+        (
+            "datatype_constructor_discriminators",
+            "theory T imports Main begin\n"
+            "datatype pr_op = is_PUSH: PUSH | is_RELABEL: RELABEL\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,
         ),
+        (
+            "datatype_subscripted_type_var_and_constructor",
+            "theory T imports Main begin\n"
+            "datatype 'a\\<^sub>h blindable\\<^sub>h = Content 'a\\<^sub>h\n"
+            "end",
+            True,
+        ),
         # -----------------------------------------------------------------------
         # datatype BNF type-argument annotations (dead / selectors)
         # -----------------------------------------------------------------------