src/Pure/Thy/export_theory.scala
author wenzelm
Thu May 24 16:56:14 2018 +0200 (14 months ago)
changeset 68264 bb9a3be6952a
parent 68232 4b93573ac5b4
child 68267 6a29709906c6
permissions -rw-r--r--
more exports;
read_session: proper signature;
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@68264
    29
    consts: Boolean = true,
wenzelm@68264
    30
    axioms: Boolean = true,
wenzelm@68264
    31
    facts: Boolean = true,
wenzelm@68264
    32
    classes: Boolean = true,
wenzelm@68264
    33
    typedefs: Boolean = true): Session =
wenzelm@68206
    34
  {
wenzelm@68206
    35
    val thys =
wenzelm@68210
    36
      using(store.open_database(session_name))(db =>
wenzelm@68206
    37
      {
wenzelm@68206
    38
        db.transaction {
wenzelm@68222
    39
          Export.read_theory_names(db, session_name).map((theory_name: String) =>
wenzelm@68264
    40
            read_theory(db, session_name, theory_name, types = types, consts = consts,
wenzelm@68264
    41
              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs))
wenzelm@68206
    42
        }
wenzelm@68206
    43
      })
wenzelm@68206
    44
wenzelm@68206
    45
    val graph0 =
wenzelm@68206
    46
      (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) }
wenzelm@68206
    47
    val graph1 =
wenzelm@68206
    48
      (graph0 /: thys) { case (g0, thy) =>
wenzelm@68206
    49
        (g0 /: thy.parents) { case (g1, parent) =>
wenzelm@68206
    50
          g1.default_node(parent, empty_theory(parent)).add_edge_acyclic(parent, thy.name) } }
wenzelm@68206
    51
wenzelm@68206
    52
    Session(session_name, graph1)
wenzelm@68206
    53
  }
wenzelm@68206
    54
wenzelm@68206
    55
wenzelm@68206
    56
wenzelm@68203
    57
  /** theory content **/
wenzelm@68203
    58
wenzelm@68208
    59
  sealed case class Theory(name: String, parents: List[String],
wenzelm@68208
    60
    types: List[Type],
wenzelm@68208
    61
    consts: List[Const],
wenzelm@68232
    62
    axioms: List[Axiom],
wenzelm@68264
    63
    facts: List[Fact],
wenzelm@68264
    64
    classes: List[Class],
wenzelm@68264
    65
    typedefs: List[Typedef])
wenzelm@68206
    66
  {
wenzelm@68206
    67
    override def toString: String = name
wenzelm@68206
    68
  }
wenzelm@68206
    69
wenzelm@68264
    70
  def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
wenzelm@68203
    71
wenzelm@68203
    72
  def read_theory(db: SQL.Database, session_name: String, theory_name: String,
wenzelm@68203
    73
    types: Boolean = true,
wenzelm@68208
    74
    consts: Boolean = true,
wenzelm@68232
    75
    axioms: Boolean = true,
wenzelm@68264
    76
    facts: Boolean = true,
wenzelm@68264
    77
    classes: Boolean = true,
wenzelm@68264
    78
    typedefs: Boolean = true): Theory =
wenzelm@68203
    79
  {
wenzelm@68206
    80
    val parents =
wenzelm@68206
    81
      Export.read_entry(db, session_name, theory_name, "theory/parents") match {
wenzelm@68231
    82
        case Some(entry) => split_lines(entry.uncompressed().text)
wenzelm@68206
    83
        case None =>
wenzelm@68206
    84
          error("Missing theory export in session " + quote(session_name) + ": " +
wenzelm@68206
    85
            quote(theory_name))
wenzelm@68206
    86
      }
wenzelm@68206
    87
    Theory(theory_name, parents,
wenzelm@68203
    88
      if (types) read_types(db, session_name, theory_name) else Nil,
wenzelm@68208
    89
      if (consts) read_consts(db, session_name, theory_name) else Nil,
wenzelm@68232
    90
      if (axioms) read_axioms(db, session_name, theory_name) else Nil,
wenzelm@68264
    91
      if (facts) read_facts(db, session_name, theory_name) else Nil,
wenzelm@68264
    92
      if (classes) read_classes(db, session_name, theory_name) else Nil,
wenzelm@68264
    93
      if (typedefs) read_typedefs(db, session_name, theory_name) else Nil)
wenzelm@68203
    94
  }
