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