export_helper.ml revision 045eb445945abe778eba4f86c806e6b20e957957
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroedersignature ParserHelper =
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val scan : string -> cmd list
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder type theory_body_elem
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder type parsed_theory
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val test : cmd list -> string (*parsed_theory*)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroederstructure ParserHelper : ParserHelper =
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun partition f l = #2 (List.foldr
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (fn (x,(l1,l2)) => if (f x) then ([],(x::l1)::l2)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else (x::l1,l2)) ([],[]) l);
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun scan str = str |> Source.of_string |> Symbol.source
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> Token.source {do_recover = SOME false}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> Token.source_proper |> Source.exhaust
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder datatype theory_body_elem = DataType of (string list * (string *
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (string * string list) list)) list
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |Consts of (string * string) list
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |Axioms of (string * string) list
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |Lemma of {name: string,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder statement: string,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |Class of {name:string,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder parents:string list,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder assumes:(string*string) list,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fixes:(string list*string) list}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |Locale of {name:string,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder parents:string list,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder assumes:(string*string) list,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fixes:(string list*string) list}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |TypeSynonym of string * string
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |Function of {name: string,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder def_eqs: string list}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |PrimRec of {names: (string*string) list,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder def_eqs: string list}
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |Definition of string * (string*string);
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder datatype parsed_theory = ParsedTheory of {
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder imports: string list,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder body: theory_body_elem list
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val empty_theory = ParsedTheory {
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder datatype ('a,'b) p = State of ('a list) * 'b
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder | Failed of string;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun valP (State (_,v)) = v;
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;
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)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun expect_end (Failed s) = Failed s
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder | expect_end (State ([],v)) = State ([],v)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder | expect_end (State (v,_)) = Failed "Expected end!";
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (* val p : ('a -> ('a,'c) r) -> ('a,'b) p -> ('a,('b,'c)) p;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder 'parsers' can be combined using #> and
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder applied in 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!";
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun p2r (State (_,v)) = Result v
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |p2r (Failed s) = Fail s;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder infix 1 >> >>> >>=;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (* modify result value *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun (State (d,v)) >> f = State (d,f v)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(Failed s) >> _ = Failed s;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun (f >>> g) x = x |> f >> g;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (* get result value and apply f to it *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun (State (d,v)) >>= f = SOME (f v)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(Failed _) >>= _ = NONE
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun getError (State (d,v)) = ""
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |getError (Failed s) = s;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun return v1 (State (d,v)) = State (d,(v,v1))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |return _ (Failed s) = Failed s;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder exception Test of string;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun pack (State (d,((v,v1),v2))) = State (d,(v,(v1,v2)))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |pack (Failed s) = Failed s;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun failT s t = Fail (s^" at "^Token.pos_of t);
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (* create a parser discarding the result of f *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun e f s = p f s >> #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
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |State (ds,(v,v1)) => State (ds,v);
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)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |Failed s => (ds,[])
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder in State (ds',(v,v1::vs)) end
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(Failed s,State (ds,v)) => State (ds,(v,[]))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(_,Failed s) => Failed s;
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;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (* if p and p1 are parsers then `optional (p #> p1)`
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder is the optional version of `p |> p1` *)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun optional p (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)));
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun oneOf ps s = List.foldl (fn (p,s') => case s' of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder Failed _ => p s
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (Failed "No parser supplied") ps
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun content s t = if Token.content_of t = s then Result true
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else failT ("Expected content '"^s^"' but found "^
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder "content '"^Token.content_of t^"'") t;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun ident p t = if Token.ident_with p t
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else failT "Not a valid identifier!" t;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun type_ident t = if Token.kind_of t = Token.TypeIdent
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else failT "Not a TypeIdent!" t;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun str_ t = if Token.kind_of t = Token.String
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else failT "Not a String!" t;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun keyword p t = if Token.keyword_with p t
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else failT "Not a valid keyword!" t;
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun parse_theory_head cmd = State (cmd,"") |> e (content "theory")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> p (ident (K true)) >> #2
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> e (keyword (curry op= "imports"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> many (p (ident (K true)))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> e (keyword (curry op= "begin"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun parse_theory_end cmd = State (cmd,"") |> e (content "end")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun parse_body_elem cmd =
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder let val dt_type = e (content "datatype")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> sepBy (e (keyword (curry op="and")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (oneOf [e (keyword (curry op= "(")) #>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder sepBy (e (keyword (curry op= ",")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (p type_ident) #>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder e (keyword (curry op= ")")),
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder many (p type_ident), return []]
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= "="))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> sepBy (e (keyword (curry op="|")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (oneOf [p (ident (K true)),
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder [p (ident (K true)),
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder p str_]) #> pack)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> pack #> pack)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> expect_end >>> DataType o #2
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val consts = e (content "consts")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> many (p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= "::"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> (p str_) #> pack) #> expect_end
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder >>> Consts o #2
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val axioms = e (content "axioms")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> many (p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= ":"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> (p str_) #> pack) #> expect_end
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder >>> Axioms o #2
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val cls_assumes = e (keyword (curry op= "assumes"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (e (keyword (curry op= "and")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= ":"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p str_ #> pack)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val cls_assumes1 = e (keyword (curry op= "assumes"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (e (keyword (curry op= "and")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= ":"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p str_ #> pack)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val cls_fixes = e (keyword (curry op= "fixes"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (e (keyword (curry op= "and")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (many (p (ident (K true)))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= "::"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p str_ #> pack)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val cls = e (content "class")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> succeed (keyword (curry op= "="))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> sepBy (e (keyword (curry op= "+")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (p (ident (K true)))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> succeed (keyword (curry op= "+"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> optional cls_assumes #> optional cls_fixes
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> optional cls_assumes1
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder >>> (fn (((((_,n),ps),a),f),a1) =>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder Class { name = n,parents = ps,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder assumes = case (a,a1) of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (SOME v,SOME v1) => v@v1
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(SOME v,NONE) => v
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(NONE,SOME v) => v
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(NONE,NONE) => [],
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fixes = case f of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val locale = e (content "locale")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> succeed (keyword (curry op= "="))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> sepBy (e (keyword (curry op= "+")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (p (ident (K true)))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> succeed (keyword (curry op= "+"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> optional cls_assumes #> optional cls_fixes
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> optional cls_assumes1
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder >>> (fn (((((_,n),ps),a),f),a1) =>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder Locale { name = n,parents = ps,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder assumes = case (a,a1) of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (SOME v,SOME v1) => v@v1
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(SOME v,NONE) => v
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(NONE,SOME v) => v
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |(NONE,NONE) => [],
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fixes = case f of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val tp_synonym = e (content "type_synonym")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= "="))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p str_ #> pack >>> TypeSynonym o #2
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val fun_ = e (content "fun")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= "::"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p str_ #> e (keyword (curry op= "where"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> sepBy (e (keyword (curry op= "|")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder >>> (fn (((_,n),t),def) =>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder Function { name = n, tp = t,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder def_eqs = def })
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val primrec = e (content "primrec")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> sepBy (e (keyword (curry op= "and")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (p (ident (K true)) #>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder e (keyword (curry op= "::")) #>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder p str_ #> pack)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= "where"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> sepBy (e (keyword (curry op= "|")))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder >>> (fn ((_,ns),def) =>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder PrimRec { names = ns, def_eqs = def })
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val def = e (content "definition")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= "::"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> e (keyword (curry op= "where"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder #> pack #> pack >>> Definition o #2
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder in State (cmd,"") |> oneOf [dt_type,consts,axioms,cls,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder tp_synonym,fun_,primrec,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun parse_lemma cmd = State (cmd,"") |> e (content "lemma")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> p (ident (K true))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> e (keyword (curry op= ":"))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> (p str_) |> pack >> #2 |> p2r
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun proof_qed l cmd = case cmd of
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder t::ts => if Token.content_of t = "qed"
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder then Result (List.rev (cmd::l))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else More (proof_qed (cmd::l))
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |_ => Fail "Expected non-empty command!";
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun cmdList2string cmds = List.map (List.map Token.unparse) cmds
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> List.map (space_implode " ")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder val proof = oneOf [p (fn cmd =>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder t::ts => if Token.content_of t = "proof"
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder then More (proof_qed [cmd])
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder else Fail "Unexpected command!"
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |_ => Fail "Expected non-empty command!")
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder >>> (fn (v,cmds) => (v,cmdList2string cmds))];
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder fun test cmds = State (cmds,"") |> p (parse_theory_head #> p2r) >> #2
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> many (oneOf [p (parse_body_elem #> p2r),
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder p parse_lemma #> proof #> pack >>>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (fn (v,((n,stmt),prf)) =>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder (v,Lemma {name=n,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder statement=stmt,
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> e (parse_theory_end #> p2r)
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder |> expect_end >> (fn ((n,i),b) =>
045eb445945abe778eba4f86c806e6b20e957957Jonathan von Schroeder ParsedTheory {name = n,
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!")
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroeder val dt_desc = fn info => List.map (fn (i,(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
617719566ec7a718fc4f601c02ca91f21ca6deb6Jonathan von Schroederfun xml_of_datatype T 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)