/* Title: Pure/Thy/export_theory.scala
Author: Makarius
Export foundational theory content.
*/
package isabelle
object Export_Theory
{
/** session content **/
sealed case class Session(name: String, theory_graph: Graph[String, Theory])
{
override def toString: String = name
def theory(theory_name: String): Theory =
if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name)
else error("Bad theory " + quote(theory_name))
def theories: List[Theory] =
theory_graph.topological_order.map(theory_graph.get_node(_))
}
def read_session(store: Sessions.Store,
session_name: String,
types: Boolean = true,
consts: Boolean = true,
axioms: Boolean = true,
facts: Boolean = true,
classes: Boolean = true,
typedefs: Boolean = true,
classrel: Boolean = true,
arities: Boolean = true,
cache: Term.Cache = Term.make_cache()): Session =
{
val thys =
using(store.open_database(session_name))(db =>
{
db.transaction {
Export.read_theory_names(db, session_name).map((theory_name: String) =>
read_theory(Export.Provider.database(db, session_name, theory_name),
session_name, theory_name, types = types, consts = consts,
axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
cache = Some(cache)))
}
})
val graph0 =
(Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) }
val graph1 =
(graph0 /: thys) { case (g0, thy) =>
(g0 /: thy.parents) { case (g1, parent) =>
g1.default_node(parent, empty_theory(parent)).add_edge_acyclic(parent, thy.name) } }
Session(session_name, graph1)
}
/** theory content **/
val export_prefix: String = "theory/"
sealed case class Theory(name: String, parents: List[String],
types: List[Type],
consts: List[Const],
axioms: List[Axiom],
facts: List[Fact],
classes: List[Class],
typedefs: List[Typedef],
classrel: List[Classrel],
arities: List[Arity])
{
override def toString: String = name
lazy val entities: Set[Long] =
Set.empty[Long] ++
types.iterator.map(_.entity.serial) ++
consts.iterator.map(_.entity.serial) ++
axioms.iterator.map(_.entity.serial) ++
facts.iterator.map(_.entity.serial) ++
classes.iterator.map(_.entity.serial)
def cache(cache: Term.Cache): Theory =
Theory(cache.string(name),
parents.map(cache.string(_)),
types.map(_.cache(cache)),
consts.map(_.cache(cache)),
axioms.map(_.cache(cache)),
facts.map(_.cache(cache)),
classes.map(_.cache(cache)),
typedefs.map(_.cache(cache)),
classrel.map(_.cache(cache)),
arities.map(_.cache(cache)))
}
def empty_theory(name: String): Theory =
Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
types: Boolean = true,
consts: Boolean = true,
axioms: Boolean = true,
facts: Boolean = true,
classes: Boolean = true,
typedefs: Boolean = true,
classrel: Boolean = true,
arities: Boolean = true,
cache: Option[Term.Cache] = None): Theory =
{
val parents =
provider(export_prefix + "parents") match {
case Some(entry) => split_lines(entry.uncompressed().text)
case None =>
error("Missing theory export in session " + quote(session_name) + ": " +
quote(theory_name))
}
val theory =
Theory(theory_name, parents,
if (types) read_types(provider) else Nil,
if (consts) read_consts(provider) else Nil,
if (axioms) read_axioms(provider) else Nil,
if (facts) read_facts(provider) else Nil,
if (classes) read_classes(provider) else Nil,
if (typedefs) read_typedefs(provider) else Nil,
if (classrel) read_classrel(provider) else Nil,
if (arities) read_arities(provider) else Nil)
if (cache.isDefined) theory.cache(cache.get) else theory
}
def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
{
val session_name = Thy_Header.PURE
val theory_name = Thy_Header.PURE
using(store.open_database(session_name))(db =>
{
db.transaction {
read_theory(Export.Provider.database(db, session_name, theory_name),
session_name, theory_name, cache = cache)
}
})
}
/* entities */
object Kind extends Enumeration
{
val TYPE = Value("type")
val CONST = Value("const")
val AXIOM = Value("axiom")
val FACT = Value("fact")
val CLASS = Value("class")
}
sealed case class Entity(kind: Kind.Value, name: String, serial: Long, pos: Position.T)
{
override def toString: String = kind.toString + quote(name)
def cache(cache: Term.Cache): Entity =
Entity(kind, cache.string(name), serial, cache.position(pos))
}
def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
{
def err(): Nothing = throw new XML.XML_Body(List(tree))
tree match {
case XML.Elem(Markup(Markup.ENTITY, props), body) =>
val name = Markup.Name.unapply(props) getOrElse err()
val serial = Markup.Serial.unapply(props) getOrElse err()
val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
(Entity(kind, name, serial, pos), body)
case _ => err()
}
}
/* types */
sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
{
def cache(cache: Term.Cache): Type =
Type(entity.cache(cache),
args.map(cache.string(_)),
abbrev.map(cache.typ(_)))
}
def read_types(provider: Export.Provider): List[Type] =
provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.TYPE, tree)
val (args, abbrev) =
{
import XML.Decode._
pair(list(string), option(Term_XML.Decode.typ))(body)
}
Type(entity, args, abbrev)
})
/* consts */
sealed case class Const(
entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
{
def cache(cache: Term.Cache): Const =
Const(entity.cache(cache),
typargs.map(cache.string(_)),
cache.typ(typ),
abbrev.map(cache.term(_)))
}
def read_consts(provider: Export.Provider): List[Const] =
provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.CONST, tree)
val (args, typ, abbrev) =
{
import XML.Decode._
triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
}
Const(entity, args, typ, abbrev)
})
/* axioms and facts */
def decode_props(body: XML.Body):
(List[(String, Term.Sort)], List[(String, Term.Typ)], List[Term.Term]) =
{
import XML.Decode._
import Term_XML.Decode._
triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
}
sealed case class Axiom(
entity: Entity,
typargs: List[(String, Term.Sort)],
args: List[(String, Term.Typ)],
prop: Term.Term)
{
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))
}
def read_axioms(provider: Export.Provider): List[Axiom] =
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)
})
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] =
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)
})
/* type classes */
sealed case class Class(
entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
{
def cache(cache: Term.Cache): Class =
Class(entity.cache(cache),
params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
axioms.map(cache.term(_)))
}
def read_classes(provider: Export.Provider): List[Class] =
provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.CLASS, tree)
val (params, axioms) =
{
import XML.Decode._
import Term_XML.Decode._
pair(list(pair(string, typ)), list(term))(body)
}
Class(entity, params, axioms)
})
/* sort algebra */
sealed case class Classrel(class_name: String, super_names: List[String])
{
def cache(cache: Term.Cache): Classrel =
Classrel(cache.string(class_name), super_names.map(cache.string(_)))
}
def read_classrel(provider: Export.Provider): List[Classrel] =
{
val body = provider.uncompressed_yxml(export_prefix + "classrel")
val classrel =
{
import XML.Decode._
list(pair(string, list(string)))(body)
}
for ((c, cs) <- classrel) yield Classrel(c, cs)
}
sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
{
def cache(cache: Term.Cache): Arity =
Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
}
def read_arities(provider: Export.Provider): List[Arity] =
{
val body = provider.uncompressed_yxml(export_prefix + "arities")
val arities =
{
import XML.Decode._
import Term_XML.Decode._
list(triple(string, list(sort), string))(body)
}
for ((a, b, c) <- arities) yield Arity(a, b, c)
}
/* HOL typedefs */
sealed case class Typedef(name: String,
rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
{
def cache(cache: Term.Cache): Typedef =
Typedef(cache.string(name),
cache.typ(rep_type),
cache.typ(abs_type),
cache.string(rep_name),
cache.string(abs_name),
cache.string(axiom_name))
}
def read_typedefs(provider: Export.Provider): List[Typedef] =
{
val body = provider.uncompressed_yxml(export_prefix + "typedefs")
val typedefs =
{
import XML.Decode._
import Term_XML.Decode._
list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
}
for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
}
}