# HG changeset patch # User wenzelm # Date 1566242593 -7200 # Node ID 5a8e3e4b37604daa18491110950cf9c41245e5f3 # Parent 7bb2bbb3ccd66d907bcf2a923bf8d31231575bbe clarified export of axioms and theorems (identified derivations instead of projected facts); diff -r 7bb2bbb3ccd6 -r 5a8e3e4b3760 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Mon Aug 19 20:08:12 2019 +0200 +++ b/src/Pure/Thy/export_theory.ML Mon Aug 19 21:23:13 2019 +0200 @@ -218,7 +218,7 @@ (#constants (Consts.dest (Sign.consts_of thy))); - (* axioms and facts *) + (* axioms *) fun standard_prop used extra_shyps raw_prop raw_proof = let @@ -236,12 +236,26 @@ fun encode_axiom used prop = encode_prop (#1 (standard_prop used [] prop NONE)); + val _ = + export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t)) + Theory.axiom_space (Theory.axioms_of thy); + + + (* theorems *) + val clean_thm = Thm.transfer thy #> Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps; - val encode_fact = clean_thm #> (fn thm => + fun entity_markup_thm (serial, (name, i)) = + let + val space = Facts.space_of (Global_Theory.facts_of thy); + val xname = Name_Space.extern_shortest thy_ctxt space name; + val {pos, ...} = Name_Space.the_entry space name; + in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end; + + val encode_thm = clean_thm #> (fn thm => standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) @@ -249,13 +263,16 @@ let open XML.Encode Term_XML.Encode in pair encode_prop (option Proofterm.encode_full) end); - val _ = - export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t)) - Theory.axiom_space (Theory.axioms_of thy); - val _ = - export_entities "facts" (K (SOME o XML.Encode.list encode_fact)) - (Facts.space_of o Global_Theory.facts_of) - (Facts.dest_static true [] (Global_Theory.facts_of thy)); + fun export_thms thms = + let val elems = + thms |> map (fn (serial, thm_name) => + let + val markup = entity_markup_thm (serial, thm_name); + val body = encode_thm (Global_Theory.get_thm_name thy (thm_name, Position.none)); + in XML.Elem (markup, body) end) + in if null elems then () else export_body thy "thms" elems end; + + val _ = export_thms (Global_Theory.dest_thm_names thy); (* type classes *) diff -r 7bb2bbb3ccd6 -r 5a8e3e4b3760 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Mon Aug 19 20:08:12 2019 +0200 +++ b/src/Pure/Thy/export_theory.scala Mon Aug 19 21:23:13 2019 +0200 @@ -28,7 +28,7 @@ types: Boolean = true, consts: Boolean = true, axioms: Boolean = true, - facts: Boolean = true, + thms: Boolean = true, classes: Boolean = true, locales: Boolean = true, locale_dependencies: Boolean = true, @@ -44,7 +44,7 @@ Export.read_theory_names(db, session_name).map((theory_name: String) => read_theory(Export.Provider.database(db, session_name, theory_name), session_name, theory_name, types = types, consts = consts, - axioms = axioms, facts = facts, classes = classes, locales = locales, + axioms = axioms, thms = thms, classes = classes, locales = locales, locale_dependencies = locale_dependencies, classrel = classrel, arities = arities, typedefs = typedefs, cache = Some(cache))) } @@ -70,8 +70,8 @@ sealed case class Theory(name: String, parents: List[String], types: List[Type], consts: List[Const], - axioms: List[Fact_Single], - facts: List[Fact_Multi], + axioms: List[Axiom], + thms: List[Thm], classes: List[Class], locales: List[Locale], locale_dependencies: List[Locale_Dependency], @@ -86,7 +86,7 @@ types.iterator.map(_.entity.serial) ++ consts.iterator.map(_.entity.serial) ++ axioms.iterator.map(_.entity.serial) ++ - facts.iterator.map(_.entity.serial) ++ + thms.iterator.map(_.entity.serial) ++ classes.iterator.map(_.entity.serial) ++ locales.iterator.map(_.entity.serial) ++ locale_dependencies.iterator.map(_.entity.serial) @@ -97,7 +97,7 @@ types.map(_.cache(cache)), consts.map(_.cache(cache)), axioms.map(_.cache(cache)), - facts.map(_.cache(cache)), + thms.map(_.cache(cache)), classes.map(_.cache(cache)), locales.map(_.cache(cache)), locale_dependencies.map(_.cache(cache)), @@ -113,7 +113,7 @@ types: Boolean = true, consts: Boolean = true, axioms: Boolean = true, - facts: Boolean = true, + thms: Boolean = true, classes: Boolean = true, locales: Boolean = true, locale_dependencies: Boolean = true, @@ -134,7 +134,7 @@ if (types) read_types(provider) else Nil, if (consts) read_consts(provider) else Nil, if (axioms) read_axioms(provider) else Nil, - if (facts) read_facts(provider) else Nil, + if (thms) read_thms(provider) else Nil, if (classes) read_classes(provider) else Nil, if (locales) read_locales(provider) else Nil, if (locale_dependencies) read_locale_dependencies(provider) else Nil, @@ -166,7 +166,7 @@ val TYPE = Value("type") val CONST = Value("const") val AXIOM = Value("axiom") - val FACT = Value("fact") + val THM = Value("thm") val CLASS = Value("class") val LOCALE = Value("locale") val LOCALE_DEPENDENCY = Value("locale_dependency") @@ -285,7 +285,7 @@ }) - /* axioms and facts */ + /* axioms */ sealed case class Prop( typargs: List[(String, Term.Sort)], @@ -310,62 +310,40 @@ Prop(typargs, args, t) } - - sealed case class Fact(prop: Prop, proof: Option[Term.Proof]) + sealed case class Axiom(entity: Entity, prop: Prop) { - def cache(cache: Term.Cache): Fact = - Fact(prop.cache(cache), proof.map(cache.proof _)) - } - - def decode_fact(body: XML.Body): Fact = - { - val (prop, proof) = - { - import XML.Decode._ - pair(decode_prop _, option(Term_XML.Decode.proof))(body) - } - Fact(prop, proof) + def cache(cache: Term.Cache): Axiom = + Axiom(entity.cache(cache), prop.cache(cache)) } - sealed case class Fact_Single(entity: Entity, fact: Fact) - { - def cache(cache: Term.Cache): Fact_Single = - Fact_Single(entity.cache(cache), fact.cache(cache)) - - def prop: Prop = fact.prop - def proof: Option[Term.Proof] = fact.proof - } - - sealed case class Fact_Multi(entity: Entity, facts: List[Fact]) - { - def cache(cache: Term.Cache): Fact_Multi = - Fact_Multi(entity.cache(cache), facts.map(_.cache(cache))) - - def props: List[Prop] = facts.map(_.prop) - - def split: List[Fact_Single] = - facts match { - case List(fact) => List(Fact_Single(entity, fact)) - case _ => - for ((fact, i) <- facts.zipWithIndex) - yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), fact) - } - } - - def read_axioms(provider: Export.Provider): List[Fact_Single] = + def read_axioms(provider: Export.Provider): List[Axiom] = provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.AXIOM, tree) val prop = decode_prop(body) - Fact_Single(entity, Fact(prop, None)) + Axiom(entity, prop) }) - def read_facts(provider: Export.Provider): List[Fact_Multi] = - provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) => + + /* theorems */ + + sealed case class Thm(entity: Entity, prop: Prop, proof: Option[Term.Proof]) + { + def cache(cache: Term.Cache): Thm = + Thm(entity.cache(cache), prop.cache(cache), proof.map(cache.proof _)) + } + + def read_thms(provider: Export.Provider): List[Thm] = + provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) => { - val (entity, body) = decode_entity(Kind.FACT, tree) - val facts = XML.Decode.list(decode_fact)(body) - Fact_Multi(entity, facts) + val (entity, body) = decode_entity(Kind.THM, tree) + val (prop, prf) = + { + import XML.Decode._ + import Term_XML.Decode._ + pair(decode_prop _, option(proof))(body) + } + Thm(entity, prop, prf) }) def read_proof(