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