src/Pure/Thy/export_theory.scala
author wenzelm
Thu, 17 Oct 2019 21:03:59 +0200
changeset 70896 8017d382a0d7
parent 70891 f21a76a4d01f
child 70899 5f6dea6a7a4c
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/export_theory.scala
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     3
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     4
Export foundational theory content.
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     5
*/
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     6
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     8
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
     9
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    10
object Export_Theory
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    11
{
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    12
  /** session content **/
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    13
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    14
  sealed case class Session(name: String, theory_graph: Graph[String, Option[Theory]])
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    15
  {
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    16
    override def toString: String = name
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    17
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    18
    def theory(theory_name: String): Option[Theory] =
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    19
      if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name)
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    20
      else None
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    21
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    22
    def theories: List[Theory] =
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    23
      theory_graph.topological_order.flatMap(theory(_))
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    24
  }
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    25
70790
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    26
  def read_session(
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    27
    store: Sessions.Store,
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    28
    sessions_structure: Sessions.Structure,
68209
aeffd8f1f079 support Store with options;
wenzelm
parents: 68208
diff changeset
    29
    session_name: String,
70790
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    30
    progress: Progress = No_Progress,
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    31
    types: Boolean = true,
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
    32
    consts: Boolean = true,
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
    33
    axioms: Boolean = true,
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
    34
    thms: Boolean = true,
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
    35
    classes: Boolean = true,
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
    36
    locales: Boolean = true,
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
    37
    locale_dependencies: Boolean = true,
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
    38
    classrel: Boolean = true,
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
    39
    arities: Boolean = true,
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
    40
    typedefs: Boolean = true,
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
    41
    cache: Term.Cache = Term.make_cache()): Session =
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    42
  {
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    43
    val thys =
70790
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    44
      sessions_structure.build_requirements(List(session_name)).flatMap(session =>
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    45
        using(store.open_database(session))(db =>
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    46
        {
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    47
          db.transaction {
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    48
            for (theory <- Export.read_theory_names(db, session))
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    49
            yield {
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    50
              progress.echo("Reading theory " + theory)
70891
wenzelm
parents: 70890
diff changeset
    51
              read_theory(Export.Provider.database(db, session, theory),
wenzelm
parents: 70890
diff changeset
    52
                session, theory, types = types, consts = consts,
wenzelm
parents: 70890
diff changeset
    53
                axioms = axioms, thms = thms, classes = classes, locales = locales,
wenzelm
parents: 70890
diff changeset
    54
                locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
wenzelm
parents: 70890
diff changeset
    55
                typedefs = typedefs, cache = Some(cache))
70790
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    56
            }
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    57
          }
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    58
        }))
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    59
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    60
    val graph0 =
70890
15ad4c045590 more robust;
wenzelm
parents: 70884
diff changeset
    61
      (Graph.string[Option[Theory]] /: thys) {
15ad4c045590 more robust;
wenzelm
parents: 70884
diff changeset
    62
        case (g, thy) => g.default_node(thy.name, Some(thy)) }
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    63
    val graph1 =
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    64
      (graph0 /: thys) { case (g0, thy) =>
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    65
        (g0 /: thy.parents) { case (g1, parent) =>
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    66
          g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) } }
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    67
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    68
    Session(session_name, graph1)
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    69
  }
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    70
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    71
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    72
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
    73
  /** theory content **/
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
    74
68346
b44010800a19 tuned signature;
wenzelm
parents: 68295
diff changeset
    75
  val export_prefix: String = "theory/"
70539
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70534
diff changeset
    76
  val export_prefix_proofs: String = "proofs/"
68346
b44010800a19 tuned signature;
wenzelm
parents: 68295
diff changeset
    77
