# HG changeset patch
# User wenzelm
# Date 1563619949 -7200
# Node ID 8ce08b154aa146600b75f4d0cb625b050413c2b3
# Parent  38ac2e714729b1b0a456874d76e76372e85c955a
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;

diff -r 38ac2e714729 -r 8ce08b154aa1 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sat Jul 20 11:48:30 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sat Jul 20 12:52:29 2019 +0200
@@ -325,16 +325,24 @@
       Sorts.dest_algebra (map (#2 o #classes o Type.rep_tsig o Sign.tsig_of) parents)
         (#2 (#classes rep_tsig));
 
+    val encode_prop0 =
+      encode_axiom Name.context o Logic.varify_global;
+
     val encode_classrel =
       let open XML.Encode
-      in list (pair string (list string)) end;
+      in list (pair encode_prop0 (pair string string)) end;
 
     val encode_arities =
       let open XML.Encode Term_XML.Encode
-      in list (triple string (list sort) string) end;
+      in list (pair encode_prop0 (triple string (list sort) string)) end;
+
+    val export_classrel =
+      maps (fn (c, cs) => map (pair c) cs) #> map (`Logic.mk_classrel) #> encode_classrel;
 
-    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);
+    val export_arities = map (`Logic.mk_arity) #> encode_arities;
+
+    val _ = if null classrel then () else export_body thy "classrel" (export_classrel classrel);
+    val _ = if null arities then () else export_body thy "arities" (export_arities arities);
 
 
     (* locales *)
diff -r 38ac2e714729 -r 8ce08b154aa1 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat Jul 20 11:48:30 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sat Jul 20 12:52:29 2019 +0200
@@ -440,10 +440,10 @@
 
   /* sort algebra */
 
-  sealed case class Classrel(class_name: String, super_names: List[String])
+  sealed case class Classrel(class1: String, class2: String, prop: Prop)
   {
     def cache(cache: Term.Cache): Classrel =
-      Classrel(cache.string(class_name), super_names.map(cache.string(_)))
+      Classrel(cache.string(class1), cache.string(class2), prop.cache(cache))
   }
 
   def read_classrel(provider: Export.Provider): List[Classrel] =
@@ -452,15 +452,16 @@
     val classrel =
     {
       import XML.Decode._
-      list(pair(string, list(string)))(body)
+      list(pair(decode_prop, pair(string, string)))(body)
     }
-    for ((c, cs) <- classrel) yield Classrel(c, cs)
+    for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop)
   }
 
-  sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
+  sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String, prop: Prop)
   {
     def cache(cache: Term.Cache): Arity =
-      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
+      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain),
+        prop.cache(cache))
   }
 
   def read_arities(provider: Export.Provider): List[Arity] =
@@ -470,9 +471,9 @@
     {
       import XML.Decode._
       import Term_XML.Decode._
-      list(triple(string, list(sort), string))(body)
+      list(pair(decode_prop, triple(string, list(sort), string)))(body)
     }
-    for ((a, b, c) <- arities) yield Arity(a, b, c)
+    for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop)
   }
 
 
diff -r 38ac2e714729 -r 8ce08b154aa1 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Jul 20 11:48:30 2019 +0200
+++ b/src/Pure/logic.ML	Sat Jul 20 12:52:29 2019 +0200
@@ -54,6 +54,7 @@
   val name_arities: arity -> string list
   val name_arity: string * sort list * class -> string
   val mk_arities: arity -> term list
+  val mk_arity: string * sort list * class -> term
   val dest_arity: term -> string * sort list * class
   val unconstrainT: sort list -> term ->
     ((typ -> typ) * ((typ * class) * term) list * (typ * class) list) * term
@@ -319,6 +320,8 @@
   let val T = Type (t, ListPair.map TFree (Name.invent Name.context Name.aT (length Ss), Ss))
   in map (fn c => mk_of_class (T, c)) S end;
 
+fun mk_arity (t, Ss, c) = the_single (mk_arities (t, Ss, [c]));
+
 fun dest_arity tm =
   let
     fun err () = raise TERM ("dest_arity", [tm]);