diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark index 816fd25..9fac9d6 100644 --- a/isabelle_parser/thy_grammar.lark +++ b/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: "\\" 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]+>))+/ | "\\" 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,7 +2189,7 @@ spec: name ("\\" | "==") 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 @@ -2193,7 +2197,7 @@ ml : ( "ML" | "ml" | "ML_file" | "ML_val" | "ML_prf" | "ML_command" 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? diff --git a/tests/test_parser.py b/tests/test_parser.py index 06e38a9..6043582 100644 --- a/tests/test_parser.py +++ b/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 = \\int mpoly\\\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 \\\\<^sub>\\_cong = foo\nend", + True, + ), + # ----------------------------------------------------------------------- # class with multiple superclasses # ----------------------------------------------------------------------- ( @@ -854,6 +940,12 @@ "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" @@ -861,6 +953,13 @@ "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) # -----------------------------------------------------------------------