68208
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
    78
  sealed case class Theory(name: String, parents: List[String],
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
    79
    types: List[Type],
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
    80
    consts: List[Const],
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
    81
    axioms: List[Axiom],
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
    82
    thms: List[Thm],
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
    83
    classes: List[Class],
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
    84
    locales: List[Locale],
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
    85
    locale_dependencies: List[Locale_Dependency],
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
    86
    classrel: List[Classrel],
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
    87
    arities: List[Arity],
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
    88
    typedefs: List[Typedef])
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    89
  {
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    90
    override def toString: String = name
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
    91
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    92
    def entity_iterator: Iterator[Entity] =
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    93
      types.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    94
      consts.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    95
      axioms.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    96
      thms.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    97
      classes.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    98
      locales.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    99
      locale_dependencies.iterator.map(_.entity)
68711
d1d03b7b6696 tuned signature;
wenzelm
parents: 68710
diff changeset
   100
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   101
    def cache(cache: Term.Cache): Theory =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   102
      Theory(cache.string(name),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   103
        parents.map(cache.string(_)),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   104
        types.map(_.cache(cache)),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   105
        consts.map(_.cache(cache)),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   106
        axioms.map(_.cache(cache)),
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   107
        thms.map(_.cache(cache)),
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   108
        classes.map(_.cache(cache)),
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   109
        locales.map(_.cache(cache)),
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   110
        locale_dependencies.map(_.cache(cache)),
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   111
        classrel.map(_.cache(cache)),
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   112
        arities.map(_.cache(cache)),
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   113
        typedefs.map(_.cache(cache)))
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
   114
  }
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
   115
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   116
  def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   117
    types: Boolean = true,
68208
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   118
    consts: Boolean = true,
68232
4b93573ac5b4 export facts;
wenzelm
parents: 68231
diff changeset
   119
    axioms: Boolean = true,
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   120
    thms: Boolean = true,
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   121
    classes: Boolean = true,
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   122
    locales: Boolean = true,
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   123
    locale_dependencies: Boolean = true,
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   124
    classrel: Boolean = true,
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   125
    arities: Boolean = true,
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   126
    typedefs: Boolean = true,
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   127
    cache: Option[Term.Cache] = None): Theory =
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   128
  {
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
   129
    val parents =
70891
wenzelm
parents: 70890
diff changeset
   130
      if (theory_name == Thy_Header.PURE) Nil
wenzelm
parents: 70890
diff changeset
   131
      else {
wenzelm
parents: 70890
diff changeset
   132
        provider(export_prefix + "parents") match {
wenzelm
parents: 70890
diff changeset
   133
          case Some(entry) => split_lines(entry.uncompressed().text)
wenzelm
parents: 70890
diff changeset
   134
          case None =>
wenzelm
parents: 70890
diff changeset
   135
            error("Missing theory export in session " + quote(session_name) + ": " +
wenzelm
parents: 70890
diff changeset
   136
              quote(theory_name))
wenzelm
parents: 70890
diff changeset
   137
        }
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
   138
      }
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   139
    val theory =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   140
      Theory(theory_name, parents,
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   141
        if (types) read_types(provider) else Nil,
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   142
        if (consts) read_consts(provider) else Nil,
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   143
        if (axioms) read_axioms(provider) else Nil,
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   144
        if (thms) read_thms(provider) else Nil,
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   145
        if (classes) read_classes(provider) else Nil,
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   146
        if (locales) read_locales(provider) else Nil,
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   147
        if (locale_dependencies) read_locale_dependencies(provider) else Nil,
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   148
        if (classrel) read_classrel(provider) else Nil,
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   149
        if (arities) read_arities(provider) else Nil,
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   150
        if (typedefs) read_typedefs(provider) else Nil)
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   151
    if (cache.isDefined) theory.cache(cache.get) else theory
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   152
  }
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   153
70883
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   154
  def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A =
68710
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   155
  {
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   156
    val session_name = Thy_Header.PURE
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   157
    val theory_name = Thy_Header.PURE
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   158
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   159
    using(store.open_database(session_name))(db =>
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   160
    {
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   161
      db.transaction {
70883
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   162
        read(Export.Provider.database(db, session_name, theory_name), session_name, theory_name)
68710
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   163
      }
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   164
    })
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   165
  }
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   166
70883
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   167
  def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   168
    read_pure(store, read_theory(_, _, _, cache = cache))
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   169
70884
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   170
  def read_pure_proof(store: Sessions.Store, id: Thm_Id, cache: Option[Term.Cache] = None): Proof =
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   171
    read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache))
