export_helper.ml revision f0051190a4466db48632aa2137e50a14a434caa2
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiusignature ParserHelper =
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu type ('a,'b) p;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu datatype ('a,'b) r = Result of 'b
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu | More of 'a -> ('a,'b) r
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu | Fail of string;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu val result : 'a list -> ('a -> ('a,'b) r) -> 'a list * ('a,'b) r;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu val p : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c * 'b) p;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu val p2r : (('a, string) p -> ('b, 'c) p) -> 'a list -> ('d, 'c) r;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu val >> : ('a, 'b) p * ('b -> 'c) -> ('a, 'c) p;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu val >>> : ('a -> ('b, 'c) p) * ('c -> 'd) -> 'a -> ('b, 'd) p;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu val >>= : ('a, 'b) p * ('b -> 'c) -> 'c option;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu val getError : ('a, 'b) p -> string;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu val return : 'a -> ('b, 'c) p -> ('b, 'c * 'a) p;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu val initialState : 'a list -> ('a,string) p;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu val pack : ('a, ('b * 'c) * 'd) p -> ('a, 'b * ('c * 'd)) p;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu val expect_end : ('a, 'b) p -> ('c, 'b) p;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu val e : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c) p;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu val succeed : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c) p;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu val many : (('a, 'b) p -> ('a, 'b * 'c) p) ->
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu ('a, 'b) p -> ('a, 'b * 'c list) p;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu val sepBy : (('a, 'b * 'c) p -> ('a, 'd * 'c) p) ->
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu (('a, 'd) p -> ('a, 'b * 'c) p) ->
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu ('a, 'd) p -> ('a, 'd * 'c list) p;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu val optional : (('a, 'b) p -> ('a, 'b * 'c) p) ->
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu ('a, 'b) p -> ('a, 'b * 'c option) p;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu val oneOf : ('a -> ('b, 'c) p) list -> 'a -> ('b, 'c) p;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiuinfix 1 >> >>> >>=;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiustructure ParserHelper : ParserHelper =
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu (* Parser state consisting either of
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu * a valid state containing a list of tokens and a parser result
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu * or an error message *)
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu datatype ('a,'b) p = State of ('a list) * 'b
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu | Failed of string;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu (* Parse result:
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu * Result (parsing finished)
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu * More (needs to consume more token using returned function)
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu * End (parsing ended before the current token - do not consume it)
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu * Fail (parsing failed with error message) *)
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu datatype ('a,'b) r = Result of 'b
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu | More of 'a -> ('a,'b) r
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu | Fail of string;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu (* Obtain a parser result sensibly handling More and End *)
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu fun result [] _ = ([],Fail "No more data!")
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu | result (d::ds) f = case f d of
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu More f => result ds f
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu |End v => (d::ds,Result v)
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu (* Interpret a parsing result as an action on a parser state.
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu Old and new result value are combined as a tuple.
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu "parsers" can be combined using #> and applied in
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu sequence using |> *)
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu fun p _ (Failed s) = Failed s
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu | p f (State (ds,v)) = case result ds f of
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu (ds',Result v1) => State (ds',(v,v1))
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu |(_,Fail s) => Failed s
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu |_ => Failed "Unexpected!";
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu (* Interpret a parser state as a parser result *)
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu fun p2r' (State (_,v)) = Result v
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu |p2r' (Failed s) = Fail s;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu fun p2r f v = State (v,"") |> f |> p2r';
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu (* apply f to presult value *)
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu fun (State (d,v)) >> f = State (d,f v)
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu |(Failed s) >> _ = Failed s;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu (* apply g to the result produced by f *)
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu fun (f >>> g) x = x |> f >> g;
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu (* extract result and apply f *)
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu fun (State (_,v)) >>= f = SOME (f v)
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu |(Failed _) >>= _ = NONE
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu fun getError (Failed s) = s
c756abd5f6eb3e73e300c4fe8efcb080b613fbacFrancisc Nicolae Bungiu |getError _ ="";
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu (* add result v1 to the state *)
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu fun return v1 (State (d,v)) = State (d,(v,v1))
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu |return _ (Failed s) = Failed s;
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu fun initialState d = State (d,"");
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu (* reorder result tuple *)
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu fun pack (State (d,((v,v1),v2))) = State (d,(v,(v1,v2)))
dad40397fd7ca8e2c00b58d19e506326a6570669Francisc Nicolae Bungiu |pack (Failed s) = Failed s;
fun oneOf ps s = List.foldl (fn (p,s') => case s' of
type cmd = Token.T list;
i.e. the start of each sublist will satisfy p and all
fun partition p l = #2 (List.foldr
type cmd = Token.T list;
|> Token.source {do_recover = SOME false}
|> partition Token.is_command;
assumes = List.map (fn (n,t) => {name=n,term=t}) a,
fixes = List.map (fn (ns,t) => {names=ns,tp=t}) f };
fun failT s t = Fail (s^" at "^Token.pos_of t);
fun content s t = if Token.content_of t = s then Result true
"content '"^Token.content_of t^"'") t;
fun ident t = if Token.ident_with (K true) t
then Result (Token.content_of t)
then Result (Token.content_of t)
then Result (Token.content_of t)
fun keyword s t = if Token.keyword_with (curry op= s) t
then Result (Token.content_of t)
t::ts => if Token.content_of t = s
(v,mkLocalData (List.concat (the_default [] a @
(List.concat (the_default [] f)))) end
val i' = case Token.content_of t of
in if i' = 0 then List.rev l' |> Result
|> List.map (space_implode " ")
t::_ => let val res = case Token.content_of t of
|_ => raise (Test (Token.unparse t))
val pretty_as_str : Pretty.T -> string
val repr_term : theory -> term -> Pretty.T
val repr_typ : theory -> typ -> Pretty.T
val repr_name : string -> Pretty.T
(term list * term) list) -> Pretty.T
(string * typ) list) -> Pretty.T
string list) -> Pretty.T
typ list) list) list -> Pretty.T
val xml_of_theories : theory_data list -> XML.tree
fun unqualify n = if Long_Name.is_qualified n
val thmNum = Unsynchronized.ref 0
Position.start text parents) end
op$ (Const ("HOL.Trueprop",_), tm) => tm
val prettify_term = Logic.strip_imp_concl o remove_hol_true_prop
val theory_by_name = Thy_Info.get_theory
val name_of_theory = Context.theory_name
val axioms_of = Theory.axioms_of
fun is_non_image_theory T = length (Thy_Info.loaded_files (name_of_theory T)) > 0
(Context.parents_of T))
val body = Term.strip_qnt_body qnt tm
val vars = List.map (fn (s,tp) => Var ((s,0),tp))
(Term.strip_qnt_vars qnt tm)
fun hol_conjunctions tm = case HOLogic.dest_conj tm of
fun thms_of T = List.map (fn (s,d) => (s,prop_of d))
(remove_parent_data Global_Theory.all_thms_of
let val get_consts = fn T => List.map (fn (n,(t,_)) => (n,t))
Datatype.DtTFree (s,srt) => TFree (s,srt)
| Datatype.DtType (s,ts) =>
Type (s,List.map (curry dtyp2typ descs) ts)
| Datatype.DtRec i =>
case List.find (curry op= i o #1) descs of
SOME (_,(s,ts,_)) => Type (s, List.map
val dt_desc = fn info => List.map (fn (_,(s,vs,eqs)) =>
let val vs' = List.map (curry dtyp2typ info) vs
val eqs' = List.map (fn (s,ts) =>
(s,List.map (curry dtyp2typ info) ts)) eqs
HOLogic is in HOL/Tools/hologic.ML
dest_Const is in Pure/term.ML
Logic is in Pure/logic.ML *)
o Logic.dest_implies o prop_of
in List.map (fn (c,i) => case dest_Const c of
(n,t) => (n,t,List.map fun_def (#psimps i))) d end
(List.map #1 thms))
in List.map (fn name =>
let val i = AxClass.get_info T name
(fn tm => Term.add_const_names tm [])
((Logic.dest_conjunction_list o #2
(not (String.isPrefix "HOL" n))) parents')
o Logic.dest_implies) t))
val sub_vars = List.map (fn (s,t) => ((s,0),Free (s,t))) all_params
let val all_locales = fn T => List.map (fn l => (#name l, #parents l))
val locales = Ord_List.subtract
(Ord_List.make (lift fast_string_ord #1)
(Ord_List.make (lift fast_string_ord #1)
in List.map (fn (name,ps) =>
val params = Ord_List.subtract (fn (s,((s1,_),_)) =>
(Ord_List.make fast_string_ord parent_params)
(Ord_List.make (lift fast_string_ord (#1 o #1))
(Locale.params_of T name))
val filter = ["_axioms.intro","_axioms_def","_def",".intro",".axioms_"]
val axioms' = List.filter
(fn t => (not (List.exists
(fn s => String.isPrefix (name ^ s) (#1 t))
o Thm.prop_of) t)) axioms'
(List.map (fn ((s,tp),_) =>
val parse_axioms = fn v => List.map hol_forall_elim
case List.find ((curry op= (name^"_axioms_def")) o #1) axs of
case List.find ((curry op= (name^"_def")) o #1) axs of
val in_loc = List.filter (fn (_,t) =>
List.exists (fn t' => t = t') in_locale_axioms) axioms
val ex_loc = List.filter (fn (_,t) =>
not (List.exists (fn t' => t = t') in_locale_axioms)) axioms
fun pretty_as_str p = Pretty.str_of p
in Syntax.pretty_term ctxt end
let val n = Long_Name.base_name n'
else Pretty.str n end
((Pretty.breaks ([repr_name s]
[Pretty.str " = ",repr_term T tm]))) def_eqs
in Pretty.block (head@Pretty.separate " | " body) end
let val head = [Pretty.str "class", repr_name s]
then [Pretty.str "="] else [])
val parents = List.map repr_name ps
[repr_name s,Pretty.str "::",
Pretty.quote (repr_typ T tp)])) fixes
[repr_name s, Pretty.str ":",
Pretty.quote (repr_term T tm)])) assumes
then [Pretty.str "+"] else [])@
let val head = [Pretty.str "locale", repr_name s]
then [Pretty.str "="] else [])
val parents = List.map repr_name ps
Pretty.quote (repr_typ T tp)])) fixes
[repr_name s, Pretty.str ":",
Pretty.quote (repr_term T tm)])) in_loc
then [Pretty.str "+"] else [])@
let val dts = List.map (fn (s,vs,eqs) =>
let val vs' = Pretty.enclose "(" ")"
([vs']@[repr_name s,Pretty.str "="]@eqs')) end) d
Pretty.separate "and" dts) end
val classes_Graph = String_Graph.make
(List.map (fn l => ((#1 l,l),#2 l)) (classes_of T))
val classes = List.map
(#1 o #2 o (String_Graph.get_entry classes_Graph))
val locales_Graph = String_Graph.make
(List.map (fn l => ((#1 l,l),#5 l)) (locales_of T))
val locales = List.map
(#1 o #2 o (String_Graph.get_entry locales_Graph))
in theory_of_string (unlines (List.map pretty_as_str
((List.map (repr_datatype T) datatypes)
@(List.map (repr_function T) functions)
@(List.map (repr_class T) classes)
val axs = Ord_List.subtract cmp
(Ord_List.make (lift fast_string_ord #1) (axioms_of T))
val thms = Ord_List.subtract cmp
(Ord_List.make (lift fast_string_ord #1) (thms_of T))
val consts = Ord_List.subtract cmp
(Ord_List.make (lift fast_string_ord #1) (consts_of T))
in List.map (fn T =>
List.map (fn (n,s) =>
if n = "name" andalso String.isPrefix (moduleName^".") s
List.map (fixTypeNames moduleName) c)
| XML.Elem (d,c) =>
SOME(Mixfix.Infixl (s,j)) => [("infixl",s), ("mixfix_i",string_of_int j)]
| SOME(Mixfix.Infixr (s,j)) => [("infixr",s), ("mixfix_i",string_of_int j)]
| SOME(Mixfix.Infix (s,j)) => [("infix",s), ("mixifix_i",string_of_int j)]
XML.Elem (("Const",a),t) =>
in XML.Elem (("Const",a@b),map (xml_of_term' T tbl) t) end
fun xml_of_term T t = xml_of_term' T Symtab.empty
(("Constructor",[("name",Long_Name.base_name s)]),
::(List.map(fn (pats,tm) =>
(List.map (fn p =>
@(List.map (fn (s,t) =>
@(List.map (fn (s,t) =>
[XML_Syntax.xml_of_type t])) fixes))
(List.map (fn ((s,t),m) =>
[XML_Syntax.xml_of_type t])) fixes)
@(List.map (fn (s,t) =>
@(List.map (fn (s,t) =>
@(List.map (fn p =>
val imports = List.map
(fn T => XML.Elem (("Import",[("name",name_of_theory T)]),[]))
(("Axiom",[("name",Long_Name.base_name n)]),
(("Theorem",[("name",Long_Name.base_name n)]),
(("Const",[("name",Long_Name.base_name n)]),
[XML_Syntax.xml_of_type tp])) cs
val datatypes = List.map (xml_of_datatype T) dts
val functions = List.map (xml_of_function T) fns
val classes = List.map (xml_of_class T) cls
val locales' = List.map (xml_of_locale T) locales
in fixTypeNames name (XML.Elem (("IsaTheory",[("name",name)]),