export facts;
authorwenzelm
Sun May 20 16:25:27 2018 +0200 (14 months ago)
changeset 682324b93573ac5b4
parent 68231 0004e7a9fa10
child 68233 5e0e9376b2b0
export facts;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun May 20 15:37:16 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun May 20 16:25:27 2018 +0200
     1.3 @@ -97,23 +97,28 @@
     1.4          (#constants (Consts.dest (Sign.consts_of thy)));
     1.5  
     1.6  
     1.7 -    (* axioms *)
     1.8 +    (* axioms and facts *)
     1.9  
    1.10 -    val encode_axiom =
    1.11 +    val encode_props =
    1.12        let open XML.Encode Term_XML.Encode
    1.13 -      in triple (list (pair string sort)) (list (pair string typ)) term end;
    1.14 +      in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
    1.15  
    1.16 -    fun export_axiom prop =
    1.17 +    fun export_props props =
    1.18        let
    1.19 -        val prop' = Logic.unvarify_global prop;
    1.20 -        val typargs = rev (Term.add_tfrees prop' []);
    1.21 -        val args = rev (Term.add_frees prop' []);
    1.22 -      in encode_axiom (typargs, args, prop') end;
    1.23 +        val props' = map Logic.unvarify_global props;
    1.24 +        val typargs = rev (fold Term.add_tfrees props' []);
    1.25 +        val args = rev (fold Term.add_frees props' []);
    1.26 +      in encode_props (typargs, args, props') end;
    1.27  
    1.28      val _ =
    1.29 -      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
    1.30 +      export_entities "axioms" (K (SOME o export_props o single)) Theory.axiom_space
    1.31          (Theory.axioms_of thy);
    1.32  
    1.33 +    val _ =
    1.34 +      export_entities "facts" (K (SOME o export_props o map Thm.full_prop_of))
    1.35 +        (Facts.space_of o Global_Theory.facts_of)
    1.36 +        (Facts.dest_static true [] (Global_Theory.facts_of thy));
    1.37 +
    1.38      in () end);
    1.39  
    1.40  end;
     2.1 --- a/src/Pure/Thy/export_theory.scala	Sun May 20 15:37:16 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Sun May 20 16:25:27 2018 +0200
     2.3 @@ -54,17 +54,19 @@
     2.4    sealed case class Theory(name: String, parents: List[String],
     2.5      types: List[Type],
     2.6      consts: List[Const],
     2.7 -    axioms: List[Axiom])
     2.8 +    axioms: List[Axiom],
     2.9 +    facts: List[Fact])
    2.10    {
    2.11      override def toString: String = name
    2.12    }
    2.13  
    2.14 -  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil)
    2.15 +  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil)
    2.16  
    2.17    def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    2.18      types: Boolean = true,
    2.19      consts: Boolean = true,
    2.20 -    axioms: Boolean = true): Theory =
    2.21 +    axioms: Boolean = true,
    2.22 +    facts: Boolean = true): Theory =
    2.23    {
    2.24      val parents =
    2.25        Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    2.26 @@ -76,7 +78,8 @@
    2.27      Theory(theory_name, parents,
    2.28        if (types) read_types(db, session_name, theory_name) else Nil,
    2.29        if (consts) read_consts(db, session_name, theory_name) else Nil,
    2.30 -      if (axioms) read_axioms(db, session_name, theory_name) else Nil)
    2.31 +      if (axioms) read_axioms(db, session_name, theory_name) else Nil,
    2.32 +      if (facts) read_facts(db, session_name, theory_name) else Nil)
    2.33    }
    2.34  
    2.35  
    2.36 @@ -148,7 +151,15 @@
    2.37          })
    2.38  
    2.39  
    2.40 -  /* axioms */
    2.41 +  /* axioms and facts */
    2.42 +
    2.43 +  def decode_props(body: XML.Body):
    2.44 +    (List[(String, Term.Sort)], List[(String, Term.Typ)], List[Term.Term]) =
    2.45 +  {
    2.46 +    import XML.Decode._
    2.47 +    import Term_XML.Decode._
    2.48 +    triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
    2.49 +  }
    2.50  
    2.51    sealed case class Axiom(
    2.52      entity: Entity,
    2.53 @@ -161,12 +172,22 @@
    2.54        (tree: XML.Tree) =>
    2.55          {
    2.56            val (entity, body) = decode_entity(tree)
    2.57 -          val (typargs, args, prop) =
    2.58 -          {
    2.59 -            import XML.Decode._
    2.60 -            import Term_XML.Decode._
    2.61 -            triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
    2.62 -          }
    2.63 +          val (typargs, args, List(prop)) = decode_props(body)
    2.64            Axiom(entity, typargs, args, prop)
    2.65          })
    2.66 +
    2.67 +  sealed case class Fact(
    2.68 +    entity: Entity,
    2.69 +    typargs: List[(String, Term.Sort)],
    2.70 +    args: List[(String, Term.Typ)],
    2.71 +    props: List[Term.Term])
    2.72 +
    2.73 +  def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
    2.74 +    read_entities(db, session_name, theory_name, "facts",
    2.75 +      (tree: XML.Tree) =>
    2.76 +        {
    2.77 +          val (entity, body) = decode_entity(tree)
    2.78 +          val (typargs, args, props) = decode_props(body)
    2.79 +          Fact(entity, typargs, args, props)
    2.80 +        })
    2.81  }