--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Dec 06 11:43:29 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Dec 06 15:44:55 2019 +0100
@@ -177,17 +177,17 @@
structure Data = Generic_Data
(
- type T = ctr_sugar Symtab.table;
+ type T = (Position.T * ctr_sugar) Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data : T = Symtab.merge (K true) data;
);
fun ctr_sugar_of_generic context =
- Option.map (transfer_ctr_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context);
+ Option.map (transfer_ctr_sugar (Context.theory_of context) o #2) o Symtab.lookup (Data.get context);
fun ctr_sugars_of_generic context =
- Symtab.fold (cons o transfer_ctr_sugar (Context.theory_of context) o snd) (Data.get context) [];
+ Symtab.fold (cons o transfer_ctr_sugar (Context.theory_of context) o #2 o #2) (Data.get context) [];
fun ctr_sugar_of_case_generic context s =
find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false)
@@ -210,20 +210,24 @@
val interpret_ctr_sugar = Ctr_Sugar_Plugin.data;
-fun register_ctr_sugar_raw (ctr_sugar as {T = Type (s, _), ...}) =
+fun register_ctr_sugar_raw (ctr_sugar as {T = Type (name, _), ...}) =
Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Data.map (Symtab.update (s, morph_ctr_sugar phi ctr_sugar)));
+ (fn phi => fn context =>
+ let val pos = Position.thread_data ()
+ in Data.map (Symtab.update (name, (pos, morph_ctr_sugar phi ctr_sugar))) context end);
fun register_ctr_sugar plugins ctr_sugar =
register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar plugins ctr_sugar;
-fun default_register_ctr_sugar_global plugins (ctr_sugar as {T = Type (s, _), ...}) thy =
- let val tab = Data.get (Context.Theory thy) in
- if Symtab.defined tab s then
- thy
+fun default_register_ctr_sugar_global plugins (ctr_sugar as {T = Type (name, _), ...}) thy =
+ let
+ val tab = Data.get (Context.Theory thy);
+ val pos = Position.thread_data ();
+ in
+ if Symtab.defined tab name then thy
else
thy
- |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
+ |> Context.theory_map (Data.put (Symtab.update_new (name, (pos, ctr_sugar)) tab))
|> Named_Target.theory_map (Ctr_Sugar_Plugin.data plugins ctr_sugar)
end;
@@ -1189,7 +1193,9 @@
-(** document antiquotations **)
+(** external views **)
+
+(* document antiquotations *)
local
@@ -1231,4 +1237,35 @@
end;
+
+(* theory export *)
+
+val _ = Export_Theory.setup_presentation (fn {adjust_pos, ...} => fn thy =>
+ let
+ val parents = map (Data.get o Context.Theory) (Theory.parents_of thy);
+ val datatypes =
+ (Data.get (Context.Theory thy), []) |-> Symtab.fold
+ (fn (name, (pos, {kind, T, ctrs, ...})) =>
+ if exists (fn tab => Symtab.defined tab name) parents then I
+ else
+ let
+ val pos_properties =
+ Position.offset_properties_of (adjust_pos pos) @ Position.id_properties_of pos;
+ val typ = Logic.unvarifyT_global T;
+ val constrs = map Logic.unvarify_global ctrs;
+ val typargs = rev (fold Term.add_tfrees (Logic.mk_type typ :: constrs) []);
+ val constructors = map (fn t => (t, Term.type_of t)) constrs;
+ in
+ cons (pos_properties, (name, (kind = Codatatype, (typargs, (typ, constructors)))))
+ end);
+ in
+ if null datatypes then ()
+ else
+ Export_Theory.export_body thy "datatypes"
+ let open XML.Encode Term_XML.Encode in
+ list (pair properties (pair string (pair bool (pair (list (pair string sort))
+ (pair typ (list (pair (term (Sign.consts_of thy)) typ))))))) datatypes
+ end
+ end);
+
end;
--- a/src/Pure/Thy/export_theory.scala Fri Dec 06 11:43:29 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala Fri Dec 06 15:44:55 2019 +0100
@@ -42,6 +42,7 @@
arities: Boolean = true,
constdefs: Boolean = true,
typedefs: Boolean = true,
+ datatypes: Boolean = true,
spec_rules: Boolean = true,
cache: Term.Cache = Term.make_cache()): Session =
{
@@ -57,7 +58,7 @@
session, theory, types = types, consts = consts,
axioms = axioms, thms = thms, classes = classes, locales = locales,
locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
- constdefs = constdefs, typedefs = typedefs,
+ constdefs = constdefs, typedefs = typedefs, datatypes = datatypes,
spec_rules = spec_rules, cache = Some(cache))
}
}
@@ -93,6 +94,7 @@
arities: List[Arity],
constdefs: List[Constdef],
typedefs: List[Typedef],
+ datatypes: List[Datatype],
spec_rules: List[Spec_Rule])
{
override def toString: String = name
@@ -120,6 +122,7 @@
arities.map(_.cache(cache)),
constdefs.map(_.cache(cache)),
typedefs.map(_.cache(cache)),
+ datatypes.map(_.cache(cache)),
spec_rules.map(_.cache(cache)))
}
@@ -135,6 +138,7 @@
arities: Boolean = true,
constdefs: Boolean = true,
typedefs: Boolean = true,
+ datatypes: Boolean = true,
spec_rules: Boolean = true,
cache: Option[Term.Cache] = None): Theory =
{
@@ -161,6 +165,7 @@
if (arities) read_arities(provider) else Nil,
if (constdefs) read_constdefs(provider) else Nil,
if (typedefs) read_typedefs(provider) else Nil,
+ if (datatypes) read_datatypes(provider) else Nil,
if (spec_rules) read_spec_rules(provider) else Nil)
if (cache.isDefined) theory.cache(cache.get) else theory
}
@@ -646,6 +651,43 @@
}
+ /* HOL datatypes */
+
+ sealed case class Datatype(
+ pos: Position.T,
+ name: String,
+ co: Boolean,
+ typargs: List[(String, Term.Sort)],
+ typ: Term.Typ,
+ constructors: List[(Term.Term, Term.Typ)])
+ {
+ def id: Option[Long] = Position.Id.unapply(pos)
+
+ def cache(cache: Term.Cache): Datatype =
+ Datatype(
+ cache.position(pos),
+ cache.string(name),
+ co,
+ typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
+ cache.typ(typ),
+ constructors.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }))
+ }
+
+ def read_datatypes(provider: Export.Provider): List[Datatype] =
+ {
+ val body = provider.uncompressed_yxml(export_prefix + "datatypes")
+ val datatypes =
+ {
+ import XML.Decode._
+ import Term_XML.Decode._
+ list(pair(properties, pair(string, pair(bool, pair(list(pair(string, sort)),
+ pair(typ, list(pair(term, typ))))))))(body)
+ }
+ for ((pos, (name, (co, (typargs, (typ, constructors))))) <- datatypes)
+ yield Datatype(pos, name, co, typargs, typ, constructors)
+ }
+
+
/* Pure spec rules */
sealed abstract class Recursion