parser.ml revision 93cd42c036c9ef3fed58d4872bab5d72371d80d1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructure TheoryData = struct
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski type opt_target = (xstring * Position.T) option;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski datatype misc_body = Chapter of opt_target * string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |Section of opt_target * string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |Subsection of opt_target * string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Subsubsection of opt_target * string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Text of opt_target * string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |TextRaw of opt_target * string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Sect of string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |Subsect of string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |Subsubsect of string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |Txt of string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |TxtRaw of string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |DiagnosticCommand of string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |TopLevelCommand of string;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski type proof = string;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski type ml_text = string * Position.T;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski type orig = Token.T list;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski datatype context_head = ContextNamed of xstring * Position.T
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |ContextHead of ((xstring * Position.T) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski datatype instance_type = InstanceArity of string list * string list *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |InstanceSubset of string * string * string;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski datatype thy_body =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Classes of (binding * string list) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |Classrel of (string * string) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |DefaultSort of opt_target * string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |TypeDecl of ((opt_target * string list) * binding) * mixfix
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |TypeSynonym of ((opt_target * string list) * binding) *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (string * mixfix)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |Nonterminal of binding list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |Arities of (string * string list * string) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Judgement of (binding * string * mixfix)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Consts of (binding * string * mixfix) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Syntax of (string * bool) * (string * string * mixfix) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |NoSyntax of (string * bool) * (string * string * mixfix) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Translations of (xstring * string) Syntax.trrule list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |NoTranslations of (xstring * string) Syntax.trrule list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Axioms of (Attrib.binding * string) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Defs of (bool * bool) * ((binding * string) * Args.src list) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Definition of opt_target * ((binding * string option * mixfix) option
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Abbreviation of opt_target * ((string * bool) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ((binding * string option * mixfix) option * string))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |TypeNotation of opt_target * ((string * bool) * (string * mixfix) list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |NoTypeNotation of opt_target * ((string * bool) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (string * mixfix) list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Notation of opt_target * ((string * bool) * (string * mixfix) list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |NoNotation of opt_target * ((string * bool) * (string * mixfix) list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Axiomatization of (binding * string option * mixfix) list *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Attrib.binding * string list) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |Theorems of (opt_target * (Attrib.binding *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (binding * string option * mixfix) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Lemmas of (opt_target * (Attrib.binding *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (binding * string option * mixfix) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Declare of (opt_target * (Facts.ref * Args.src list) list list) *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (binding * string option * mixfix) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Hide of string * (bool * xstring list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Use of string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |ML of ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |ML_prf of ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |ML_val of ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |ML_command of ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Setup of ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |LocalSetup of opt_target * ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |AttributeSetup of (bstring * Position.T) * (ml_text * string)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |MethodSetup of (bstring * Position.T) * (ml_text * string)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Declaration of (opt_target * bool) * ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |SyntaxDeclaration of (opt_target * bool) * ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |SimprocSetup of (((opt_target * (bstring * Position.T)) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski string list) * ml_text) * xstring list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |ParseAstTranslation of bool * (string * Position.T)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |ParseTranslation of bool * (string * Position.T)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |PrintTranslation of bool * (string * Position.T)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |TypedPrintTranslation of bool * (string * Position.T)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |PrintAstTranslation of bool * (string * Position.T)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |Oracle of (bstring * Position.T) * ml_text
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |Bundle of ((opt_target * binding) * (Facts.ref * Args.src list) list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (binding * string option * mixfix) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Include of (xstring * Position.T) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Including of (xstring * Position.T) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |PrintBundles
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Context of context_head * (orig * thy_body) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Locale of (binding * (Expression.expression * Element.context list))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * (orig * thy_body) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Sublocale of ((xstring * Position.T) * (Expression.expression *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Attrib.binding * string) list)) * proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Interpretation of (Expression.expression *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Attrib.binding * string) list) * proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Class of (binding * (string list * Element.context list)) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (orig * thy_body) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Subclass of opt_target * string * proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Instantiation of (string list * string list * string) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (orig * thy_body) list
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski |Instance of (instance_type option) * proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Overloading of (bstring * string * bool) list * (orig * thy_body) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Theorem of (((opt_target * Attrib.binding) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (xstring * Position.T) list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Element.context list * Element.statement)) * proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Lemma of (((opt_target * Attrib.binding) *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (xstring * Position.T) list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Element.context list * Element.statement)) * proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Corollary of (((opt_target * Attrib.binding) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (xstring * Position.T) list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Element.context list * Element.statement)) * proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |SchematicTheorem of (((opt_target * Attrib.binding) *
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski (xstring * Position.T) list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Element.context list * Element.statement)) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |SchematicLemma of (((opt_target * Attrib.binding) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (xstring * Position.T) list) *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (Element.context list * Element.statement)) * proof
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski |SchematicCorollary of (((opt_target * Attrib.binding) *
e91e02579a34e005734059ad09e0d1d1304a03e0Till Mossakowski (xstring * Position.T) list) *
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (Element.context list * Element.statement)) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Primrec of (opt_target * (binding * string option * mixfix) list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Datatype of Datatype.spec_cmd list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |RepDatatype of string list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Fun of opt_target * ((Function_Common.function_config * (binding *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski string option * mixfix) list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Attrib.binding * string) list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |PartialFunction of xstring * ((binding * string option * mixfix) list *
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski |Function of (opt_target * ((Function_Common.function_config *
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (binding * string option * mixfix) list)
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski * (Attrib.binding * string) list)) * proof
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski |Termination of string option * proof
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski |Misc of misc_body;
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskisignature ParserHelper =
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val cmd_theory : (Token.T list * Thy_Header.header) parser
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val cmd_header : string parser
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val thy_body : (Token.T list * TheoryData.thy_body) parser
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val init_thy : (Token.T list * Thy_Header.header) ->
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskistructure ParserHelper : ParserHelper =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski open TheoryData
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val hide = curry Hide;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun preserve_toks f toks =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val (v,toks') = f toks
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val consumed_toks = List.take(toks,List.length toks-
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in ((consumed_toks,v),toks') end;
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski(* Common Functions *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fun RESET_VALUE atom =
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (fn (arg, x) => (Token.assign NONE arg; x));
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fun token p = RESET_VALUE (Scan.one p);
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fun unparse_kind k = Parse.group (fn () => Token.str_of_kind k)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (token (Token.is_kind k) >> Token.unparse);
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val unparse_verbatim = unparse_kind Token.Verbatim;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val not_command = Parse.group (fn () => "non-command token")
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (token (not o Token.is_command));
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun command s = Parse.group (fn () => "command "^s)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (token (fn t => Token.is_command t andalso
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun command_with_args s = command s -- Scan.repeat not_command >> op::;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* line 12 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val cmd_theory = preserve_toks (Parse.command_name "theory"
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (* line 14 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val cmd_header = Parse.command_name "header" |-- unparse_verbatim;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (* line 133 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val opt_mode =
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* line 129 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski let val mode_spec = (@{keyword "output"} >> K ("", false)) ||
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder (@{keyword "output"} >> K false) true;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski in Scan.optional (@{keyword "("} |-- Parse.!!!
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski (mode_spec --| @{keyword ")"})) Syntax.mode_default end;
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val trans_line = (* line 157 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski let val trans_pat = (* line 147 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (@{keyword "("} |-- Parse.!!!
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (Parse.xname --| @{keyword ")"}))
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fun trans_arrow toks = (* line 152 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"})
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (@{keyword "\<leftharpoondown>"} || @{keyword "<="})
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (@{keyword "\<rightleftharpoons>"} || @{keyword "=="})
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >> (fn (left, (arr, right)) => arr (left, right)) end;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun first' l = Scan.first (List.map preserve_toks l);
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun parse_interpretation_arguments mandatory = (* line 428 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Parse.!!! (Parse_Spec.locale_expression mandatory) --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* line 514 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val parse_theorem = Parse.opt_target --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Scan.optional (Parse_Spec.opt_thm_name ":" --|
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Parse_Spec.statement_keyword)) Attrib.empty_binding --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val mk_thy_body = List.map (fn (s,p) => Parse.command_name s |-- p);
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* partition (l : a' list) into sublist according predicate
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (p : 'a -> bool) which signals the start of a new sublist,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski i.e. the start of each sublist will satisfy p and all
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski other elements of each sublist will not. Only the first
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski sublist may start with an element that does not satisfy p.
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski example: partition (curry op= "a") "abababab"
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski = ["ab","ab","ab","ab"] *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski fun partition p l = #2 (List.foldr
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (fn (x,(l1,l2)) => if (p x) then ([],(x::l1)::l2)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski else (x::l1,l2)) ([],[]) l);
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun proof_qed i = Parse.group (fn () => "proof_qed")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski [command_with_args "qed" --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski proof_qed (i-1) >> op@,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski command "oops" >> single,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski command_with_args "proof"
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski -- proof_qed (i+1) >> op@,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Scan.repeat not_command >> op::)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski -- proof_qed i >> op@] t
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski else ([],t));
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski [command_with_args "apply",
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski command_with_args "using",
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski command_with_args "unfolding"]) >> flat;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val unparse_tokens = (List.map (List.map Token.unparse)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> List.map (space_implode " ")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> cat_lines) o (partition Token.is_command);
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val proof = Parse.!!! ((proof_prefix -- Scan.first
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski [command_with_args "proof" -- proof_qed 1 >> op@,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski command "oops" >> single,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski command_with_args "by",
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski command ".." >> single,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski command "." >> single]) >> op@
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >> unparse_tokens);
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val simple_thy_body' = first' (mk_thy_body [
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("chapter", Parse.opt_target -- unparse_verbatim
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >> (Misc o Chapter)), (* line 19 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("section", Parse.opt_target -- unparse_verbatim
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >> (Misc o Section)), (* line 24 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("subsection", Parse.opt_target -- unparse_verbatim
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >> (Misc o Subsection)), (* line 29 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("subsubsection", Parse.opt_target -- unparse_verbatim
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >> (Misc o Subsubsection)), (* line 34 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("text", Parse.opt_target -- unparse_verbatim
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski >> (Misc o Text)), (* line 39 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski ("text_raw", Parse.opt_target -- unparse_verbatim
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >> (Misc o Text)), (* line 44 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("sect", unparse_verbatim >> (Misc o Sect)), (* line 49 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("subsect", unparse_verbatim >> (Misc o Sect)), (* line 54 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("subsubsect", unparse_verbatim
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >> (Misc o Subsubsect)), (* line 59 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("txt", unparse_verbatim >> (Misc o Txt)), (* line 64 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("txt_raw", unparse_verbatim >> (Misc o TxtRaw)), (* line 69 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("classes",Scan.repeat1 (Parse.binding -- (* line 79 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Scan.optional ((@{keyword "\<subseteq>"}
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski || @{keyword "<"}) |-- Parse.!!!
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (Parse.list1 Parse.class)) []) >> Classes),
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("classrel",Parse.and_list1 (Parse.class -- (* line 85 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski ((@{keyword "\<subseteq>"} || @{keyword "<"})
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski |-- Parse.!!! Parse.class)) >> Classrel),
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski ("default_sort",Parse.opt_target -- Parse.sort
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski >> DefaultSort), (* line 92 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski ("type_decl",Parse.opt_target -- Parse.type_args (* line 99 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski >> TypeDecl),
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("type_synonym", (* line 104 *)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski let val p = Parse.opt_target -- Parse.type_args --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Parse.binding -- (Parse.$$$ "=" |-- Parse.!!!
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski in p >> TypeSynonym end),
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski ("nonterminal",Parse.and_list1 Parse.binding
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski >> Nonterminal), (* line 110 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("arities",Scan.repeat1 Parse.arity >> Arities), (* line 115 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("judgement",Parse.const_binding >> Judgement), (* line 122 *)
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski >> Consts), (* line 126 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("syntax",opt_mode -- Scan.repeat1 Parse.const_decl
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski >> Syntax), (* line 137 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("no_syntax",opt_mode -- Scan.repeat1
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Parse.const_decl >> Syntax), (* line 141 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("translations",Scan.repeat1 trans_line
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski >> Translations), (* line 162 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("no_translations",Scan.repeat1 trans_line
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski >> NoTranslations), (* line 166 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("axioms",Scan.repeat1 Parse_Spec.spec >> Axioms), (* line 173 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("defs", (* line 186 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski let val opt_unchecked_overloaded =
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Scan.optional (@{keyword "("} |-- Parse.!!!
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (((@{keyword "unchecked"} >> K true) --
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Scan.optional (@{keyword "overloaded"} >> K true) false ||
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski @{keyword "overloaded"} >> K (false, true)) --|
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski @{keyword ")"})) (false, false);
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski in opt_unchecked_overloaded --
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski >> (fn ((x, y), z) => ((x, z), y)))
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski >> Defs end),
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("definition",Parse.opt_target -- Parse_Spec.constdef
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski >> Definition), (* line 195 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("abbreviation",Parse.opt_target -- (* line 199 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski Parse.prop)) >> Abbreviation),
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("type_notation",Parse.opt_target -- (* line 204 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski >> TypeNotation),
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("no_type_notation",Parse.opt_target -- (* line 210 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski >> NoTypeNotation),
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski >> Notation), (* line 216 *)
2c66eeb1cc9ad264525901f10c35c66638f91865Till Mossakowski ("no_notation",Parse.opt_target --
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski >> NoNotation), (* line 216 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("axiomatization",Scan.optional Parse.fixes [] -- (* line 231 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski >> Axiomatization),
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("theorems",Parse.opt_target -- (* line 244 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("lemmas",Parse.opt_target -- (* line 248 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ("declare",Parse.opt_target -- (* line 251 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("hide_class",(Parse.opt_keyword "open" >> not) -- (* line 264 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >> hide "class"),
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("hide_type",(Parse.opt_keyword "open" >> not) -- (* line 265 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski >> hide "type"),
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski ("hide_const",(Parse.opt_keyword "open" >> not) -- (* line 266 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >> hide "const"),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("hide_fact",(Parse.opt_keyword "open" >> not) -- (* line 267 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >> hide "fact"),
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("use",Parse.path >> Use), (* line 273 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("ML",Parse.ML_source >> ML), (* line 280 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("ML_prf",Parse.ML_source >> ML_prf), (* line 287 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("ML_val",Parse.ML_source >> ML_val), (* line 293 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("ML_command",Parse.ML_source >> ML_command), (* line 297 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("setup",Parse.ML_source >> Setup), (* line 301 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("local_setup",Parse.opt_target --
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski Parse.ML_source >> LocalSetup), (* line 305 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("attribute_setup",Parse.position Parse.name -- (* line 309 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski Parse.!!! (@{keyword "="} |--
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski Parse.text "") >> AttributeSetup),
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("method_setup",Parse.position Parse.name -- (* line 315 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski Parse.!!! (@{keyword "="} |--
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Parse.text "") >> MethodSetup),
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski ("declaration",Parse.opt_target -- (* line 321 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Parse.ML_source >> Declaration),
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski ("syntax_declaration",Parse.opt_target -- (* line 326 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Parse.ML_source >> SyntaxDeclaration),
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski ("simproc_setup",Parse.opt_target -- (* line 331 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (@{keyword "("} |-- Parse.enum1 "|"
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Parse.term --| @{keyword ")"} --|
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski @{keyword "="}) -- Parse.ML_source
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski -- Scan.optional (@{keyword "identifier"}
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski >> SimprocSetup),
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("parse_ast_translation",trfun >>
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ParseAstTranslation), (* line 343 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("parse_translation",trfun >> ParseTranslation), (* line 348 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("print_translation",trfun >> PrintTranslation), (* line 353 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("typed_print_translation", trfun >>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski TypedPrintTranslation), (* line 358 *)
1e1cb538d4c4dc09e86cd8c209f55f9e37ae4970Till Mossakowski ("print_ast_translation", trfun >>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski PrintAstTranslation), (* line 364 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (@{keyword "="} |-- Parse.ML_source) >> Oracle),(* line 371 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ("bundle", Parse.opt_target -- (Parse.binding (* line 379 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski --| @{keyword "="}) -- Parse_Spec.xthms1 --
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Parse.xname) >> Include), (* line 384 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Parse.xname) >> Including), (* line 390 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("print_bundles", Scan.succeed PrintBundles), (* line 396 *)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ("sublocale", Parse.position Parse.xname --| (* line 434 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (@{keyword "\<subseteq>"} ||
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski @{keyword "<"}) --
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski parse_interpretation_arguments false
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >> Sublocale),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("interpretation", (* line 442 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski parse_interpretation_arguments true
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -- proof >> Interpretation),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("interpret", (* line 449 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski parse_interpretation_arguments true
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >> Interpret),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("subclass", Parse.opt_target -- (* line 471 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Parse.class -- proof >> Parse.triple1 >> Subclass),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("instance",Scan.option ( (* line 481 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ((Parse.class -- (@{keyword "\<subseteq>"}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski || @{keyword "<"})
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -- Parse.!!! Parse.class) >> Parse.triple1 >> InstanceSubset
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski || Parse.multi_arity >> InstanceArity))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski -- proof >> Instance),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("theorem", parse_theorem -- proof >> Theorem), (* line 525 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("lemma", parse_theorem -- proof >> Lemma), (* line 526 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("corollary", parse_theorem -- proof >> Corollary),(* line 527 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("schematic_theorem", parse_theorem -- proof (* line 528 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >> SchematicTheorem),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("schematic_lemma", parse_theorem -- proof (* line 529 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >> SchematicLemma),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("schematic_corollary", parse_theorem -- proof (* line 530 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >> SchematicCorollary),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (* line 313 HOL/Tools/Datatype/primrec.ML *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("primrec", Parse.opt_target -- Parse.fixes --
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* line 795 HOL/Tools/Datatype/datatype.ML *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("datatype",Parse.and_list1 Datatype.spec_cmd
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >> Datatype),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* line 646 HOL/Tools/Datatype/rep_datatype.ML *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >> RepDatatype),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("fun",Parse.opt_target -- Function_Common.function_parser
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* line 285 HOL/Tools/Function/partial_function.ML *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("partial_function",((@{keyword "("} |-- Parse.xname --|
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski @{keyword ")"}) -- (Parse.fixes -- (Parse.where_ |--
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Parse_Spec.spec))) >> PartialFunction),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (* line 284 HOL/Tools/Function/function.ML *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("function",Parse.opt_target -- Function_Common.function_parser
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski >> Function),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (* line 290 HOL/Tools/Function/function.ML *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ("termination",Scan.option Parse.term -- proof
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski >> Termination)]);
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun unparse_cmd s = Parse.group (fn () => s)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski if Token.is_command t andalso Token.content_of t = s then
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski let val (cmd,toks'') = take_suffix Token.is_command toks'
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski |> space_implode " ",toks'') end
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val diagnostic_commands = ["pretty_setmargin","help","print_commands",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "print_configs","print_context","print_theory","print_syntax",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "print_abbrevs","print_theorems","print_locales","print_classes",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "print_locale","print_interps","print_dependencies",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "print_attributes","print_simpset","print_rules","print_trans_rules",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "print_methods","print_antiquotations","thy_deps","locale_deps",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "class_deps","thm_deps","print_binds","print_facts","print_cases",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "print_statement","thm","prf","full_prf","prop","term","typ",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "print_codesetup","unused_thms"];
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val toplevel_commands = ["cd","pwd","use_thy","remove_thy",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "kill_thy","display_drafts","print_drafts","pr","disable_pr",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "enable_pr","commit","quit","exit","welcome","init_toplevel",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "linear_undo","undo","undos_proof","cannot_undo","kill",
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski "realizers","realizability","extract_type","extract"];
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val simple_thy_body = simple_thy_body' ||
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski first' (List.map (fn s => unparse_cmd s >>
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (Misc o DiagnosticCommand)) diagnostic_commands) ||
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski first' (List.map (fn s => unparse_cmd s >>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (Misc o TopLevelCommand)) diagnostic_commands);
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val locale_val =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Scan.optional (@{keyword "+"} |-- Parse.!!!
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (Scan.repeat1 Parse_Spec.context_element)) [] ||
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowski Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun rec_thy_body toks = first' [
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (Parse.command_name "context" |-- (* line 405 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ((Parse.position Parse.xname >> ContextNamed) ||
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski >> ContextHead))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski -- Scan.repeat (simple_thy_body || rec_thy_body)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Parse.command_name "locale" |-- (* line 421 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Scan.optional (@{keyword "="} |--
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Parse.!!! locale_val) (([], []), []) --
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (simple_thy_body || rec_thy_body)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Scan.succeed []) >> Locale),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (* line 464 *)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (let val class_val = (* Pure/Isar/isar_syn.ML line 458 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Parse_Spec.class_expression -- Scan.optional (@{keyword "+"}
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Scan.repeat1 Parse_Spec.context_element >> pair []
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski val p = Parse.binding -- Scan.optional (@{keyword "="}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski |-- class_val) ([], [])
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski in Parse.command_name "class" |-- p --
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (simple_thy_body || rec_thy_body)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Scan.succeed []) >> Class end),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ((Parse.command_name "instantiation" |-- (* line 475 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Scan.repeat (simple_thy_body ||
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski rec_thy_body)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski --| Parse.command_name "end")) >> Instantiation),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (let val p = Scan.repeat1 (Parse.name --| (* line 493 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (@{keyword "\<equiv>"} || @{keyword "=="}) --
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Parse.term -- Scan.optional (@{keyword "("} |--
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (@{keyword "unchecked"} >> K false) --|
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski @{keyword ")"}) true >> Parse.triple1)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski in Parse.command_name "overloading" |-- p
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (simple_thy_body || rec_thy_body) --|
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski >> Overloading end)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val thy_body = simple_thy_body || rec_thy_body;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski fun read init state toks =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski let val master_dir = Thy_Load.get_master_path ()
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val spans = (*map (resolve_files master_dir)*)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val elements = Thy_Syntax.parse_elements spans
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski (* fun excursion *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val immediate = not (Goal.future_enabled ())
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski fun proof_result (tr, trs) (st, _) =
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowski val (result, st') = Toplevel.proof_result immediate
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val pos' = Toplevel.pos_of (List.last (tr :: trs))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski in (result, (st', pos')) end
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski fun element_result elem x =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski fold_map proof_result
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (Outer_Syntax.get_syntax ())) init elem) x
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val (results, (end_state, end_pos)) = fold_map element_result
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski elements (state, Position.none)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski in end_state end;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski fun init_thy (toks,header) =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski let val t = read (K
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (let val {name = (name, _), imports, uses, ...} = header
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val master_dir = Thy_Load.get_master_path ()
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val parents = List.map (Thy_Info.get_theory o #1) imports
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski in Thy_Load.begin_theory master_dir header parents
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski |> Present.begin_theory 0 master_dir uses end))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski in (t Toplevel.toplevel toks,t) end;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisignature Parser =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val scan : string -> Token.T list;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val dbg : Token.T list -> (Token.kind * string) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski datatype thy = Thy of {header:string option,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val thy : Token.T list -> thy
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val read_sort : Toplevel.state -> (string * Position.T) option
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski -> string -> sort
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val read_typ : Toplevel.state -> (string * Position.T) option
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski -> string -> typ
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val read_term : Proof_Context.mode -> Toplevel.state ->
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * Position.T) option -> string -> term
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val read_prop : Toplevel.state -> (string * Position.T) option ->
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski string -> term
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val read_class : Toplevel.state -> (string * Position.T) option ->
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski string -> class
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val pretty_tokens : unit -> unit
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski datatype symb =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski TypArg of int |
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski String of bool * string |
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Break of int |
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Block of int * symb list;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val format_type_mixfix : string -> Mixfix.mixfix ->
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski int -> mixfix
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val format_const_mixfix : Toplevel.state -> string -> Mixfix.mixfix ->
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski typ option -> mixfix
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructure Parser : Parser =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski open ParserHelper
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski datatype thy = Thy of {header:string option,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski body:(Token.T list * TheoryData.thy_body) list};
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* scan isabelle source transforming it into a sequence of commands *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |> Token.source {do_recover = SOME false}
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >> K NONE || Parse.not_eof >> SOME)) NONE
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val dbg = List.map (fn t => (Token.kind_of t,Token.content_of t));
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val thy = Scan.catch (Scan.option cmd_header -- cmd_theory
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski #> (fn (((h,a),b),_) => Thy {header=h,args=a,body=b}));
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun read_sort state loc =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val ctxt = Named_Target.context_cmd (the_default
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("-", Position.none) loc) (Toplevel.theory_of state)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun do_read read mode state loc =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val ctxt' = Named_Target.context_cmd (the_default
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ("-", Position.none) loc) (Toplevel.theory_of state)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val ctxt = Proof_Context.set_mode mode ctxt'
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in read ctxt end;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val read_typ = do_read Syntax.read_typ Proof_Context.mode_default;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val read_term = do_read Syntax.read_term;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val read_prop = do_read Syntax.read_prop Proof_Context.mode_default;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val read_class = do_read Proof_Context.read_class
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun pretty_tokens () = (Token.unparse #> PolyML.PrettyString)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski datatype symb = (* line 92 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski TypArg of int |
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski String of bool * string |
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Break of int |
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Block of int * symb list;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski type mixfix = symb list * int * int
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* line 107 *)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | xprod_to_fmt (Syntax_Ext.XProd (_, xsymbs, const, pri)) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun arg (s, p) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if s = "type" then TypArg else Arg)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if Lexicon.is_terminal s then 1000 else p);
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski apfst (cons (String (not (exists Symbol.is_block_ctrl (Symbol.explode s)), s)))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (xsyms_to_syms xsyms)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski | xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski apfst (cons (String (false, s))) (xsyms_to_syms xsyms)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | xsyms_to_syms (Syntax_Ext.Bg i :: xsyms) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val (bsyms, xsyms') = xsyms_to_syms xsyms;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val (syms, xsyms'') = xsyms_to_syms xsyms';
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Block (i, bsyms) :: syms, xsyms'')
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski apfst (cons (Break i)) (xsyms_to_syms xsyms)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | xsyms_to_syms (Syntax_Ext.En :: xsyms) = ([], xsyms)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | xsyms_to_syms [] = ([], []);
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun nargs (Arg _ :: syms) = nargs syms + 1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | nargs (TypArg _ :: syms) = nargs syms + 1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | nargs (String _ :: syms) = nargs syms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | nargs (Break _ :: syms) = nargs syms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | nargs [] = 0;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (case xsyms_to_syms xsymbs of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (symbs, []) => SOME (const, (symbs, nargs symbs, pri))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | _ => raise Fail "Unbalanced pretty-printing blocks")
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski fun format_type_mixfix name mx nargs =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val (Syntax_Ext.Syn_Ext {xprods=p,...}) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Mixfix.syn_ext_types [(name,Mixfix.make_type nargs,mx)]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in case xprod_to_fmt (List.hd p) of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski SOME (_,(symbs,_,prio)) => (symbs,nargs,prio)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |_ => raise Fail ("Failed to format mixfix "^
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun format_const_mixfix state name mx tp =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val (Syntax_Ext.Syn_Ext {xprods=p,...}) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Sign.is_logtype (Toplevel.theory_of state))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [(name,case tp of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski SOME tp' => tp'
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |NONE => Simple_Syntax.read_typ "'a",mx)]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in case xprod_to_fmt (List.last p) of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski SOME (_,(symbs,nargs,prio)) => (symbs,nargs,prio)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |_ => raise Fail ("Failed to format mixfix "^
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructure XML_Helper = struct
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun variant (vname : string) (mk : 'a -> string)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fs : ('a -> 'b) list) (v : 'a)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski = case get_first (fn f => SOME (f v)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski handle General.Match => NONE) fs of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski SOME result => result
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |NONE => raise Fail
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (vname^" not implemented for "^
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (mk v |> space_explode " " |> List.hd));
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun attr (name : string) (f : 'a -> string) (v : 'a) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [(name,f v)];
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun a (name : string) (v : string) = attr name I v;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun attr_of_option (vname : string) (name : string) (f : 'a -> string)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski = variant vname (K "") [fn SOME v' => attr name f v',
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fn NONE => []];
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun xml name attrs body = XML.Elem ((name,attrs),body);
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun xml' name body attrs = xml name attrs body;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisignature Export =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskistructure Export : Export =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski datatype sigdata = AddConst of string * typ option *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |RemConst of string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |AddType of string * (int * Parser.mixfix option)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |RemType of string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |AddTypeSynonym of string * typ;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski structure XML_Syntax = Legacy_XML_Syntax
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski open TheoryData
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski open XML_Helper
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski datatype thy = datatype Parser.thy;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val xml_of_import = attr "name" #1 #> xml' "Import" [];
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val xml_of_keyword = variant "xml_of_keyword" PolyML.makestring
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [fn (s,SOME ((s1,[]),[])) => a "name" ("\""^s^"\" :: "^s1),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fn (s,NONE) => a "name" s] #> xml' "Keyword" [];
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun xml_of_use (p,b) = xml "UseFile" (attr "name"
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Path.print #> b ? (fn s => "("^s^")")) p) [];
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val xml_of_expr = variant "xml_of_expr" PolyML.makestring
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [fn ((name,_),(("",false),Expression.Named [])) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski a "name" name] #> xml' "Parent" [];
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun extract_context (t : Token.T list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (body : (Token.T list * 'b) list) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val btoks = List.map #1 body |> flat
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val blen = List.length btoks
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun eq t1 t2 = (Token.kind_of t1 = Token.kind_of t2)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in if blen = 0 then (t,[])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski if not (eq (List.nth (t,len-blen-1)) (List.hd btoks))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski orelse not (eq (List.nth (t,len-2)) (List.last btoks))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski then raise (Fail "extract_context failed!")
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski else (List.take (t,len-blen-1),
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val attr_of_target =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski attr_of_option "attr_of_target" "target" #1;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun attr_of_mixfix mx = case mx of
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski |_ => attr "mixfix" (Mixfix.pretty_mixfix
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun xml_of_typ state target (SOME typ) = [
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Parser.read_typ state target typ
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |xml_of_typ _ _ _ = [];
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun string_of_binding b =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in String.substring (b',1,String.size b'-2) end;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val attr_of_binding = attr "name" string_of_binding;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun attrs_of_binding state (name,args) =
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski attr_of_binding name@
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski Toplevel.context_of state) #> Pretty.string_of)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski #> space_implode ", ") args;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun xml_of_context state target = variant "xml_of_context"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [fn Element.Fixes fixes => List.map (fn (b,tp,mx) =>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski xml "Fix" (attr_of_binding b@attr_of_mixfix mx)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (xml_of_typ state target tp)) fixes
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |> xml "Fixes" [],
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fn Element.Assumes ass => List.map (fn (b,tms) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski variant "xml_context (Assumes)"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [Parser.read_term Proof_Context.mode_default
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski state target tm |> XML_Syntax.xml_of_term]] tms
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski |> xml "Assumption" (attrs_of_binding state b)) ass
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |> xml "Assumes" []];
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun format_mixfix state name tp = variant "format_mixfix"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fn mx => Parser.format_const_mixfix state name mx tp
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun sigdata_of_context state target =
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski variant "sigdata_of_context" PolyML.makestring [
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (fn (b,tp,mx) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val name = string_of_binding b
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (Parser.read_typ state target) tp
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val mx' = format_mixfix state name tp' mx
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski in AddConst (name,tp',mx') end) fixes,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski fun sigdata_of_equations state target eqs =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski let val tps = List.map (fn (_,tm) =>
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski Parser.read_term Proof_Context.mode_pattern
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski state target tm |> HOLogic.dest_eq |> #1 |>
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski head_of |> dest_Const) eqs
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski |> sort_distinct
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (prod_ord fast_string_ord (K EQUAL))
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski in List.map (fn (name,tp) =>
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski AddConst (name,SOME tp,NONE)) tps end;
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski fun xml_of_symb v = variant "xml_of_symb" PolyML.makestring [
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski xml "Arg" (attr "prio" string_of_int i) [],
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski xml "Arg" (attr "prio" string_of_int i) [],
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski xml "String" (a "val" s) [],
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski xml "Break" (attr "prio" string_of_int i) [],
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fn Parser.Block (i,symbs) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski xml "Block" (attr "prio" string_of_int i)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (List.map xml_of_symb symbs)] v;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val attrs_of_mixfix = variant "attrs_of_mixfix"
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski [fn SOME (symbs, nargs, prio) =>
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski attr "nargs" string_of_int nargs@
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski attr "prio" string_of_int prio,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski fn NONE => []];
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val xml_of_sigdata = List.map (variant "xml_of_sigdata"
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski fn AddConst (n, tp, mx) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val attrs = a "name" n@attrs_of_mixfix mx
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val elems = (Option.map (XML_Syntax.xml_of_type #>
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski single) tp |> these)@(Option.map (#1 #>
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski List.map xml_of_symb) mx |> these)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski in xml "AddConst" attrs elems end,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski fn AddType (n,(arity,mx)) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski let val attrs = a "name" n@
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski attr "arity" string_of_int arity@
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski attrs_of_mixfix mx
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val elems = Option.map (#1 #> List.map xml_of_symb)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in xml "AddType" attrs elems end,
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fn AddTypeSynonym (n,tp) =>
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski xml "AddTypeSynonym" (a "name" n)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski #> xml "SigData" [];
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun xml_of_statement state target name =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski variant "xml_of_statement" PolyML.makestring
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [fn Element.Shows s => List.map (fn (b,tms) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if string_of_binding (#1 b) = "" then
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski attr_of_binding name
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski else attrs_of_binding state b)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (List.map (fn (t,ts) => xml "Show" [] (
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski state target #>
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski in t'::ts' end)) tms)) s];
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski fun attr_of_function_config
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski (Function_Common.FunctionConfig {sequential,
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski default,domintros,partials}) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if sequential then a "sequential" "" else [])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski @(Option.map (a "default") default |> the_default [])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski @(if domintros then a "domintros" "" else [])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski @(if partials then a "partials" "" else []);
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun add_type name vars mixfix =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (case mixfix of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (string_of_binding name) mixfix
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |> (curry AddType) (string_of_binding name);
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fun xml_of_sort s = xml "Sort" []
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (List.map (fn n => xml "class" (a "name" n) []) s)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski fun xml_of_arity (s,s') = xml "Arity" []
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (List.map xml_of_sort (s'::s))
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski in fun xml_of_body_elem ((toks,e),((state,trans),l)) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val (elem,state') = variant "xml_of_body" PolyML.makestring [
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski fn Instantiation (arity,body) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val ([name],args',sort) = Class.read_multi_arity
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val args = List.map #2 args'
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski val (begin_,end_) = extract_context toks body
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val s1 = trans state begin_
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val ((s2,_),b_elems) =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski List.foldl xml_of_body_elem ((s1,trans),[]) body
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val s3 = trans s2 end_
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski in (xml "Instantiation" (a "type" name)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski ([xml_of_arity (args,sort)]@
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski [xml "Body" [] (List.rev b_elems)]),s3) end,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski fn Instance (head,proof) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val s1 = trans state toks
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val (attrs,elems) = case head of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski SOME (InstanceArity arity) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val (names,args',sort) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val args = List.map #2 args'
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val vars = xml "Vars" [] (List.map (fn s =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ([vars,xml_of_arity (args,sort)]))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |SOME (InstanceSubset (cls,rel,cls1)) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (a "class" cls@a "rel" rel@a "class1" cls1,[])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |NONE => ([],[])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in (xml "Instance" attrs
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowski ([xml "Proof" [] [XML.Text proof]]@elems), s1) end,
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowski fn Subclass (target,cls,proof) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val s1 = trans state toks
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski in (xml "Subclass" (a "class"
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (Parser.read_class state target cls)@
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski attr_of_target target)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski [xml "Proof" [] [XML.Text proof]],
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski fn Locale ((name,(parents,ctxt)),body) =>
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski let val (begin_,end_) = extract_context toks body
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val s1 = trans state begin_
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val ((s2,_),b_elems) =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski List.foldl xml_of_body_elem ((s1,trans),[]) body
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val s3 = trans s2 end_
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val parents' = variant "xml_of_body_elem (Locale)"
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski [fn (ps,[]) => List.map xml_of_expr ps] parents
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val name' = attr_of_binding name
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski val target = SOME (string_of_binding name,Position.none)
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski val ctxt' = xml "Ctxt" []
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (List.map (xml_of_context s1 target) ctxt)
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski val sigdata = List.map (sigdata_of_context s1 target)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in (xml "Locale" name' (ctxt'::(xml_of_sigdata sigdata)::
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski [xml "Body" [] (List.rev b_elems)]),s3) end,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fn Class ((name,(parents,ctxt)),body) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val (begin_,end_) = extract_context toks body
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val s1 = trans state begin_
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val ((s2,_),b_elems) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski List.foldl xml_of_body_elem ((s1,trans),[]) body
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val s3 = trans s2 end_
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val target = SOME (string_of_binding name,Position.none)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val parents' = List.map (attr "name"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (Parser.read_sort s1 target #> the_single)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski #> xml' "Parent" []) parents
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski handle List.Empty => raise Fail
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski "Unhandled case in xml_of_body_elem (Class)"
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val name' = attr_of_binding name
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val ctxt' = xml "Ctxt" []
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (List.map (xml_of_context s1 target) ctxt)
a231094086321e19f9a689de4745512c91e00e4bTill Mossakowski val sigdata = List.map (sigdata_of_context s1 target)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in (xml "Cls" name' (ctxt'::(xml_of_sigdata sigdata)::
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski [xml "Body" [] (List.rev b_elems)]),s3) end,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski fn TypeSynonym (((target,vars),name),(typ,mixfix))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val s1 = trans state toks
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val typ' = Parser.read_typ state target typ
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val name' = attr_of_binding name
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val target' = attr_of_target target
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val mixfix' = attr_of_mixfix mixfix
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val vars' = xml "Vars" [] (List.map
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (fn s => TFree (s,[]) |> XML_Syntax.xml_of_type)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val sigdata = [add_type name vars mixfix,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski AddTypeSynonym (string_of_binding name,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski Parser.read_typ state target typ)]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski in (xml "TypeSynonym" (name'@target'@mixfix')
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski ([xml_of_sigdata sigdata]@[vars']@[typ']),s1) end,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski fn Datatype dts =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski let val s1 = trans state toks
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski fun sigdata_of_dt ((name,vars,mx),cs) =
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski (add_type name vars mx)::
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (List.map (fn (c,tms,mx) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski if String.isSubstring " " (string_of_binding c)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski then AddTypeSynonym (string_of_binding name,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (string_of_binding c))
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski let val cname = string_of_binding c
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val tps = List.map (Parser.read_typ s1 NONE)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val tp = (tps ---> Type (string_of_binding name,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski SOME(s') => [s']
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski |NONE => [])) vars)) |> SOME
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val mx' = format_mixfix s1 cname tp mx
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski in AddConst (cname,tp,mx') end) cs)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (fn ((name,vars,mx),cs) => xml "Datatype"
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (attr_of_binding name@attr_of_mixfix mx)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski ((xml_of_sigdata (sigdata_of_dt
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski ((name,vars,mx),cs)))::
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (List.map (fn (c,tms,mx) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski xml "Constructor" (attr_of_binding c
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski @attr_of_mixfix mx) (List.map
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski @(List.map (fn (v,s) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski SOME(s') => [s']
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski |NONE => []))) vars)))) dts
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski in (xml "Datatypes" [] dts', s1) end,
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski fn Consts cs => (xml "Consts" [] (List.map
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (fn (name,tp,mx) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski let val tp' = Parser.read_typ state NONE tp
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val name' = string_of_binding name
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val mx' = format_mixfix state name' (SOME tp') mx
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski in xml "ConstDef"
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski ([("name",name')]@attr_of_mixfix mx)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski [xml_of_sigdata [AddConst (name',SOME tp',mx')],
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski tp' |> XML_Syntax.xml_of_type] end) cs), trans state toks),
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski fn Axioms axs => (xml "Axioms" [] (List.map
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (fn (b,tm) => xml "Axiom"
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (attrs_of_binding state b)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski [Parser.read_term Proof_Context.mode_default state NONE tm
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski |> XML_Syntax.xml_of_term]) axs), trans state toks),
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski fn Lemma ((((target,(name,args)), strs),(ctxt,stmt)),proof) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski let val result = case (args,strs) of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski let val s1 = trans state toks
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val ctxt' = xml "Ctxt" []
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (List.map (xml_of_context state target) ctxt)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski in (xml "Lemma" (attr_of_target target)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (ctxt'::[xml "Proof" [] [XML.Text proof]]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski @xml_of_statement state target name stmt),s1) end
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski |_ => raise Fail ("Case not implemented: "^PolyML.makestring
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski in result end,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski fn Definition (target,(name,(binding,tm))) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski let val s1 = trans state toks
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val _ = case binding of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (b,[]) => if string_of_binding b <> "" then
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski raise Fail "Case not implemented" else ()
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski |_ => raise Fail "Case not implemented"
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val (attrs,tp') = case name of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski SOME (name',tp,mx) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (attr_of_binding name'@
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski attr_of_mixfix mx,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski xml_of_typ state target tp)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski |NONE => ([],[])
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val ((_,[(_,tm')]),_) =
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski Specification.read_free_spec (the_list name)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski [(binding,tm)] (Toplevel.context_of state)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val (name',tp) = HOLogic.dest_Trueprop tm' |>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski HOLogic.dest_eq |> #1 |> head_of |> dest_Free;
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski in (xml "Definition" (attrs@attr_of_target target)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski ((xml_of_sigdata [AddConst (name',
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski SOME tp,NONE)])::
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski tp'@[tm' |> XML_Syntax.xml_of_term]),s1) end,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski fn Fun (target,((cfg,f),a)) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski let val s1 = trans state toks
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val fixes = List.map (fn (b,typ,mixfix) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski xml "FunSig" (attr_of_mixfix mixfix
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski @attr_of_binding b)
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski |NONE => [])) f
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val eqs = List.map (fn ((b,l),tm) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski case ((string_of_binding b,l),tm) of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (("",[]),tm) =>
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (Parser.read_term Proof_Context.mode_pattern
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski state target tm
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski raise (Fail "Not yet implemented for Fun!"))
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski val sigdata = sigdata_of_equations s1 target a
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski in (xml "Fun" (attr_of_target target
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski @attr_of_function_config cfg)
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski (xml_of_sigdata sigdata::fixes@eqs),s1) end,
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski fn Primrec ((target,f),a) =>
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski let val s1 = trans state toks
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski val fixes = List.map (fn (b,typ,mixfix) =>
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowski xml "FunSig" (attr_of_mixfix mixfix
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski @attr_of_binding b)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski |NONE => [])) f
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski val eqs = List.map (fn ((b,l),tm) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski case ((string_of_binding b,l),tm) of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (("",[]),tm) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Parser.read_term Proof_Context.mode_pattern
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski state target tm
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski raise (Fail "Not yet implemented for Fun!"))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val sigdata = sigdata_of_equations s1 target a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in (xml "Primrec" (attr_of_target target)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (xml_of_sigdata sigdata::fixes@eqs),s1) end] e
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in ((state',trans),elem::l) end end;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun xml_of_body state body =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski List.foldl xml_of_body_elem (state,[]) body
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |> #2 |> List.rev |> xml "Body" [];
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun xml_of_theory (Thy {header,args=(th,h),body}) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val imports = List.map xml_of_import (#imports h)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val keywords = List.map xml_of_keyword (#keywords h)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val uses = List.map xml_of_use (#uses h)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val name = attr "name" #1 (#name h)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val header' = attr_of_option "header" "header" I header
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val (s,t) = ParserHelper.init_thy (th,h)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val body' = [xml_of_body (s,t) body]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in xml "Export" []
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [xml "Thy" (name@header') (imports@keywords@body')] end;