# HG changeset patch # User wenzelm # Date 1575643495 -3600 # Node ID adf5e53d2b2b7d6c5848a80078b6722f36dee4ab # Parent 6e0ff949073e6a1d62628da044b80360e4716a89 export datatypes; diff -r 6e0ff949073e -r adf5e53d2b2b src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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; diff -r 6e0ff949073e -r adf5e53d2b2b src/Pure/Thy/export_theory.scala --- 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