--- 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)
})