# HG changeset patch
# User wenzelm
# Date 1571668330 -7200
# Node ID 1e0ad25c94c85ad137e708f63b6614ca4d1f7150
# Parent  692095bafcd905513fc439e66a4690f1f4463805
export constdefs according to defs.ML;

diff -r 692095bafcd9 -r 1e0ad25c94c8 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sun Oct 20 22:26:44 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Mon Oct 21 16:32:10 2019 +0200
@@ -399,6 +399,20 @@
       |> export_body thy "locale_dependencies";
 
 
+    (* constdefs *)
+
+    val constdefs =
+      Defs.dest_constdefs (map Theory.defs_of (Theory.parents_of thy)) (Theory.defs_of thy)
+      |> sort_by #1;
+
+    val encode_constdefs =
+      let open XML.Encode
+      in list (pair string string) end;
+
+    val _ =
+      if null constdefs then () else export_body thy "constdefs" (encode_constdefs constdefs);
+
+
     (* parents *)
 
     val _ =
diff -r 692095bafcd9 -r 1e0ad25c94c8 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun Oct 20 22:26:44 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Mon Oct 21 16:32:10 2019 +0200
@@ -37,6 +37,7 @@
     locale_dependencies: Boolean = true,
     classrel: Boolean = true,
     arities: Boolean = true,
+    constdefs: Boolean = true,
     typedefs: Boolean = true,
     cache: Term.Cache = Term.make_cache()): Session =
   {
@@ -52,7 +53,7 @@
                 session, theory, types = types, consts = consts,
                 axioms = axioms, thms = thms, classes = classes, locales = locales,
                 locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
-                typedefs = typedefs, cache = Some(cache))
+                constdefs = constdefs, typedefs = typedefs, cache = Some(cache))
             }
           }
         }))
@@ -85,6 +86,7 @@
     locale_dependencies: List[Locale_Dependency],
     classrel: List[Classrel],
     arities: List[Arity],
+    constdefs: List[Constdef],
     typedefs: List[Typedef])
   {
     override def toString: String = name
@@ -110,6 +112,7 @@
         locale_dependencies.map(_.cache(cache)),
         classrel.map(_.cache(cache)),
         arities.map(_.cache(cache)),
+        constdefs.map(_.cache(cache)),
         typedefs.map(_.cache(cache)))
   }
 
@@ -123,6 +126,7 @@
     locale_dependencies: Boolean = true,
     classrel: Boolean = true,
     arities: Boolean = true,
+    constdefs: Boolean = true,
     typedefs: Boolean = true,
     cache: Option[Term.Cache] = None): Theory =
   {
@@ -147,6 +151,7 @@
         if (locale_dependencies) read_locale_dependencies(provider) else Nil,
         if (classrel) read_classrel(provider) else Nil,
         if (arities) read_arities(provider) else Nil,
+        if (constdefs) read_constdefs(provider) else Nil,
         if (typedefs) read_typedefs(provider) else Nil)
     if (cache.isDefined) theory.cache(cache.get) else theory
   }
@@ -555,6 +560,26 @@
   }
 
 
+  /* Pure constdefs */
+
+  sealed case class Constdef(name: String, axiom_name: String)
+  {
+    def cache(cache: Term.Cache): Constdef =
+      Constdef(cache.string(name), cache.string(axiom_name))
+  }
+
+  def read_constdefs(provider: Export.Provider): List[Constdef] =
+  {
+    val body = provider.uncompressed_yxml(export_prefix + "constdefs")
+    val constdefs =
+    {
+      import XML.Decode._
+      list(pair(string, string))(body)
+    }
+    for ((name, axiom_name) <- constdefs) yield Constdef(name, axiom_name)
+  }
+
+
   /* HOL typedefs */
 
   sealed case class Typedef(name: String,
diff -r 692095bafcd9 -r 1e0ad25c94c8 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Sun Oct 20 22:26:44 2019 +0200
+++ b/src/Pure/defs.ML	Mon Oct 21 16:32:10 2019 +0200
@@ -31,6 +31,7 @@
   val dest: T ->
    {restricts: (entry * string) list,
     reducts: (entry * entry list) list}
+  val dest_constdefs: T list -> T -> (string * string) list
   val empty: T
   val merge: context -> T * T -> T
   val define: context -> bool -> string option -> string -> entry -> entry list -> T -> T
@@ -140,6 +141,19 @@
       fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
   in {restricts = restricts, reducts = reducts} end;
 
+fun dest_constdefs prevs (Defs defs) =
+  let
+    fun prev_spec c i = prevs |> exists (fn Defs prev_defs =>
+      (case Itemtab.lookup prev_defs c of
+        NONE => false
+      | SOME {specs, ...} => Inttab.defined specs i));
+  in
+    (defs, []) |-> Itemtab.fold (fn (c, {specs, ...}) =>
+      specs |> Inttab.fold (fn (i, spec) =>
+        if #1 c = Const andalso is_some (#def spec) andalso not (prev_spec c i)
+        then cons (#2 c, the (#def spec)) else I))
+  end;
+
 val empty = Defs Itemtab.empty;