wenzelm@68203
    95
wenzelm@68203
    96
wenzelm@68171
    97
  /* entities */
wenzelm@68171
    98
wenzelm@68172
    99
  sealed case class Entity(name: String, serial: Long, pos: Position.T)
wenzelm@68171
   100
  {
wenzelm@68171
   101
    override def toString: String = name
wenzelm@68171
   102
  }
wenzelm@68171
   103
wenzelm@68171
   104
  def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
wenzelm@68171
   105
  {
wenzelm@68171
   106
    def err(): Nothing = throw new XML.XML_Body(List(tree))
wenzelm@68171
   107
wenzelm@68171
   108
    tree match {
wenzelm@68171
   109
      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
wenzelm@68171
   110
        val name = Markup.Name.unapply(props) getOrElse err()
wenzelm@68171
   111
        val serial = Markup.Serial.unapply(props) getOrElse err()
wenzelm@68171
   112
        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
wenzelm@68172
   113
        (Entity(name, serial, pos), body)
wenzelm@68171
   114
      case _ => err()
wenzelm@68171
   115
    }
wenzelm@68171
   116
  }
wenzelm@68171
   117
wenzelm@68264
   118
  def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
wenzelm@68264
   119
    export_name: String, decode: XML.Body => List[A]): List[A] =
wenzelm@68264
   120
  {
wenzelm@68264
   121
    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
wenzelm@68264
   122
      case Some(entry) => decode(entry.uncompressed_yxml())
wenzelm@68264
   123
      case None => Nil
wenzelm@68264
   124
    }
wenzelm@68264
   125
  }
wenzelm@68264
   126
wenzelm@68203
   127
  def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
wenzelm@68203
   128
    export_name: String, decode: XML.Tree => A): List[A] =
wenzelm@68203
   129
  {
wenzelm@68264
   130
    read_export(db, session_name, theory_name, export_name,
wenzelm@68264
   131
      (body: XML.Body) => body.map(decode(_)))
wenzelm@68203
   132
  }
wenzelm@68203
   133
wenzelm@68171
   134
wenzelm@68171
   135
  /* types */
wenzelm@68171
   136
wenzelm@68171
   137
  sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
wenzelm@68171
   138
wenzelm@68203
   139
  def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
wenzelm@68203
   140
    read_entities(db, session_name, theory_name, "types",
wenzelm@68203
   141
      (tree: XML.Tree) =>
wenzelm@68203
   142
        {
wenzelm@68203
   143
          val (entity, body) = decode_entity(tree)
wenzelm@68203
   144
          val (args, abbrev) =
wenzelm@68203
   145
          {
wenzelm@68203
   146
            import XML.Decode._
wenzelm@68203
   147
            pair(list(string), option(Term_XML.Decode.typ))(body)
wenzelm@68203
   148
          }
wenzelm@68203
   149
          Type(entity, args, abbrev)
wenzelm@68203
   150
        })
wenzelm@68171
   151
wenzelm@68171
   152
wenzelm@68171
   153
  /* consts */
wenzelm@68171
   154