70883
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   172
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   173
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   174
  /* entities */
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   175
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   176
  object Kind extends Enumeration
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   177
  {
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   178
    val TYPE = Value("type")
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   179
    val CONST = Value("const")
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   180
    val AXIOM = Value("axiom")
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   181
    val THM = Value("thm")
70882
dbc82c54f6f0 support for proof terms;
wenzelm
parents: 70881
diff changeset
   182
    val PROOF = Value("proof")
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   183
    val CLASS = Value("class")
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   184
    val LOCALE = Value("locale")
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   185
    val LOCALE_DEPENDENCY = Value("locale_dependency")
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   186
  }
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   187
68835
2e59da922630 more robust: Pure entities may lack id;
wenzelm
parents: 68830
diff changeset
   188
  sealed case class Entity(
68997
4278947ba336 more exports;
wenzelm
parents: 68864
diff changeset
   189
    kind: Kind.Value, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long)
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   190
  {
68718
ce18a3924864 tuned output;
wenzelm
parents: 68717
diff changeset
   191
    override def toString: String = kind.toString + " " + quote(name)
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   192
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   193
    def cache(cache: Term.Cache): Entity =
68997
4278947ba336 more exports;
wenzelm
parents: 68864
diff changeset
   194
      Entity(kind, cache.string(name), cache.string(xname), cache.position(pos), id, serial)
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   195
  }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   196
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   197
  def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   198
  {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   199
    def err(): Nothing = throw new XML.XML_Body(List(tree))
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   200
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   201
    tree match {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   202
      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   203
        val name = Markup.Name.unapply(props) getOrElse err()
68997
4278947ba336 more exports;
wenzelm
parents: 68864
diff changeset
   204
        val xname = Markup.XName.unapply(props) getOrElse err()
68830
44ec6fdaacf8 retain original id, which is command_id/exec_id for PIDE;
wenzelm
parents: 68726
diff changeset
   205
        val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
68835
2e59da922630 more robust: Pure entities may lack id;
wenzelm
parents: 68830
diff changeset
   206
        val id = Position.Id.unapply(props)
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   207
        val serial = Markup.Serial.unapply(props) getOrElse err()
68997
4278947ba336 more exports;
wenzelm
parents: 68864
diff changeset
   208
        (Entity(kind, name, xname, pos, id, serial), body)
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   209
      case _ => err()
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   210
    }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   211
  }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   212
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   213
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   214
  /* approximative syntax */
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   215
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   216
  object Assoc extends Enumeration
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   217
  {
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   218
    val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   219
  }
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   220
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   221
  sealed abstract class Syntax
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   222
  case object No_Syntax extends Syntax
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   223
  case class Prefix(delim: String) extends Syntax
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   224
  case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   225
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   226
  def decode_syntax: XML.Decode.T[Syntax] =
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   227
    XML.Decode.variant(List(
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   228
      { case (Nil, Nil) => No_Syntax },
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   229
      { case (List(delim), Nil) => Prefix(delim) },
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   230
      { case (Nil, body) =>
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   231
          import XML.Decode._
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   232
          val (ass, delim, pri) = triple(int, string, int)(body)
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   233
          Infix(Assoc(ass), delim, pri) }))
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   234
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   235
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   236
  /* types */
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   237
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   238
  sealed case class Type(
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   239
    entity: Entity, syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   240
  {
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   241
    def cache(cache: Term.Cache): Type =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   242
      Type(entity.cache(cache),
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   243
        syntax,
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   244
        args.map(cache.string(_)),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   245
        abbrev.map(cache.typ(_)))
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   246
  }
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   247
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   248
  def read_types(provider: Export.Provider): List[Type] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   249
    provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   250
      {
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   251
        val (entity, body) = decode_entity(Kind.TYPE, tree)
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   252
        val (syntax, args, abbrev) =
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   253
        {
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   254
          import XML.Decode._
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   255
          triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   256
        }
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   257
        Type(entity, syntax, args, abbrev)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   258
      })
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   259
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   260
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   261
  /* consts */
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   262
68173
7ed88a534bb6 more uniform types vs. consts;
wenzelm
parents: 68172
diff changeset
   263
  sealed case class Const(
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   264
    entity: Entity,
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   265
    syntax: Syntax,
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   266
    typargs: List[String],
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   267
    typ: Term.Typ,
69988
6fa51a36b7f7 export propositional status of consts;
wenzelm
parents: 69077
diff changeset
   268
    abbrev: Option[Term.Term],
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69988
diff changeset
   269
    propositional: Boolean,
69996
8f2d3a27aff0 more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents: 69992
diff changeset
   270
    primrec_types: List[String],
8f2d3a27aff0 more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents: 69992
diff changeset
   271
    corecursive: Boolean)
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   272
  {
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   273
    def cache(cache: Term.Cache): Const =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   274
      Const(entity.cache(cache),
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   275
        syntax,
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   276
        typargs.map(cache.string(_)),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   277
        cache.typ(typ),
69988
6fa51a36b7f7 export propositional status of consts;
wenzelm
parents: 69077
diff changeset
   278
        abbrev.map(cache.term(_)),
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69988
diff changeset
   279
        propositional,
69996
8f2d3a27aff0 more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents: 69992
diff changeset
   280
        primrec_types.map(cache.string(_)),
8f2d3a27aff0 more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents: 69992
diff changeset
   281
        corecursive)
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   282
  }
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   283
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   284
  def read_consts(provider: Export.Provider): List[Const] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   285
    provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   286
      {
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   287
        val (entity, body) = decode_entity(Kind.CONST, tree)
69996
8f2d3a27aff0 more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents: 69992
diff changeset
   288
        val (syntax, (args, (typ, (abbrev, (propositional, (primrec_types, corecursive)))))) =
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   289
        {
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   290
          import XML.Decode._
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69988
diff changeset
   291
          pair(decode_syntax,
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69988
diff changeset
   292
            pair(list(string),
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69988
diff changeset
   293
              pair(Term_XML.Decode.typ,
69996
8f2d3a27aff0 more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents: 69992
diff changeset
   294
                pair(option(Term_XML.Decode.term), pair(bool,
8f2d3a27aff0 more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents: 69992
diff changeset
   295
                  pair(list(string), bool))))))(body)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   296
        }
69996
8f2d3a27aff0 more informative Spec_Rules.Equational: support corecursion;
wenzelm
parents: 69992
diff changeset
   297
        Const(entity, syntax, args, typ, abbrev, propositional, primrec_types, corecursive)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   298
      })
