--- 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 _ =
--- 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,
--- 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;