src/Pure/Thy/export_theory.scala
author wenzelm
Sun May 20 16:25:27 2018 +0200 (14 months ago)
changeset 68232 4b93573ac5b4
parent 68231 0004e7a9fa10
child 68264 bb9a3be6952a
permissions -rw-r--r--
export facts;
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@68206
    12
  /** session content **/
wenzelm@68206
    13
wenzelm@68206
    14
  sealed case class Session(name: String, theory_graph: Graph[String, Theory])
wenzelm@68206
    15
  {
wenzelm@68206
    16
    override def toString: String = name
wenzelm@68206
    17
wenzelm@68206
    18
    def theory(theory_name: String): Theory =
wenzelm@68206
    19
      if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name)
wenzelm@68206
    20
      else error("Bad theory " + quote(theory_name))
wenzelm@68206
    21
wenzelm@68206
    22
    def theories: List[Theory] =
wenzelm@68206
    23
      theory_graph.topological_order.map(theory_graph.get_node(_))
wenzelm@68206
    24
  }
wenzelm@68206
    25
wenzelm@68209
    26
  def read_session(store: Sessions.Store,
wenzelm@68209
    27
    session_name: String,
wenzelm@68206
    28
    types: Boolean = true,
wenzelm@68206
    29
    consts: Boolean = true): Session =
wenzelm@68206
    30
  {
wenzelm@68206
    31
    val thys =
wenzelm@68210
    32
      using(store.open_database(session_name))(db =>
wenzelm@68206
    33
      {
wenzelm@68206
    34
        db.transaction {
wenzelm@68222
    35
          Export.read_theory_names(db, session_name).map((theory_name: String) =>
wenzelm@68222
    36
            read_theory(db, session_name, theory_name, types = types, consts = consts))
wenzelm@68206
    37
        }
wenzelm@68206
    38
      })
wenzelm@68206
    39
wenzelm@68206
    40
    val graph0 =
wenzelm@68206
    41
      (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) }
wenzelm@68206
    42
    val graph1 =
wenzelm@68206
    43
      (graph0 /: thys) { case (g0, thy) =>
wenzelm@68206
    44
        (g0 /: thy.parents) { case (g1, parent) =>
wenzelm@68206
    45
          g1.default_node(parent, empty_theory(parent)).add_edge_acyclic(parent, thy.name) } }
wenzelm@68206
    46
wenzelm@68206
    47
    Session(session_name, graph1)
wenzelm@68206
    48
  }
wenzelm@68206
    49
wenzelm@68206
    50
wenzelm@68206
    51
wenzelm@68203
    52
  /** theory content **/
wenzelm@68203
    53
wenzelm@68208
    54
  sealed case class Theory(name: String, parents: List[String],
wenzelm@68208
    55
    types: List[Type],
wenzelm@68208
    56
    consts: List[Const],
wenzelm@68232
    57
    axioms: List[Axiom],
wenzelm@68232
    58
    facts: List[Fact])
wenzelm@68206
    59
  {
wenzelm@68206
    60
    override def toString: String = name
wenzelm@68206
    61
  }
wenzelm@68206
    62
wenzelm@68232
    63
  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil)
wenzelm@68203
    64
wenzelm@68203
    65
  def read_theory(db: SQL.Database, session_name: String, theory_name: String,
wenzelm@68203
    66
    types: Boolean = true,
wenzelm@68208
    67
    consts: Boolean = true,
wenzelm@68232
    68
    axioms: Boolean = true,
wenzelm@68232
    69
    facts: Boolean = true): Theory =
wenzelm@68203
    70
  {
wenzelm@68206
    71
    val parents =
wenzelm@68206
    72
      Export.read_entry(db, session_name, theory_name, "theory/parents") match {
wenzelm@68231
    73
        case Some(entry) => split_lines(entry.uncompressed().text)
wenzelm@68206
    74
        case None =>
wenzelm@68206
    75
          error("Missing theory export in session " + quote(session_name) + ": " +
wenzelm@68206
    76
            quote(theory_name))
wenzelm@68206
    77
      }
wenzelm@68206
    78
    Theory(theory_name, parents,
wenzelm@68203
    79
      if (types) read_types(db, session_name, theory_name) else Nil,
wenzelm@68208
    80
      if (consts) read_consts(db, session_name, theory_name) else Nil,
wenzelm@68232
    81
      if (axioms) read_axioms(db, session_name, theory_name) else Nil,
wenzelm@68232
    82
      if (facts) read_facts(db, session_name, theory_name) else Nil)
wenzelm@68203
    83
  }
wenzelm@68203
    84
wenzelm@68203
    85
wenzelm@68171
    86
  /* entities */
wenzelm@68171
    87
wenzelm@68172
    88
  sealed case class Entity(name: String, serial: Long, pos: Position.T)
wenzelm@68171
    89
  {
wenzelm@68171
    90
    override def toString: String = name
wenzelm@68171
    91
  }
wenzelm@68171
    92
wenzelm@68171
    93
  def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