68208
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   299
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   300
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   301
  /* axioms */
68232
4b93573ac5b4 export facts;
wenzelm
parents: 68231
diff changeset
   302
68726
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   303
  sealed case class Prop(
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   304
    typargs: List[(String, Term.Sort)],
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   305
    args: List[(String, Term.Typ)],
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   306
    term: Term.Term)
68232
4b93573ac5b4 export facts;
wenzelm
parents: 68231
diff changeset
   307
  {
68726
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   308
    def cache(cache: Term.Cache): Prop =
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   309
      Prop(
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   310
        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   311
        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   312
        cache.term(term))
68232
4b93573ac5b4 export facts;
wenzelm
parents: 68231
diff changeset
   313
  }
68208
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   314
68726
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   315
  def decode_prop(body: XML.Body): Prop =
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   316
  {
68726
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   317
    val (typargs, args, t) =
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   318
    {
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   319
      import XML.Decode._
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   320
      import Term_XML.Decode._
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   321
      triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   322
    }
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   323
    Prop(typargs, args, t)
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   324
  }
68208
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   325
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   326
  sealed case class Axiom(entity: Entity, prop: Prop)
70534
fb876ebbf5a7 export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents: 70384
diff changeset
   327
  {
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   328
    def cache(cache: Term.Cache): Axiom =
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   329
      Axiom(entity.cache(cache), prop.cache(cache))
70534
fb876ebbf5a7 export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents: 70384
diff changeset
   330
  }
