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