045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroedersignature ParserHelper =
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder type ('a,'b) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder datatype ('a,'b) r = Result of 'b
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder | More of 'a -> ('a,'b) r
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder | Fail of string;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val result : 'a list -> ('a -> ('a,'b) r) -> 'a list * ('a,'b) r;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val p : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c * 'b) p;
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder val liftP : (('a,'b) p -> ('a,'c) p) -> ('a list,'b) p
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder -> ('a list,'c) p;
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder val >> : ('a -> ('b, 'c) p) * ('c -> 'd) -> 'a -> ('b, 'd) p;
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder val >>> : ('a -> ('b,'c*'d) p) * ('d -> 'e) -> 'a -> ('b,'c*'e) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val >>= : ('a, 'b) p * ('b -> 'c) -> 'c option;
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder val getError : ('a, 'b) p -> string;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val return : 'a -> ('b, 'c) p -> ('b, 'c * 'a) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val initialState : 'a list -> ('a,string) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val pack : ('a, ('b * 'c) * 'd) p -> ('a, 'b * ('c * 'd)) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val expect_end : ('a, 'b) p -> ('c, 'b) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val e : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val succeed : ('a -> ('a, 'b) r) -> ('a, 'c) p -> ('a, 'c) p;
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder val succeedP : (('a, 'b) p -> ('a, 'b * 'c) p) ->
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder ('a, 'b) p -> ('a, 'b) p;
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder val fail : ('a, 'b) p -> ('c, 'd) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val many : (('a, 'b) p -> ('a, 'b * 'c) p) ->
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder ('a, 'b) p -> ('a, 'b * 'c list) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val sepBy : (('a, 'b * 'c) p -> ('a, 'd * 'c) p) ->
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (('a, 'd) p -> ('a, 'b * 'c) p) ->
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder ('a, 'd) p -> ('a, 'd * 'c list) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val optional : (('a, 'b) p -> ('a, 'b * 'c) p) ->
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder ('a, 'b) p -> ('a, 'b * 'c option) p;
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder val oneOf : (('a, 'b) p -> ('a, 'b * 'c) p) list ->
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder ('a, 'b) p -> ('a, 'b * 'c) p;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederinfix 1 >> >>> >>=;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroederstructure ParserHelper : ParserHelper =
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* Parser state consisting either of
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder * a valid state containing a list of tokens and a parser result
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder * or an error message *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder datatype ('a,'b) p = State of ('a list) * 'b
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder | Failed of string;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* Parse result:
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder * Result (parsing finished)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder * More (needs to consume more token using returned function)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder * End (parsing ended before the current token - do not consume it)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder * Fail (parsing failed with error message) *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder datatype ('a,'b) r = Result of 'b
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder | More of 'a -> ('a,'b) r
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder | Fail of string;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* Obtain a parser result sensibly handling More and End *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun result [] _ = ([],Fail "No more data!")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder | result (d::ds) f = case f d of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder More f => result ds f
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |End v => (d::ds,Result v)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* Interpret a parsing result as an action on a parser state.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder Old and new result value are combined as a tuple.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder "parsers" can be combined using #> and applied in
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder sequence using |> *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun p _ (Failed s) = Failed s
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder | p f (State (ds,v)) = case result ds f of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (ds',Result v1) => State (ds',(v,v1))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(_,Fail s) => Failed s
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |_ => Failed "Unexpected!";
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder fun liftP _ (Failed s) = Failed s
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder |liftP _ (State ([],_)) = Failed "Expected command"
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder |liftP p (State (d::ds,v)) = case p (State (d,v)) of
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder State (_,v') => State (ds,v')
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder |Failed s => Failed s;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* apply g to the result produced by f *)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder fun (f >> g) x = case f x of
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder Failed s => Failed s
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder |State (ds,v) => State (ds,g v);
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder fun (f >>> g) = (f >> (fn (v,v1) => (v,g v1)))
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* extract result and apply f *)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun (State (_,v)) >>= f = SOME (f v)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(Failed _) >>= _ = NONE
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder fun getError (Failed s) = s
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder |getError _ ="";
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* add result v1 to the state *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun return v1 (State (d,v)) = State (d,(v,v1))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |return _ (Failed s) = Failed s;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun initialState d = State (d,"");
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* reorder result tuple *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun pack (State (d,((v,v1),v2))) = State (d,(v,(v1,v2)))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |pack (Failed s) = Failed s;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* expect the end of the token stream
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (useful to check if all tokens were consumed) *)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun expect_end (Failed s) = Failed s
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder | expect_end (State ([],v)) = State ([],v)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder | expect_end (State (_,_)) = Failed "Expected end!";
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (* create a parser discarding the result of f *)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder fun e f = p f >> #1;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (* always succeeds, but only consumes input if the
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder parsing is successful *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun succeed f s = case p f s of
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder |State (ds,(v,_)) => State (ds,v);
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder fun succeedP p s = case p s of
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder |State (ds,(v,_)) => State (ds,v);
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder fun fail (_ : ('a, 'b) p) = Failed "Always fails!";
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (* apply parser p as many times as possible *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder case (p s,s) of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (State (ds,(v,v1)),_) =>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder let val (ds',vs) = case many p (State (ds,v)) of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder State (ds',(_,vs)) => (ds',vs)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder |Failed _ => (ds,[])
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder in State (ds',(v,v1::vs)) end
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder |(Failed _,State (ds,v)) => State (ds,(v,[]))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(_,Failed s) => Failed s;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* apply parser p multiple times separated by sep *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun sepBy sep p s = case many (p #> sep) s of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder State (ds,(v,vs)) =>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder let val (ds',vs') =
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder case p (State (ds,v)) of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder State (ds',(_,v')) => (ds',(v'::vs))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |Failed _ => (ds,vs)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder in State (ds',(v,vs')) end
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |Failed s => Failed s;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* if p is a parser then optional p either has the result
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder SOME("result of p") or NONE (if p fails)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder if p and p1 are parsers then `optional (p #> p1)`
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder is the optional version of `p |> p1` *)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun optional _ (Failed s) = Failed s
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |optional p (State (ds,v)) = case p (State (ds,v)) of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder Failed _ => State (ds,(v,NONE))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |State (ds',(v',v1)) => State (ds',(v',SOME(v1)));
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* try each of the parsers ps from left to right
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder until one succeeds or fail if all parsers fail *)
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder fun oneOf (ps : (('a, 'b) p -> ('a, 'b * 'c) p) list) s =
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder List.foldl (fn (p,s') => case s' of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder Failed _ => p s
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (Failed "No parser supplied") ps;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroedersignature Parser =
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder type cmd = Token.T list;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val scan : string -> cmd list;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder type parsed_theory;
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder val test : cmd list -> (parsed_theory option * string);
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederstructure Parser : Parser =
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder open ParserHelper
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* partition (l : a' list) into sublist according predicate
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (p : 'a -> bool) which signals the start of a new sublist,
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder i.e. the start of each sublist will satisfy p and all
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder other elements of each sublist will not. Only the first
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder sublist may start with an element that does not satisfy p.
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder example: partition (curry op= "a") "abababab"
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder = ["ab","ab","ab","ab"] *)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun partition p l = #2 (List.foldr
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (fn (x,(l1,l2)) => if (p x) then ([],(x::l1)::l2)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder else (x::l1,l2)) ([],[]) l);
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder type cmd = Token.T list;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* scan isabelle source transforming it into a sequence of commands *)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun scan str = str |> Source.of_string |> Symbol.source
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder |> Token.source {do_recover = SOME false}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder |> Token.source_proper |> Source.exhaust
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder datatype local_data = LocalData of
11215d71075e01a34e70e0499503aac1ce4b8954Jonathan von Schroeder {assumes: {name:string option, term:string} list,
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder fixes: {names:string list, tp:string} list};
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder fun mkLocalData a f = LocalData {
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder assumes = List.map (fn (n,t) => {name=n,term=t}) a,
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder fixes = List.map (fn (ns,t) => {names=ns,tp=t}) f };
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von Schroeder val emptyLocalData = LocalData { assumes = [], fixes = [] };
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder datatype mixfix_data = Infix of string * int
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder |InfixL of string * int
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder |InfixR of string * int
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder |Binder of {template:string,
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder prios:int list option,
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder |Template of {template:string,
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder prios:int list option,
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder def_prio:int option};
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder datatype qualifier = Optional | Mandatory;
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder datatype hide_what = HideLocal | HideAll;
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder(* http://stackoverflow.com/questions/16254465/how-to-hide-defined-constants *)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder datatype arity = Arity of (string list option) * string;
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder datatype instance_data = InstanceA of string list * arity
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |InstanceR of {name:string,rel:string,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder parent:string};
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder datatype theory_body_elem = Context of string * theory_body_elem list
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder |DataType of (string list * (string *
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (string * string list) list)) list
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder |Consts of (string * string) list
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder |Axioms of (string * string) list
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |Lemma of {name: string option,
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder attrs: string list option,
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder target: string option,
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder statement: string,
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von Schroeder local_data:local_data,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |Theorem of {name: string option,
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder attrs: string list option,
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder target: string option,
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder statement: string,
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von Schroeder local_data:local_data,
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder |Class of {name:string,
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder parents:string list,
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder local_data:local_data}
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder |Locale of {name:string,
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder parents:string list,
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder local_data:local_data}
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |TypeSynonym of string list *
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder (string * string)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder |Function of {name: string,
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder def_eqs: string list}
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder names: (string*(string option)) list,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder def_eqs: string list}
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder {name_tp:(string*string option) option,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder eq:string,target:string option,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder attrs:string list option}
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder |Notation of {modes:string list option,
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder notations:(string*mixfix_data) list}
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |NoNotation of {modes:string list option,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder notations:(string*mixfix_data) list}
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder |Interpretation of {name:string,
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder qualifier:qualifier,
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder eqs:(string*string list),
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |Instantiation of {names:string list,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder arity:arity, body:theory_body_elem list}
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |Instance of instance_data option * string
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |Abbreviation of string
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder |Declaration of string
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |Axiomatization of {names:string list,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder tp: string,mixfix_data:mixfix_data option}
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |Hide of {what:string*hide_what,
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder names:string list}
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |MiscCmd of string * string
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |CodeCmd of string * string;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder datatype parsed_theory = ParsedTheory of {
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder header: string option,
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder imports: string list,
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroeder keywords: (string list*string) option,
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder body: theory_body_elem list
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (* Add token position to error message *)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun failT s t = Fail (s^" at "^Token.pos_of t);
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder fun content s t = if Token.content_of t = s then Result s
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else failT ("Expected content '"^s^"' but found "^
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder "content '"^Token.content_of t^"'") t;
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder fun name t = if Token.is_name t orelse Token.kind_of t =
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder else failT "Not a valid name!" t;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun type_ident t = if Token.kind_of t = Token.TypeIdent
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else failT "Not a TypeIdent!" t;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun str_ t = if Token.kind_of t = Token.String
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else failT "Not a String!" t;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun keyword s t = if Token.keyword_with (curry op= s) t
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder else failT "Not a valid keyword!" t;
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder fun unparse_cmd s cmd = case cmd of
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder |> space_implode " "
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder else Fail "Unexpected command!"
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder |_ => Fail "Expected non-empty command!";
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder fun unparse_code_cmd cmd = case cmd of
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder t::ts => if String.isPrefix "code_"
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |> space_implode " " |> (fn v =>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder else Fail "Unexpected command!"
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |_ => Fail "Expected non-empty command!";
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder val parse_theory_head = e (content "theory") #> p name
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> e (keyword "imports") #> many (p name)
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroeder #> optional (e (keyword "keywords") #>
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroeder many (p str_) #>
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroeder e (keyword "::") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder p name #> pack)
26a00c47de4332eaf1ed218f7bb4df92cc44c53fJonathan von Schroeder #> e (keyword "begin") #> pack #> expect_end;
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val parse_theory_end = e (content "end") #> expect_end;
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder fun parse_local_data a =
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder let val assumes = fn k => e k #>
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder sepBy (e (keyword "and"))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder (optional (p name #> e (keyword ":"))
11215d71075e01a34e70e0499503aac1ce4b8954Jonathan von Schroeder #> p str_ #> pack)
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder val fixes = e (keyword "fixes") #>
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder sepBy (e (keyword "and"))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder (many (p name) #> e (keyword "::")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> oneOf [p name,
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder p type_ident] #> pack)
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder in optional (many (assumes a)) #> optional (many fixes)
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder #> optional (many (assumes a)) (* a = keyword "assumes" *)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder >> (fn (((v,a),f),a1) =>
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder (v,mkLocalData (List.concat (the_default [] a @
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder the_default [] a1))
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder (List.concat (the_default [] f)))) end
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder val parse_mixfix = fn p_ =>
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder let val s2i = raw_explode #> read_int #> #1
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder val prio = fn s2i => p str_ >>> s2i
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder val prios = optional (many (prio s2i))
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder in oneOf [p_,p str_ #> prios #> optional (prio s2i) #>
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder expect_end #> pack #> pack >>>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder (fn (t,(ps,p)) => Template
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder {template=t,prios=ps,def_prio=p}),
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder e (content "infix") #> p str_ #> prio s2i
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder #> pack >>> Infix,
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder e (content "infixl") #> p str_ #> prio s2i
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder #> pack >>> InfixL,
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder e (content "infixr") #> p str_ #> prio s2i
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder #> pack >>> InfixR,
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder e (content "binder") #> p str_ #> prios
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder #> prio s2i #> pack #> pack >>>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder (fn (t,(ps,p)) => Binder
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder {template=t,prios=ps,def_prio=p})] end;
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder fun parse_body_elem _ =
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder let val dt_type = e (content "datatype")
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> sepBy (e (keyword "and"))
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder (oneOf [e (keyword "(") #>
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder sepBy (e (keyword ","))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (p type_ident) #>
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder e (keyword ")"),
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder many (p type_ident), return []]
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> p name #> e (keyword "=")
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> sepBy (e (keyword "|"))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder (p name #> many (p name) #> pack)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> pack #> pack)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder #> expect_end >>> DataType
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val consts = e (content "consts") #> many (
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder p name #> e (keyword "::") #> p str_ #> pack)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder #> expect_end >>> Consts
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder val axioms = e (content "axioms") #> many ((p name)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> e (keyword ":") #> (p str_) #> pack)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder #> expect_end >>> Axioms
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder val cls = e (content "class") #> p name
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> succeed (keyword "=")
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> sepBy (e (keyword "+"))
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> succeed (keyword "+")
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder #> parse_local_data (keyword "assumes")
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder >> (fn (((v,n),ps),l) =>
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder (v,Class { name = n,parents = ps,
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder local_data = l}))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder val locale = e (content "locale") #> p name
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> succeed (keyword "=")
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> sepBy (e (keyword "+"))
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> succeed (keyword "+")
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder #> parse_local_data (keyword "assumes")
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder >> (fn (((v,n),ps),l) =>
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder (v,Locale { name = n,parents = ps,
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder local_data = l}))
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val tp_synonym = e (content "type_synonym")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> oneOf [p type_ident >>> (fn v => [v]),
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder e (keyword "(")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> many (p type_ident)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> e (keyword ")"), return []]
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> p name #> e (keyword "=")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> p str_ #> pack #> pack >>> TypeSynonym
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder val fun_ = e (content "fun") #> p name
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> e (keyword "::") #> p str_
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> e (keyword "where")
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> sepBy (e (keyword "|"))
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder >> (fn (((v,n),t),def) =>
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder (v,Function { name = n, tp = t,
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder def_eqs = def }))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val primrec = e (content "primrec")
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> sepBy (e (keyword "and"))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder (p name #> optional (e (keyword "::") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder p str_) #> pack)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> e (keyword "where")
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder #> sepBy (e (keyword "|")) (p str_)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder >> (fn ((v,ns),def) =>
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder (v,PrimRec { names = ns, def_eqs = def }))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder (* see HOL/Quickcheck.thy line 136 for an example with
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder : instead of where *)
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val def = e (content "definition")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> optional (e (keyword "(") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder e (keyword "in") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder e (keyword ")"))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> optional (e (keyword "[") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder many (p name) #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder e (keyword "]"))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> optional (p name
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> optional (e (keyword "::")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> p str_) #> pack)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> succeed (keyword "where")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> succeed (keyword ":")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> p str_ #> pack #> pack #> pack >>>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder (fn (t,(a,(n,e))) => Definition {
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder name_tp=n,eq=e,target=t,attrs=a})
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder val notation = (oneOf [p (content "notation"),
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder p (content "no_notation")])
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder #> optional (e (keyword "(")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> many (p name)
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder #> e (keyword ")"))
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder #> sepBy (e (keyword "and"))
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder parse_mixfix fail #> pack)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> pack #> pack >>> (fn (n,(m,ns)) =>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder if n = "notation"
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder then Notation {modes=m,notations=ns}
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder else NoNotation {modes=m,notations=ns})
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder in oneOf [dt_type,consts,axioms,cls,
f5bd703382ad26d86ba0ad390d82a4a3e81aba74Jonathan von Schroeder tp_synonym,fun_,primrec,locale,def,notation] end;
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder fun parse_thm s = e (content s)
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder e (keyword "(") #> e (keyword "in")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> p name #> e (keyword ")"))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> optional (p name)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> optional (e (keyword "[") #> many (p name)
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder #> e (keyword "]"))
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder #> e (keyword ":")
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder #> optional (parse_local_data (keyword "assumes")
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder #> e (keyword "shows"))
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder #> (p str_) #> pack #> pack #> pack #> pack;
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von Schroeder fun proof_qed i l cmd = case cmd of
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von Schroeder t::_ => let val l' = cmd::l
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von Schroeder val i' = case Token.content_of t of
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von Schroeder |"proof" => i+1
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von Schroeder in if i' = 0 then List.rev l' |> Result
b48dcb6f74075d06b770ac905ff25f0c592e2258Jonathan von Schroeder else More (proof_qed i' l') end
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |_ => Fail "Expected non-empty command!";
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder fun proof_prefix l cmd = case cmd of
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von Schroeder t::_ => if List.exists (Token.content_of t |>
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder ["apply","using","unfolding"]
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder then cmd::l |> proof_prefix |> More
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder else cmd::l |> End
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von Schroeder |_ => Fail "Expected non-empty command!";
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder fun cmdList2string cmds = List.map (List.map Token.unparse) cmds
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> List.map (space_implode " ")
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder exception Test of string;
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder fun proof p_ = succeedP p_ #> p (proof_prefix []) #> p (fn cmd =>
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder t::_ => let val res = case Token.content_of t of
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder "proof" => More (proof_qed 1 [cmd])
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder |"oops" => Result [cmd]
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder |"by" => Result [cmd]
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder |".." => Result [cmd]
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder |"." => Result [cmd]
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder |"done" => Result [cmd]
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder |_ => raise (Test (Token.unparse t))
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder |_ => Fail "Expected non-empty command!") #> pack
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder >>> (fn (cmds,cmds1) => cmds@cmds1 |>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder cmdList2string);
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder fun parse_qualifier default = optional (oneOf [p (keyword "?"),
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder p (keyword "!")])
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder >>> (fn v1 => case v1 of
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder SOME "?" => Optional
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder |SOME "!" => Mandatory
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder |_ => default);
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder val parse_arity = fn _ => optional (e (keyword "(") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder sepBy (e (keyword ","))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder e (keyword ")")) #> (p name) #> pack
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder fun parse_theory_body p1 p2 = [parse_body_elem p1 |> liftP,
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder (parse_thm "lemma" |> liftP) #> (proof p2)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder (fn ((t,(n,(a,(l,stmt)))),prf) =>
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder statement=stmt,
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von Schroeder local_data=the_default
e2f6183cac38aa0c12ebb42f526d92749fba6b43Jonathan von Schroeder emptyLocalData l,
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder (parse_thm "theorem" |> liftP) #> (proof p2)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder (fn ((t,(n,(a,(l,stmt)))),prf) =>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder Theorem {name=n,
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder statement=stmt,
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder local_data=the_default
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder emptyLocalData l,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder ((e (content "instance")) #> optional (
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder oneOf [sepBy (e (keyword "and"))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder e (keyword "::") #> parse_arity fail
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> pack >>> InstanceA,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder oneOf [p (keyword "<"),
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder p (keyword "\<subseteq>")]
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> pack #> pack >>>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder (fn (n,(r,p)) => InstanceR {
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder name=n,rel=r,parent=p})])
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |> liftP) #> proof fail #> pack
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder ((e (content "interpretation") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder p name #> parse_qualifier Mandatory #>
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder e (keyword ":") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder p name #> many (p str_)
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder #> pack #> pack #> pack)
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder |> liftP) #> proof fail #> pack
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder >>> (fn ((n,(q,e)),prf) =>
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder Interpretation {name=n,
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder ((e (content "axiomatization") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder sepBy (e (keyword "and"))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder (many (p name) #> e (keyword "::")
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> p str_ #> optional (parse_mixfix fail)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> pack #> pack)) |> liftP)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder >>> (List.map (fn (ns,(t,m)) =>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder {names=ns,tp=t,mixfix_data=m})
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> Axiomatization),
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder ((p (fn t => if String.isPrefix "hide_"
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder else failT "Unexpected Token!" t)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> optional (e (keyword "(") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder p (keyword "open") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder e (keyword ")")) #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder many (p name) #> pack #> pack) |> liftP)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder >>> (fn (s,(opt,ns)) =>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder Hide {what=case opt of
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder SOME _ => (s,HideLocal)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder |NONE => (s,HideAll),
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder p (unparse_cmd "abbreviation") >>>
3467ccbc8c4b69ead06a6b4c7516c666f9b0618eJonathan von Schroeder p (unparse_cmd "declaration") >>>
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder p (unparse_cmd "text") >>>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder (fn v => MiscCmd ("text",v)),
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder p (unparse_cmd "section") >>>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder (fn v => MiscCmd ("section",v)),
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder p (unparse_cmd "subsection") >>>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder (fn v => MiscCmd ("subsection",v)),
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder p (unparse_cmd "value") >>>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder (fn v => MiscCmd ("value",v)),
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder p (unparse_cmd "unused_thms") >>>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder (fn v => MiscCmd ("unused_thms",v)),
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder p (unparse_cmd "ML_file") >>>
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder (fn v => MiscCmd ("ML_file",v)),
f0051190a4466db48632aa2137e50a14a434caa2Jonathan von Schroeder p (unparse_cmd "setup") >>>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder (fn v => MiscCmd ("setup",v)),
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder p unparse_code_cmd >>> CodeCmd];
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder val parse_context = ((e (content "context") #> p name #>
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder e (keyword "begin")) |> liftP)
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder #> many (oneOf (parse_theory_body fail fail))
39ff2c70fb322676a393422acea71fa49b3ac4cdJonathan von Schroeder #> ((e (content "end") #> expect_end) |> liftP)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder #> pack >>> Context;
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder val parse_instantiation = ((e (content "instantiation") #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder sepBy (e (keyword "and")) (p name) #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder e (keyword "::") #> parse_arity fail #>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder e (keyword "begin")) |> liftP)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> many (oneOf (parse_theory_body fail fail))
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> ((e (content "end") #> expect_end) |> liftP)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> pack #> pack >>> (fn (ns,(a,b)) =>
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder Instantiation { names=ns,arity=a,body=b })
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder val test = initialState #> optional (p (unparse_cmd "header"))
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder #> (parse_theory_head |> liftP)
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder #> many (oneOf (parse_context::parse_instantiation::
da97cb224435c57d2e1acdbff1ba2727aef8c46cJonathan von Schroeder parse_theory_body fail fail))
a7a2cb9f6c10d948f32c2f8c4ef130f5e562a5c6Jonathan von Schroeder #> (parse_theory_end |> liftP)
5ae58979133bc1f8c1d9e400b95fb24d5007b18dJonathan von Schroeder #> expect_end >> (fn ((((_,h),n),(i,k)),b) =>
5dcd4b1e4a14c450b981acc5a4895efaaa667b93Jonathan von Schroeder ParsedTheory {header = h,
9c1fa7e08c15b47b33a070e87fc057f2e49b9270Jonathan von Schroeder #> (fn v => (v >>= I,getError v));
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroedersignature ExportHelper =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder type named_term = (string * term)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* general helper functions *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val unlines : string list -> string
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val unqualify : string -> string
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* isabelle specific functions *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val theory_of_string : string -> theory list -> theory
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val theory_by_name : string -> theory
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val name_of_theory : theory -> string
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms_of : theory -> named_term list
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val non_image_theories : theory -> theory list
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val thms_of : theory -> named_term list
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val consts_of : theory -> (string * typ) list
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val datatypes_of : theory -> ((string * typ list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ list) list) list) list
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* mutually_rec_types@(name * type_params *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder constructors@(constructor_name * type_args))) *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val functions_of : theory -> (string * typ *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (term list * term) list) list
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* name * type *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder def_eqs@(pats * defterm) *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes_of : theory -> (class * string list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * term) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list) list
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* name * parents * assumes * fixes *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales_of : theory -> (string *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((string * typ) * mixfix) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder named_term list * named_term list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder string list) list
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* name * fixes * in-locale axioms *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ex-locale axioms * parents *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val pretty_as_str : Pretty.T -> string
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_term : theory -> term -> Pretty.T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_typ : theory -> typ -> Pretty.T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_name : string -> Pretty.T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_function : theory -> (string * typ *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (term list * term) list) -> Pretty.T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_class : theory -> (class * string list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * term) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list) -> Pretty.T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_locale : theory -> (string *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((string * typ) * mixfix) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder named_term list * named_term list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val repr_datatype : theory -> (string * typ list * (string *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder typ list) list) list -> Pretty.T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val theory_of_exportable_data : theory -> theory
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val get_basic_theory_data : theory -> (named_term list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder named_term list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* axioms * theorems * consts *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder type theory_data = (string * named_term list * named_term list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list * ((string * typ list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ list) list) list) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ * (term list * term) list) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (class * string list * (string * term) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * ((string * typ) * mixfix) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder named_term list * named_term list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder string list) list)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* name * axioms * theorems * consts * datatypes *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder functions * classes * locales *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val get_theories : theory -> theory_data list
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val xml_of_theories : theory_data list -> XML.tree
97dc615bc3ce381eaa3e75cc23dfc3c4b566d9a0Jonathan von Schroeder exception ExportError of string
067b7cf571968fe8e91212059da1590c2dfa741aJonathan von Schroederstructure ExportHelper : ExportHelper =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederexception ExportError of string
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedertype named_term = string * term
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroedertype theory_data = (string * named_term list * named_term list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list * ((string * typ list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ list) list) list) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ * (term list * term) list) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (class * string list * (string * term) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * typ) list) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (string * ((string * typ) * mixfix) list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder named_term list * named_term list *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder string list) list)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* name * axioms * theorems * consts * datatypes *
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder functions * classes * locales *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* ------------------------------ General helper functions *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval unlines = String.concatWith (String.str (Char.chr 10))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun lift f sel = fn (t1,t2) => f (sel t1,sel t2)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun unqualify n = if Long_Name.is_qualified n
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then (Long_Name.implode (List.tl (Long_Name.explode n)))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* ------------------------------ Isabelle specific functions *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* Keep track of the number of theories created from a string *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* create a theory from a string of its body *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun theory_of_string body parents =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val name = "TempTheory"^Int.toString (Unsynchronized.inc thmNum)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val header = Thy_Header.make ("TempTheory",Position.none) [] [] []
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val text = unlines ["theory "^name,"begin",body,"end"]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in #1 (Thy_Load.load_thy 0 (Thy_Load.get_master_path ()) header
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Position.start text parents) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun remove_hol_true_prop t = case t of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder op$ (Const ("HOL.Trueprop",_), tm) => tm
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | (t $ u) => (remove_hol_true_prop t) $ (remove_hol_true_prop u)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | Abs (s,T,t) => Abs (s,T,remove_hol_true_prop t)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval prettify_term = Logic.strip_imp_concl o remove_hol_true_prop
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* remove data that is already present in a parent theory *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun remove_parent_data df cmp T =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val d = df T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val pd = (List.foldl op@ [] (List.map df (Context.parents_of T)))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in Ord_List.subtract cmp (Ord_List.make cmp pd) (Ord_List.make cmp d) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* a couple of aliases *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval theory_by_name = Thy_Info.get_theory
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval name_of_theory = Context.theory_name
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* check if the theory is not part of the logic image *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun is_non_image_theory T = length (Thy_Info.loaded_files (name_of_theory T)) > 0
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun non_image_theories T = List.concat (List.map
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn T' => if is_non_image_theory T'
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then T'::(non_image_theories T') else [])
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun hol_forall_elim tm =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val qnt = #1 (Term.dest_Const (HOLogic.all_const HOLogic.boolT))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val body = Term.strip_qnt_body qnt tm
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val vars = List.map (fn (s,tp) => Var ((s,0),tp))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in Term.subst_bounds (List.rev vars, body) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun hol_conjunctions tm = case HOLogic.dest_conj tm of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | tms => List.concat (List.map hol_conjunctions tms)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun thms_of T = List.map (fn (s,d) => (s,prop_of d))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (remove_parent_data Global_Theory.all_thms_of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (lift fast_string_ord #1) T)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* currently there seems to be no way (anymore) to
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder attach any terms to a const directly. Thus the discarded
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder part is (hopefully) always NONE
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder todo: maybe throw an exception if this is not the case? *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun consts_of T =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val get_consts = fn T => List.map (fn (n,(t,_)) => (n,t))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (((Name_Space.dest_table (Syntax.init_pretty_global T)) o
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder #constants o Consts.dest o Sign.consts_of) T)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in remove_parent_data get_consts (lift fast_string_ord #1) T end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun datatypes_of T =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val get_datatypes = (#log_types o Type.rep_tsig o Sign.tsig_of)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val ts = remove_parent_data get_datatypes fast_string_ord T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val is_mutually_rec_type = fn (_,i) => length (#descr i) >1
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val check_rec = fn (n,v) => if is_mutually_rec_type (n,v)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then (#index v) < 1 else true
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val rec dtyp2typ = fn (descs,t) => case t of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Datatype.DtTFree (s,srt) => TFree (s,srt)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Type (s,List.map (curry dtyp2typ descs) ts)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder case List.find (curry op= i o #1) descs of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME (_,(s,ts,_)) => Type (s, List.map
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (curry dtyp2typ descs) ts)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | NONE => raise ExportError("Internal Error!")
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroeder val dt_desc = fn info => List.map (fn (_,(s,vs,eqs)) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val vs' = List.map (curry dtyp2typ info) vs
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val eqs' = List.map (fn (s,ts) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (s,List.map (curry dtyp2typ info) ts)) eqs
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (s,vs',eqs') end) info
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in List.foldl (fn (n,l) => case Datatype.get_info T n of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME(v) => if check_rec (n,v)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then (dt_desc (#descr v))::l
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | NONE => l) [] ts end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederval functions_of =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val get_funs = fn T =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val d = Item_Net.content (Function_Common.get_function
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val fun_def = (fn (pats,def) => (#2 (strip_comb pats),def))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder o HOLogic.dest_eq o HOLogic.dest_Trueprop o #2
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in List.map (fn (c,i) => case dest_Const c of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (n,t) => (n,t,List.map fun_def (#psimps i))) d end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in remove_parent_data get_funs (lift fast_string_ord #1) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun classes_of T =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val cls_suffix = "_class_def"
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val thms = thms_of T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val cls_names = List.map (fn n => String.substring (n,0,String.size n-
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder String.size cls_suffix)) (List.filter (String.isSuffix cls_suffix)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val i = AxClass.get_info T name
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn tm => Term.add_const_names tm [])
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder o Logic.dest_equals o Thm.prop_of o #def) i))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val parents = List.map (fn n => String.substring
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (n,0,String.size n - String.size "_class"))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.filter (fn n => (String.isSuffix "_class" n) andalso
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (not (String.isPrefix "HOL" n))) parents')
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms' = List.map (fn (n,t) => (n,(HOLogic.dest_Trueprop o #2
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.filter ((String.isPrefix (name^".")) o #1) thms)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (* note: instead of cls_names we should only use
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ancestors of the class *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val all_params = List.map (fn (s,t) => (Long_Name.base_name s,t))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.concat (List.map (#params o AxClass.get_info T) cls_names))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val sub_vars = List.map (fn (s,t) => ((s,0),Free (s,t))) all_params
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms = List.map (fn (s,t) => (s,Term.subst_Vars sub_vars t))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (name,parents,axioms,#params i) end) cls_names end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun locales_of T =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val all_locales = fn T => List.map (fn l => (#name l, #parents l))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn (c,l) => fast_string_ord (#1 c,#1 l))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord #1)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (classes_of T))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord #1)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (remove_parent_data all_locales
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (lift fast_string_ord #1) T))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in List.map (fn (name,ps) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val parent_params = List.map (#1 o #1) (List.concat
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.filter (fn (s,_) => List.exists (curry op= s) ps) locales)))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val params = Ord_List.subtract (fn (s,((s1,_),_)) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder fast_string_ord (s,s1))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make fast_string_ord parent_params)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord (#1 o #1))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val filter = ["_axioms.intro","_axioms_def","_def",".intro",".axioms_"]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axs = List.filter ((String.isPrefix name) o #1)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn s => String.isPrefix (name ^ s) (#1 t))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms = List.map (fn (s,t) => (s,(HOLogic.dest_Trueprop o #2
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val fix_consts = List.map (fn (s,t) => (s, Term.subst_Vars
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (fn ((s,tp),_) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((s,0),Const (s,tp))) params) t))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val parse_axioms = fn v => List.map hol_forall_elim
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((hol_conjunctions o #2 o Logic.dest_equals o Thm.prop_of o #2) v)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val in_locale_axioms =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder case List.find ((curry op= (name^"_axioms_def")) o #1) axs of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME v => parse_axioms v
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder case List.find ((curry op= (name^"_def")) o #1) axs of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME v => parse_axioms v
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val in_loc = List.filter (fn (_,t) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder List.exists (fn t' => t = t') in_locale_axioms) axioms
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val ex_loc = List.filter (fn (_,t) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder not (List.exists (fn t' => t = t') in_locale_axioms)) axioms
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (name,params,fix_consts in_loc,fix_consts ex_loc,ps) end) locales end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* ------------------------------ Represent as string *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun pretty_as_str p = Pretty.str_of p
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_term T =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val ctxt = Config.put Printer.show_question_marks false
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_typ T = Syntax.pretty_typ (Proof_Context.init_global T)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_name n' =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in if String.isSubstring " " n then Pretty.quote (Pretty.str n)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_function T (s,tp,def_eqs) =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val head = [Pretty.str "fun ", repr_name s, Pretty.str " :: ",
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.quote (repr_typ T tp), Pretty.str " where "]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val body = List.map (fn (pats,tm) => Pretty.quote (Pretty.block
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (fn p => Pretty.enclose "(" ")" [repr_term T p])
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [Pretty.str " = ",repr_term T tm]))) def_eqs
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in Pretty.block (head@Pretty.separate " | " body) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_class T (s,ps,assumes,fixes) =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val head = [Pretty.str "class", repr_name s]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(if length fixes + length assumes + length ps > 0
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "="] else [])
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val parents = List.map repr_name ps
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val fixes' = List.map (fn (s,tp) => Pretty.block (Pretty.breaks
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [repr_name s,Pretty.str "::",
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.quote (repr_typ T tp)])) fixes
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val assumes' = List.map (fn (s,tm) => Pretty.block (Pretty.breaks
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [repr_name s, Pretty.str ":",
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.quote (repr_term T tm)])) assumes
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (Pretty.block o Pretty.breaks) (head@(Pretty.separate "+" parents)@
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length (fixes'@assumes') > 0 andalso length parents > 0
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "+"] else [])@
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length fixes' > 0
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "fixes"]@(Pretty.separate "and" fixes') else [])@
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length assumes' > 0
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "assumes"]@(Pretty.separate "and" assumes') else [])) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_locale T (s,fixes,in_loc,_,ps) =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val head = [Pretty.str "locale", repr_name s]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(if length fixes + length in_loc + length ps > 0
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "="] else [])
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val parents = List.map repr_name ps
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val fixes' = List.map (fn ((s,tp),_) => Pretty.block (Pretty.breaks
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.quote (repr_typ T tp)])) fixes
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val assumes' = List.map (fn (s,tm) => Pretty.block (Pretty.breaks
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [repr_name s, Pretty.str ":",
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder Pretty.quote (repr_term T tm)])) in_loc
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (Pretty.block o Pretty.breaks) (head@(Pretty.separate "+" parents)@
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length (fixes'@assumes') > 0 andalso length parents > 0
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "+"] else [])@
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length fixes' > 0
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "fixes"]@(Pretty.separate "and" fixes') else [])@
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (if length assumes' > 0
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then [Pretty.str "assumes"]@(Pretty.separate "and" assumes') else [])) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun repr_datatype T d =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val dts = List.map (fn (s,vs,eqs) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val vs' = Pretty.enclose "(" ")"
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Pretty.separate "," (List.map (repr_typ T) vs))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val eqs' = Pretty.separate "|" (List.map
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn (s,vs) => Pretty.block (Pretty.breaks
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ([repr_name s]@
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (Pretty.quote o repr_typ T) vs)))) eqs)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ([vs']@[repr_name s,Pretty.str "="]@eqs')) end) d
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (Pretty.block o Pretty.breaks) ([Pretty.str "datatype"]@
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun theory_of_exportable_data T =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val datatypes = datatypes_of T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val functions = functions_of T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes_Graph = String_Graph.make
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (fn l => ((#1 l,l),#2 l)) (classes_of T))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes_sorted =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder List.rev (String_Graph.topological_order classes_Graph)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (#1 o #2 o (String_Graph.get_entry classes_Graph))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales_Graph = String_Graph.make
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (fn l => ((#1 l,l),#5 l)) (locales_of T))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales_sorted =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder List.rev (String_Graph.topological_order locales_Graph)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (#1 o #2 o (String_Graph.get_entry locales_Graph))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in theory_of_string (unlines (List.map pretty_as_str
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ((List.map (repr_datatype T) datatypes)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (repr_function T) functions)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (repr_class T) classes)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(List.map (repr_locale T) locales)))) (Context.parents_of T) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun get_basic_theory_data T =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val T' = theory_of_exportable_data T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val cmp = (fn (s,(s1,_)) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (lift fast_string_ord unqualify) (s,s1))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make fast_string_ord (List.map #1 (axioms_of T')))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord #1) (axioms_of T))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make fast_string_ord (List.map #1 ((thms_of T')@axs)))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord #1) (thms_of T))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make fast_string_ord (List.map #1 (consts_of T')))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (Ord_List.make (lift fast_string_ord #1) (consts_of T))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (axs, thms, consts) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun get_theories T =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val Ts = T::(non_image_theories T)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val name = name_of_theory T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val (axs,thms,consts) = get_basic_theory_data T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val datatypes = datatypes_of T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val functions = functions_of T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes = classes_of T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales = locales_of T
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in (name,axs,thms,consts,datatypes,functions,
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder classes,locales) end) Ts end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* Generate XML Output *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederstructure XML_Syntax = Legacy_XML_Syntax
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun fixTypeNames moduleName t = case t of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Type",a),c) => XML.Elem (("Type",
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder if n = "name" andalso String.isPrefix (moduleName^".") s
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder then (n,String.extract (s,(String.size moduleName)+1,NONE))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder else (n,s)) a),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder List.map (fixTypeNames moduleName) c)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (d,List.map (fixTypeNames moduleName) c)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder(* Enrich the (isabelle-builtin) XML representation of terms with infix information *)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun mixfix_to_args m = case m of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME(Mixfix.Infixl (s,j)) => [("infixl",s), ("mixfix_i",string_of_int j)]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | SOME(Mixfix.Infixr (s,j)) => [("infixr",s), ("mixfix_i",string_of_int j)]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | SOME(Mixfix.Infix (s,j)) => [("infix",s), ("mixifix_i",string_of_int j)]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_term' T tbl t = case t of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Const",a),t) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val b = case (Syntax.guess_infix (Sign.syn_of T)
8c38757c50d7e8f76897f7e88097a2d3acc118a0Jonathan von Schroeder (Lexicon.mark_const ((#2 o List.hd) a))) of
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder SOME(mx) => mixfix_to_args (SOME mx)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | NONE => mixfix_to_args (Symtab.lookup tbl ((#2 o List.hd) a))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in XML.Elem (("Const",a@b),map (xml_of_term' T tbl) t) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder | XML.Elem ((s,a),t) => XML.Elem ((s,a),map (xml_of_term' T tbl) t)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_term T t = xml_of_term' T Symtab.empty
1b814cc172570ad1eff000a2b9c7bf638371aa59Jonathan von Schroederfun xml_of_datatype _ eqs = XML.Elem (("RecDatatypes",[]),List.map
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn (name,type_params,constructors) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Datatype",[("name",Long_Name.base_name name)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map XML_Syntax.xml_of_type type_params)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (("Constructor",[("name",Long_Name.base_name s)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder List.map XML_Syntax.xml_of_type tps))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder constructors))) eqs)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_function T (name,tp,def_eqs) =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Function",[("name",Long_Name.base_name name)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder ::(List.map(fn (pats,tm) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Equations",[]),List.map (xml_of_term T)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (pats@[tm]))) def_eqs))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_class T (name,parents,assumps,fixes) =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("ClassDef",[("name",Long_Name.base_name name)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Parent",[("name",Long_Name.base_name p)]),[])) parents)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Assumption",[("name",Long_Name.base_name s)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [xml_of_term T t])) assumps)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("ClassParam",[("name",Long_Name.base_name s)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_locale T (name,fixes,assumps,thms,parents) =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Locale",[("name",Long_Name.base_name name)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (List.map (fn ((s,t),m) =>
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("LocaleParam",[("name",Long_Name.base_name s)]
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @(mixfix_to_args (SOME m))),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Assumption",[("name",Long_Name.base_name s)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [xml_of_term T t])) assumps)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Theorem",[("name",Long_Name.base_name s)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [xml_of_term T t])) thms)
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("Parent",[("name",Long_Name.base_name p)]),[])) parents))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_theory (name, axs, thms, cs, dts, fns, cls, locales) =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder let val T = theory_by_name name
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (fn T => XML.Elem (("Import",[("name",name_of_theory T)]),[]))
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val axioms = List.map (fn (n,t) => XML.Elem
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (("Axiom",[("name",Long_Name.base_name n)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [(xml_of_term T o prettify_term) t])) axs
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val theorems = List.map (fn (n,t) => XML.Elem
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (("Theorem",[("name",Long_Name.base_name n)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder [(xml_of_term T o prettify_term) t])) thms
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val consts = List.map (fn (n,tp) => XML.Elem
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder (("Const",[("name",Long_Name.base_name n)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val datatypes = List.map (xml_of_datatype T) dts
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val functions = List.map (xml_of_function T) fns
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val classes = List.map (xml_of_class T) cls
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val locales' = List.map (xml_of_locale T) locales
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder in fixTypeNames name (XML.Elem (("IsaTheory",[("name",name)]),
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder imports@axioms@theorems@consts@datatypes
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder @functions@classes@locales')) end
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_theories theories =
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder XML.Elem (("IsaExport",[]),List.map xml_of_theory theories)