src/Pure/Thy/export_theory.scala
author wenzelm
Thu May 17 14:50:48 2018 +0200 (14 months ago)
changeset 68203 cda4f24331d5
parent 68173 7ed88a534bb6
child 68206 dedf1a70d1fa
permissions -rw-r--r--
read theory content from session database;
wenzelm@68171
     1
/*  Title:      Pure/Thy/export_theory.scala
wenzelm@68171
     2
    Author:     Makarius
wenzelm@68171
     3
wenzelm@68171
     4
Export foundational theory content.
wenzelm@68171
     5
*/
wenzelm@68171
     6
wenzelm@68171
     7
package isabelle
wenzelm@68171
     8
wenzelm@68171
     9
wenzelm@68171
    10
object Export_Theory
wenzelm@68171
    11
{
wenzelm@68203
    12
  /** theory content **/
wenzelm@68203
    13
wenzelm@68203
    14
  sealed case class Theory(types: List[Type], consts: List[Const])
wenzelm@68203
    15
wenzelm@68203
    16
  def read_theory(db: SQL.Database, session_name: String, theory_name: String,
wenzelm@68203
    17
    types: Boolean = true,
wenzelm@68203
    18
    consts: Boolean = true): Theory =
wenzelm@68203
    19
  {
wenzelm@68203
    20
    Theory(
wenzelm@68203
    21
      if (types) read_types(db, session_name, theory_name) else Nil,
wenzelm@68203
    22
      if (consts) read_consts(db, session_name, theory_name) else Nil)
wenzelm@68203
    23
  }
wenzelm@68203
    24
wenzelm@68203
    25
wenzelm@68171
    26
  /* entities */
wenzelm@68171
    27
wenzelm@68172
    28
  sealed case class Entity(name: String, serial: Long, pos: Position.T)
wenzelm@68171
    29
  {
wenzelm@68171
    30
    override def toString: String = name
wenzelm@68171
    31
  }
wenzelm@68171
    32
wenzelm@68171
    33
  def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
wenzelm@68171
    34
  {
wenzelm@68171
    35
    def err(): Nothing = throw new XML.XML_Body(List(tree))
wenzelm@68171
    36
wenzelm@68171
    37
    tree match {
wenzelm@68171
    38
      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
wenzelm@68171
    39
        val name = Markup.Name.unapply(props) getOrElse err()
wenzelm@68171
    40
        val serial = Markup.Serial.unapply(props) getOrElse err()
wenzelm@68171
    41
        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
wenzelm@68172
    42
        (Entity(name, serial, pos), body)
wenzelm@68171
    43
      case _ => err()
wenzelm@68171
    44
    }
wenzelm@68171
    45
  }
wenzelm@68171
    46
wenzelm@68203
    47
  def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
wenzelm@68203
    48
    export_name: String, decode: XML.Tree => A): List[A] =
wenzelm@68203
    49
  {
wenzelm@68203
    50
    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
wenzelm@68203
    51
      case Some(entry) => entry.uncompressed_yxml().map(decode(_))
wenzelm@68203
    52
      case None => Nil
wenzelm@68203
    53
    }
wenzelm@68203
    54
  }
wenzelm@68203
    55
wenzelm@68171
    56
wenzelm@68171
    57
  /* types */
wenzelm@68171
    58
wenzelm@68171
    59
  sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
wenzelm@68171
    60
wenzelm@68203
    61
  def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
wenzelm@68203
    62
    read_entities(db, session_name, theory_name, "types",
wenzelm@68203
    63
      (tree: XML.Tree) =>
wenzelm@68203
    64
        {
wenzelm@68203
    65
          val (entity, body) = decode_entity(tree)
wenzelm@68203
    66
          val (args, abbrev) =
wenzelm@68203
    67
          {
wenzelm@68203
    68
            import XML.Decode._
wenzelm@68203
    69
            pair(list(string), option(Term_XML.Decode.typ))(body)
wenzelm@68203
    70
          }
wenzelm@68203
    71
          Type(entity, args, abbrev)
wenzelm@68203
    72
        })
wenzelm@68171
    73
wenzelm@68171
    74
wenzelm@68171
    75
  /* consts */
wenzelm@68171
    76
wenzelm@68173
    77
  sealed case class Const(
wenzelm@68173
    78
    entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
wenzelm@68171
    79
wenzelm@68203
    80
  def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
wenzelm@68203
    81
    read_entities(db, session_name, theory_name, "consts",
wenzelm@68203
    82
      (tree: XML.Tree) =>
wenzelm@68203
    83
        {
wenzelm@68203
    84
          val (entity, body) = decode_entity(tree)
wenzelm@68203
    85
          val (args, typ, abbrev) =
wenzelm@68203
    86
          {
wenzelm@68203
    87
            import XML.Decode._
wenzelm@68203
    88
            triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
wenzelm@68203
    89
          }
wenzelm@68203
    90
          Const(entity, args, typ, abbrev)
wenzelm@68203
    91
        })
wenzelm@68171
    92
}