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