export_helper.ml revision f0051190a4466db48632aa2137e50a14a434caa2
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisignature ParserHelper =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski type ('a,'b) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski datatype ('a,'b) r = Result of 'b
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | More of 'a -> ('a,'b) r
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | Fail of string;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val result : 'a list -> ('a -> ('a,'b) r) -> 'a list * ('a,'b) r;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val p : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c * 'b) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val p2r : (('a, string) p -> ('b, 'c) p) -> 'a list -> ('d, 'c) r;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val >> : ('a, 'b) p * ('b -> 'c) -> ('a, 'c) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val >>> : ('a -> ('b, 'c) p) * ('c -> 'd) -> 'a -> ('b, 'd) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val >>= : ('a, 'b) p * ('b -> 'c) -> 'c option;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val getError : ('a, 'b) p -> string;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val return : 'a -> ('b, 'c) p -> ('b, 'c * 'a) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val initialState : 'a list -> ('a,string) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val pack : ('a, ('b * 'c) * 'd) p -> ('a, 'b * ('c * 'd)) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val expect_end : ('a, 'b) p -> ('c, 'b) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val e : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val succeed : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val many : (('a, 'b) p -> ('a, 'b * 'c) p) ->
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ('a, 'b) p -> ('a, 'b * 'c list) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val sepBy : (('a, 'b * 'c) p -> ('a, 'd * 'c) p) ->
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (('a, 'd) p -> ('a, 'b * 'c) p) ->
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ('a, 'd) p -> ('a, 'd * 'c list) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val optional : (('a, 'b) p -> ('a, 'b * 'c) p) ->
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ('a, 'b) p -> ('a, 'b * 'c option) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val oneOf : ('a -> ('b, 'c) p) list -> 'a -> ('b, 'c) p;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiinfix 1 >> >>> >>=;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructure ParserHelper : ParserHelper =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* Parser state consisting either of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * a valid state containing a list of tokens and a parser result
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * or an error message *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski datatype ('a,'b) p = State of ('a list) * 'b
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | Failed of string;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* Parse result:
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * Result (parsing finished)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * More (needs to consume more token using returned function)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * End (parsing ended before the current token - do not consume it)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski * Fail (parsing failed with error message) *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski datatype ('a,'b) r = Result of 'b
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | More of 'a -> ('a,'b) r
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | Fail of string;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* Obtain a parser result sensibly handling More and End *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun result [] _ = ([],Fail "No more data!")
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | result (d::ds) f = case f d of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski More f => result ds f
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |End v => (d::ds,Result v)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |r => (ds,r);
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* Interpret a parsing result as an action on a parser state.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Old and new result value are combined as a tuple.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski "parsers" can be combined using #> and applied in
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski sequence using |> *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun p _ (Failed s) = Failed s
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | p f (State (ds,v)) = case result ds f of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (ds',Result v1) => State (ds',(v,v1))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |(_,Fail s) => Failed s
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |_ => Failed "Unexpected!";
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* Interpret a parser state as a parser result *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun p2r' (State (_,v)) = Result v
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |p2r' (Failed s) = Fail s;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun p2r f v = State (v,"") |> f |> p2r';
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* apply f to presult value *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun (State (d,v)) >> f = State (d,f v)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |(Failed s) >> _ = Failed s;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* apply g to the result produced by f *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun (f >>> g) x = x |> f >> g;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* extract result and apply f *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun (State (_,v)) >>= f = SOME (f v)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |(Failed _) >>= _ = NONE
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun getError (Failed s) = s
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |getError _ ="";
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* add result v1 to the state *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun return v1 (State (d,v)) = State (d,(v,v1))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |return _ (Failed s) = Failed s;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun initialState d = State (d,"");
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* reorder result tuple *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun pack (State (d,((v,v1),v2))) = State (d,(v,(v1,v2)))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |pack (Failed s) = Failed s;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* expect the end of the token stream
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (useful to check if all tokens were consumed) *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun expect_end (Failed s) = Failed s
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | expect_end (State ([],v)) = State ([],v)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | expect_end (State (_,_)) = Failed "Expected end!";
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* create a parser discarding the result of f *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun e f s = p f s >> #1;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* always succeeds, but only consumes input if the
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski parsing is successful *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun succeed f s = case p f s of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Failed _ => s
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |State (ds,(v,_)) => State (ds,v);
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* apply parser p as many times as possible *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun many p s =
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski case (p s,s) of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (State (ds,(v,v1)),_) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val (ds',vs) = case many p (State (ds,v)) of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski State (ds',(_,vs)) => (ds',vs)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Failed _ => (ds,[])
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in State (ds',(v,v1::vs)) end
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |(Failed _,State (ds,v)) => State (ds,(v,[]))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |(_,Failed s) => Failed s;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* apply parser p multiple times separated by sep *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun sepBy sep p s = case many (p #> sep) s of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski State (ds,(v,vs)) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val (ds',vs') =
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski case p (State (ds,v)) of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski State (ds',(_,v')) => (ds',(v'::vs))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Failed _ => (ds,vs)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in State (ds',(v,vs')) end
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |Failed s => Failed s;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (* if p is a parser then optional p either has the result
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski SOME("result of p") or NONE (if p fails)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski if p and p1 are parsers then `optional (p #> p1)`
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski is the optional version of `p |> p1` *)
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder fun optional _ (Failed s) = Failed s
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |optional p (State (ds,v)) = case p (State (ds,v)) of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Failed _ => State (ds,(v,NONE))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |State (ds',(v',v1)) => State (ds',(v',SOME(v1)));
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* try each of the parsers ps from left to right
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski until one succeeds or fail if all parsers fail *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun oneOf ps s = List.foldl (fn (p,s') => case s' of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Failed _ => p s
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Failed "No parser supplied") ps;
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisignature Parser =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski type cmd = Token.T list;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val scan : string -> cmd list;
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski type parsed_theory;
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val test : cmd list -> (parsed_theory option * string);
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskistructure Parser : Parser =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski open ParserHelper
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* partition (l : a' list) into sublist according predicate
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski (p : 'a -> bool) which signals the start of a new sublist,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski i.e. the start of each sublist will satisfy p and all
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski other elements of each sublist will not. Only the first
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski sublist may start with an element that does not satisfy p.
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski example: partition (curry op= "a") "abababab"
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski = ["ab","ab","ab","ab"] *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun partition p l = #2 (List.foldr
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (x,(l1,l2)) => if (p x) then ([],(x::l1)::l2)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski else (x::l1,l2)) ([],[]) l);
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski type cmd = Token.T list;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* scan isabelle source transforming it into a sequence of commands *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun scan str = str |> Source.of_string |> Symbol.source
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |> Token.source {do_recover = SOME false}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski datatype local_data = LocalData of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski {assumes: {name:string option, term:string} list,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fixes: {names:string list, tp:string} list};
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun mkLocalData a f = LocalData {
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski assumes = List.map (fn (n,t) => {name=n,term=t}) a,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fixes = List.map (fn (ns,t) => {names=ns,tp=t}) f };
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val emptyLocalData = LocalData { assumes = [], fixes = [] };
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski datatype theory_body_elem = DataType of (string list * (string *
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (string * string list) list)) list
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |Consts of (string * string) list
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski |Axioms of (string * string) list
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder |Lemma of {name: string,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski attrs: string list option,
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski target: string option,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski statement: string,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski local_data:local_data,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski proof: string}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |Theorem of {name: string,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski attrs: string list option,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski target: string option,
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski statement: string,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski local_data:local_data,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski proof: string}
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski |Class of {name:string,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski parents:string list,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski local_data:local_data}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |Locale of {name:string,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski parents:string list,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski local_data:local_data}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |TypeSynonym of string * string
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |Function of {name: string,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski def_eqs: string list}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |PrimRec of {names: (string*string) list,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski def_eqs: string list}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |Definition of (string*string) option *
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |Text of string
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |MiscCmd of string * string;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski datatype parsed_theory = ParsedTheory of {
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski header: string option,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski name: string,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski imports: string list,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski keywords: (string list*string) option,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski body: theory_body_elem list
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* Add token position to error message *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun failT s t = Fail (s^" at "^Token.pos_of t);
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun content s t = if Token.content_of t = s then Result true
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski else failT ("Expected content '"^s^"' but found "^
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski "content '"^Token.content_of t^"'") t;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun ident t = if Token.ident_with (K true) t
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski else failT "Not a valid identifier!" t;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun type_ident t = if Token.kind_of t = Token.TypeIdent
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski else failT "Not a TypeIdent!" t;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun str_ t = if Token.kind_of t = Token.String
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski else failT "Not a String!" t;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun keyword s t = if Token.keyword_with (curry op= s) t
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski else failT "Not a valid keyword!" t;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun unparse_cmd s cmd = case cmd of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski t::ts => if Token.content_of t = s
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |> space_implode " "
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski else Fail "Unexpected command!"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |_ => Fail "Expected non-empty command!";
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val parse_theory_head = e (content "theory") #> p ident >>> #2
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> e (keyword "imports") #> many (p ident)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> optional (e (keyword "keywords") #>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski many (p str_) #>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski e (keyword "::") #>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski oneOf [p str_, p ident] #> pack)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> e (keyword "begin") #> pack #> expect_end;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val parse_theory_end = e (content "end") #> expect_end;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun parse_local_data a =
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski let val assumes = fn k => e k #>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski sepBy (e (keyword "and"))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (optional (p ident #> e (keyword ":"))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> p str_ #> pack)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val fixes = e (keyword "fixes") #>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski sepBy (e (keyword "and"))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (many (p ident) #> e (keyword "::")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> oneOf [p str_,p ident,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski p type_ident] #> pack)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski in optional (many (assumes a)) #> optional (many fixes)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> optional (many (assumes a)) (* a = keyword "assumes" *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >>> (fn (((v,a),f),a1) =>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (v,mkLocalData (List.concat (the_default [] a @
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski the_default [] a1))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (List.concat (the_default [] f)))) end
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val parse_body_elem =
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski let val dt_type = e (content "datatype")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> sepBy (e (keyword "and"))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (oneOf [e (keyword "(") #>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski sepBy (e (keyword ","))
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski (p type_ident) #>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski e (keyword ")"),
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski many (p type_ident), return []]
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski #> p ident #> e (keyword "=")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> sepBy (e (keyword "|"))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (oneOf [p ident,p str_]
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> many (oneOf [p ident,p str_])
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski #> pack #> pack)
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski #> expect_end >>> DataType o #2
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val consts = e (content "consts") #> many (
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski p ident #> e (keyword "::") #> p str_ #> pack)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski #> expect_end >>> Consts o #2
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val axioms = e (content "axioms") #> many ((p ident)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski #> e (keyword ":") #> (p str_) #> pack)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski #> expect_end >>> Axioms o #2
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val cls = e (content "class") #> p ident
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski #> succeed (keyword "=")
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski #> sepBy (e (keyword "+"))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski #> succeed (keyword "+")
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski #> parse_local_data (keyword "assumes")
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >>> (fn (((_,n),ps),l) =>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Class { name = n,parents = ps,
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski local_data = l})
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val locale = e (content "locale") #> p ident
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski #> succeed (keyword "=")
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski #> sepBy (e (keyword "+"))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski #> succeed (keyword "+")
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski #> parse_local_data (keyword "assumes")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >>> (fn (((_,n),ps),l) =>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Locale { name = n,parents = ps,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski local_data = l})
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val tp_synonym = e (content "type_synonym")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> p ident #> e (keyword "=")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> p str_ #> pack >>> TypeSynonym o #2
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val fun_ = e (content "fun") #> p ident
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> e (keyword "::") #> p str_
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> e (keyword "where")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> sepBy (e (keyword "|"))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >>> (fn (((_,n),t),def) =>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski Function { name = n, tp = t,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski def_eqs = def })
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val primrec = e (content "primrec")
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski #> sepBy (e (keyword "and"))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (p ident #> e (keyword "::") #>
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski p str_ #> pack)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> e (keyword "where")
7e7c1b5990145d02f8abb7c74d3c0d609735b54cTill Mossakowski #> sepBy (e (keyword "|")) (p str_)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski >>> (fn ((_,ns),def) =>
7e7c1b5990145d02f8abb7c74d3c0d609735b54cTill Mossakowski PrimRec { names = ns, def_eqs = def })
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val def = e (content "definition")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> optional (p ident #> e (keyword "::")
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski #> p str_ #> pack #> e (keyword "where"))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> p str_ #> pack >>> Definition o #2
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski in oneOf [dt_type,consts,axioms,cls,
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski tp_synonym,fun_,primrec,locale,def] end;
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski fun parse_thm s = e (content s)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> optional (
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski e (keyword "(") #> e (keyword "in")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> p ident #> e (keyword ")"))
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski #> optional (e (keyword "[") #> many (p ident)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> e (keyword "]"))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> e (keyword ":")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> optional (parse_local_data (keyword "assumes")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski #> e (keyword "shows"))
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski #> (p str_) #> pack #> pack #> pack #> pack >>> #2;
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski fun proof_qed i l cmd = case cmd of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski t::_ => let val l' = cmd::l
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val i' = case Token.content_of t of
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski |"proof" => i+1
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski in if i' = 0 then List.rev l' |> Result
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski else More (proof_qed i' l') end
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |_ => Fail "Expected non-empty command!";
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fun proof_prefix l cmd = case cmd of
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski t::_ => if List.exists (Token.content_of t |>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski ["apply","using","unfolding"]
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski then cmd::l |> proof_prefix |> More
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski else cmd::l |> End
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |_ => Fail "Expected non-empty command!";
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski fun cmdList2string cmds = List.map (List.map Token.unparse) cmds
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |> List.map (space_implode " ")
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski |> cat_lines;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski exception Test of string;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val proof = p (proof_prefix []) #> p (fn cmd =>
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski t::_ => let val res = case Token.content_of t of
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski "proof" => More (proof_qed 1 [cmd])
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |"oops" => Result [cmd]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |"by" => Result [cmd]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |".." => Result [cmd]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski |"." => Result [cmd]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski |"done" => Result [cmd]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski |_ => raise (Test (Token.unparse t))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski |_ => Fail "Expected non-empty command!")
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski >>> (fn ((v,cmds),cmds1) => (v,cmds@cmds1 |>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski cmdList2string));
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val test = initialState #> optional (p (unparse_cmd "header"))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski #> p (parse_theory_head |> p2r) #> pack >>> #2
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski #> many (oneOf [p (parse_body_elem |> p2r),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski p (parse_thm "lemma" |> p2r) #> proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (v,((t,(n,(a,(l,stmt)))),prf)) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (v,Lemma {name=n,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski statement=stmt,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski local_data=the_default
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski emptyLocalData l,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski proof=prf})),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski p (parse_thm "theorem" |> p2r) #> proof
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (v,((t,(n,(a,(l,stmt)))),prf)) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (v,Theorem {name=n,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski statement=stmt,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski local_data=the_default
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski emptyLocalData l,
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski proof=prf})),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski p (unparse_cmd "text") >>>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (v,v1) => (v,Text v1)),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski p (unparse_cmd "section") >>>
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (fn (v,v1) => (v,MiscCmd ("section",v1))),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski p (unparse_cmd "subsection") >>>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (v,v1) => (v,MiscCmd ("subsection",v1))),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski p (unparse_cmd "value") >>>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (v,v1) => (v,MiscCmd ("value",v1))),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski p (unparse_cmd "unused_thms") >>>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (v,v1) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (v,MiscCmd ("unused_thms",v1))),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski p (unparse_cmd "ML_file") >>>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (v,v1) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (v,MiscCmd ("ML_file",v1))),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski p (unparse_cmd "setup") >>>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (v,v1) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (v,MiscCmd ("setup",v1)))])
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski #> e (parse_theory_end |> p2r)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski #> expect_end >>> (fn ((h,(n,(i,k))),b) =>
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ParsedTheory {header = h,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski keywords = k,
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski #> (fn v => (v >>= I,getError v));
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskisignature ExportHelper =
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski type named_term = (string * term)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (* general helper functions *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val unlines : string list -> string
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val unqualify : string -> string
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski (* isabelle specific functions *)
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val theory_of_string : string -> theory list -> theory
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val theory_by_name : string -> theory
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val name_of_theory : theory -> string
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val axioms_of : theory -> named_term list
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val non_image_theories : theory -> theory list
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val thms_of : theory -> named_term list
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val consts_of : theory -> (string * typ) list
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val datatypes_of : theory -> ((string * typ list *
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski (string * typ list) list) list) list
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski (* mutually_rec_types@(name * type_params *
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski constructors@(constructor_name * type_args))) *)
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val functions_of : theory -> (string * typ *
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski (term list * term) list) list
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski (* name * type *
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski def_eqs@(pats * defterm) *)
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski val classes_of : theory -> (class * string list *
f4dd7b59c284145a320a4b976312de41921d3f9eMaciek Makowski (string * term) list *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (string * typ) list) list
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (* name * parents * assumes * fixes *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val locales_of : theory -> (string *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ((string * typ) * mixfix) list *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski named_term list * named_term list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski string list) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (* name * fixes * in-locale axioms *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ex-locale axioms * parents *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val pretty_as_str : Pretty.T -> string
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val repr_term : theory -> term -> Pretty.T
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowski val repr_typ : theory -> typ -> Pretty.T
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val repr_name : string -> Pretty.T
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val repr_function : theory -> (string * typ *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (term list * term) list) -> Pretty.T
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val repr_class : theory -> (class * string list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * term) list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * typ) list) -> Pretty.T
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val repr_locale : theory -> (string *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski ((string * typ) * mixfix) list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski named_term list * named_term list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski string list) -> Pretty.T
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val repr_datatype : theory -> (string * typ list * (string *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski typ list) list) list -> Pretty.T
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val theory_of_exportable_data : theory -> theory
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val get_basic_theory_data : theory -> (named_term list *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski named_term list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * typ) list)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (* axioms * theorems * consts *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski type theory_data = (string * named_term list * named_term list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * typ) list * ((string * typ list *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (string * typ list) list) list) list *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (string * typ * (term list * term) list) list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (class * string list * (string * term) list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * typ) list) list *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (string * ((string * typ) * mixfix) list *
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski named_term list * named_term list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski string list) list)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (* name * axioms * theorems * consts * datatypes *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski functions * classes * locales *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val get_theories : theory -> theory_data list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val xml_of_theories : theory_data list -> XML.tree
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski exception ExportError of string
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskistructure ExportHelper : ExportHelper =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskiexception ExportError of string
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitype named_term = string * term
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskitype theory_data = (string * named_term list * named_term list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * typ) list * ((string * typ list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * typ list) list) list) list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * typ * (term list * term) list) list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (class * string list * (string * term) list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * typ) list) list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (string * ((string * typ) * mixfix) list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski named_term list * named_term list *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski string list) list)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski (* name * axioms * theorems * consts * datatypes *
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski functions * classes * locales *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(* ------------------------------ General helper functions *)
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowskival unlines = String.concatWith (String.str (Char.chr 10))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifun lift f sel = fn (t1,t2) => f (sel t1,sel t2)
9101c1cc72e8daa5e9b56c7c9e841c377f98402eTill Mossakowskifun unqualify n = if Long_Name.is_qualified n
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski then (Long_Name.implode (List.tl (Long_Name.explode n)))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(* ------------------------------ Isabelle specific functions *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(* Keep track of the number of theories created from a string *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(* create a theory from a string of its body *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifun theory_of_string body parents =
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski let val name = "TempTheory"^Int.toString (Unsynchronized.inc thmNum)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val header = Thy_Header.make ("TempTheory",Position.none) [] [] []
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski val text = unlines ["theory "^name,"begin",body,"end"]
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski in #1 (Thy_Load.load_thy 0 (Thy_Load.get_master_path ()) header
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski Position.start text parents) end
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskifun remove_hol_true_prop t = case t of
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski op$ (Const ("HOL.Trueprop",_), tm) => tm
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski | (t $ u) => (remove_hol_true_prop t) $ (remove_hol_true_prop u)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski | Abs (s,T,t) => Abs (s,T,remove_hol_true_prop t)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowskival prettify_term = Logic.strip_imp_concl o remove_hol_true_prop
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(* remove data that is already present in a parent theory *)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun remove_parent_data df cmp T =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val d = df T
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val pd = (List.foldl op@ [] (List.map df (Context.parents_of T)))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in Ord_List.subtract cmp (Ord_List.make cmp pd) (Ord_List.make cmp d) end
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(* a couple of aliases *)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskival theory_by_name = Thy_Info.get_theory
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskival name_of_theory = Context.theory_name
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski(* check if the theory is not part of the logic image *)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun is_non_image_theory T = length (Thy_Info.loaded_files (name_of_theory T)) > 0
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun non_image_theories T = List.concat (List.map
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (fn T' => if is_non_image_theory T'
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski then T'::(non_image_theories T') else [])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun hol_forall_elim tm =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val qnt = #1 (Term.dest_Const (HOLogic.all_const HOLogic.boolT))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val body = Term.strip_qnt_body qnt tm
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val vars = List.map (fn (s,tp) => Var ((s,0),tp))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in Term.subst_bounds (List.rev vars, body) end
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun hol_conjunctions tm = case HOLogic.dest_conj tm of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | tms => List.concat (List.map hol_conjunctions tms)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun thms_of T = List.map (fn (s,d) => (s,prop_of d))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (remove_parent_data Global_Theory.all_thms_of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (lift fast_string_ord #1) T)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(* currently there seems to be no way (anymore) to
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski attach any terms to a const directly. Thus the discarded
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski part is (hopefully) always NONE
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski todo: maybe throw an exception if this is not the case? *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun consts_of T =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val get_consts = fn T => List.map (fn (n,(t,_)) => (n,t))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (((Name_Space.dest_table (Syntax.init_pretty_global T)) o
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski #constants o Consts.dest o Sign.consts_of) T)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in remove_parent_data get_consts (lift fast_string_ord #1) T end
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun datatypes_of T =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val get_datatypes = (#log_types o Type.rep_tsig o Sign.tsig_of)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val ts = remove_parent_data get_datatypes fast_string_ord T
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val is_mutually_rec_type = fn (_,i) => length (#descr i) >1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val check_rec = fn (n,v) => if is_mutually_rec_type (n,v)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski then (#index v) < 1 else true
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val rec dtyp2typ = fn (descs,t) => case t of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Datatype.DtTFree (s,srt) => TFree (s,srt)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Type (s,List.map (curry dtyp2typ descs) ts)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski case List.find (curry op= i o #1) descs of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski SOME (_,(s,ts,_)) => Type (s, List.map
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (curry dtyp2typ descs) ts)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | NONE => raise ExportError("Internal Error!")
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val dt_desc = fn info => List.map (fn (_,(s,vs,eqs)) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val vs' = List.map (curry dtyp2typ info) vs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val eqs' = List.map (fn (s,ts) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (s,List.map (curry dtyp2typ info) ts)) eqs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in (s,vs',eqs') end) info
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in List.foldl (fn (n,l) => case Datatype.get_info T n of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski SOME(v) => if check_rec (n,v)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski then (dt_desc (#descr v))::l
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski | NONE => l) [] ts end
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski dest_Const is in Pure/term.ML
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskival functions_of =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val get_funs = fn T =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val d = Item_Net.content (Function_Common.get_function
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val fun_def = (fn (pats,def) => (#2 (strip_comb pats),def))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski o HOLogic.dest_eq o HOLogic.dest_Trueprop o #2
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in List.map (fn (c,i) => case dest_Const c of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (n,t) => (n,t,List.map fun_def (#psimps i))) d end
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in remove_parent_data get_funs (lift fast_string_ord #1) end
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun classes_of T =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val cls_suffix = "_class_def"
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowski val thms = thms_of T
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val cls_names = List.map (fn n => String.substring (n,0,String.size n-
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski String.size cls_suffix)) (List.filter (String.isSuffix cls_suffix)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in List.map (fn name =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val i = AxClass.get_info T name
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski o Logic.dest_equals o Thm.prop_of o #def) i))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val parents = List.map (fn n => String.substring
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (n,0,String.size n - String.size "_class"))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (List.filter (fn n => (String.isSuffix "_class" n) andalso
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (not (String.isPrefix "HOL" n))) parents')
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val axioms' = List.map (fn (n,t) => (n,(HOLogic.dest_Trueprop o #2
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (List.filter ((String.isPrefix (name^".")) o #1) thms)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (* note: instead of cls_names we should only use
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ancestors of the class *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val all_params = List.map (fn (s,t) => (Long_Name.base_name s,t))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (List.concat (List.map (#params o AxClass.get_info T) cls_names))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val sub_vars = List.map (fn (s,t) => ((s,0),Free (s,t))) all_params
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val axioms = List.map (fn (s,t) => (s,Term.subst_Vars sub_vars t))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in (name,parents,axioms,#params i) end) cls_names end
e31c49c9f2b85b768519a2e1ebc143e6a8484aecTill Mossakowskifun locales_of T =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val all_locales = fn T => List.map (fn l => (#name l, #parents l))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn (c,l) => fast_string_ord (#1 c,#1 l))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Ord_List.make (lift fast_string_ord #1)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (classes_of T))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Ord_List.make (lift fast_string_ord #1)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (remove_parent_data all_locales
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (lift fast_string_ord #1) T))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in List.map (fn (name,ps) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val parent_params = List.map (#1 o #1) (List.concat
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (List.filter (fn (s,_) => List.exists (curry op= s) ps) locales)))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val params = Ord_List.subtract (fn (s,((s1,_),_)) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski fast_string_ord (s,s1))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Ord_List.make fast_string_ord parent_params)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (Ord_List.make (lift fast_string_ord (#1 o #1))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val filter = ["_axioms.intro","_axioms_def","_def",".intro",".axioms_"]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val axs = List.filter ((String.isPrefix name) o #1)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (fn s => String.isPrefix (name ^ s) (#1 t))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski filter))) axs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val axioms = List.map (fn (s,t) => (s,(HOLogic.dest_Trueprop o #2
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val fix_consts = List.map (fn (s,t) => (s, Term.subst_Vars
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski (List.map (fn ((s,tp),_) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ((s,0),Const (s,tp))) params) t))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val parse_axioms = fn v => List.map hol_forall_elim
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ((hol_conjunctions o #2 o Logic.dest_equals o Thm.prop_of o #2) v)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val in_locale_axioms =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski case List.find ((curry op= (name^"_axioms_def")) o #1) axs of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski SOME v => parse_axioms v
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski case List.find ((curry op= (name^"_def")) o #1) axs of
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski SOME v => parse_axioms v
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val in_loc = List.filter (fn (_,t) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski List.exists (fn t' => t = t') in_locale_axioms) axioms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val ex_loc = List.filter (fn (_,t) =>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski not (List.exists (fn t' => t = t') in_locale_axioms)) axioms
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in (name,params,fix_consts in_loc,fix_consts ex_loc,ps) end) locales end
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(* ------------------------------ Represent as string *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun pretty_as_str p = Pretty.str_of p
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun repr_term T =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val ctxt = Config.put Printer.show_question_marks false
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun repr_typ T = Syntax.pretty_typ (Proof_Context.init_global T)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun repr_name n' =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in if String.isSubstring " " n then Pretty.quote (Pretty.str n)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskifun repr_function T (s,tp,def_eqs) =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski let val head = [Pretty.str "fun ", repr_name s, Pretty.str " :: ",
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski Pretty.quote (repr_typ T tp), Pretty.str " where "]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski val body = List.map (fn (pats,tm) => Pretty.quote (Pretty.block
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski ((Pretty.breaks ([repr_name s]
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski @(List.map (fn p => Pretty.enclose "(" ")" [repr_term T p])
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski [Pretty.str " = ",repr_term T tm]))) def_eqs
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski in Pretty.block (head@Pretty.separate " | " body) end
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun repr_class T (s,ps,assumes,fixes) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val head = [Pretty.str "class", repr_name s]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski @(if length fixes + length assumes + length ps > 0
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski then [Pretty.str "="] else [])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val parents = List.map repr_name ps
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val fixes' = List.map (fn (s,tp) => Pretty.block (Pretty.breaks
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [repr_name s,Pretty.str "::",
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Pretty.quote (repr_typ T tp)])) fixes
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val assumes' = List.map (fn (s,tm) => Pretty.block (Pretty.breaks
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [repr_name s, Pretty.str ":",
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Pretty.quote (repr_term T tm)])) assumes
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in (Pretty.block o Pretty.breaks) (head@(Pretty.separate "+" parents)@
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if length (fixes'@assumes') > 0 andalso length parents > 0
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski then [Pretty.str "+"] else [])@
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if length fixes' > 0
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski then [Pretty.str "fixes"]@(Pretty.separate "and" fixes') else [])@
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if length assumes' > 0
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski then [Pretty.str "assumes"]@(Pretty.separate "and" assumes') else [])) end
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun repr_locale T (s,fixes,in_loc,_,ps) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val head = [Pretty.str "locale", repr_name s]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski @(if length fixes + length in_loc + length ps > 0
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski then [Pretty.str "="] else [])
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val parents = List.map repr_name ps
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val fixes' = List.map (fn ((s,tp),_) => Pretty.block (Pretty.breaks
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Pretty.quote (repr_typ T tp)])) fixes
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski val assumes' = List.map (fn (s,tm) => Pretty.block (Pretty.breaks
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski [repr_name s, Pretty.str ":",
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski Pretty.quote (repr_term T tm)])) in_loc
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in (Pretty.block o Pretty.breaks) (head@(Pretty.separate "+" parents)@
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if length (fixes'@assumes') > 0 andalso length parents > 0
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski then [Pretty.str "+"] else [])@
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (if length fixes' > 0
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski then [Pretty.str "fixes"]@(Pretty.separate "and" fixes') else [])@
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (if length assumes' > 0
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski then [Pretty.str "assumes"]@(Pretty.separate "and" assumes') else [])) end
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowskifun repr_datatype T d =
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski let val dts = List.map (fn (s,vs,eqs) =>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski let val vs' = Pretty.enclose "(" ")"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (Pretty.separate "," (List.map (repr_typ T) vs))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski ([repr_name s]@
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski (List.map (Pretty.quote o repr_typ T) vs)))) eqs)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski ([vs']@[repr_name s,Pretty.str "="]@eqs')) end) d
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski in (Pretty.block o Pretty.breaks) ([Pretty.str "datatype"]@
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifun theory_of_exportable_data T =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski let val datatypes = datatypes_of T
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val functions = functions_of T
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val classes_Graph = String_Graph.make
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (List.map (fn l => ((#1 l,l),#2 l)) (classes_of T))
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val classes_sorted =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski List.rev (String_Graph.topological_order classes_Graph)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (#1 o #2 o (String_Graph.get_entry classes_Graph))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski classes_sorted
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val locales_Graph = String_Graph.make
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (List.map (fn l => ((#1 l,l),#5 l)) (locales_of T))
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val locales_sorted =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski List.rev (String_Graph.topological_order locales_Graph)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (#1 o #2 o (String_Graph.get_entry locales_Graph))
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski locales_sorted
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski in theory_of_string (unlines (List.map pretty_as_str
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski ((List.map (repr_datatype T) datatypes)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski @(List.map (repr_function T) functions)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski @(List.map (repr_class T) classes)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski @(List.map (repr_locale T) locales)))) (Context.parents_of T) end
47af295501ed5f407848f61b9943d58ccb43be29Till Mossakowskifun get_basic_theory_data T =
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski let val T' = theory_of_exportable_data T
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowski val cmp = (fn (s,(s1,_)) =>
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (lift fast_string_ord unqualify) (s,s1))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (Ord_List.make fast_string_ord (List.map #1 (axioms_of T')))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (Ord_List.make (lift fast_string_ord #1) (axioms_of T))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (Ord_List.make fast_string_ord (List.map #1 ((thms_of T')@axs)))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (Ord_List.make (lift fast_string_ord #1) (thms_of T))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (Ord_List.make fast_string_ord (List.map #1 (consts_of T')))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (Ord_List.make (lift fast_string_ord #1) (consts_of T))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski in (axs, thms, consts) end
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun get_theories T =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val Ts = T::(non_image_theories T)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski let val name = name_of_theory T
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val (axs,thms,consts) = get_basic_theory_data T
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val datatypes = datatypes_of T
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val functions = functions_of T
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski val classes = classes_of T
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski val locales = locales_of T
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski in (name,axs,thms,consts,datatypes,functions,
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski classes,locales) end) Ts end
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski(* Generate XML Output *)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskistructure XML_Syntax = Legacy_XML_Syntax
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun fixTypeNames moduleName t = case t of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski XML.Elem (("Type",a),c) => XML.Elem (("Type",
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski if n = "name" andalso String.isPrefix (moduleName^".") s
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski then (n,String.extract (s,(String.size moduleName)+1,NONE))
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski else (n,s)) a),
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski List.map (fixTypeNames moduleName) c)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski XML.Elem (d,List.map (fixTypeNames moduleName) c)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski(* Enrich the (isabelle-builtin) XML representation of terms with infix information *)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun mixfix_to_args m = case m of
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski SOME(Mixfix.Infixl (s,j)) => [("infixl",s), ("mixfix_i",string_of_int j)]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | SOME(Mixfix.Infixr (s,j)) => [("infixr",s), ("mixfix_i",string_of_int j)]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski | SOME(Mixfix.Infix (s,j)) => [("infix",s), ("mixifix_i",string_of_int j)]
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun xml_of_term' T tbl t = case t of
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski XML.Elem (("Const",a),t) =>
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski let val b = case (Syntax.guess_infix (Sign.syn_of T)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (Lexicon.mark_const ((#2 o List.hd) a))) of
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski SOME(mx) => mixfix_to_args (SOME mx)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski | NONE => mixfix_to_args (Symtab.lookup tbl ((#2 o List.hd) a))
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski in XML.Elem (("Const",a@b),map (xml_of_term' T tbl) t) end
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski | XML.Elem ((s,a),t) => XML.Elem ((s,a),map (xml_of_term' T tbl) t)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun xml_of_term T t = xml_of_term' T Symtab.empty
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun xml_of_datatype _ eqs = XML.Elem (("RecDatatypes",[]),List.map
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (fn (name,type_params,constructors) =>
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski XML.Elem (("Datatype",[("name",Long_Name.base_name name)]),
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (List.map XML_Syntax.xml_of_type type_params)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (("Constructor",[("name",Long_Name.base_name s)]),
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski constructors))) eqs)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskifun xml_of_function T (name,tp,def_eqs) =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski XML.Elem (("Function",[("name",Long_Name.base_name name)]),
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowski ::(List.map(fn (pats,tm) =>
e8f5a6ef56e210093ad852ed147d7f5f0a24cce9Till Mossakowski XML.Elem (("Equations",[]),List.map (xml_of_term T)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski (pats@[tm]))) def_eqs))
53eb610e03705ac6499371cde16cc37482fb3313Till Mossakowskifun xml_of_class T (name,parents,assumps,fixes) =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski XML.Elem (("ClassDef",[("name",Long_Name.base_name name)]),
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski XML.Elem (("Parent",[("name",Long_Name.base_name p)]),[])) parents)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski @(List.map (fn (s,t) =>
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski XML.Elem (("Assumption",[("name",Long_Name.base_name s)]),
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski [xml_of_term T t])) assumps)
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski @(List.map (fn (s,t) =>
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski XML.Elem (("ClassParam",[("name",Long_Name.base_name s)]),
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifun xml_of_locale T (name,fixes,assumps,thms,parents) =
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski XML.Elem (("Locale",[("name",Long_Name.base_name name)]),
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowski (List.map (fn ((s,t),m) =>
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski XML.Elem (("LocaleParam",[("name",Long_Name.base_name s)]
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski @(mixfix_to_args (SOME m))),
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski @(List.map (fn (s,t) =>
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski XML.Elem (("Assumption",[("name",Long_Name.base_name s)]),
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski [xml_of_term T t])) assumps)
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski @(List.map (fn (s,t) =>
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski XML.Elem (("Theorem",[("name",Long_Name.base_name s)]),
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski [xml_of_term T t])) thms)
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski XML.Elem (("Parent",[("name",Long_Name.base_name p)]),[])) parents))
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowskifun xml_of_theory (name, axs, thms, cs, dts, fns, cls, locales) =
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski let val T = theory_by_name name
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski (fn T => XML.Elem (("Import",[("name",name_of_theory T)]),[]))
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski val axioms = List.map (fn (n,t) => XML.Elem
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski (("Axiom",[("name",Long_Name.base_name n)]),
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski [(xml_of_term T o prettify_term) t])) axs
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski val theorems = List.map (fn (n,t) => XML.Elem
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski (("Theorem",[("name",Long_Name.base_name n)]),
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski [(xml_of_term T o prettify_term) t])) thms
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski val consts = List.map (fn (n,tp) => XML.Elem
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski (("Const",[("name",Long_Name.base_name n)]),
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski val datatypes = List.map (xml_of_datatype T) dts
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski val functions = List.map (xml_of_function T) fns
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski val classes = List.map (xml_of_class T) cls
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski val locales' = List.map (xml_of_locale T) locales
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski in fixTypeNames name (XML.Elem (("IsaTheory",[("name",name)]),
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski imports@axioms@theorems@consts@datatypes
460a5052a96ce648bbecc9a0bd41c1b82a1c4e59Till Mossakowski @functions@classes@locales')) end
9cb7b59cc1442c507b0eac2a795d68b5571788eaTill Mossakowskifun xml_of_theories theories =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski XML.Elem (("IsaExport",[]),List.map xml_of_theory theories)