more exports;
authorwenzelm
Fri May 18 16:30:20 2018 +0200 (14 months ago)
changeset 68208d9f2cf4fc002
parent 68207 1463c4996fb2
child 68209 aeffd8f1f079
more exports;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu May 17 19:16:41 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Fri May 18 16:30:20 2018 +0200
     1.3 @@ -97,6 +97,24 @@
     1.4        export_entities "consts" export_const Sign.const_space
     1.5          (#constants (Consts.dest (Sign.consts_of thy)));
     1.6  
     1.7 +
     1.8 +    (* axioms *)
     1.9 +
    1.10 +    val encode_axiom =
    1.11 +      let open XML.Encode Term_XML.Encode
    1.12 +      in triple (list (pair string sort)) (list (pair string typ)) term end;
    1.13 +
    1.14 +    fun export_axiom prop =
    1.15 +      let
    1.16 +        val prop' = Logic.unvarify_global prop;
    1.17 +        val typargs = rev (Term.add_tfrees prop' []);
    1.18 +        val args = rev (Term.add_frees prop' []);
    1.19 +      in encode_axiom (typargs, args, prop') end;
    1.20 +
    1.21 +    val _ =
    1.22 +      export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
    1.23 +        (Theory.axioms_of thy);
    1.24 +
    1.25      in () end);
    1.26  
    1.27  end;
     2.1 --- a/src/Pure/Thy/export_theory.scala	Thu May 17 19:16:41 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Fri May 18 16:30:20 2018 +0200
     2.3 @@ -54,17 +54,20 @@
     2.4  
     2.5    /** theory content **/
     2.6  
     2.7 -  sealed case class Theory(
     2.8 -    name: String, parents: List[String], types: List[Type], consts: List[Const])
     2.9 +  sealed case class Theory(name: String, parents: List[String],
    2.10 +    types: List[Type],
    2.11 +    consts: List[Const],
    2.12 +    axioms: List[Axiom])
    2.13    {
    2.14      override def toString: String = name
    2.15    }
    2.16  
    2.17 -  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil)
    2.18 +  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil)
    2.19  
    2.20    def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    2.21      types: Boolean = true,
    2.22 -    consts: Boolean = true): Theory =
    2.23 +    consts: Boolean = true,
    2.24 +    axioms: Boolean = true): Theory =
    2.25    {
    2.26      val parents =
    2.27        Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    2.28 @@ -77,7 +80,8 @@
    2.29        }
    2.30      Theory(theory_name, parents,
    2.31        if (types) read_types(db, session_name, theory_name) else Nil,
    2.32 -      if (consts) read_consts(db, session_name, theory_name) else Nil)
    2.33 +      if (consts) read_consts(db, session_name, theory_name) else Nil,
    2.34 +      if (axioms) read_axioms(db, session_name, theory_name) else Nil)
    2.35    }
    2.36  
    2.37  
    2.38 @@ -147,4 +151,27 @@
    2.39            }
    2.40            Const(entity, args, typ, abbrev)
    2.41          })
    2.42 +
    2.43 +
    2.44 +  /* axioms */
    2.45 +
    2.46 +  sealed case class Axiom(
    2.47 +    entity: Entity,
    2.48 +    typargs: List[(String, Term.Sort)],
    2.49 +    args: List[(String, Term.Typ)],
    2.50 +    prop: Term.Term)
    2.51 +
    2.52 +  def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
    2.53 +    read_entities(db, session_name, theory_name, "axioms",
    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 +          Axiom(entity, typargs, args, prop)
    2.64 +        })
    2.65  }