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