# HG changeset patch # User wenzelm # Date 1537388316 -7200 # Node ID a6ba77af64862a030e526a7b1681b377abd53ca1 # Parent 7d77eab54b178ceb39066a92cd3bb253c609889c export semi-unfolded locale axioms; diff -r 7d77eab54b17 -r a6ba77af6486 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Wed Sep 19 21:06:12 2018 +0200 +++ b/src/Pure/Thy/export_theory.ML Wed Sep 19 22:18:36 2018 +0200 @@ -35,6 +35,25 @@ end; +(* locale support *) + +fun locale_axioms thy loc = + let + val (intro1, intro2) = Locale.intros_of thy loc; + fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2); + val res = + Proof_Context.init_global thy + |> Interpretation.interpretation ([(loc, (("", false), (Expression.Named [], [])))], []) + |> Proof.refine (Method.Basic (METHOD o intros_tac)) + |> Seq.filter_results + |> try Seq.hd; + in + (case res of + SOME st => Thm.prems_of (#goal (Proof.goal st)) + | NONE => raise Fail ("Cannot unfold locale " ^ quote loc)) + end; + + (* general setup *) fun setup_presentation f = @@ -212,20 +231,18 @@ (* locales *) - fun encode_locale ({type_params, params, asm, defs}: Locale.content) = + fun encode_locale loc ({type_params, params, ...}: Locale.content) = let + val axioms = locale_axioms thy loc; val args = map #1 params; - val typargs = type_params @ rev (fold Term.add_tfrees (map Free args @ the_list asm) []); + val typargs = type_params @ rev (fold Term.add_tfrees (map Free args @ axioms) []); val encode = - let open XML.Encode Term_XML.Encode in - pair (list (pair string sort)) - (pair (list (pair string typ)) - (pair (option term) (list term))) - end; - in encode (typargs, (args, (asm, defs))) end; + let open XML.Encode Term_XML.Encode + in triple (list (pair string sort)) (list (pair string typ)) (list term) end; + in encode (typargs, args, axioms) end; val _ = - export_entities "locales" (fn _ => SOME o encode_locale) Locale.locale_space + export_entities "locales" (SOME oo encode_locale) Locale.locale_space (Locale.dest_locales thy); diff -r 7d77eab54b17 -r a6ba77af6486 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Wed Sep 19 21:06:12 2018 +0200 +++ b/src/Pure/Thy/export_theory.scala Wed Sep 19 22:18:36 2018 +0200 @@ -353,30 +353,29 @@ /* locales */ sealed case class Locale( - entity: Entity, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], - asm: Option[Term.Term], defs: List[Term.Term]) + entity: Entity, + typargs: List[(String, Term.Sort)], + args: List[(String, Term.Typ)], + axioms: List[Term.Term]) { def cache(cache: Term.Cache): Locale = Locale(entity.cache(cache), typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), - asm.map(cache.term(_)), - defs.map(cache.term(_))) + axioms.map(cache.term(_))) } def read_locales(provider: Export.Provider): List[Locale] = provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.LOCALE, tree) - val (typargs, (args, (asm, defs))) = + val (typargs, args, axioms) = { import XML.Decode._ import Term_XML.Decode._ - pair(list(pair(string, sort)), - pair(list(pair(string, typ)), - pair(option(term), list(term))))(body) + triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body) } - Locale(entity, typargs, args, asm, defs) + Locale(entity, typargs, args, axioms) })