fb876ebbf5a7 export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents: 70384
diff changeset
   331
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   332
  def read_axioms(provider: Export.Provider): List[Axiom] =
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   333
    provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   334
      {
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   335
        val (entity, body) = decode_entity(Kind.AXIOM, tree)
68726
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   336
        val prop = decode_prop(body)
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   337
        Axiom(entity, prop)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   338
      })
68232
4b93573ac5b4 export facts;
wenzelm
parents: 68231
diff changeset
   339
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   340
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   341
  /* theorems */
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   342
70884
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   343
  sealed case class Thm_Id(serial: Long, theory_name: String)
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   344
  {
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   345
    def pure: Boolean = theory_name == Thy_Header.PURE
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   346
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   347
    def cache(cache: Term.Cache): Thm_Id =
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   348
      Thm_Id(serial, cache.string(theory_name))
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   349
  }
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   350
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   351
  sealed case class Thm(
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   352
    entity: Entity,
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   353
    prop: Prop,
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   354
    deps: List[String],
70896
8017d382a0d7 tuned signature;
wenzelm
parents: 70891
diff changeset
   355
    proof_boxes: List[Thm_Id],
8017d382a0d7 tuned signature;
wenzelm
parents: 70891
diff changeset
   356
    proof: Term.Proof)
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   357
  {
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   358
    def cache(cache: Term.Cache): Thm =
70884
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   359
      Thm(
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   360
        entity.cache(cache),
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   361
        prop.cache(cache),
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   362
        deps.map(cache.string _),
70896
8017d382a0d7 tuned signature;
wenzelm
parents: 70891
diff changeset
   363
        proof_boxes.map(_.cache(cache)),
8017d382a0d7 tuned signature;
wenzelm
parents: 70891
diff changeset
   364
        cache.proof(proof))
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   365
  }
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   366
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   367
  def read_thms(provider: Export.Provider): List[Thm] =
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   368
    provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   369
      {
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   370
        val (entity, body) = decode_entity(Kind.THM, tree)
70896
8017d382a0d7 tuned signature;
wenzelm
parents: 70891
diff changeset
   371
        val (prop, (deps, (prf_boxes, prf))) =
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   372
        {
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   373
          import XML.Decode._
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   374
          import Term_XML.Decode._
70884
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   375
          def thm_id(body: XML.Body): Thm_Id =
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   376
          {
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   377
            val (serial, theory_name) = pair(long, string)(body)
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   378
            Thm_Id(serial, theory_name)
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   379
          }
70896
8017d382a0d7 tuned signature;
wenzelm
parents: 70891
diff changeset
   380
          pair(decode_prop _, pair(list(string), pair(list(thm_id), proof)))(body)
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   381
        }
70896
8017d382a0d7 tuned signature;
wenzelm
parents: 70891
diff changeset
   382
        Thm(entity, prop, deps, prf_boxes, prf)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   383
      })
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   384
70881
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   385
  sealed case class Proof(
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   386
    typargs: List[(String, Term.Sort)],
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   387
    args: List[(String, Term.Typ)],
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   388
    term: Term.Term,
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   389
    proof: Term.Proof)
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   390
  {
70883
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   391
    def prop: Prop = Prop(typargs, args, term)
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   392
70881
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   393
    def cache(cache: Term.Cache): Proof =
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   394
      Proof(
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   395
        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   396
        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   397
        cache.term(term),
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   398
        cache.proof(proof))
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   399
  }
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   400
70884
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   401
  def read_proof(provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Proof =
70539
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70534
diff changeset
   402
  {
70884
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   403
    val body = provider.focus(id.theory_name).uncompressed_yxml(export_prefix_proofs + id.serial)
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   404
    if (body.isEmpty) error("Bad proof export " + id.serial)
70843
cc987440d776 more compact XML: separate environment for free variables;
wenzelm
parents: 70790
diff changeset
   405
70881
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   406
    val (typargs, (args, (prop_body, proof_body))) =
70843
cc987440d776 more compact XML: separate environment for free variables;
wenzelm
parents: 70790
diff changeset
   407
    {
cc987440d776 more compact XML: separate environment for free variables;
wenzelm
parents: 70790
diff changeset
   408
      import XML.Decode._
cc987440d776 more compact XML: separate environment for free variables;
wenzelm
parents: 70790
diff changeset
   409
      import Term_XML.Decode._
70881
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   410
      pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(x => x, x => x)))(body)
70843
cc987440d776 more compact XML: separate environment for free variables;
wenzelm
parents: 70790
diff changeset
   411
    }
