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