parser.ml revision 61d26ef772466529400bc460e7c69f67c1173b56
structure TheoryData = struct
type opt_target = (xstring * Position.T) option;
datatype misc_body = Chapter of opt_target * string
|Section of opt_target * string
|Subsection of opt_target * string
|Subsubsection of opt_target * string
|Text of opt_target * string
|TextRaw of opt_target * string
|Sect of string
|Subsect of string
|Subsubsect of string
|Txt of string
|TxtRaw of string
|DiagnosticCommand of string
|TopLevelCommand of string;
type proof = string;
type ml_text = string * Position.T;
type orig = Token.T list;
(* isar-ref.pdf page 78 *)
datatype context_head = ContextNamed of xstring * Position.T
|ContextHead of ((xstring * Position.T) list
* Element.context list);
datatype instance_type = InstanceArity of string list * string list
*string
|InstanceSubset of string;
datatype thy_body =
Classes of (binding * string list) list
|Classrel of (string * string) list
|DefaultSort of opt_target * string
|TypeDecl of ((opt_target * string list) * binding) * mixfix
|TypeSynonym of ((opt_target * string list) * binding) *
(string * mixfix)
|Nonterminal of binding list
|Arities of (string * string list * string) list
|Judgement of (binding * string * mixfix)
|Consts of (binding * string * mixfix) list
|Syntax of (string * bool) * (string * string * mixfix) list
|NoSyntax of (string * bool) * (string * string * mixfix) list
|Translations of (xstring * string) Syntax.trrule list
|NoTranslations of (xstring * string) Syntax.trrule list
|Axioms of (Attrib.binding * string) list
|Defs of (bool * bool) * ((binding * string) * Args.src list) list
|Definition of opt_target * ((binding * string option * mixfix) option
* (Attrib.binding * string))
|Abbreviation of opt_target * ((string * bool) *
((binding * string option * mixfix) option * string))
|TypeNotation of opt_target * ((string * bool) * (string * mixfix) list)
|NoTypeNotation of opt_target * ((string * bool) *
(string * mixfix) list)
|Notation of opt_target * ((string * bool) * (string * mixfix) list)
|NoNotation of opt_target * ((string * bool) * (string * mixfix) list)
|Axiomatization of (binding * string option * mixfix) list *
(Attrib.binding * string list) list
|Theorems of (opt_target * (Attrib.binding *
(binding * string option * mixfix) list
|Lemmas of (opt_target * (Attrib.binding *
(binding * string option * mixfix) list
(binding * string option * mixfix) list
|Hide of string * (bool * xstring list)
|Use of string
|ML of ml_text
|ML_prf of ml_text
|ML_val of ml_text
|ML_command of ml_text
|Setup of ml_text
|LocalSetup of opt_target * ml_text
|AttributeSetup of (bstring * Position.T) * (ml_text * string)
|MethodSetup of (bstring * Position.T) * (ml_text * string)
|Declaration of (opt_target * bool) * ml_text
|SyntaxDeclaration of (opt_target * bool) * ml_text
|SimprocSetup of (((opt_target * (bstring * Position.T)) *
string list) * ml_text) * xstring list
|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
(binding * string option * mixfix) list
|Include of (xstring * Position.T) list
|Including of (xstring * Position.T) list
|PrintBundles
|Context of context_head * (orig * thy_body) list
|Locale of (binding * (Expression.expression * Element.context list))
* (orig * thy_body) list
|Sublocale of ((xstring * Position.T) * (Expression.expression *
(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)) *
(orig * thy_body) list
|Subclass of string * proof
|Instantiation of (string list * string list * string) *
(orig * thy_body) list
|Instance of ((string * instance_type) option) * proof
|Overloading of (bstring * string * bool) list * (orig * thy_body) list
|Theorem of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
(Element.context list * Element.statement)) * proof
|Lemma of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
(Element.context list * Element.statement)) * proof
|Corollary of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
(Element.context list * Element.statement)) * proof
|SchematicTheorem of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
(Element.context list * Element.statement)) *
proof
|SchematicLemma of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
(Element.context list * Element.statement)) * proof
|SchematicCorollary of (((opt_target * Attrib.binding) *
(xstring * Position.T) list) *
(Element.context list * Element.statement)) *
proof
|Primrec of (opt_target * (binding * string option * mixfix) list) *
(Attrib.binding * string) list
|Datatype of Datatype.spec_cmd list
|RepDatatype of string list
|Fun of opt_target * ((Function_Common.function_config * (binding *
string option * mixfix) list) *
(Attrib.binding * string) list)
|PartialFunction of xstring * ((binding * string option * mixfix) list *
(Attrib.binding * string))
|Function of (opt_target * ((Function_Common.function_config *
(binding * string option * mixfix) list)
* (Attrib.binding * string) list)) * proof
|Termination of string option * proof
|Misc of misc_body;
end;
signature ParserHelper =
sig
val cmd_theory : (Token.T list * Thy_Header.header) parser
val cmd_header : string parser
val thy_body : (Token.T list * TheoryData.thy_body) parser
val unparse_tokens : Token.T list -> string
val init_thy : (Token.T list * Thy_Header.header) ->
Toplevel.state * (Toplevel.state ->
Token.T list -> Toplevel.state)
end;
structure ParserHelper : ParserHelper =
struct
open TheoryData
val hide = curry Hide;
fun preserve_toks f toks =
let val (v,toks') = f toks
val consumed_toks = List.take(toks,List.length toks-
List.length toks')
in ((consumed_toks,v),toks') end;
(* Common Functions *)
(* taken from Pure/Isar/parse.ML *)
fun RESET_VALUE atom =
Scan.ahead (Scan.one (K true)) -- atom >>
(fn (arg, x) => (Token.assign NONE arg; x));
fun token p = RESET_VALUE (Scan.one p);
fun unparse_kind k = Parse.group (fn () => Token.str_of_kind k)
(token (Token.is_kind k) >> Token.unparse);
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 *)
(* line 12 *)
val cmd_theory = preserve_toks (Parse.command_name "theory"
|-- Thy_Header.args);
(* Pure/Isar/isar_syn.ML *)
(* line 14 *)
val cmd_header = Parse.command_name "header" |-- unparse_verbatim;
(* line 133 *)
val opt_mode =
(* line 129 *)
let val mode_spec = (@{keyword "output"} >> K ("", false)) ||
(@{keyword "output"} >> K false) true;
in Scan.optional (@{keyword "("} |-- Parse.!!!
(mode_spec --| @{keyword ")"})) Syntax.mode_default end;
val trans_line = (* line 157 *)
let val trans_pat = (* line 147 *)
(@{keyword "("} |-- Parse.!!!
(Parse.xname --| @{keyword ")"}))
"logic" -- Parse.inner_syntax Parse.string
fun trans_arrow toks = (* line 152 *)
((@{keyword "\<rightharpoonup>"} || @{keyword "=>"})
>> K Syntax.Parse_Rule ||
(@{keyword "\<leftharpoondown>"} || @{keyword "<="})
>> K Syntax.Print_Rule ||
(@{keyword "\<rightleftharpoons>"} || @{keyword "=="})
>> K Syntax.Parse_Print_Rule) toks
in trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
>> (fn (left, (arr, right)) => arr (left, right)) end;
val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
fun first' l = Scan.first (List.map preserve_toks l);
fun parse_interpretation_arguments mandatory = (* line 428 *)
Parse.!!! (Parse_Spec.locale_expression mandatory) --
(Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
(* line 514 *)
val parse_theorem = Parse.opt_target --
Scan.optional (Parse_Spec.opt_thm_name ":" --|
Scan.ahead (Parse_Spec.includes >> K "" ||
val mk_thy_body = List.map (fn (s,p) => Parse.command_name s |-- p);
(* partition (l : a' list) into sublist according predicate
(p : 'a -> bool) which signals the start of a new sublist,
i.e. the start of each sublist will satisfy p and all
other elements of each sublist will not. Only the first
sublist may start with an element that does not satisfy p.
example: partition (curry op= "a") "abababab"
= ["ab","ab","ab","ab"] *)
fun partition p l = #2 (List.foldr
(fn (x,(l1,l2)) => if (p x) then ([],(x::l1)::l2)
else (x::l1,l2)) ([],[]) l);
fun proof_qed i = Parse.group (fn () => "proof_qed")
(fn t =>
if i > 0 then Scan.first
[command "qed" -- proof_qed (i-1) >> op::,
command "oops" >> single,
command_with_args "proof"
-- proof_qed (i+1) >> op@,
(token Token.is_command --
Scan.repeat not_command >> op::)
-- proof_qed i >> op@] t
else ([],t));
val proof_prefix = Scan.repeat (Scan.first
[command_with_args "apply",
command_with_args "using",
command_with_args "unfolding"]) >> flat;
#> List.map (space_implode " ")
#> cat_lines) o (partition Token.is_command);
val proof = Parse.!!! ((proof_prefix -- Scan.first
[command_with_args "proof" -- proof_qed 1 >> op@,
command "oops" >> single,
command_with_args "by",
command ".." >> single,
command "." >> single]) >> op@
>> unparse_tokens);
val simple_thy_body' = first' (mk_thy_body [
("chapter", Parse.opt_target -- unparse_verbatim
>> (Misc o Chapter)), (* line 19 *)
("section", Parse.opt_target -- unparse_verbatim
>> (Misc o Section)), (* line 24 *)
("subsection", Parse.opt_target -- unparse_verbatim
>> (Misc o Subsection)), (* line 29 *)
("subsubsection", Parse.opt_target -- unparse_verbatim
>> (Misc o Subsubsection)), (* line 34 *)
("text", Parse.opt_target -- unparse_verbatim
>> (Misc o Text)), (* line 39 *)
("text_raw", Parse.opt_target -- unparse_verbatim
>> (Misc o Text)), (* line 44 *)
("sect", unparse_verbatim >> (Misc o Sect)), (* line 49 *)
("subsect", unparse_verbatim >> (Misc o Sect)), (* line 54 *)
("subsubsect", unparse_verbatim
>> (Misc o Subsubsect)), (* line 59 *)
("txt", unparse_verbatim >> (Misc o Txt)), (* line 64 *)
("txt_raw", unparse_verbatim >> (Misc o TxtRaw)), (* line 69 *)
("classes",Scan.repeat1 (Parse.binding -- (* line 79 *)
Scan.optional ((@{keyword "\<subseteq>"}
|| @{keyword "<"}) |-- Parse.!!!
(Parse.list1 Parse.class)) []) >> Classes),
("classrel",Parse.and_list1 (Parse.class -- (* line 85 *)
((@{keyword "\<subseteq>"} || @{keyword "<"})
|-- Parse.!!! Parse.class)) >> Classrel),
("default_sort",Parse.opt_target -- Parse.sort
>> DefaultSort), (* line 92 *)
("type_decl",Parse.opt_target -- Parse.type_args (* line 99 *)
>> TypeDecl),
("type_synonym", (* line 104 *)
let val p = Parse.opt_target -- Parse.type_args --
Parse.binding -- (Parse.$$$ "=" |-- Parse.!!!
(Parse.typ -- Parse.opt_mixfix'))
in p >> TypeSynonym end),
("nonterminal",Parse.and_list1 Parse.binding
>> Nonterminal), (* line 110 *)
("arities",Scan.repeat1 Parse.arity >> Arities), (* line 115 *)
("judgement",Parse.const_binding >> Judgement), (* line 122 *)
("consts",Scan.repeat1 Parse.const_binding
>> Consts), (* line 126 *)
("syntax",opt_mode -- Scan.repeat1 Parse.const_decl
>> Syntax), (* line 137 *)
("no_syntax",opt_mode -- Scan.repeat1
Parse.const_decl >> Syntax), (* line 141 *)
("translations",Scan.repeat1 trans_line
>> Translations), (* line 162 *)
("no_translations",Scan.repeat1 trans_line
>> NoTranslations), (* line 166 *)
("axioms",Scan.repeat1 Parse_Spec.spec >> Axioms), (* line 173 *)
("defs", (* line 186 *)
let val opt_unchecked_overloaded =
Scan.optional (@{keyword "("} |-- Parse.!!!
(((@{keyword "unchecked"} >> K true) --
Scan.optional (@{keyword "overloaded"} >> K true) false ||
@{keyword "overloaded"} >> K (false, true)) --|
@{keyword ")"})) (false, false);
in opt_unchecked_overloaded --
>> (fn ((x, y), z) => ((x, z), y)))
>> Defs end),
("definition",Parse.opt_target -- Parse_Spec.constdef
>> Definition), (* line 195 *)
("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
(Parse.type_const -- Parse.mixfix))
>> TypeNotation),
("no_type_notation",Parse.opt_target -- (* line 210 *)
(opt_mode -- Parse.and_list1
(Parse.type_const -- Parse.mixfix))
>> NoTypeNotation),
("notation",Parse.opt_target --
(opt_mode -- Parse.and_list1
>> Notation), (* line 216 *)
("no_notation",Parse.opt_target --
(opt_mode -- Parse.and_list1
>> NoNotation), (* line 216 *)
("axiomatization",Scan.optional Parse.fixes [] -- (* line 231 *)
Parse.!!! (Parse.and_list1
Parse_Spec.specs)) []
>> Axiomatization),
("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 "class"),
("hide_type",(Parse.opt_keyword "open" >> not) -- (* line 265 *)
>> hide "type"),
("hide_const",(Parse.opt_keyword "open" >> not) -- (* line 266 *)
>> hide "const"),
("hide_fact",(Parse.opt_keyword "open" >> not) -- (* line 267 *)
>> hide "fact"),
("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 *)
("attribute_setup",Parse.position Parse.name -- (* line 309 *)
Parse.!!! (@{keyword "="} |--
Parse.text "") >> AttributeSetup),
("method_setup",Parse.position Parse.name -- (* line 315 *)
Parse.!!! (@{keyword "="} |--
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"}
|-- Scan.repeat1 Parse.xname) []
>> SimprocSetup),
("parse_ast_translation",trfun >>
ParseAstTranslation), (* line 343 *)
("parse_translation",trfun >> ParseTranslation), (* line 348 *)
("print_translation",trfun >> PrintTranslation), (* line 353 *)
("typed_print_translation", trfun >>
TypedPrintTranslation), (* line 358 *)
("print_ast_translation", trfun >>
PrintAstTranslation), (* line 364 *)
("oracle", Parse.position Parse.name --
(@{keyword "="} |-- Parse.ML_source) >> Oracle),(* line 371 *)
("bundle", Parse.opt_target -- (Parse.binding (* line 379 *)
--| @{keyword "="}) -- Parse_Spec.xthms1 --
Parse.for_fixes >> Bundle),
("include", Scan.repeat1 (Parse.position
Parse.xname) >> Include), (* line 384 *)
("including", Scan.repeat1 (Parse.position
Parse.xname) >> Including), (* line 390 *)
("print_bundles", Scan.succeed PrintBundles), (* line 396 *)
("sublocale", Parse.position Parse.xname --| (* line 434 *)
(@{keyword "\<subseteq>"} ||
@{keyword "<"}) --
parse_interpretation_arguments false
-- proof
>> Sublocale),
("interpretation", (* line 442 *)
parse_interpretation_arguments true
-- proof >> Interpretation),
("interpret", (* line 449 *)
parse_interpretation_arguments true
>> Interpret),
("subclass", (* line 471 *)
Parse.class -- proof >> Subclass),
("instance",Scan.option (Parse.class -- (* line 481 *)
(((@{keyword "\<subseteq>"} || @{keyword "<"})
|-- Parse.!!! Parse.class) >> InstanceSubset
|| Parse.multi_arity >> InstanceArity))
-- proof >> Instance),
("theorem", parse_theorem -- proof >> Theorem), (* line 525 *)
("lemma", parse_theorem -- proof >> Lemma), (* line 526 *)
("corollary", parse_theorem -- proof >> Corollary),(* line 527 *)
("schematic_theorem", parse_theorem -- proof (* line 528 *)
>> SchematicTheorem),
("schematic_lemma", parse_theorem -- proof (* line 529 *)
>> SchematicLemma),
("schematic_corollary", parse_theorem -- proof (* line 530 *)
>> SchematicCorollary),
(* line 313 HOL/Tools/Datatype/primrec.ML *)
("primrec", Parse.opt_target -- Parse.fixes --
Parse_Spec.where_alt_specs >> Primrec),
(* line 795 HOL/Tools/Datatype/datatype.ML *)
("datatype",Parse.and_list1 Datatype.spec_cmd
>> Datatype),
(* line 646 HOL/Tools/Datatype/rep_datatype.ML *)
("rep_datatype",Scan.repeat1 Parse.term
>> RepDatatype),
(* line 173 HOL/Tools/Function/fun.ML *)
>> Fun),
(* line 285 HOL/Tools/Function/partial_function.ML *)
("partial_function",((@{keyword "("} |-- Parse.xname --|
@{keyword ")"}) -- (Parse.fixes -- (Parse.where_ |--
Parse_Spec.spec))) >> PartialFunction),
(* line 284 HOL/Tools/Function/function.ML *)
("function",Parse.opt_target -- Function_Common.function_parser
-- proof
>> Function),
(* line 290 HOL/Tools/Function/function.ML *)
("termination",Scan.option Parse.term -- proof
>> Termination)]);
fun unparse_cmd s = Parse.group (fn () => s)
(fn toks =>
case toks of
t::toks' =>
if Token.is_command t andalso Token.content_of t = s then
let val (cmd,toks'') = take_suffix Token.is_command toks'
in (t::cmd |> List.map Token.unparse
|> space_implode " ",toks'') end
else Scan.fail ()
|[] => Scan.fail ());
val diagnostic_commands = ["pretty_setmargin","help","print_commands",
"print_configs","print_context","print_theory","print_syntax",
"print_abbrevs","print_theorems","print_locales","print_classes",
"print_locale","print_interps","print_dependencies",
"print_attributes","print_simpset","print_rules","print_trans_rules",
"print_methods","print_antiquotations","thy_deps","locale_deps",
"class_deps","thm_deps","print_binds","print_facts","print_cases",
"print_statement","thm","prf","full_prf","prop","term","typ",
"print_codesetup","unused_thms"];
val toplevel_commands = ["cd","pwd","use_thy","remove_thy",
"kill_thy","display_drafts","print_drafts","pr","disable_pr",
"enable_pr","commit","quit","exit","welcome","init_toplevel",
"linear_undo","undo","undos_proof","cannot_undo","kill",
"realizers","realizability","extract_type","extract"];
val simple_thy_body = simple_thy_body' ||
first' (List.map (fn s => unparse_cmd s >>
(Misc o DiagnosticCommand)) diagnostic_commands) ||
first' (List.map (fn s => unparse_cmd s >>
(Misc o TopLevelCommand)) diagnostic_commands);
(* Isabelle/Isar/isar_syn.ML line 415 *)
val locale_val =
Parse_Spec.locale_expression false --
Scan.optional (@{keyword "+"} |-- Parse.!!!
(Scan.repeat1 Parse_Spec.context_element)) [] ||
Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
fun rec_thy_body toks = first' [
(Parse.command_name "context" |-- (* line 405 *)
((Parse.position Parse.xname >> ContextNamed) ||
(Scan.optional Parse_Spec.includes [] --
>> ContextHead))
--| Parse.begin
-- Scan.repeat (simple_thy_body || rec_thy_body)
--| Parse.command_name "end"
>> Context),
(Parse.command_name "locale" |-- (* line 421 *)
Scan.optional (@{keyword "="} |--
Parse.!!! locale_val) (([], []), []) --
((Parse.begin |-- Scan.repeat
(simple_thy_body || rec_thy_body)
--| Parse.command_name "end") ||
Scan.succeed []) >> Locale),
(* line 464 *)
(let val class_val = (* Pure/Isar/isar_syn.ML line 458 *)
Parse_Spec.class_expression -- Scan.optional (@{keyword "+"}
|-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
Scan.repeat1 Parse_Spec.context_element >> pair []
val p = Parse.binding -- Scan.optional (@{keyword "="}
|-- class_val) ([], [])
in Parse.command_name "class" |-- p --
((Parse.begin |-- Scan.repeat
(simple_thy_body || rec_thy_body)
--| Parse.command_name "end") ||
Scan.succeed []) >> Class end),
((Parse.command_name "instantiation" |-- (* line 475 *)
Parse.multi_arity -- (Parse.begin |--
Scan.repeat (simple_thy_body ||
rec_thy_body)
--| Parse.command_name "end")) >> Instantiation),
(let val p = Scan.repeat1 (Parse.name --| (* line 493 *)
(@{keyword "\<equiv>"} || @{keyword "=="}) --
Parse.term -- Scan.optional (@{keyword "("} |--
(@{keyword "unchecked"} >> K false) --|
@{keyword ")"}) true >> Parse.triple1)
in Parse.command_name "overloading" |-- p
-- (Parse.begin |-- Scan.repeat
(simple_thy_body || rec_thy_body) --|
Parse.command_name "end")
>> Overloading end)
] toks;
val thy_body = simple_thy_body || rec_thy_body;
(* taken from Pure/Thy/thy_load.ML *)
fun read init state toks =
let val master_dir = Thy_Load.get_master_path ()
val spans = (*map (resolve_files master_dir)*)
(Thy_Syntax.parse_spans toks)
val elements = Thy_Syntax.parse_elements spans
(* fun excursion *)
val immediate = not (Goal.future_enabled ())
fun proof_result (tr, trs) (st, _) =
let
val (result, st') = Toplevel.proof_result immediate
(tr, trs) st
val pos' = Toplevel.pos_of (List.last (tr :: trs))
in (result, (st', pos')) end
fun element_result elem x =
fold_map proof_result
(Outer_Syntax.get_syntax ())) init elem) x
val (results, (end_state, end_pos)) = fold_map element_result
elements (state, Position.none)
in end_state end;
fun init_thy (toks,header) =
let val t = read (K
(let val {name = (name, _), imports, uses, ...} = header
val _ = Thy_Header.define_keywords header
val _ = Present.init_theory name
val master_dir = Thy_Load.get_master_path ()
val parents = List.map (Thy_Info.get_theory o #1) imports
in Thy_Load.begin_theory master_dir header parents
|> Present.begin_theory 0 master_dir uses end))
in (t Toplevel.toplevel toks,t) end;
end;
signature Parser =
sig
val scan : string -> Token.T list;
val dbg : Token.T list -> (Token.kind * string) list
datatype thy = Thy of {header:string option,
args:(Token.T list * Thy_Header.header),
body:(Token.T list * TheoryData.thy_body)
list};
val thy : Token.T list -> thy
val read_sort : Toplevel.state -> (string * Position.T) option
-> string -> sort
val read_typ : Toplevel.state -> (string * Position.T) option
-> string -> typ
val read_term : Proof_Context.mode -> Toplevel.state ->
(string * Position.T) option -> string -> term
val pretty_tokens : unit -> unit
end;
structure Parser : Parser =
struct
open ParserHelper
datatype thy = Thy of {header:string option,
args:(Token.T list * Thy_Header.header),
body:(Token.T list * TheoryData.thy_body) list};
(* scan isabelle source transforming it into a sequence of commands *)
fun scan s = File.read (Path.explode s)
|> Token.source {do_recover = SOME false}
val thy = Scan.catch (Scan.option cmd_header -- cmd_theory
-- Scan.repeat thy_body
--| Parse.command_name "end"
#> (fn (((h,a),b),_) => Thy {header=h,args=a,body=b}));
fun read_sort state loc =
let val ctxt = Named_Target.context_cmd (the_default
("-", Position.none) loc) (Toplevel.theory_of state)
in Syntax.read_sort ctxt end;
fun read_typ state loc =
let val ctxt = Named_Target.context_cmd (the_default
("-", Position.none) loc) (Toplevel.theory_of state)
in Syntax.read_typ ctxt end;
fun read_term mode state loc =
let val ctxt' = Named_Target.context_cmd (the_default
("-", Position.none) loc) (Toplevel.theory_of state)
val ctxt = Proof_Context.set_mode mode ctxt'
in Syntax.read_term ctxt end;
fun pretty_tokens () = (Token.unparse #> PolyML.PrettyString)
|> K |> K |> PolyML.addPrettyPrinter;
end;
signature Export =
sig
val xml_of_theory : Parser.thy -> XML.tree
end;
structure Export : Export =
struct
structure XML_Syntax = Legacy_XML_Syntax
open TheoryData
datatype thy = datatype Parser.thy;
fun xml name attrs body = XML.Elem ((name,attrs),body);
fun xml_of_import (name,_) = xml "Import" [("name",name)] [];
fun xml_of_keyword (s,spec) =
case spec of
SOME ((s1,[]),[]) => xml "Keyword"
[("name","\""^s^"\" :: "^s1)] []
|NONE => xml "Keyword" [("name",s)] []
|_ => raise
(Fail ("xml_of_keyword not implemented for "^
PolyML.makestring (s,spec)));
fun xml_of_use (s,b) =
let val p = if b then "("^Path.print s^")"
else Path.print s
in xml "UseFile" [("name",p)] [] end;
fun xml_of_expr ((name,_),(("",false),Expression.Named [])) =
xml "Parent" [("name",name)] []
|xml_of_expr v = raise (Fail ("xml_of_expr not implemented for "^
PolyML.makestring v));
fun xml_of_body_elem ((toks,e),((state,trans),l)) =
let fun extract_context t body =
let val btoks = List.map #1 body |> flat
val blen = List.length btoks
val len = List.length t
fun eq t1 t2 = (Token.kind_of t1 = Token.kind_of t2)
andalso (Token.content_of t1 =
Token.content_of t2)
in if blen = 0 then (t,[])
else
then raise (Fail "Unexpected result!")
else (List.take (t,len-blen-1),
[List.last t]) end
fun attr_of_target (SOME (s,_)) = [("target",s)]
|attr_of_target NONE = []
fun attr_of_mixfix Mixfix.NoSyn = []
|attr_of_mixfix m = [("mixfix",Mixfix.pretty_mixfix m
|> Pretty.str_of)]
fun xml_of_typ state target (SOME typ) = [
Parser.read_typ state target typ
|xml_of_typ _ _ _ = []
fun binding_to_str b =
let val b' = Binding.print b
in String.substring (b',1,String.size b'-2) end
fun attrs_of_binding (name,args) =
[("name",binding_to_str name),
("args",List.map (Args.pretty_src
(Toplevel.context_of state) #> Pretty.string_of) args
|> space_implode ", ")];
fun xml_of_context state target
(Element.Fixes fixes) = xml "Fixes" []
(List.map (fn (b,tp,mx) =>
(xml "Fix" ([("name",binding_to_str b)]
@attr_of_mixfix mx)
(xml_of_typ state target tp))) fixes)
|xml_of_context state target
(Element.Assumes ass) = xml "Assumes" []
(List.map (fn (b,tms) => case tms of
[(tm,[])] => xml "Assumption" (attrs_of_binding b)
state target tm |> XML_Syntax.xml_of_term]
|v => raise (Fail ("xml_of_context not implemented for "^
PolyML.makestring v^" (Assumption)")))
ass)
|xml_of_context _ _ v =
raise (Fail ("xml_of_context not implemented for "^
PolyML.makestring v));
fun xml_of_statement state target (Element.Shows s) =
List.map (fn (b,tms) =>
xml "Shows" (attrs_of_binding b)
(List.map (fn (t,ts) => xml "Show" [] (
let val t' = Parser.read_term Proof_Context.mode_default
state target t |> XML_Syntax.xml_of_term
val ts' = map (Parser.read_term
state target #>
in t'::ts' end)) tms)) s
|xml_of_statement _ _ v =
raise (Fail ("xml_of_statement not implemented for "^
PolyML.makestring v));
fun attr_of_function_config
(Function_Common.FunctionConfig {sequential,
default,domintros,partials}) =
(if sequential then [("sequential","")] else [])
@(case default of
SOME v => [("default",v)] | NONE => [])
@(if domintros then [("domintros" ,"")] else [])
@(if partials then [("partials" ,"")] else [])
val (elem,state') = case e of
Locale ((name,(parents,ctxt)),body) =>
let val (begin_,end_) = extract_context toks body
val s1 = trans state begin_
val ((s2,_),b_elems) =
List.foldl xml_of_body_elem ((s1,trans),[]) body
val s3 = trans s2 end_
val parents' = case parents of
(ps,[]) => List.map xml_of_expr ps
|_ => raise (Fail "Case not implemented!")
val name' = [("name",binding_to_str name)]
val target = SOME (binding_to_str name,Position.none)
val ctxt' = xml "Ctxt" []
(List.map (xml_of_context s3 target) ctxt)
in (xml "Locale" name' (ctxt'::parents'@
[xml "Body" [] (List.rev b_elems)]),s3) end
|Class ((name,(parents,ctxt)),body) =>
let val (begin_,end_) = extract_context toks body
val s1 = trans state begin_
val ((s2,_),b_elems) =
List.foldl xml_of_body_elem ((s1,trans),[]) body
val s3 = trans s2 end_
val target = SOME (binding_to_str name,Position.none)
val parents' = List.map (fn p => xml "Parent"
[("name",case Parser.read_sort s1 target p of
[cls] => cls
|_ => raise (Fail "Unexpected result"))
] []) parents
val name' = [("name",binding_to_str name)]
val ctxt' = xml "Ctxt" []
(List.map (xml_of_context s3 target) ctxt)
in (xml "Cls" name' (ctxt'::parents'@
[xml "Body" [] (List.rev b_elems)]),s3) end
|TypeSynonym (((target,vars),name),(typ,mixfix))
=>
let val s1 = trans state toks
val typ' = Parser.read_typ state target typ
val name' = [("name",binding_to_str name)]
val target' = attr_of_target target
val mixfix' = attr_of_mixfix mixfix
val vars' = xml "Vars" [] (List.map
(fn s => TFree (s,[]) |> XML_Syntax.xml_of_type)
vars)
in (xml "TypeSynonym" (name'@target'@mixfix')
([vars']@[typ']),s1) end
|Datatype dts =>
let val s1 = trans state toks
val dts' = List.map
(fn ((name,vars,mx),cs) => xml "Datatype"
([("name",binding_to_str name)]
@(attr_of_mixfix mx))
(List.map (fn (c,tms,mx) =>
xml "Constructor" ([("name",binding_to_str c)]
@attr_of_mixfix mx) (List.map
(Parser.read_typ s1 NONE #>
XML_Syntax.xml_of_type) tms)) cs
@(List.map (fn (v,s) =>
XML_Syntax.xml_of_type (TFree (v,
case s of
SOME(s') => [s']
|NONE => []))) vars))) dts
in (xml "Datatypes" [] dts', s1) end
|Consts cs => (xml "Consts" [] (List.map
(fn (name,tp,mx) => xml "Const"
([("name",binding_to_str name)]
@attr_of_mixfix mx)
[Parser.read_typ state NONE tp
|> XML_Syntax.xml_of_type]) cs), trans state toks)
|Axioms axs => (xml "Axioms" [] (List.map
(fn (b,tm) => xml "Axiom"
(attrs_of_binding b)
[Parser.read_term Proof_Context.mode_default state NONE tm
|> XML_Syntax.xml_of_term]) axs), trans state toks)
|Lemma ((((target,(name,args)), strs),(ctxt,stmt)),proof) =>
let val result = case (binding_to_str name,args,strs) of
("",[],[]) =>
let val s1 = trans state toks
val ctxt' = xml "Ctxt" []
(List.map (xml_of_context state target) ctxt)
in (xml "Lemma" (attr_of_target target)
(ctxt'::[xml "Proof" [] [XML.Text proof]]
@xml_of_statement state target stmt),s1) end
|_ => raise (Fail "Case not implemented")
in result end
|Definition (target,(name,(binding,tm))) =>
let val s1 = trans state toks
val (attrs,tp') = case name of
SOME (name,tp,mx) =>
(("name",binding_to_str name)::
(attr_of_mixfix mx),
xml_of_typ state target tp)
|NONE => ([],[])
val tm' = [Parser.read_term Proof_Context.mode_default
state target tm |> XML_Syntax.xml_of_term]
in (xml "Definition" (attrs@attr_of_target target)
(tp'@tm'),s1) end
|Fun (target,((cfg,f),a)) =>
let val s1 = trans state toks
val fixes = List.map (fn (b,typ,mixfix) =>
xml "FunSig" (attr_of_mixfix mixfix
@[("name",binding_to_str b)])
(case typ of
SOME s =>
[Parser.read_typ state target s
|NONE => [])) f
val eqs = List.map (fn ((b,l),tm) =>
case ((binding_to_str b,l),tm) of
(("",[]),tm) =>
state target tm
| _ =>
raise (Fail "Not yet implemented for Fun!"))
a
in (xml "Fun" (attr_of_target target
@attr_of_function_config cfg)
(fixes@eqs),s1) end
|Primrec ((target,f),a) =>
let val s1 = trans state toks
val fixes = List.map (fn (b,typ,mixfix) =>
xml "FunSig" (attr_of_mixfix mixfix
@[("name",binding_to_str b)])
(case typ of
SOME s =>
[Parser.read_typ state target s
|NONE => [])) f
val eqs = List.map (fn ((b,l),tm) =>
case ((binding_to_str b,l),tm) of
(("",[]),tm) =>
state target tm
| _ =>
raise (Fail "Not yet implemented for Fun!"))
a
in (xml "Primrec" (attr_of_target target)
(fixes@eqs),s1) end
|_ => raise (Fail ("Export of "^(PolyML.makestring e |>
space_explode " " |>
^" not yet implemented"))
in ((state',trans),elem::l) end;
fun xml_of_body state body =
let val (state',b_elems) = List.foldl xml_of_body_elem
(state,[]) body
in xml "Body" [] (List.rev b_elems) end;
fun xml_of_theory (Thy {header,args=(th,h),body}) =
let 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 name = ("name", #1 (#name h))
val header' = case header of
SOME s => [("header",s)]
|NONE => []
val (s,t) = ParserHelper.init_thy (th,h)
val body' = [xml_of_body (s,t) body]
in xml "Export" []
[xml "Thy" (name::header') (imports@keywords@body')] end;
end;