70881
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   412
    val env = args.toMap
70843
cc987440d776 more compact XML: separate environment for free variables;
wenzelm
parents: 70790
diff changeset
   413
    val prop = Term_XML.Decode.term_env(env)(prop_body)
cc987440d776 more compact XML: separate environment for free variables;
wenzelm
parents: 70790
diff changeset
   414
    val proof = Term_XML.Decode.proof_env(env)(proof_body)
cc987440d776 more compact XML: separate environment for free variables;
wenzelm
parents: 70790
diff changeset
   415
70884
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   416
    val result = Proof(typargs, args, prop, proof)
70881
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   417
    cache.map(result.cache(_)) getOrElse result
70539
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70534
diff changeset
   418
  }
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70534
diff changeset
   419
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   420
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   421
  /* type classes */
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   422
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   423
  sealed case class Class(
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 69019
diff changeset
   424
    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Prop])
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   425
  {
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   426
    def cache(cache: Term.Cache): Class =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   427
      Class(entity.cache(cache),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   428
        params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 69019
diff changeset
   429
        axioms.map(_.cache(cache)))
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   430
  }
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   431
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   432
  def read_classes(provider: Export.Provider): List[Class] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   433
    provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   434
      {
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   435
        val (entity, body) = decode_entity(Kind.CLASS, tree)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   436
        val (params, axioms) =
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   437
        {
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   438
          import XML.Decode._
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   439
          import Term_XML.Decode._
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 69019
diff changeset
   440
          pair(list(pair(string, typ)), list(decode_prop))(body)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   441
        }
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   442
        Class(entity, params, axioms)
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   443
      })
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   444
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   445
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   446
  /* locales */
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   447
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   448
  sealed case class Locale(
69019
a6ba77af6486 export semi-unfolded locale axioms;
wenzelm
parents: 69003
diff changeset
   449
    entity: Entity,
a6ba77af6486 export semi-unfolded locale axioms;
wenzelm
parents: 69003
diff changeset
   450
    typargs: List[(String, Term.Sort)],
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   451
    args: List[((String, Term.Typ), Syntax)],
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 69019
diff changeset
   452
    axioms: List[Prop])
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   453
  {
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   454
    def cache(cache: Term.Cache): Locale =
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   455
      Locale(entity.cache(cache),
68864
1dacce27bc25 clarified signature: proper typargs;
wenzelm
parents: 68862
diff changeset
   456
        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
69076
90cce2f79e77 proper syntax for locale vs. class parameters;
wenzelm
parents: 69069
diff changeset
   457
        args.map({ case ((name, typ), syntax) => ((cache.string(name), cache.typ(typ)), syntax) }),
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 69019
diff changeset
   458
        axioms.map(_.cache(cache)))
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   459
  }
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   460
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   461
  def read_locales(provider: Export.Provider): List[Locale] =
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   462
    provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   463
      {
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   464
        val (entity, body) = decode_entity(Kind.LOCALE, tree)
69019
a6ba77af6486 export semi-unfolded locale axioms;
wenzelm
parents: 69003
diff changeset
   465
        val (typargs, args, axioms) =
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   466
        {
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   467
          import XML.Decode._
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   468
          import Term_XML.Decode._
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   469
          triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)),
69076
90cce2f79e77 proper syntax for locale vs. class parameters;
wenzelm
parents: 69069
diff changeset
   470
            list(decode_prop))(body)
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   471
        }
