# HG changeset patch # User wenzelm # Date 1533493938 -7200 # Node ID 782d6b89fb19cb6f74684a56dfaf38c52d91dca4 # Parent 367e60d9aa1ba6c5a8281dc537428ff64ab48984 more uniform facts: single vs. multi; diff -r 367e60d9aa1b -r 782d6b89fb19 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sun Aug 05 14:50:11 2018 +0200 +++ b/src/Pure/Thy/export_theory.ML Sun Aug 05 20:32:18 2018 +0200 @@ -131,27 +131,27 @@ Thm.transfer thy #> Thm.check_hyps (Context.Theory thy) #> Drule.sort_constraint_intr_shyps #> - Thm.full_prop_of; + Thm.full_prop_of #> + Term_Subst.zero_var_indexes; - val encode_props = - let open XML.Encode Term_XML.Encode - in triple (list (pair string sort)) (list (pair string typ)) (list (term o named_bounds)) end; - - fun export_props props = + fun encode_prop prop = let - val props' = map Logic.unvarify_global props; - val typargs = rev (fold Term.add_tfrees props' []); - val args = rev (fold Term.add_frees props' []); - in encode_props (typargs, args, props') end; + val prop' = Logic.unvarify_global (named_bounds prop); + val typargs = rev (Term.add_tfrees prop' []); + val args = rev (Term.add_frees prop' []); + open XML.Encode Term_XML.Encode; + in + triple (list (pair string sort)) (list (pair string typ)) term + (typargs, args, prop') + end; - val export_axiom = export_props o single; - val export_fact = export_props o Term_Subst.zero_var_indexes_list o map standard_prop_of; + val encode_fact = XML.Encode.list encode_prop o map standard_prop_of; val _ = - export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space + export_entities "axioms" (K (SOME o encode_prop)) Theory.axiom_space (Theory.axioms_of thy); val _ = - export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of) + export_entities "facts" (K (SOME o encode_fact)) (Facts.space_of o Global_Theory.facts_of) (Facts.dest_static true [] (Global_Theory.facts_of thy)); diff -r 367e60d9aa1b -r 782d6b89fb19 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Sun Aug 05 14:50:11 2018 +0200 +++ b/src/Pure/Thy/export_theory.scala Sun Aug 05 20:32:18 2018 +0200 @@ -66,8 +66,8 @@ sealed case class Theory(name: String, parents: List[String], types: List[Type], consts: List[Const], - axioms: List[Axiom], - facts: List[Fact], + axioms: List[Fact_Single], + facts: List[Fact_Multi], classes: List[Class], typedefs: List[Typedef], classrel: List[Classrel], @@ -227,56 +227,65 @@ }) - /* axioms and facts */ + /* facts */ - def decode_props(body: XML.Body): - (List[(String, Term.Sort)], List[(String, Term.Typ)], List[Term.Term]) = + sealed case class Prop( + typargs: List[(String, Term.Sort)], + args: List[(String, Term.Typ)], + term: Term.Term) { - import XML.Decode._ - import Term_XML.Decode._ - triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body) + def cache(cache: Term.Cache): Prop = + Prop( + typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), + args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), + cache.term(term)) } - sealed case class Axiom( - entity: Entity, - typargs: List[(String, Term.Sort)], - args: List[(String, Term.Typ)], - prop: Term.Term) + def decode_prop(body: XML.Body): Prop = { - def cache(cache: Term.Cache): Axiom = - Axiom(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)) }), - cache.term(prop)) + val (typargs, args, t) = + { + import XML.Decode._ + import Term_XML.Decode._ + triple(list(pair(string, sort)), list(pair(string, typ)), term)(body) + } + Prop(typargs, args, t) } - def read_axioms(provider: Export.Provider): List[Axiom] = + sealed case class Fact_Single(entity: Entity, prop: Prop) + { + def cache(cache: Term.Cache): Fact_Single = + Fact_Single(entity.cache(cache), prop.cache(cache)) + } + + sealed case class Fact_Multi(entity: Entity, props: List[Prop]) + { + def cache(cache: Term.Cache): Fact_Multi = + Fact_Multi(entity.cache(cache), props.map(_.cache(cache))) + + def split: List[Fact_Single] = + props match { + case List(prop) => List(Fact_Single(entity, prop)) + case _ => + for ((prop, i) <- props.zipWithIndex) + yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), prop) + } + } + + def read_axioms(provider: Export.Provider): List[Fact_Single] = provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.AXIOM, tree) - val (typargs, args, List(prop)) = decode_props(body) - Axiom(entity, typargs, args, prop) + val prop = decode_prop(body) + Fact_Single(entity, prop) }) - sealed case class Fact( - entity: Entity, - typargs: List[(String, Term.Sort)], - args: List[(String, Term.Typ)], - props: List[Term.Term]) - { - def cache(cache: Term.Cache): Fact = - Fact(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)) }), - props.map(cache.term(_))) - } - - def read_facts(provider: Export.Provider): List[Fact] = + def read_facts(provider: Export.Provider): List[Fact_Multi] = provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) => { val (entity, body) = decode_entity(Kind.FACT, tree) - val (typargs, args, props) = decode_props(body) - Fact(entity, typargs, args, props) + val props = XML.Decode.list(decode_prop)(body) + Fact_Multi(entity, props) })