--- a/src/Pure/Thy/export_theory.scala Thu May 17 19:16:41 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala Fri May 18 16:30:20 2018 +0200
@@ -54,17 +54,20 @@
/** theory content **/
- sealed case class Theory(
- name: String, parents: List[String], types: List[Type], consts: List[Const])
+ sealed case class Theory(name: String, parents: List[String],
+ types: List[Type],
+ consts: List[Const],
+ axioms: List[Axiom])
{
override def toString: String = name
}
- def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil)
+ def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil)
def read_theory(db: SQL.Database, session_name: String, theory_name: String,
types: Boolean = true,
- consts: Boolean = true): Theory =
+ consts: Boolean = true,
+ axioms: Boolean = true): Theory =
{
val parents =
Export.read_entry(db, session_name, theory_name, "theory/parents") match {
@@ -77,7 +80,8 @@
}
Theory(theory_name, parents,
if (types) read_types(db, session_name, theory_name) else Nil,
- if (consts) read_consts(db, session_name, theory_name) else Nil)
+ if (consts) read_consts(db, session_name, theory_name) else Nil,
+ if (axioms) read_axioms(db, session_name, theory_name) else Nil)
}
@@ -147,4 +151,27 @@
}
Const(entity, args, typ, abbrev)
})
+
+
+ /* axioms */
+
+ sealed case class Axiom(
+ entity: Entity,
+ typargs: List[(String, Term.Sort)],
+ args: List[(String, Term.Typ)],
+ prop: Term.Term)
+
+ def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
+ read_entities(db, session_name, theory_name, "axioms",
+ (tree: XML.Tree) =>
+ {
+ val (entity, body) = decode_entity(tree)
+ val (typargs, args, prop) =
+ {
+ import XML.Decode._
+ import Term_XML.Decode._
+ triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
+ }
+ Axiom(entity, typargs, args, prop)
+ })
}