wenzelm@68173
   155
  sealed case class Const(
wenzelm@68173
   156
    entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
wenzelm@68171
   157
wenzelm@68203
   158
  def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
wenzelm@68203
   159
    read_entities(db, session_name, theory_name, "consts",
wenzelm@68203
   160
      (tree: XML.Tree) =>
wenzelm@68203
   161
        {
wenzelm@68203
   162
          val (entity, body) = decode_entity(tree)
wenzelm@68203
   163
          val (args, typ, abbrev) =
wenzelm@68203
   164
          {
wenzelm@68203
   165
            import XML.Decode._
wenzelm@68203
   166
            triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
wenzelm@68203
   167
          }
wenzelm@68203
   168
          Const(entity, args, typ, abbrev)
wenzelm@68203
   169
        })
wenzelm@68208
   170
wenzelm@68208
   171
wenzelm@68232
   172
  /* axioms and facts */
wenzelm@68232
   173
wenzelm@68232
   174
  def decode_props(body: XML.Body):
wenzelm@68232
   175
    (List[(String, Term.Sort)], List[(String, Term.Typ)], List[Term.Term]) =
wenzelm@68232
   176
  {
wenzelm@68232
   177
    import XML.Decode._
wenzelm@68232
   178
    import Term_XML.Decode._
wenzelm@68232
   179
    triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
wenzelm@68232
   180
  }
wenzelm@68208
   181
wenzelm@68208
   182
  sealed case class Axiom(
wenzelm@68208
   183
    entity: Entity,
wenzelm@68208
   184
    typargs: List[(String, Term.Sort)],
wenzelm@68208
   185
    args: List[(String, Term.Typ)],
wenzelm@68208
   186
    prop: Term.Term)
wenzelm@68208
   187
wenzelm@68208
   188
  def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
wenzelm@68208
   189
    read_entities(db, session_name, theory_name, "axioms",
wenzelm@68208
   190
      (tree: XML.Tree) =>
wenzelm@68208
   191
        {
wenzelm@68208
   192
          val (entity, body) = decode_entity(tree)
wenzelm@68232
   193
          val (typargs, args, List(prop)) = decode_props(body)
wenzelm@68208
   194
          Axiom(entity, typargs, args, prop)
wenzelm@68208
   195
        })
wenzelm@68232
   196
wenzelm@68232
   197
  sealed case class Fact(
wenzelm@68232
   198
    entity: Entity,
wenzelm@68232
   199
    typargs: List[(String, Term.Sort)],
wenzelm@68232
   200
    args: List[(String, Term.Typ)],
wenzelm@68232
   201
    props: List[Term.Term])
wenzelm@68232
   202
wenzelm@68232
   203
  def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
wenzelm@68232
   204
    read_entities(db, session_name, theory_name, "facts",
wenzelm@68232
   205
      (tree: XML.Tree) =>
wenzelm@68232
   206
        {
wenzelm@68232
   207
          val (entity, body) = decode_entity(tree)
wenzelm@68232
   208
          val (typargs, args, props) = decode_props(body)
wenzelm@68232
   209
          Fact(entity, typargs, args, props)
wenzelm@68232
   210
        })
wenzelm@68264
   211
wenzelm@68264
   212
wenzelm@68264
   213
  /* type classes */
wenzelm@68264
   214
wenzelm@68264
   215
  sealed case class Class(
wenzelm@68264
   216
    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
wenzelm@68264
   217
wenzelm@68264
   218
  def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
wenzelm@68264
   219
    read_entities(db, session_name, theory_name, "classes",
wenzelm@68264
   220
      (tree: XML.Tree) =>
wenzelm@68264
   221
        {
wenzelm@68264
   222
          val (entity, body) = decode_entity(tree)
wenzelm@68264
   223
          val (params, axioms) =
wenzelm@68264
   224
          {
wenzelm@68264
   225
            import XML.Decode._
wenzelm@68264
   226
            import Term_XML.Decode._
wenzelm@68264
   227
            pair(list(pair(string, typ)), list(term))(body)
wenzelm@68264
   228
          }
wenzelm@68264
   229
          Class(entity, params, axioms)
wenzelm@68264
   230
        })
wenzelm@68264
   231
wenzelm@68264
   232
wenzelm@68264
   233
  /* HOL typedefs */
wenzelm@68264
   234
wenzelm@68264
   235
  sealed case class Typedef(name: String,
wenzelm@68264
   236
    rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
wenzelm@68264
   237
wenzelm@68264
   238
  def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
wenzelm@68264
   239
    read_export(db, session_name, theory_name, "typedefs",
wenzelm@68264
   240
      (body: XML.Body) =>
wenzelm@68264
   241
        {
wenzelm@68264
   242
          val typedefs =
wenzelm@68264
   243
          {
wenzelm@68264
   244
            import XML.Decode._
wenzelm@68264
   245
            import Term_XML.Decode._
wenzelm@68264
   246
            list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
wenzelm@68264
   247
          }
wenzelm@68264
   248
          for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
wenzelm@68264
   249
          yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
wenzelm@68264
   250
        })
wenzelm@68171
   251
}