69019
a6ba77af6486 export semi-unfolded locale axioms;
wenzelm
parents: 69003
diff changeset
   472
        Locale(entity, typargs, args, axioms)
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   473
      })
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   474
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   475
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   476
  /* locale dependencies */
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   477
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   478
  sealed case class Locale_Dependency(
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   479
    entity: Entity,
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   480
    source: String,
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   481
    target: String,
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   482
    prefix: List[(String, Boolean)],
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   483
    subst_types: List[((String, Term.Sort), Term.Typ)],
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   484
    subst_terms: List[((String, Term.Typ), Term.Term)])
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   485
  {
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   486
    def cache(cache: Term.Cache): Locale_Dependency =
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   487
      Locale_Dependency(entity.cache(cache),
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   488
        cache.string(source),
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   489
        cache.string(target),
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   490
        prefix.map({ case (name, mandatory) => (cache.string(name), mandatory) }),
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   491
        subst_types.map({ case ((a, s), ty) => ((cache.string(a), cache.sort(s)), cache.typ(ty)) }),
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   492
        subst_terms.map({ case ((x, ty), t) => ((cache.string(x), cache.typ(ty)), cache.term(t)) }))
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   493
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   494
    def is_inclusion: Boolean =
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   495
      subst_types.isEmpty && subst_terms.isEmpty
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   496
  }
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   497
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   498
  def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] =
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   499
    provider.uncompressed_yxml(export_prefix + "locale_dependencies").map((tree: XML.Tree) =>
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   500
      {
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   501
        val (entity, body) = decode_entity(Kind.LOCALE_DEPENDENCY, tree)
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   502
        val (source, (target, (prefix, (subst_types, subst_terms)))) =
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   503
        {
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   504
          import XML.Decode._
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   505
          import Term_XML.Decode._
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   506
          pair(string, pair(string, pair(list(pair(string, bool)),
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   507
            pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body)
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   508
        }
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   509
        Locale_Dependency(entity, source, target, prefix, subst_types, subst_terms)
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   510
      })
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   511
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   512
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   513
  /* sort algebra */
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   514
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   515
  sealed case class Classrel(class1: String, class2: String, prop: Prop)
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   516
  {
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   517
    def cache(cache: Term.Cache): Classrel =
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   518
      Classrel(cache.string(class1), cache.string(class2), prop.cache(cache))
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   519
  }
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   520
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   521
  def read_classrel(provider: Export.Provider): List[Classrel] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   522
  {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   523
    val body = provider.uncompressed_yxml(export_prefix + "classrel")
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   524
    val classrel =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   525
    {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   526
      import XML.Decode._
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   527
      list(pair(decode_prop, pair(string, string)))(body)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   528
    }
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   529
    for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   530
  }
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   531
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   532
  sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String, prop: Prop)
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   533
  {
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   534
    def cache(cache: Term.Cache): Arity =
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   535
      Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain),
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   536
        prop.cache(cache))
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   537
  }
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   538
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   539
  def read_arities(provider: Export.Provider): List[Arity] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   540
  {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   541
    val body = provider.uncompressed_yxml(export_prefix + "arities")
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   542
    val arities =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   543
    {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   544
      import XML.Decode._
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   545
      import Term_XML.Decode._
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   546
      list(pair(decode_prop, triple(string, list(sort), string)))(body)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   547
    }
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   548
    for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   549
  }
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   550
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   551
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   552
  /* HOL typedefs */
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   553
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   554
  sealed case class Typedef(name: String,
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   555
    rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   556
  {
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   557
    def cache(cache: Term.Cache): Typedef =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   558
      Typedef(cache.string(name),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   559
        cache.typ(rep_type),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   560
        cache.typ(abs_type),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   561
        cache.string(rep_name),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   562
        cache.string(abs_name),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   563
        cache.string(axiom_name))
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   564
  }
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   565
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   566
  def read_typedefs(provider: Export.Provider): List[Typedef] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   567
  {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   568
    val body = provider.uncompressed_yxml(export_prefix + "typedefs")
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   569
    val typedefs =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   570
    {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   571
      import XML.Decode._
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   572
      import Term_XML.Decode._
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   573
      list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   574
    }
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   575
    for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   576
    yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   577
  }
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   578
}