export sort algebra;

--- a/src/Pure/Thy/export_theory.ML	Sat May 26 21:24:07 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sat May 26 22:02:25 2018 +0200
@@ -141,6 +141,24 @@
       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);
+
+    (* sort algebra *)
+
+    val {classrel, arities} =
+      Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
+        (#2 (#classes rep_tsig));
+
+    val encode_classrel =
+      let open XML.Encode
+      in list (pair string (list string)) end;
+
+    val encode_arities =
+      let open XML.Encode Term_XML.Encode
+      in list (triple string (list sort) string) end;
+
+    val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel);
+    val _ = if null arities then () else export_body thy "arities" (encode_arities arities);
+
+  in () end);
 
 end;

--- a/src/Pure/Thy/export_theory.scala	Sat May 26 21:24:07 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sat May 26 22:02:25 2018 +0200
@@ -31,6 +31,8 @@
     facts: Boolean = true,
     classes: Boolean = true,
     typedefs: Boolean = true,
+    classrel: Boolean = true,
+    arities: Boolean = true,
     cache: Term.Cache = Term.make_cache()): Session =
   {
     val thys =
@@ -64,7 +66,9 @@
     axioms: List[Axiom],
     facts: List[Fact],
     classes: List[Class],
-    typedefs: List[Typedef])
+    typedefs: List[Typedef],
+    classrel: List[Classrel],
+    arities: List[Arity])
   {
     override def toString: String = name
 
@@ -76,10 +80,13 @@
         axioms.map(_.cache(cache)),
         facts.map(_.cache(cache)),
         classes.map(_.cache(cache)),
-        typedefs.map(_.cache(cache)))
+        typedefs.map(_.cache(cache)),
+        classrel.map(_.cache(cache)),
+        arities.map(_.cache(cache)))
   }
 
-  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
+  def empty_theory(name: String): Theory =
+    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
 
   def read_theory(db: SQL.Database, session_name: String, theory_name: String,
     types: Boolean = true,
@@ -88,6 +95,8 @@
     facts: Boolean = true,
     classes: Boolean = true,
     typedefs: Boolean = true,
+    classrel: Boolean = true,
+    arities: Boolean = true,
     cache: Option[Term.Cache] = None): Theory =
   {
     val parents =
@@ -104,7 +113,9 @@
         if (axioms) read_axioms(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)
+        if (typedefs) read_typedefs(db, session_name, theory_name) else Nil,
+        if (classrel) read_classrel(db, session_name, theory_name) else Nil,
+        if (arities) read_arities(db, session_name, theory_name) else Nil)
     if (cache.isDefined) theory.cache(cache.get) else theory
   }
 
@@ -281,6 +292,46 @@
         })
 
 
+  /* sort algebra */
+
+  sealed case class Classrel(class_name: String, super_names: List[String])
+  {
+    def cache(cache: Term.Cache): Classrel =
+      Classrel(cache.string(class_name), super_names.map(cache.string(_)))
+  }
+
+  def read_classrel(db: SQL.Database, session_name: String, theory_name: String): List[Classrel] =
+    read_export(db, session_name, theory_name, "classrel",
+      (body: XML.Body) =>
+        {
+          val classrel =
+          {
+            import XML.Decode._
+            list(pair(string, list(string)))(body)
+          }
+          for ((c, cs) <- classrel) yield Classrel(c, cs)
+        })
+
+  sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
+  {
+    def cache(cache: Term.Cache): Arity =
+      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
+  }
+
+  def read_arities(db: SQL.Database, session_name: String, theory_name: String): List[Arity] =
+    read_export(db, session_name, theory_name, "arities",
+      (body: XML.Body) =>
+        {
+          val arities =
+          {
+            import XML.Decode._
+            import Term_XML.Decode._
+            list(triple(string, list(sort), string))(body)
+          }
+          for ((a, b, c) <- arities) yield Arity(a, b, c)
+        })
+
+
   /* HOL typedefs */
 
   sealed case class Typedef(name: String,

--- a/src/Pure/sorts.ML	Sat May 26 21:24:07 2018 +0200
+++ b/src/Pure/sorts.ML	Sat May 26 22:02:25 2018 +0200
@@ -43,6 +43,9 @@
   val add_arities: Context.generic -> string * (class * sort list) list -> algebra -> algebra
   val empty_algebra: algebra
   val merge_algebra: Context.generic -> algebra * algebra -> algebra
+  val dest_algebra: algebra list -> algebra ->
+    {classrel: (class * class list) list,
+     arities: (string * sort list * class) list}
   val subalgebra: Context.generic -> (class -> bool) -> (class * string -> sort list option)
     -> algebra -> (sort -> sort) * algebra
   type class_error
@@ -299,6 +302,26 @@
   in make_algebra (classes', arities') end;
 
 
+(* destruct *)
+
+fun dest_algebra parents (Algebra {classes, arities}) =
+  let
+    fun new_classrel rel = not (exists (fn algebra => class_less algebra rel) parents);
+    val classrel =
+      (classes, []) |-> Graph.fold (fn (c, (_, (_, ds))) =>
+        (case filter (fn d => new_classrel (c, d)) (Graph.Keys.dest ds) of
+          [] => I
+        | ds' => cons (c, sort_strings ds')))
+      |> sort_by #1;
+
+    fun is_arity t ar algebra = member (op =) (Symtab.lookup_list (arities_of algebra) t) ar;
+    fun add_arity t (c, Ss) = not (exists (is_arity t (c, Ss)) parents) ? cons (t, Ss, c);
+    val arities =
+      (arities, []) |-> Symtab.fold (fn (t, ars) => fold_rev (add_arity t) (sort_by #1 ars))
+      |> sort_by #1;
+  in {classrel = classrel, arities = arities} end;
+
+
 (* algebra projections *)  (* FIXME potentially violates abstract type integrity *)
 
 fun subalgebra context P sargs (algebra as Algebra {classes, arities}) =