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)
+        })
 }