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