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