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
dc89cfbc150be3b6792f559f57b6e91cd7affacbJonathan von Schroeder datatype instance_type = InstanceArity of string list * string list *
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder |InstanceSubset of string * string * 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
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder |Subclass of opt_target * string * proof
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder |Instantiation of (string list * string list * string) *
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder (orig * thy_body) list
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder |Instance of (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
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder |Typedef of (((((string * string option) list * binding) * mixfix) *
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder string) * (binding * binding) option) * proof
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder |Fixrec of opt_target * ((binding * string option * mixfix) list *
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (bool * (Attrib.binding * string)) list)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder |Domain of bool * ((((string * string option) list * binding) * mixfix) * ((binding * (bool * binding option * string) list) * mixfix) list)
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
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val init_thy : Path.T -> (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")
a845310274d5bcd9da2df61599fd58eaf96ded13Jonathan von Schroeder [command_with_args "qed" --
a845310274d5bcd9da2df61599fd58eaf96ded13Jonathan von Schroeder 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
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder ("subclass", Parse.opt_target -- (* line 471 *)
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder Parse.class -- proof >> Parse.triple1 >> Subclass),
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder ("instance",Scan.option ( (* line 481 *)
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder ((Parse.class -- (@{keyword "\<subseteq>"}
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder || @{keyword "<"})
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder -- Parse.!!! Parse.class) >> Parse.triple1 >> 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
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder >> Termination),
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder ("typedef",Parse.type_args_constrained --
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder (@{keyword "="} |-- Parse.term) --
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder Scan.option (@{keyword "morphisms"} |--
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder Parse.!!! (Parse.binding -- Parse.binding)) --
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder proof >> Typedef),
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (* line 404 HOL/HOLCF/Tools/fixrec.ML *)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val opt_thm_name' : (bool * Attrib.binding) parser =
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder @{keyword "("} -- @{keyword "unchecked"} --
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder @{keyword ")"} >> K (true, Attrib.empty_binding)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder || Parse_Spec.opt_thm_name ":" >> pair false
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val spec' : (bool * (Attrib.binding * string)) parser =
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder opt_thm_name' -- Parse.prop >>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (fn ((a, b), c) => (a, (b, c)))
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val alt_specs' : (bool * (Attrib.binding * string)) list parser =
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val unexpected = Scan.ahead
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (Parse.name || @{keyword "["} || @{keyword "("})
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder in Parse.enum1 "|" (spec' --| Scan.option
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (unexpected -- Parse.!!! @{keyword "|"})) end
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder in Parse.opt_target -- (Parse.fixes -- (Parse.where_
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder |-- Parse.!!! alt_specs')) >> Fixrec end),
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (* line 265 HOL/HOLCF/Tools/Domain/domain.ML *)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val dest_decl : (bool * binding option * string) parser =
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder @{keyword "("} |-- Scan.optional
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (@{keyword "lazy"} >> K true) false --
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (Parse.binding >> SOME) -- (@{keyword "::"}
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder |-- Parse.typ) --| @{keyword ")"} >> Parse.triple1
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder || @{keyword "("} |-- @{keyword "lazy"}
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder |-- Parse.typ --| @{keyword ")"}
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder >> (fn t => (true, NONE, t))
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder || Parse.typ >> (fn t => (false, NONE, t))
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val cons_decl = Parse.binding --
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder Scan.repeat dest_decl -- Parse.opt_mixfix
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val domain_decl = (Parse.type_args_constrained --
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder Parse.binding -- Parse.opt_mixfix) --
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (@{keyword "="} |-- Parse.enum1 "|" cons_decl)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val domains_decl =
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder Scan.optional (@{keyword "("} |--
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (@{keyword "unsafe"} >> K true) --|
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder @{keyword ")"}) false --Parse.and_list1 domain_decl
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder in domains_decl >> Domain end)]);
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;
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder fun init_thy dir (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
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val master_dir = dir
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 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
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder val read_typ : Toplevel.state -> (string * Position.T) option
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder -> string -> typ
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder val read_term : Proof_Context.mode -> Toplevel.state ->
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder (string * Position.T) option -> string -> term
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder val read_prop : Toplevel.state -> (string * Position.T) option ->
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder val read_class : Toplevel.state -> (string * Position.T) option ->
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder string -> class
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder val inferred_param : string -> Toplevel.state ->
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder (string * Position.T) option -> typ
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 |> Token.source {do_recover = SOME false}
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder >> K NONE || Parse.not_eof >> SOME)) NONE
b9343d2e9e7078d3261a05e7899c74bcde032a76Jonathan von Schroeder |> Source.map_filter I |> 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)
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder fun do_read read 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)
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder val ctxt = Proof_Context.set_mode mode ctxt'
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder in read ctxt end;
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder val read_typ = do_read Syntax.read_typ Proof_Context.mode_default;
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder val read_term = do_read Syntax.read_term;
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder val read_prop = do_read Syntax.read_prop Proof_Context.mode_default;
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder val read_class = do_read Proof_Context.read_class
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder fun inferred_param s state target =
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder do_read (Proof_Context.inferred_param s)
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder Proof_Context.mode_default state target |> #1;
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
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder fun variant (vname : string) (mk : 'a -> string)
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder (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 "^
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder (mk 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)
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder = variant vname (K "") [fn SOME v' => attr name f v',
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan 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 =
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val xml_of_theory : (string -> unit) -> string -> XML.tree list
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val get_non_image_parents : theory -> theory list
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroederstructure Export : Export =
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder fun get_non_image_parents T = List.concat (List.map
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder (fn T' => if length (Thy_Info.loaded_files
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder then T'::(get_non_image_parents T') else [])
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" [];
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder val xml_of_keyword = variant "xml_of_keyword" PolyML.makestring
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) [];
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder val xml_of_expr = variant "xml_of_expr" PolyML.makestring
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder [fn ((name,_),(("",false),Expression.Named [])) =>
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder a "name" name] #> xml' "Parent" [];
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder val unqualified = Binding.qualified_name #> Binding.name_of;
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;
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;
97759cc6eafaca8c6e62ae394aa28b9642a2a6d7Jonathan von Schroeder fun xml_of_symb v = variant "xml_of_symb" PolyML.makestring [
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;
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder fun format_mixfix state name tp = variant "format_mixfix"
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder fn mx => Parser.format_const_mixfix state name mx tp
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder fun format_type_mixfix name num_args = variant
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder "format_type_mixfix" PolyML.makestring
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder fn mx => Parser.format_type_mixfix name mx num_args
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder fun xml_of_mixfix state name tp mx =
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder case format_mixfix state name tp mx of
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder SOME (symbs,nargs,prio) =>
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder [xml "Mixfix" (attr "nargs" string_of_int nargs@
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder attr "prio" string_of_int prio@
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder (List.map xml_of_symb symbs)]
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder fun xml_of_type_mixfix name mx num_args =
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder case format_type_mixfix name num_args mx of
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder SOME (symbs,nargs,prio) =>
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder [xml "Mixfix" (attr "nargs" string_of_int nargs@
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder attr "prio" string_of_int prio@
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder (List.map xml_of_symb symbs)]
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder fun xml_of_context state target = variant "xml_of_context"
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder [fn Element.Fixes fixes => List.map (fn (b,_,mx) =>
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder xml "Fix" (attr_of_binding b)
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder (let val name = string_of_binding b
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder val tp = Parser.inferred_param name state target
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder xml_of_mixfix state name (SOME tp) mx end)) fixes
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder |> xml "Fixes" [],
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder fn Element.Assumes ass => List.map (fn (b,tms) =>
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder variant "xml_context (Assumes)"
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder [Parser.read_term Proof_Context.mode_default
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder state target tm |> XML_Syntax.xml_of_term]] tms
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder |> xml "Assumption" (attrs_of_binding state b)) ass
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder |> xml "Assumes" []];
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder fun strip_cfun (Const(@{const_name Rep_cfun},_)$f$f1) =
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder strip_cfun f@[f1]
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder | strip_cfun u = [u]
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder fun strip_alls t =
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder SOME (_, u) => strip_alls u
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder fun split_fixrec_equations state target f eqs =
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val (skips, raw_spec) = ListPair.unzip eqs
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val (fixes, spec) = fst (Specification.read_spec f
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder raw_spec (Toplevel.context_of state))
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val get_tms = (fn (lhs,rhs) => (strip_cfun lhs,rhs)) o
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val get_imps = map HOLogic.dest_Trueprop o
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val tms = map ((fn x => (get_imps x,get_tms x)) o
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder strip_alls o snd) spec
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val tms' = ListPair.zip (skips,tms)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val fn_eqs = List.foldl (fn (eq,t) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val (b,(imps,((c::vs),def_tm))) = eq
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val (name,tp) = dest_Free c
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder SOME (_,def_tms) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder Symtab.update (name,(tp,def_tms@
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder [(b,imps,vs,def_tm)])) t
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder |NONE => Symtab.update (name,(tp,
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder [(b,imps,vs,def_tm)])) t
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val fns = List.foldl (fn (((b,_),mx),t) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder Symtab.update (Binding.name_of b,mx) t)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder in Symtab.fold_rev (fn (k,(tp,equations)) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val b = unqualified k
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val SOME(mx) = Symtab.lookup fns b
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val equations' = List.map (fn (b,imps,vs,tm) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val imps' = xml "Premises" [] (List.map
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder in xml "FixrecEquation" (if not b then [] else
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder a "unchecked" "") (imps'::List.map
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder XML_Syntax.xml_of_term (vs@[tm])) end)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val elem = xml "FixrecFun" (a "name" b)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (xml_of_mixfix state b (SOME tp) mx@
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder in fn l => elem::l end) fn_eqs [] end end;
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder fun split_equations state target f eqs =
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder let val eqs' = List.map (fn ((b,l),tm) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val _ = if Attrib.is_empty_binding (b,l)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder then () else raise Fail
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder ("Not yet implemented "^
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder "for split_equations!")
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Proof_Context.mode_pattern state target tm |>
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder HOLogic.dest_eq |> (fn (head,body) =>
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder (strip_comb head,body)) end) eqs
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder val fn_eqs = List.foldl (fn (eq,t) =>
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder let val ((c,vs),def_tm) = eq
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder val (name,tp) = dest_Const c
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder SOME (_,def_tms) =>
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Symtab.update (name,(tp,def_tms@
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder [(vs,def_tm)])) t
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder |NONE => Symtab.update (name,(tp,
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder [(vs,def_tm)])) t
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder val fns = List.foldl (fn ((b,_,mx),t) =>
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder Symtab.update (Binding.name_of b,mx) t)
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder in Symtab.fold_rev (fn (k,(tp,equations)) =>
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder let val b = unqualified k
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder val SOME(mx) = Symtab.lookup fns b
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val equations' = List.map (fn (vs,tm) =>
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder xml "Equation" [] (List.map
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder XML_Syntax.xml_of_term (vs@[tm]))) equations
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder val elem = xml "Fun" (a "name" b)
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder (xml_of_mixfix state b (SOME tp) mx@
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder in fn l => elem::l end) fn_eqs []
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder fun xml_of_statement state target name =
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder variant "xml_of_statement" PolyML.makestring
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder [fn Element.Shows s => List.map (fn (b,tms) =>
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder (if string_of_binding (#1 b) = "" then
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder attr_of_binding name
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder else 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 []);
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder fun xml_of_sort s = xml "Sort" []
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder (List.map (fn n => xml "class" (a "name" n) []) s)
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder fun xml_of_arity (s,s') = xml "Arity" []
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder (List.map xml_of_sort (s'::s))
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder in fun xml_of_body_elem ((toks,e),((state,trans),l)) =
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder let val (elem,state') = variant "xml_of_body" PolyML.makestring [
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder fn Defs ((unchecked,overloaded),l) =>
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder let val l' = List.map (fn ((name,tm),args) =>
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder let val tm' = Parser.read_prop state NONE tm
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder val (c,def_tm) = Logic.dest_equals tm'
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder val (cname',tp) = dest_Const c
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder val cname = unqualified cname'
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder val args' = List.map (Args.pretty_src
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder (Toplevel.context_of state) #> Pretty.str_of)
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder args |> space_implode " "
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder in xml "Def" (a "args" args'@attr_of_binding name@
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder a "const" cname)
10598b3b999ecbac0347ff422d56b1d97db296b7Jonathan von Schroeder XML_Syntax.xml_of_term def_tm] end) l
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder val attrs = (if unchecked then a "unchecked" "" else [])
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder @(if overloaded then a "overloaded" "" else [])
e604ebb440d3ed0414aa2d54ff962768f0a27933Jonathan von Schroeder in (xml "Defs" attrs l',trans state toks) end,
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder fn Typedef (((((vars,tp),mx),tm),morphisms),proof) =>
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder let val vars' = List.map (fn (name,sort) => case sort of
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder SOME sort' => TFree (name,
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder |NONE => TFree (name,[])) vars
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder val tm' = Parser.read_term Proof_Context.mode_default
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder val morphisms' = case morphisms of
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder SOME (m1,m2) => attr "m1" string_of_binding m1@
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder attr "m2" string_of_binding m2
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder val mx' = xml_of_type_mixfix (string_of_binding tp)
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder in (xml "Typedef" (attr "type" string_of_binding tp
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder (mx'@[xml "Proof" [] [XML.Text proof]]@
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder List.map XML_Syntax.xml_of_type vars'),
fce31f9f7a2e653c2cc7e55efafe3a7cee585bffJonathan von Schroeder trans state toks) end,
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder fn Instantiation (arity,body) =>
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder let val ([name],args',sort) = Class.read_multi_arity
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder val args = List.map #2 args'
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder val (begin_,end_) = extract_context toks body
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder val s1 = trans state begin_
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder val ((s2,_),b_elems) =
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder List.foldl xml_of_body_elem ((s1,trans),[]) body
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder val s3 = trans s2 end_
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder in (xml "Instantiation" (a "type" name)
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder ([xml_of_arity (args,sort)]@
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder [xml "Body" [] (List.rev b_elems)]),s3) end,
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder fn Instance (head,proof) =>
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder let val s1 = trans state toks
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder val (attrs,elems) = case head of
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder SOME (InstanceArity arity) =>
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder let val (names,args',sort) =
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder val args = List.map #2 args'
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder val vars = xml "Vars" [] (List.map (fn s =>
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder TFree (s,[]) |> XML_Syntax.xml_of_type)
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder ([vars,xml_of_arity (args,sort)]))
85b227b458a885d075f3934c210c7de0cc89ccffJonathan von Schroeder |SOME (InstanceSubset (cls,rel,cls1)) =>
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder (a "class" cls@a "rel" rel@a "class1" cls1,[])
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder |NONE => ([],[])
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder in (xml "Instance" attrs
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder ([xml "Proof" [] [XML.Text proof]]@elems), s1) end,
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder fn Subclass (target,cls,proof) =>
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder let val s1 = trans state toks
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder in (xml "Subclass" (a "class"
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder (Parser.read_class state target cls)@
93cd42c036c9ef3fed58d4872bab5d72371d80d1Jonathan von Schroeder attr_of_target target)
0a4b44b3c2c874af72bf50468e14db804c8285d2Jonathan von Schroeder [xml "Proof" [] [XML.Text proof]],
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)
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder in (xml "Locale" name' (ctxt'::parents'@
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)
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder in (xml "Cls" name' (ctxt'::parents'@
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder [xml "Body" [] (List.rev b_elems)]),s3) end,
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder fn TypeSynonym (((target,vars),name),(typ,mx))
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
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder val mx' = xml_of_type_mixfix (string_of_binding name)
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder val vars' = xml "Vars" [] (List.map
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder (fn s => TFree (s,[]) |> XML_Syntax.xml_of_type)
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder in (xml "TypeSynonym" (name'@target')
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder (mx'@[vars']@[typ']),s1) end,
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder fn Datatype dts =>
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder let val s1 = trans state toks
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder (fn ((name,vars,mx),cs) => xml "Datatype"
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder (attr_of_binding name)
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder (xml_of_type_mixfix (string_of_binding name)
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder List.map (fn (c,tms,mx) =>
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder let val cname = string_of_binding c
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder val tp = (tps ---> Type
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder (string_of_binding name,
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder TFree (v,case s of
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder |NONE => [])) vars))
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder val is_c = not (String.isSubstring " " cname)
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder val attrs = if is_c then attr_of_binding c
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder val elems' = List.map XML_Syntax.xml_of_type
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder (if is_c then (tp::tps)
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder else (Parser.read_typ s1 NONE cname::tps))
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder val elems = if is_c then (xml_of_mixfix s1
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder cname (SOME tp) mx@elems') else elems'
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder in xml "Constructor" attrs elems end) cs
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder SOME(s') => [s']
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan 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
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder val mx' = xml_of_mixfix state name' (SOME tp') mx
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder in xml "ConstDef" [("name",name')]
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder (mx'@[tp' |> XML_Syntax.xml_of_type]) end) cs),
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder 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) =>
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder let val result = case (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]]
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder @xml_of_statement state target name stmt),s1) end
eacba3959b7c09945bfb0d28ca32898c4606c220Jonathan von Schroeder |_ => raise Fail ("Case not implemented: "^PolyML.makestring
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"
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroeder val ((_,[(_,tm')]),_) =
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroeder Specification.read_free_spec (the_list name)
c2356bf325a50171577ca2ffb33cf83bcd0786b1Jonathan von Schroeder [(binding,tm)] (Toplevel.context_of state)
4259e185f367aa660369432548aae92f9d828bdeJonathan von Schroeder handle ex => tm'
4259e185f367aa660369432548aae92f9d828bdeJonathan von Schroeder val (((name',tp),vs),def_tm) = tm'' |>
4259e185f367aa660369432548aae92f9d828bdeJonathan von Schroeder |> (fn (head,body) =>
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder case strip_comb head of
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder (f,vs) => ((dest_Free f,vs),body))
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder val mx' = case name of
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder SOME (_,_,mx) => xml_of_mixfix state name' (SOME tp)
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder in (xml "Definition" (a "name" name'@
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder attr_of_target target)
b9492cbb3cc06b0d06bee92643e48c8e0f595369Jonathan von Schroeder List.map XML_Syntax.xml_of_term (vs@[def_tm])),s1) end,
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder fn Fun (target,((cfg,f),a)) =>
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder let val s1 = trans state toks
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder val elems = split_equations s1 target f a
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder in (xml "Funs" (attr_of_target target
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder @attr_of_function_config cfg) elems,s1) end,
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder fn Primrec ((target,f),a) =>
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder let val s1 = trans state toks
6764d16780980d70ed80b17465e07c3bb811e28aJonathan von Schroeder val elems = split_equations s1 target f a
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder in (xml "Primrec" (attr_of_target target) elems,s1) end,
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder fn Fixrec (target,(f,a)) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val s1 = trans state toks
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val elems = split_fixrec_equations s1 target f a
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder in (xml "Fixrec" (attr_of_target target) elems,s1) end,
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder fn Domain (unsafe,dts) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val s1 = trans state toks
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val dts' = List.map (fn (((vs,name),mx), cs) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val vars = List.map (fn (a,s) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder TFree (a, case s of
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder SOME s' => Parser.read_sort state NONE s'
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder |NONE => [])) vs
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val mx' = xml_of_type_mixfix (string_of_binding
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder val cs' = List.map (fn ((c,args),mx1) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder let val t = string_of_binding c |>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder xml "DomainConstructor" (attr_of_binding c)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (List.map (fn (l,sel,tp) =>
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder xml "DomainConstructorArg"
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder ((if l then a "lazy" "" else [])
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder SOME sel' => attr_of_binding sel'
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder in xml "Domain" (attr_of_binding name)
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder (mx'@List.map XML_Syntax.xml_of_type vars@cs')
5e4fe646cad79449dff25a3bb7fcebad76b72c95Jonathan von Schroeder in (xml "Domains" [] dts',s1) end] e
9a527ab7e7c0247ab32162f00c9ec630eff38a88Jonathan von Schroeder in ((state',trans),elem::l) end end;
6df4343f46cc159371dfa671c5943354480f4e1cJonathan von Schroeder fun xml_of_body state body =
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder List.foldl xml_of_body_elem (state,[]) body;
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder fun xml_of_theory v file' =
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder let val _ = v ("Reading "^file'^"\n")
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val file = file' |> Path.explode |> Path.expand |>
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder File.full_path Path.current |> File.check_file
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val tname = Path.explode file' |> Path.base |>
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val (Thy {header,args=(th,h),body}) =
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val _ = v ("Loading parents of theory "^tname^"\n")
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val thys = map (fn (i,_) => (Thy_Info.get_theory i; [])
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder let val full = Path.explode i |>
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder in xml_of_theory v full end) (#imports h)
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder 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
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val (s,t) = ParserHelper.init_thy dir (th,h)
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val _ = v ("Exporting theory "^tname^"\n")
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val (s',body'') = xml_of_body (s,t) body
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val _ = Toplevel.command (Toplevel.exit
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder val body' = [body'' |> List.rev |> xml "Body" []]
3496342433a87c2a3ab9950e78b33ecb03f29e15Jonathan von Schroeder in thys@[xml "Thy" (name@header') (imports@keywords@body')] end;