parser.ml revision 4259e185f367aa660369432548aae92f9d828bde
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiustructure TheoryData = struct
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu type opt_target = (xstring * Position.T) option;
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu datatype misc_body = Chapter of opt_target * string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Section of opt_target * string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Subsection of opt_target * string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Subsubsection of opt_target * string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Text of opt_target * string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |TextRaw of opt_target * string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Sect of string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Subsect of string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Subsubsect of string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |TxtRaw of string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |DiagnosticCommand of string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |TopLevelCommand of string;
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu type proof = string;
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu type ml_text = string * Position.T;
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu type orig = Token.T list;
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu datatype context_head = ContextNamed of xstring * Position.T
e2f328730bd39975b02329b81b608d23193f1c3aFrancisc Nicolae Bungiu |ContextHead of ((xstring * Position.T) list
e2f328730bd39975b02329b81b608d23193f1c3aFrancisc Nicolae Bungiu datatype instance_type = InstanceArity of string list * string list *
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |InstanceSubset of string * string * string;
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu datatype thy_body =
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu Classes of (binding * string list) list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Classrel of (string * string) list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |DefaultSort of opt_target * string
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |TypeDecl of ((opt_target * string list) * binding) * mixfix
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |TypeSynonym of ((opt_target * string list) * binding) *
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu (string * mixfix)
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Nonterminal of binding list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Arities of (string * string list * string) list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Judgement of (binding * string * mixfix)
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Consts of (binding * string * mixfix) list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Syntax of (string * bool) * (string * string * mixfix) list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |NoSyntax of (string * bool) * (string * string * mixfix) list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Translations of (xstring * string) Syntax.trrule list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |NoTranslations of (xstring * string) Syntax.trrule list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Axioms of (Attrib.binding * string) list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Defs of (bool * bool) * ((binding * string) * Args.src list) list
b3801e7f361759d6748a661df75c01c084299c67Francisc Nicolae Bungiu |Definition of opt_target * ((binding * string option * mixfix) option
* (Attrib.binding * string))
(Attrib.binding * string list) list
|Theorems of (opt_target * (Attrib.binding *
|Lemmas of (opt_target * (Attrib.binding *
|AttributeSetup of (bstring * Position.T) * (ml_text * string)
|MethodSetup of (bstring * Position.T) * (ml_text * string)
|SimprocSetup of (((opt_target * (bstring * Position.T)) *
|ParseAstTranslation of bool * (string * Position.T)
|ParseTranslation of bool * (string * Position.T)
|PrintTranslation of bool * (string * Position.T)
|TypedPrintTranslation of bool * (string * Position.T)
|PrintAstTranslation of bool * (string * Position.T)
|Oracle of (bstring * Position.T) * ml_text
|Include of (xstring * Position.T) list
|Including of (xstring * Position.T) list
(Attrib.binding * string) list)) * proof
|Interpretation of (Expression.expression *
(Attrib.binding * string) list) * proof
|Interpret of Expression.expression *
(Attrib.binding * string) list
|Class of (binding * (string list * Element.context list)) *
|Theorem of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
|Lemma of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
|Corollary of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
|SchematicTheorem of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
|SchematicLemma of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
|SchematicCorollary of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
(Attrib.binding * string) list
|Datatype of Datatype.spec_cmd list
|Fun of opt_target * ((Function_Common.function_config * (binding *
(Attrib.binding * string) list)
(Attrib.binding * string))
|Function of (opt_target * ((Function_Common.function_config *
* (Attrib.binding * string) list)) * proof
(bool * (Attrib.binding * string)) list)
|Domain of bool * ((((string * string option) list * binding) * mixfix) * ((binding * (bool * binding option * string) list) * mixfix) list)
List.length toks')
(* taken from Pure/Isar/parse.ML *)
(fn (arg, x) => (Token.assign NONE arg; x));
fun token p = RESET_VALUE (Scan.one p);
val unparse_verbatim = unparse_kind Token.Verbatim;
val not_command = Parse.group (fn () => "non-command token")
(token (not o Token.is_command));
fun command s = Parse.group (fn () => "command "^s)
(token (fn t => Token.is_command t andalso
Token.content_of t = s));
fun command_with_args s = command s -- Scan.repeat not_command >> op::;
(* Pure/pure_syn.ML *)
val cmd_theory = preserve_toks (Parse.command_name "theory"
|-- Thy_Header.args);
(* Pure/Isar/isar_syn.ML *)
val cmd_header = Parse.command_name "header" |-- unparse_verbatim;
in Scan.optional (@{keyword "("} |-- Parse.!!!
(mode_spec --| @{keyword ")"})) Syntax.mode_default end;
(Parse.xname --| @{keyword ")"}))
>> K Syntax.Parse_Rule ||
>> K Syntax.Print_Rule ||
>> K Syntax.Parse_Print_Rule) toks
Parse.!!! (Parse_Spec.locale_expression mandatory) --
val parse_theorem = Parse.opt_target --
i.e. the start of each sublist will satisfy p and all
fun partition p l = #2 (List.foldr
fun proof_qed i = Parse.group (fn () => "proof_qed")
if i > 0 then Scan.first
(token Token.is_command --
Scan.repeat not_command >> op::)
#> List.map (space_implode " ")
#> cat_lines) o (partition Token.is_command);
val proof = Parse.!!! ((proof_prefix -- Scan.first
("chapter", Parse.opt_target -- unparse_verbatim
("section", Parse.opt_target -- unparse_verbatim
("subsection", Parse.opt_target -- unparse_verbatim
("subsubsection", Parse.opt_target -- unparse_verbatim
("text", Parse.opt_target -- unparse_verbatim
("text_raw", Parse.opt_target -- unparse_verbatim
Scan.optional ((@{keyword "\<subseteq>"}
|-- Parse.!!! Parse.class)) >> Classrel),
Parse.binding -- (Parse.$$$ "=" |-- Parse.!!!
("judgement",Parse.const_binding >> Judgement), (* line 122 *)
("no_syntax",opt_mode -- Scan.repeat1
Parse.const_decl >> Syntax), (* line 141 *)
("translations",Scan.repeat1 trans_line
("no_translations",Scan.repeat1 trans_line
Scan.optional (@{keyword "("} |-- Parse.!!!
Scan.optional (@{keyword "overloaded"} >> K true) false ||
("abbreviation",Parse.opt_target -- (* line 199 *)
(opt_mode -- (Scan.option
Parse.prop)) >> Abbreviation),
("type_notation",Parse.opt_target -- (* line 204 *)
(opt_mode -- Parse.and_list1
("no_type_notation",Parse.opt_target -- (* line 210 *)
(opt_mode -- Parse.and_list1
("notation",Parse.opt_target --
(opt_mode -- Parse.and_list1
("no_notation",Parse.opt_target --
(opt_mode -- Parse.and_list1
Parse.!!! (Parse.and_list1
Parse_Spec.specs)) []
("theorems",Parse.opt_target -- (* line 244 *)
Parse.for_fixes >> Theorems),
("lemmas",Parse.opt_target -- (* line 248 *)
Parse.for_fixes >> Lemmas),
("declare",Parse.opt_target -- (* line 251 *)
Parse.for_fixes >> Declare),
("hide_class",(Parse.opt_keyword "open" >> not) -- (* line 264 *)
("hide_type",(Parse.opt_keyword "open" >> not) -- (* line 265 *)
("hide_const",(Parse.opt_keyword "open" >> not) -- (* line 266 *)
("hide_fact",(Parse.opt_keyword "open" >> not) -- (* line 267 *)
("use",Parse.path >> Use), (* line 273 *)
("ML",Parse.ML_source >> ML), (* line 280 *)
("ML_prf",Parse.ML_source >> ML_prf), (* line 287 *)
("ML_val",Parse.ML_source >> ML_val), (* line 293 *)
("ML_command",Parse.ML_source >> ML_command), (* line 297 *)
("setup",Parse.ML_source >> Setup), (* line 301 *)
("local_setup",Parse.opt_target --
Parse.ML_source >> LocalSetup), (* line 305 *)
Parse.text "") >> AttributeSetup),
Parse.text "") >> MethodSetup),
("declaration",Parse.opt_target -- (* line 321 *)
Parse.opt_keyword "pervasive" --
Parse.ML_source >> Declaration),
("syntax_declaration",Parse.opt_target -- (* line 326 *)
Parse.opt_keyword "pervasive" --
Parse.ML_source >> SyntaxDeclaration),
("simproc_setup",Parse.opt_target -- (* line 331 *)
(@{keyword "("} |-- Parse.enum1 "|"
Parse.term --| @{keyword ")"} --|
@{keyword "="}) -- Parse.ML_source
-- Scan.optional (@{keyword "identifier"}
(@{keyword "="} |-- Parse.ML_source) >> Oracle),(* line 371 *)
--| @{keyword "="}) -- Parse_Spec.xthms1 --
Parse.for_fixes >> Bundle),
Parse.xname) >> Include), (* line 384 *)
Parse.xname) >> Including), (* line 390 *)
("print_bundles", Scan.succeed PrintBundles), (* line 396 *)
("subclass", Parse.opt_target -- (* line 471 *)
("instance",Scan.option ( (* line 481 *)
((Parse.class -- (@{keyword "\<subseteq>"}
|| Parse.multi_arity >> InstanceArity))
(* line 313 HOL/Tools/Datatype/primrec.ML *)
Parse_Spec.where_alt_specs >> Primrec),
(* line 795 HOL/Tools/Datatype/datatype.ML *)
(* line 646 HOL/Tools/Datatype/rep_datatype.ML *)
(* line 173 HOL/Tools/Function/fun.ML *)
(* line 285 HOL/Tools/Function/partial_function.ML *)
("partial_function",((@{keyword "("} |-- Parse.xname --|
Parse_Spec.spec))) >> PartialFunction),
(* line 284 HOL/Tools/Function/function.ML *)
(* line 290 HOL/Tools/Function/function.ML *)
(* line 275 HOL/Tools/typedef.ML *)
("typedef",Parse.type_args_constrained --
(@{keyword "="} |-- Parse.term) --
Scan.option (@{keyword "morphisms"} |--
(* line 404 HOL/HOLCF/Tools/fixrec.ML *)
let val opt_thm_name' : (bool * Attrib.binding) parser =
@{keyword ")"} >> K (true, Attrib.empty_binding)
|| Parse_Spec.opt_thm_name ":" >> pair false
val spec' : (bool * (Attrib.binding * string)) parser =
opt_thm_name' -- Parse.prop >>
val alt_specs' : (bool * (Attrib.binding * string)) list parser =
let val unexpected = Scan.ahead
(Parse.name || @{keyword "["} || @{keyword "("})
(* line 265 HOL/HOLCF/Tools/Domain/domain.ML *)
@{keyword "("} |-- Scan.optional
(Parse.binding >> SOME) -- (@{keyword "::"}
|-- Parse.typ --| @{keyword ")"}
|| Parse.typ >> (fn t => (false, NONE, t))
val cons_decl = Parse.binding --
val domain_decl = (Parse.type_args_constrained --
(@{keyword "="} |-- Parse.enum1 "|" cons_decl)
Scan.optional (@{keyword "("} |--
@{keyword ")"}) false --Parse.and_list1 domain_decl
fun unparse_cmd s = Parse.group (fn () => s)
let val (cmd,toks'') = take_suffix Token.is_command toks'
else Scan.fail ()
|[] => Scan.fail ());
first' (List.map (fn s => unparse_cmd s >>
first' (List.map (fn s => unparse_cmd s >>
(* Isabelle/Isar/isar_syn.ML line 415 *)
Parse_Spec.locale_expression false --
Scan.optional (@{keyword "+"} |-- Parse.!!!
(Parse.command_name "context" |-- (* line 405 *)
--| Parse.begin
-- Scan.repeat (simple_thy_body || rec_thy_body)
--| Parse.command_name "end"
(Parse.command_name "locale" |-- (* line 421 *)
Scan.optional (@{keyword "="} |--
--| Parse.command_name "end") ||
Scan.succeed []) >> Locale),
(let val class_val = (* Pure/Isar/isar_syn.ML line 458 *)
in Parse.command_name "class" |-- p --
--| Parse.command_name "end") ||
Scan.succeed []) >> Class end),
((Parse.command_name "instantiation" |-- (* line 475 *)
Scan.repeat (simple_thy_body ||
--| Parse.command_name "end")) >> Instantiation),
@{keyword ")"}) true >> Parse.triple1)
in Parse.command_name "overloading" |-- p
Parse.command_name "end")
(* taken from Pure/Thy/thy_load.ML *)
let val master_dir = Thy_Load.get_master_path ()
(Thy_Syntax.parse_spans toks)
val elements = Thy_Syntax.parse_elements spans
val immediate = not (Goal.future_enabled ())
val (result, st') = Toplevel.proof_result immediate
(Outer_Syntax.get_syntax ())) init elem) x
elements (state, Position.none)
val _ = Thy_Header.define_keywords header
val _ = Present.init_theory name
in Thy_Load.begin_theory master_dir header parents
|> Present.begin_theory 0 master_dir uses end))
in (t Toplevel.toplevel toks,t) end;
val thy : Token.T list -> thy
(string * Position.T) option -> string -> term
val inferred_param : string -> Toplevel.state ->
(string * Position.T) option -> typ
val format_type_mixfix : string -> Mixfix.mixfix ->
fun scan p = File.read p
|> Token.source {do_recover = SOME false}
>> K NONE || Parse.not_eof >> SOME)) NONE
-- Scan.repeat thy_body
--| Parse.command_name "end"
let val ctxt = Named_Target.context_cmd (the_default
in Syntax.read_sort ctxt end;
let val ctxt' = Named_Target.context_cmd (the_default
val ctxt = Proof_Context.set_mode mode ctxt'
val read_term = do_read Syntax.read_term;
val read_class = do_read Proof_Context.read_class
do_read (Proof_Context.inferred_param s)
Proof_Context.mode_default state target |> #1;
|> K |> K |> PolyML.addPrettyPrinter;
(* Taken from Pure/Syntax/printer.ML *)
fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE
| xprod_to_fmt (Syntax_Ext.XProd (_, xsymbs, const, pri)) =
(if Lexicon.is_terminal s then 1000 else p);
fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
| xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
| xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
| xsyms_to_syms (Syntax_Ext.Bg i :: xsyms) =
| xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) =
| xsyms_to_syms (Syntax_Ext.En :: xsyms) = ([], xsyms)
let val (Syntax_Ext.Syn_Ext {xprods=p,...}) =
in case xprod_to_fmt (List.hd p) of
PolyML.makestring mx) end
let val (Syntax_Ext.Syn_Ext {xprods=p,...}) =
|NONE => Simple_Syntax.read_typ "'a",mx)]
in case xprod_to_fmt (List.last p) of
PolyML.makestring mx) end
handle General.Match => NONE) fs of
(mk v |> space_explode " " |> List.hd));
fun xml name attrs body = XML.Elem ((name,attrs),body);
val xml_of_theory : (string -> unit) -> string -> XML.tree list
(fn T' => if length (Thy_Info.loaded_files
(Context.theory_name T')) > 0
(Context.parents_of T))
datatype thy = datatype Parser.thy;
val xml_of_keyword = variant "xml_of_keyword" PolyML.makestring
(Path.print #> b ? (fn s => "("^s^")")) p) [];
val xml_of_expr = variant "xml_of_expr" PolyML.makestring
[fn ((name,_),(("",false),Expression.Named [])) =>
fun extract_context (t : Token.T list)
(body : (Token.T list * 'b) list) =
let val btoks = List.map #1 body |> flat
val blen = List.length btoks
val len = List.length t
andalso (Token.content_of t1 =
Token.content_of t2)
else (List.take (t,len-blen-1),
[List.last t]) end;
Parser.read_typ state target typ
let val b' = Binding.print b
fun xml_of_symb v = variant "xml_of_symb" PolyML.makestring [
fn Parser.Arg i =>
fn Parser.TypArg i =>
fn Parser.String (_,s) =>
fn Parser.Break i =>
fn Parser.Block (i,symbs) =>
(List.map xml_of_symb symbs)] v;
[fn Mixfix.NoSyn => NONE,
fn mx => Parser.format_const_mixfix state name mx tp
"format_type_mixfix" PolyML.makestring
[fn Mixfix.NoSyn => NONE,
fn mx => Parser.format_type_mixfix name mx num_args
attr "pretty" (Mixfix.pretty_mixfix
#> Pretty.str_of) mx)
(List.map xml_of_symb symbs)]
attr "pretty" (Mixfix.pretty_mixfix
#> Pretty.str_of) mx)
(List.map xml_of_symb symbs)]
val tp = Parser.inferred_param name state target
in [XML_Syntax.xml_of_type tp]@
PolyML.makestring [fn [(tm,[])] =>
state target tm |> XML_Syntax.xml_of_term]] tms
(case try Logic.dest_all t of
let val (skips, raw_spec) = ListPair.unzip eqs
val (fixes, spec) = fst (Specification.read_spec f
raw_spec (Toplevel.context_of state))
dest_eqs o Logic.strip_imp_concl
val get_imps = map HOLogic.dest_Trueprop o
val tms' = ListPair.zip (skips,tms)
val fn_eqs = List.foldl (fn (eq,t) =>
val old = Symtab.lookup t name
Symtab.update (name,(tp,def_tms@
|NONE => Symtab.update (name,(tp,
end) Symtab.empty tms'
val fns = List.foldl (fn (((b,_),mx),t) =>
Symtab.empty fixes
in Symtab.fold_rev (fn (k,(tp,equations)) =>
val SOME(mx) = Symtab.lookup fns b
val equations' = List.map (fn (b,imps,vs,tm) =>
let val imps' = xml "Premises" [] (List.map
(XML_Syntax.xml_of_term) imps)
a "unchecked" "") (imps'::List.map
XML_Syntax.xml_of_term (vs@[tm])) end)
[XML_Syntax.xml_of_type tp]@
let val eqs' = List.map (fn ((b,l),tm) =>
let val _ = if Attrib.is_empty_binding (b,l)
Proof_Context.mode_pattern state target tm |>
HOLogic.dest_eq |> (fn (head,body) =>
val fn_eqs = List.foldl (fn (eq,t) =>
val old = Symtab.lookup t name
Symtab.update (name,(tp,def_tms@
|NONE => Symtab.update (name,(tp,
end) Symtab.empty eqs'
val fns = List.foldl (fn ((b,_,mx),t) =>
in Symtab.fold_rev (fn (k,(tp,equations)) =>
val SOME(mx) = Symtab.lookup fns b
val equations' = List.map (fn (vs,tm) =>
xml "Equation" [] (List.map
XML_Syntax.xml_of_term (vs@[tm]))) equations
[XML_Syntax.xml_of_type tp]@
variant "xml_of_statement" PolyML.makestring
(List.map (fn (t,ts) => xml "Show" [] (
let val t' = Parser.read_term
state target t |> XML_Syntax.xml_of_term
(Function_Common.FunctionConfig {sequential,
@(Option.map (a "default") default |> the_default [])
(List.map (fn n => xml "class" (a "name" n) []) s)
(List.map xml_of_sort (s'::s))
let val (elem,state') = variant "xml_of_body" PolyML.makestring [
let val l' = List.map (fn ((name,tm),args) =>
let val tm' = Parser.read_prop state NONE tm
val (c,def_tm) = Logic.dest_equals tm'
XML_Syntax.xml_of_term def_tm] end) l
let val vars' = List.map (fn (name,sort) => case sort of
Parser.read_sort state NONE sort')
mx (List.length vars)
(mx'@[xml "Proof" [] [XML.Text proof]]@
[XML_Syntax.xml_of_term tm']@
let val ([name],args',sort) = Class.read_multi_arity
(Toplevel.theory_of state) arity
val args = List.map #2 args'
List.foldl xml_of_body_elem ((s1,trans),[]) body
[xml "Body" [] (List.rev b_elems)]),s3) end,
(Toplevel.theory_of state) arity
val args = List.map #2 args'
val vars = xml "Vars" [] (List.map (fn s =>
TFree (s,[]) |> XML_Syntax.xml_of_type)
([xml "Proof" [] [XML.Text proof]]@elems), s1) end,
(Parser.read_class state target cls)@
[xml "Proof" [] [XML.Text proof]],
List.foldl xml_of_body_elem ((s1,trans),[]) body
[fn (ps,[]) => List.map xml_of_expr ps] parents
val target = SOME (string_of_binding name,Position.none)
(List.map (xml_of_context s1 target) ctxt)
[xml "Body" [] (List.rev b_elems)]),s3) end,
List.foldl xml_of_body_elem ((s1,trans),[]) body
val target = SOME (string_of_binding name,Position.none)
val parents' = List.map (attr "name"
(Parser.read_sort s1 target #> the_single)
handle List.Empty => raise Fail
(List.map (xml_of_context s1 target) ctxt)
[xml "Body" [] (List.rev b_elems)]),s3) end,
val typ' = Parser.read_typ state target typ
mx (List.length vars)
val vars' = xml "Vars" [] (List.map
(fn s => TFree (s,[]) |> XML_Syntax.xml_of_type)
val dts' = List.map
mx (List.length vars)@
List.map (fn (c,tms,mx) =>
val tps = List.map
(Parser.read_typ s1 NONE) tms
List.map (fn (v,s) =>
SOME(s') => Parser.read_sort
val is_c = not (String.isSubstring " " cname)
else (Parser.read_typ s1 NONE cname::tps))
@(List.map (fn (v,s) =>
XML_Syntax.xml_of_type (TFree (v,
fn Consts cs => (xml "Consts" [] (List.map
let val tp' = Parser.read_typ state NONE tp
(mx'@[tp' |> XML_Syntax.xml_of_type]) end) cs),
fn Axioms axs => (xml "Axioms" [] (List.map
|> XML_Syntax.xml_of_term]) axs), trans state toks),
(List.map (xml_of_context state target) ctxt)
(ctxt'::[xml "Proof" [] [XML.Text proof]]
|_ => raise Fail ("Case not implemented: "^PolyML.makestring
Specification.read_free_spec (the_list name)
[(binding,tm)] (Toplevel.context_of state)
val tm'' = HOLogic.dest_Trueprop tm'
(fn t => (HOLogic.dest_eq t
handle ex => Logic.dest_equals t))
(mx'@[XML_Syntax.xml_of_type tp]@
val dts' = List.map (fn (((vs,name),mx), cs) =>
let val vars = List.map (fn (a,s) =>
SOME s' => Parser.read_sort state NONE s'
name) mx (List.length vs)
val cs' = List.map (fn ((c,args),mx1) =>
Proof_Context.mode_default s1 NONE
|> Term.type_of in
([XML_Syntax.xml_of_type t]@
(List.map (fn (l,sel,tp) =>
(Parser.read_typ s1 NONE tp)]))
List.foldl xml_of_body_elem (state,[]) body;
val dir = Path.dir file
val thys = map (fn (i,_) => (Thy_Info.get_theory i; [])
let val full = Path.explode i |>
val imports = List.map xml_of_import (#imports h)
val keywords = List.map xml_of_keyword (#keywords h)
val uses = List.map xml_of_use (#uses h)
val (s,t) = ParserHelper.init_thy dir (th,h)
Toplevel.empty) (#1 s') |>
val body' = [body'' |> List.rev |> xml "Body" []]