# HG changeset patch # User wenzelm # Date 1527173774 -7200 # Node ID bb9a3be6952aee2af74d7f318e28f4c3df84ede7 # Parent 61188c781cddb7326825aa92d1310542a066859f more exports; read_session: proper signature; diff -r 61188c781cdd -r bb9a3be6952a src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Thu May 24 09:18:29 2018 +0200 +++ b/src/HOL/Tools/typedef.ML Thu May 24 16:56:14 2018 +0200 @@ -348,4 +348,27 @@ val overloaded = typedef_overloaded; + + +(** theory export **) + +val _ = Export_Theory.setup_presentation (fn _ => fn thy => + let + val parent_spaces = map Sign.type_space (Theory.parents_of thy); + val typedefs = + Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy))) + |> maps (fn (name, _) => + if exists (fn space => Name_Space.declared space name) parent_spaces then [] + else + get_info_global thy name + |> map (fn ({rep_type, abs_type, Rep_name, Abs_name, axiom_name}, _) => + (name, (rep_type, (abs_type, (Rep_name, (Abs_name, axiom_name))))))); + in + if null typedefs then () + else + Export_Theory.export_body thy "typedefs" + let open XML.Encode Term_XML.Encode + in list (pair string (pair typ (pair typ (pair string (pair string string))))) typedefs end + end); + end; diff -r 61188c781cdd -r bb9a3be6952a src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Thu May 24 09:18:29 2018 +0200 +++ b/src/Pure/Thy/export_theory.ML Thu May 24 16:56:14 2018 +0200 @@ -27,6 +27,9 @@ val _ = setup_presentation (fn {adjust_pos, ...} => fn thy => let + val rep_tsig = Type.rep_tsig (Sign.tsig_of thy); + + (* parents *) val parents = Theory.parents_of thy; @@ -76,7 +79,7 @@ val _ = export_entities "types" (K export_type) Sign.type_space - (Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy)))); + (Name_Space.dest_table (#types rep_tsig)); (* consts *) @@ -120,6 +123,24 @@ export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of) (Facts.dest_static true [] (Global_Theory.facts_of thy)); + + (* type classes *) + + val encode_class = + let open XML.Encode Term_XML.Encode + in pair (list (pair string typ)) (list term) end; + + fun export_class name = + (case try (Axclass.get_info thy) name of + NONE => ([], []) + | SOME {params, axioms, ...} => + (params, map (Logic.unvarify_global o Thm.full_prop_of) axioms)) + |> encode_class |> SOME; + + val _ = + export_entities "classes" (fn name => fn () => export_class name) + Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig))))); + in () end); end; diff -r 61188c781cdd -r bb9a3be6952a src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Thu May 24 09:18:29 2018 +0200 +++ b/src/Pure/Thy/export_theory.scala Thu May 24 16:56:14 2018 +0200 @@ -26,14 +26,19 @@ def read_session(store: Sessions.Store, session_name: String, types: Boolean = true, - consts: Boolean = true): Session = + consts: Boolean = true, + axioms: Boolean = true, + facts: Boolean = true, + classes: Boolean = true, + typedefs: Boolean = true): Session = { val thys = using(store.open_database(session_name))(db => { db.transaction { Export.read_theory_names(db, session_name).map((theory_name: String) => - read_theory(db, session_name, theory_name, types = types, consts = consts)) + read_theory(db, session_name, theory_name, types = types, consts = consts, + axioms = axioms, facts = facts, classes = classes, typedefs = typedefs)) } }) @@ -55,18 +60,22 @@ types: List[Type], consts: List[Const], axioms: List[Axiom], - facts: List[Fact]) + facts: List[Fact], + classes: List[Class], + typedefs: List[Typedef]) { override def toString: String = name } - def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil) + def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil) def read_theory(db: SQL.Database, session_name: String, theory_name: String, types: Boolean = true, consts: Boolean = true, axioms: Boolean = true, - facts: Boolean = true): Theory = + facts: Boolean = true, + classes: Boolean = true, + typedefs: Boolean = true): Theory = { val parents = Export.read_entry(db, session_name, theory_name, "theory/parents") match { @@ -79,7 +88,9 @@ if (types) read_types(db, session_name, theory_name) else Nil, if (consts) read_consts(db, session_name, theory_name) else Nil, if (axioms) read_axioms(db, session_name, theory_name) else Nil, - if (facts) read_facts(db, session_name, theory_name) else Nil) + if (facts) read_facts(db, session_name, theory_name) else Nil, + if (classes) read_classes(db, session_name, theory_name) else Nil, + if (typedefs) read_typedefs(db, session_name, theory_name) else Nil) } @@ -104,13 +115,20 @@ } } + def read_export[A](db: SQL.Database, session_name: String, theory_name: String, + export_name: String, decode: XML.Body => List[A]): List[A] = + { + Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match { + case Some(entry) => decode(entry.uncompressed_yxml()) + case None => Nil + } + } + def read_entities[A](db: SQL.Database, session_name: String, theory_name: String, export_name: String, decode: XML.Tree => A): List[A] = { - Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match { - case Some(entry) => entry.uncompressed_yxml().map(decode(_)) - case None => Nil - } + read_export(db, session_name, theory_name, export_name, + (body: XML.Body) => body.map(decode(_))) } @@ -190,4 +208,44 @@ val (typargs, args, props) = decode_props(body) Fact(entity, typargs, args, props) }) + + + /* type classes */ + + sealed case class Class( + entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term]) + + def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] = + read_entities(db, session_name, theory_name, "classes", + (tree: XML.Tree) => + { + val (entity, body) = decode_entity(tree) + val (params, axioms) = + { + import XML.Decode._ + import Term_XML.Decode._ + pair(list(pair(string, typ)), list(term))(body) + } + Class(entity, params, axioms) + }) + + + /* HOL typedefs */ + + sealed case class Typedef(name: String, + rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String) + + def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] = + read_export(db, session_name, theory_name, "typedefs", + (body: XML.Body) => + { + val typedefs = + { + import XML.Decode._ + import Term_XML.Decode._ + list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body) + } + for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs } + yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name) + }) }