wenzelm@68171
    94
  {
wenzelm@68171
    95
    def err(): Nothing = throw new XML.XML_Body(List(tree))
wenzelm@68171
    96
wenzelm@68171
    97
    tree match {
wenzelm@68171
    98
      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
wenzelm@68171
    99
        val name = Markup.Name.unapply(props) getOrElse err()
wenzelm@68171
   100
        val serial = Markup.Serial.unapply(props) getOrElse err()
wenzelm@68171
   101
        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
wenzelm@68172
   102
        (Entity(name, serial, pos), body)
wenzelm@68171
   103
      case _ => err()
wenzelm@68171
   104
    }
wenzelm@68171
   105
  }
wenzelm@68171
   106
wenzelm@68203
   107
  def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
wenzelm@68203
   108
    export_name: String, decode: XML.Tree => A): List[A] =
wenzelm@68203
   109
  {
wenzelm@68203
   110
    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
wenzelm@68203
   111
      case Some(entry) => entry.uncompressed_yxml().map(decode(_))
wenzelm@68203
   112
      case None => Nil
wenzelm@68203
   113
    }
wenzelm@68203
   114
  }
wenzelm@68203
   115
wenzelm@68171
   116
wenzelm@68171
   117
  /* types */
wenzelm@68171
   118
wenzelm@68171
   119
  sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
wenzelm@68171
   120
wenzelm@68203
   121
  def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
wenzelm@68203
   122
    read_entities(db, session_name, theory_name, "types",
wenzelm@68203
   123
      (tree: XML.Tree) =>
wenzelm@68203
   124
        {
wenzelm@68203
   125
          val (entity, body) = decode_entity(tree)
wenzelm@68203
   126
          val (args, abbrev) =
wenzelm@68203
   127
          {
wenzelm@68203
   128
            import XML.Decode._
wenzelm@68203
   129
            pair(list(string), option(Term_XML.Decode.typ))(body)
wenzelm@68203
   130
          }
wenzelm@68203
   131
          Type(entity, args, abbrev)
wenzelm@68203
   132
        })
wenzelm@68171
   133
wenzelm@68171
   134
wenzelm@68171
   135
  /* consts */
wenzelm@68171
   136
wenzelm@68173
   137
  sealed case class Const(
wenzelm@68173
   138
    entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
wenzelm@68171
   139
wenzelm@68203
   140
  def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
wenzelm@68203
   141
    read_entities(db, session_name, theory_name, "consts",
wenzelm@68203
   142
      (tree: XML.Tree) =>
wenzelm@68203
   143
        {
wenzelm@68203
   144
          val (entity, body) = decode_entity(tree)
wenzelm@68203
   145
          val (args, typ, abbrev) =
wenzelm@68203
   146
          {
wenzelm@68203
   147
            import XML.Decode._
wenzelm@68203
   148
            triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
wenzelm@68203
   149
          }
wenzelm@68203
   150
          Const(entity, args, typ, abbrev)
wenzelm@68203
   151
        })
wenzelm@68208
   152
wenzelm@68208
   153
wenzelm@68232
   154
  /* axioms and facts */
wenzelm@68232
   155
wenzelm@68232
   156
  def decode_props(body: XML.Body):
wenzelm@68232
   157
    (List[(String, Term.Sort)], List[(String, Term.Typ)], List[Term.Term]) =
wenzelm@68232
   158
  {
wenzelm@68232
   159
    import XML.Decode._
wenzelm@68232
   160
    import Term_XML.Decode._
wenzelm@68232
   161
    triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
wenzelm@68232
   162
  }
wenzelm@68208
   163
wenzelm@68208
   164
  sealed case class Axiom(
wenzelm@68208
   165
    entity: Entity,
wenzelm@68208
   166
    typargs: List[(String, Term.Sort)],
wenzelm@68208
   167
    args: List[(String, Term.Typ)],
wenzelm@68208
   168
    prop: Term.Term)
wenzelm@68208
   169
wenzelm@68208
   170
  def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
wenzelm@68208
   171
    read_entities(db, session_name, theory_name, "axioms",
wenzelm@68208
   172
      (tree: XML.Tree) =>
wenzelm@68208
   173
        {
wenzelm@68208
   174
          val (entity, body) = decode_entity(tree)
wenzelm@68232
   175
          val (typargs, args, List(prop)) = decode_props(body)
wenzelm@68208
   176
          Axiom(entity, typargs, args, prop)
wenzelm@68208
   177
        })
wenzelm@68232
   178
wenzelm@68232
   179
  sealed case class Fact(
wenzelm@68232
   180
    entity: Entity,
wenzelm@68232
   181
    typargs: List[(String, Term.Sort)],
wenzelm@68232
   182
    args: List[(String, Term.Typ)],
wenzelm@68232
   183
    props: List[Term.Term])
wenzelm@68232
   184
wenzelm@68232
   185
  def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
wenzelm@68232
   186
    read_entities(db, session_name, theory_name, "facts",
wenzelm@68232
   187
      (tree: XML.Tree) =>
wenzelm@68232
   188
        {
wenzelm@68232
   189
          val (entity, body) = decode_entity(tree)
wenzelm@68232
   190
          val (typargs, args, props) = decode_props(body)
wenzelm@68232
   191
          Fact(entity, typargs, args, props)
wenzelm@68232
   192
        })
wenzelm@68171
   193
}