src/Pure/Thy/export_theory.scala
author wenzelm
Fri, 06 Dec 2019 16:13:36 +0100
changeset 71251 297d24fb262c
parent 71248 adf5e53d2b2b
child 71601 97ccf48c2f0c
permissions -rw-r--r--
discontinued somewhat pointless options;
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
71015
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
    10
import scala.collection.immutable.SortedMap
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
    11
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
    12
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    13
object Export_Theory
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
    14
{
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    15
  /** session content **/
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    16
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    17
  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
    18
  {
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    19
    override def toString: String = name
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    20
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    21
    def theory(theory_name: String): Option[Theory] =
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    22
      if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name)
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    23
      else None
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
    def theories: List[Theory] =
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    26
      theory_graph.topological_order.flatMap(theory(_))
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    27
  }
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    28
70790
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    29
  def read_session(
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    30
    store: Sessions.Store,
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    31
    sessions_structure: Sessions.Structure,
68209
aeffd8f1f079 support Store with options;
wenzelm
parents: 68208
diff changeset
    32
    session_name: String,
70790
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    33
    progress: Progress = No_Progress,
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
    34
    cache: Term.Cache = Term.make_cache()): Session =
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    35
  {
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    36
    val thys =
70790
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    37
      sessions_structure.build_requirements(List(session_name)).flatMap(session =>
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    38
        using(store.open_database(session))(db =>
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    39
        {
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    40
          db.transaction {
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    41
            for (theory <- Export.read_theory_names(db, session))
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    42
            yield {
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    43
              progress.echo("Reading theory " + theory)
70891
wenzelm
parents: 70890
diff changeset
    44
              read_theory(Export.Provider.database(db, session, theory),
71251
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
    45
                session, theory, cache = Some(cache))
70790
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
          }
73514ccad7a6 clarified signature: read full session requirements;
wenzelm
parents: 70789
diff changeset
    48
        }))
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    49
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    50
    val graph0 =
70890
15ad4c045590 more robust;
wenzelm
parents: 70884
diff changeset
    51
      (Graph.string[Option[Theory]] /: thys) {
15ad4c045590 more robust;
wenzelm
parents: 70884
diff changeset
    52
        case (g, thy) => g.default_node(thy.name, Some(thy)) }
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    53
    val graph1 =
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    54
      (graph0 /: thys) { case (g0, thy) =>
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    55
        (g0 /: thy.parents) { case (g1, parent) =>
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    56
          g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) } }
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    57
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    58
    Session(session_name, graph1)
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
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    61
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    62
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
    63
  /** theory content **/
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
    64
68346
b44010800a19 tuned signature;
wenzelm
parents: 68295
diff changeset
    65
  val export_prefix: String = "theory/"
70539
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70534
diff changeset
    66
  val export_prefix_proofs: String = "proofs/"
68346
b44010800a19 tuned signature;
wenzelm
parents: 68295
diff changeset
    67
68208
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
    68
  sealed case class Theory(name: String, parents: List[String],
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
    69
    types: List[Type],
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
    70
    consts: List[Const],
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
    71
    axioms: List[Axiom],
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
    72
    thms: List[Thm],
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
    73
    classes: List[Class],
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
    74
    locales: List[Locale],
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
    75
    locale_dependencies: List[Locale_Dependency],
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
    76
    classrel: List[Classrel],
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
    77
    arities: List[Arity],
70920
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
    78
    constdefs: List[Constdef],
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
    79
    typedefs: List[Typedef],
71248
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
    80
    datatypes: List[Datatype],
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
    81
    spec_rules: List[Spec_Rule])
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    82
  {
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
    83
    override def toString: String = name
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
    84
70789
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    85
    def entity_iterator: Iterator[Entity] =
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    86
      types.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    87
      consts.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    88
      axioms.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    89
      thms.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    90
      classes.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    91
      locales.iterator.map(_.entity) ++
89f6af1b483f clarified signature;
wenzelm
parents: 70597
diff changeset
    92
      locale_dependencies.iterator.map(_.entity)
68711
d1d03b7b6696 tuned signature;
wenzelm
parents: 68710
diff changeset
    93
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
    94
    def cache(cache: Term.Cache): Theory =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
    95
      Theory(cache.string(name),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
    96
        parents.map(cache.string(_)),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
    97
        types.map(_.cache(cache)),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
    98
        consts.map(_.cache(cache)),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
    99
        axioms.map(_.cache(cache)),
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   100
        thms.map(_.cache(cache)),
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   101
        classes.map(_.cache(cache)),
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   102
        locales.map(_.cache(cache)),
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   103
        locale_dependencies.map(_.cache(cache)),
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   104
        classrel.map(_.cache(cache)),
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   105
        arities.map(_.cache(cache)),
70920
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   106
        constdefs.map(_.cache(cache)),
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   107
        typedefs.map(_.cache(cache)),
71248
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   108
        datatypes.map(_.cache(cache)),
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   109
        spec_rules.map(_.cache(cache)))
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
   110
  }
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
   111
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   112
  def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   113
    cache: Option[Term.Cache] = None): Theory =
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   114
  {
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
   115
    val parents =
70891
wenzelm
parents: 70890
diff changeset
   116
      if (theory_name == Thy_Header.PURE) Nil
wenzelm
parents: 70890
diff changeset
   117
      else {
wenzelm
parents: 70890
diff changeset
   118
        provider(export_prefix + "parents") match {
wenzelm
parents: 70890
diff changeset
   119
          case Some(entry) => split_lines(entry.uncompressed().text)
wenzelm
parents: 70890
diff changeset
   120
          case None =>
wenzelm
parents: 70890
diff changeset
   121
            error("Missing theory export in session " + quote(session_name) + ": " +
wenzelm
parents: 70890
diff changeset
   122
              quote(theory_name))
wenzelm
parents: 70890
diff changeset
   123
        }
68206
dedf1a70d1fa export more theory and session structure;
wenzelm
parents: 68203
diff changeset
   124
      }
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   125
    val theory =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   126
      Theory(theory_name, parents,
71251
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   127
        read_types(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   128
        read_consts(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   129
        read_axioms(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   130
        read_thms(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   131
        read_classes(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   132
        read_locales(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   133
        read_locale_dependencies(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   134
        read_classrel(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   135
        read_arities(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   136
        read_constdefs(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   137
        read_typedefs(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   138
        read_datatypes(provider),
297d24fb262c discontinued somewhat pointless options;
wenzelm
parents: 71248
diff changeset
   139
        read_spec_rules(provider))
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   140
    if (cache.isDefined) theory.cache(cache.get) else theory
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   141
  }
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   142
70883
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   143
  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
   144
  {
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   145
    val session_name = Thy_Header.PURE
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   146
    val theory_name = Thy_Header.PURE
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   147
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   148
    using(store.open_database(session_name))(db =>
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   149
    {
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   150
      db.transaction {
70883
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   151
        read(Export.Provider.database(db, session_name, theory_name), session_name, theory_name)
68710
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   152
      }
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   153
    })
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   154
  }
3db37e950118 always export Pure theory;
wenzelm
parents: 68418
diff changeset
   155
70883
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   156
  def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   157
    read_pure(store, read_theory(_, _, _, cache = cache))
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   158
70899
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   159
  def read_pure_proof(
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   160
      store: Sessions.Store, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
70884
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   161
    read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache))
70883
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   162
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   163
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   164
  /* entities */
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   165
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   166
  object Kind extends Enumeration
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   167
  {
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   168
    val TYPE = Value("type")
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   169
    val CONST = Value("const")
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   170
    val AXIOM = Value("axiom")
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   171
    val THM = Value("thm")
70882
dbc82c54f6f0 support for proof terms;
wenzelm
parents: 70881
diff changeset
   172
    val PROOF = Value("proof")
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   173
    val CLASS = Value("class")
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   174
    val LOCALE = Value("locale")
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   175
    val LOCALE_DEPENDENCY = Value("locale_dependency")
70913
935c78a90ee0 more kinds, notably for Isabelle/MMT;
wenzelm
parents: 70899
diff changeset
   176
    val DOCUMENT_HEADING = Value("document_heading")
935c78a90ee0 more kinds, notably for Isabelle/MMT;
wenzelm
parents: 70899
diff changeset
   177
    val DOCUMENT_TEXT = Value("document_text")
935c78a90ee0 more kinds, notably for Isabelle/MMT;
wenzelm
parents: 70899
diff changeset
   178
    val PROOF_TEXT = Value("proof_text")
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   179
  }
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   180
68835
2e59da922630 more robust: Pure entities may lack id;
wenzelm
parents: 68830
diff changeset
   181
  sealed case class Entity(
68997
4278947ba336 more exports;
wenzelm
parents: 68864
diff changeset
   182
    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
   183
  {
68718
ce18a3924864 tuned output;
wenzelm
parents: 68717
diff changeset
   184
    override def toString: String = kind.toString + " " + quote(name)
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   185
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   186
    def cache(cache: Term.Cache): Entity =
68997
4278947ba336 more exports;
wenzelm
parents: 68864
diff changeset
   187
      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
   188
  }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   189
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   190
  def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   191
  {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   192
    def err(): Nothing = throw new XML.XML_Body(List(tree))
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   193
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   194
    tree match {
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   195
      case XML.Elem(Markup(Markup.ENTITY, props), body) =>
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   196
        val name = Markup.Name.unapply(props) getOrElse err()
68997
4278947ba336 more exports;
wenzelm
parents: 68864
diff changeset
   197
        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
   198
        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
   199
        val id = Position.Id.unapply(props)
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   200
        val serial = Markup.Serial.unapply(props) getOrElse err()
68997
4278947ba336 more exports;
wenzelm
parents: 68864
diff changeset
   201
        (Entity(kind, name, xname, pos, id, serial), body)
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   202
      case _ => err()
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   203
    }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   204
  }
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   205
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   206
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   207
  /* approximative syntax */
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   208
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   209
  object Assoc extends Enumeration
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   210
  {
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   211
    val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   212
  }
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   213
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   214
  sealed abstract class Syntax
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   215
  case object No_Syntax extends Syntax
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   216
  case class Prefix(delim: String) extends Syntax
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   217
  case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   218
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   219
  def decode_syntax: XML.Decode.T[Syntax] =
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   220
    XML.Decode.variant(List(
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   221
      { case (Nil, Nil) => No_Syntax },
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   222
      { case (List(delim), Nil) => Prefix(delim) },
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   223
      { case (Nil, body) =>
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   224
          import XML.Decode._
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   225
          val (ass, delim, pri) = triple(int, string, int)(body)
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   226
          Infix(Assoc(ass), delim, pri) }))
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   227
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   228
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   229
  /* types */
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   230
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   231
  sealed case class Type(
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   232
    entity: Entity, syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   233
  {
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   234
    def cache(cache: Term.Cache): Type =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   235
      Type(entity.cache(cache),
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   236
        syntax,
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   237
        args.map(cache.string(_)),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   238
        abbrev.map(cache.typ(_)))
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   239
  }
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   240
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   241
  def read_types(provider: Export.Provider): List[Type] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   242
    provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   243
      {
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   244
        val (entity, body) = decode_entity(Kind.TYPE, tree)
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   245
        val (syntax, args, abbrev) =
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   246
        {
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   247
          import XML.Decode._
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   248
          triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   249
        }
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   250
        Type(entity, syntax, args, abbrev)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   251
      })
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   252
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   253
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   254
  /* consts */
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   255
68173
7ed88a534bb6 more uniform types vs. consts;
wenzelm
parents: 68172
diff changeset
   256
  sealed case class Const(
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   257
    entity: Entity,
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   258
    syntax: Syntax,
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   259
    typargs: List[String],
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   260
    typ: Term.Typ,
69988
6fa51a36b7f7 export propositional status of consts;
wenzelm
parents: 69077
diff changeset
   261
    abbrev: Option[Term.Term],
71222
2bc39c80a95d clarified export of consts: recursion is accessible via spec_rules;
wenzelm
parents: 71211
diff changeset
   262
    propositional: Boolean)
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   263
  {
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   264
    def cache(cache: Term.Cache): Const =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   265
      Const(entity.cache(cache),
69003
a015f1d3ba0c export plain infix syntax;
wenzelm
parents: 68997
diff changeset
   266
        syntax,
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   267
        typargs.map(cache.string(_)),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   268
        cache.typ(typ),
69988
6fa51a36b7f7 export propositional status of consts;
wenzelm
parents: 69077
diff changeset
   269
        abbrev.map(cache.term(_)),
71222
2bc39c80a95d clarified export of consts: recursion is accessible via spec_rules;
wenzelm
parents: 71211
diff changeset
   270
        propositional)
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   271
  }
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   272
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   273
  def read_consts(provider: Export.Provider): List[Const] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   274
    provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   275
      {
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   276
        val (entity, body) = decode_entity(Kind.CONST, tree)
71222
2bc39c80a95d clarified export of consts: recursion is accessible via spec_rules;
wenzelm
parents: 71211
diff changeset
   277
        val (syntax, (typargs, (typ, (abbrev, propositional)))) =
68203
cda4f24331d5 read theory content from session database;
wenzelm
parents: 68173
diff changeset
   278
        {
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   279
          import XML.Decode._
69992
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69988
diff changeset
   280
          pair(decode_syntax,
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69988
diff changeset
   281
            pair(list(string),
bd3c10813cc4 more informative Spec_Rules.Equational, notably primrec argument types;
wenzelm
parents: 69988
diff changeset
   282
              pair(Term_XML.Decode.typ,
71222
2bc39c80a95d clarified export of consts: recursion is accessible via spec_rules;
wenzelm
parents: 71211
diff changeset
   283
                pair(option(Term_XML.Decode.term), bool))))(body)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   284
        }
71222
2bc39c80a95d clarified export of consts: recursion is accessible via spec_rules;
wenzelm
parents: 71211
diff changeset
   285
        Const(entity, syntax, typargs, typ, abbrev, propositional)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   286
      })
68208
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   287
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   288
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   289
  /* axioms */
68232
4b93573ac5b4 export facts;
wenzelm
parents: 68231
diff changeset
   290
68726
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   291
  sealed case class Prop(
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   292
    typargs: List[(String, Term.Sort)],
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   293
    args: List[(String, Term.Typ)],
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   294
    term: Term.Term)
68232
4b93573ac5b4 export facts;
wenzelm
parents: 68231
diff changeset
   295
  {
68726
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   296
    def cache(cache: Term.Cache): Prop =
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   297
      Prop(
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   298
        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   299
        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   300
        cache.term(term))
68232
4b93573ac5b4 export facts;
wenzelm
parents: 68231
diff changeset
   301
  }
68208
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   302
68726
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   303
  def decode_prop(body: XML.Body): Prop =
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   304
  {
68726
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   305
    val (typargs, args, t) =
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   306
    {
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   307
      import XML.Decode._
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   308
      import Term_XML.Decode._
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   309
      triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   310
    }
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   311
    Prop(typargs, args, t)
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   312
  }
68208
d9f2cf4fc002 more exports;
wenzelm
parents: 68206
diff changeset
   313
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   314
  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
   315
  {
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   316
    def cache(cache: Term.Cache): Axiom =
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   317
      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
   318
  }
fb876ebbf5a7 export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents: 70384
diff changeset
   319
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   320
  def read_axioms(provider: Export.Provider): List[Axiom] =
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   321
    provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   322
      {
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   323
        val (entity, body) = decode_entity(Kind.AXIOM, tree)
68726
782d6b89fb19 more uniform facts: single vs. multi;
wenzelm
parents: 68718
diff changeset
   324
        val prop = decode_prop(body)
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   325
        Axiom(entity, prop)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   326
      })
68232
4b93573ac5b4 export facts;
wenzelm
parents: 68231
diff changeset
   327
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   328
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   329
  /* theorems */
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   330
70884
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   331
  sealed case class Thm_Id(serial: Long, theory_name: String)
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   332
  {
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   333
    def pure: Boolean = theory_name == Thy_Header.PURE
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   334
  }
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   335
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   336
  sealed case class Thm(
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   337
    entity: Entity,
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   338
    prop: Prop,
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   339
    deps: List[String],
70896
8017d382a0d7 tuned signature;
wenzelm
parents: 70891
diff changeset
   340
    proof: Term.Proof)
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   341
  {
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   342
    def cache(cache: Term.Cache): Thm =
70884
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   343
      Thm(
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   344
        entity.cache(cache),
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   345
        prop.cache(cache),
84145953b2a5 more support for proof terms;
wenzelm
parents: 70883
diff changeset
   346
        deps.map(cache.string _),
70896
8017d382a0d7 tuned signature;
wenzelm
parents: 70891
diff changeset
   347
        cache.proof(proof))
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   348
  }
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   349
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   350
  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
   351
    provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   352
      {
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   353
        val (entity, body) = decode_entity(Kind.THM, tree)
71015
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   354
        val (prop, deps, prf) =
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   355
        {
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   356
          import XML.Decode._
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   357
          import Term_XML.Decode._
71015
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   358
          triple(decode_prop, list(string), proof)(body)
70579
5a8e3e4b3760 clarified export of axioms and theorems (identified derivations instead of projected facts);
wenzelm
parents: 70539
diff changeset
   359
        }
71015
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   360
        Thm(entity, prop, deps, prf)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   361
      })
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   362
70881
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   363
  sealed case class Proof(
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   364
    typargs: List[(String, Term.Sort)],
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   365
    args: List[(String, Term.Typ)],
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   366
    term: Term.Term,
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   367
    proof: Term.Proof)
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   368
  {
70883
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   369
    def prop: Prop = Prop(typargs, args, term)
93767b7a8e7b more support for proof terms;
wenzelm
parents: 70882
diff changeset
   370
70881
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   371
    def cache(cache: Term.Cache): Proof =
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   372
      Proof(
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   373
        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   374
        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   375
        cache.term(term),
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   376
        cache.proof(proof))
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   377
  }
80f3a290b35c clarified proof export;
wenzelm
parents: 70843
diff changeset
   378
70899
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   379
  def read_proof(
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   380
    provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
70539
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70534
diff changeset
   381
  {
70899
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   382
    for { entry <- provider.focus(id.theory_name)(export_prefix_proofs + id.serial) }
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   383
    yield {
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   384
      val body = entry.uncompressed_yxml()
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   385
      val (typargs, (args, (prop_body, proof_body))) =
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   386
      {
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   387
        import XML.Decode._
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   388
        import Term_XML.Decode._
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   389
        pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(x => x, x => x)))(body)
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   390
      }
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   391
      val env = args.toMap
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   392
      val prop = Term_XML.Decode.term_env(env)(prop_body)
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   393
      val proof = Term_XML.Decode.proof_env(env)(proof_body)
70843
cc987440d776 more compact XML: separate environment for free variables;
wenzelm
parents: 70790
diff changeset
   394
70899
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   395
      val result = Proof(typargs, args, prop, proof)
5f6dea6a7a4c clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;
wenzelm
parents: 70896
diff changeset
   396
      cache.map(result.cache(_)) getOrElse result
70843
cc987440d776 more compact XML: separate environment for free variables;
wenzelm
parents: 70790
diff changeset
   397
    }
70539
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70534
diff changeset
   398
  }
30b3c58a1933 support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents: 70534
diff changeset
   399
71015
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   400
  def read_proof_boxes(
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   401
    store: Sessions.Store,
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   402
    provider: Export.Provider,
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   403
    proof: Term.Proof,
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   404
    suppress: Thm_Id => Boolean = _ => false,
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   405
    cache: Option[Term.Cache] = None): List[(Thm_Id, Proof)] =
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   406
  {
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   407
    var seen = Set.empty[Long]
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   408
    var result = SortedMap.empty[Long, (Thm_Id, Proof)]
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   409
71016
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   410
    def boxes(context: Option[(Long, Term.Proof)], prf: Term.Proof)
71015
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   411
    {
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   412
      prf match {
71016
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   413
        case Term.Abst(_, _, p) => boxes(context, p)
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   414
        case Term.AbsP(_, _, p) => boxes(context, p)
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   415
        case Term.Appt(p, _) => boxes(context, p)
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   416
        case Term.AppP(p, q) => boxes(context, p); boxes(context, q)
71015
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   417
        case thm: Term.PThm if !seen(thm.serial) =>
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   418
          seen += thm.serial
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   419
          val id = Thm_Id(thm.serial, thm.theory_name)
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   420
          if (!suppress(id)) {
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   421
            val read =
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   422
              if (id.pure) Export_Theory.read_pure_proof(store, id, cache = cache)
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   423
              else Export_Theory.read_proof(provider, id, cache = cache)
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   424
            read match {
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   425
              case Some(p) =>
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   426
                result += (thm.serial -> (id -> p))
71016
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   427
                boxes(Some((thm.serial, p.proof)), p.proof)
71015
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   428
              case None =>
71016
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   429
                error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")" +
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   430
                  (context match {
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   431
                    case None => ""
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   432
                    case Some((i, p)) => " in proof " + i + ":\n" + p
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   433
                  }))
71015
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   434
            }
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   435
          }
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   436
        case _ =>
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   437
      }
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   438
    }
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   439
71016
b05d78bfc67c clarified errors;
wenzelm
parents: 71015
diff changeset
   440
    boxes(None, proof)
71015
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   441
    result.iterator.map(_._2).toList
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   442
  }
bb49abc2ecbb determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);
wenzelm
parents: 70920
diff changeset
   443
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   444
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   445
  /* type classes */
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   446
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   447
  sealed case class Class(
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 69019
diff changeset
   448
    entity: Entity, params: List[(String, Term.Typ)], axioms: List[Prop])
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   449
  {
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   450
    def cache(cache: Term.Cache): Class =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   451
      Class(entity.cache(cache),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   452
        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
   453
        axioms.map(_.cache(cache)))
68267
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   454
  }
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   455
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   456
  def read_classes(provider: Export.Provider): List[Class] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   457
    provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   458
      {
68714
1d5ab386eaf0 more explicit entity kind;
wenzelm
parents: 68712
diff changeset
   459
        val (entity, body) = decode_entity(Kind.CLASS, tree)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   460
        val (params, axioms) =
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   461
        {
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   462
          import XML.Decode._
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   463
          import Term_XML.Decode._
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 69019
diff changeset
   464
          pair(list(pair(string, typ)), list(decode_prop))(body)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   465
        }
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   466
        Class(entity, params, axioms)
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   467
      })
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   468
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   469
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   470
  /* locales */
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   471
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   472
  sealed case class Locale(
69019
a6ba77af6486 export semi-unfolded locale axioms;
wenzelm
parents: 69003
diff changeset
   473
    entity: Entity,
a6ba77af6486 export semi-unfolded locale axioms;
wenzelm
parents: 69003
diff changeset
   474
    typargs: List[(String, Term.Sort)],
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   475
    args: List[((String, Term.Typ), Syntax)],
69023
cef000855cf4 clarified standardization of variables, with proper treatment of local variables;
wenzelm
parents: 69019
diff changeset
   476
    axioms: List[Prop])
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   477
  {
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   478
    def cache(cache: Term.Cache): Locale =
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   479
      Locale(entity.cache(cache),
68864
1dacce27bc25 clarified signature: proper typargs;
wenzelm
parents: 68862
diff changeset
   480
        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
   481
        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
   482
        axioms.map(_.cache(cache)))
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   483
  }
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   484
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   485
  def read_locales(provider: Export.Provider): List[Locale] =
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   486
    provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   487
      {
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   488
        val (entity, body) = decode_entity(Kind.LOCALE, tree)
69019
a6ba77af6486 export semi-unfolded locale axioms;
wenzelm
parents: 69003
diff changeset
   489
        val (typargs, args, axioms) =
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   490
        {
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   491
          import XML.Decode._
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   492
          import Term_XML.Decode._
69077
11529ae45786 more approximative prefix syntax, including binder;
wenzelm
parents: 69076
diff changeset
   493
          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
   494
            list(decode_prop))(body)
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   495
        }
69019
a6ba77af6486 export semi-unfolded locale axioms;
wenzelm
parents: 69003
diff changeset
   496
        Locale(entity, typargs, args, axioms)
68862
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   497
      })
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   498
47e9912c53c3 export locale content;
wenzelm
parents: 68835
diff changeset
   499
69069
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   500
  /* locale dependencies */
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   501
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   502
  sealed case class Locale_Dependency(
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   503
    entity: Entity,
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   504
    source: String,
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   505
    target: String,
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   506
    prefix: List[(String, Boolean)],
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   507
    subst_types: List[((String, Term.Sort), Term.Typ)],
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   508
    subst_terms: List[((String, Term.Typ), Term.Term)])
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   509
  {
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   510
    def cache(cache: Term.Cache): Locale_Dependency =
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   511
      Locale_Dependency(entity.cache(cache),
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   512
        cache.string(source),
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   513
        cache.string(target),
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   514
        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
   515
        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
   516
        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
   517
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   518
    def is_inclusion: Boolean =
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   519
      subst_types.isEmpty && subst_terms.isEmpty
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   520
  }
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   521
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   522
  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
   523
    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
   524
      {
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   525
        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
   526
        val (source, (target, (prefix, (subst_types, subst_terms)))) =
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   527
        {
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   528
          import XML.Decode._
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   529
          import Term_XML.Decode._
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   530
          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
   531
            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
   532
        }
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   533
        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
   534
      })
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   535
b9aca3b9619f export locale dependencies, with approx. morphism as type/term substitution;
wenzelm
parents: 69023
diff changeset
   536
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   537
  /* sort algebra */
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   538
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   539
  sealed case class Classrel(class1: String, class2: String, prop: Prop)
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   540
  {
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   541
    def cache(cache: Term.Cache): Classrel =
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   542
      Classrel(cache.string(class1), cache.string(class2), prop.cache(cache))
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   543
  }
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   544
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   545
  def read_classrel(provider: Export.Provider): List[Classrel] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   546
  {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   547
    val body = provider.uncompressed_yxml(export_prefix + "classrel")
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   548
    val classrel =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   549
    {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   550
      import XML.Decode._
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   551
      list(pair(decode_prop, pair(string, string)))(body)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   552
    }
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   553
    for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   554
  }
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   555
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   556
  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
   557
  {
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   558
    def cache(cache: Term.Cache): Arity =
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   559
      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
   560
        prop.cache(cache))
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   561
  }
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   562
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   563
  def read_arities(provider: Export.Provider): List[Arity] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   564
  {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   565
    val body = provider.uncompressed_yxml(export_prefix + "arities")
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   566
    val arities =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   567
    {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   568
      import XML.Decode._
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   569
      import Term_XML.Decode._
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   570
      list(pair(decode_prop, triple(string, list(sort), string)))(body)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   571
    }
70384
8ce08b154aa1 clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
wenzelm
parents: 69996
diff changeset
   572
    for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop)
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   573
  }
68295
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   574
781a98696638 export sort algebra;
wenzelm
parents: 68267
diff changeset
   575
70920
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   576
  /* Pure constdefs */
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   577
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   578
  sealed case class Constdef(name: String, axiom_name: String)
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   579
  {
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   580
    def cache(cache: Term.Cache): Constdef =
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   581
      Constdef(cache.string(name), cache.string(axiom_name))
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   582
  }
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   583
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   584
  def read_constdefs(provider: Export.Provider): List[Constdef] =
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   585
  {
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   586
    val body = provider.uncompressed_yxml(export_prefix + "constdefs")
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   587
    val constdefs =
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   588
    {
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   589
      import XML.Decode._
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   590
      list(pair(string, string))(body)
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   591
    }
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   592
    for ((name, axiom_name) <- constdefs) yield Constdef(name, axiom_name)
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   593
  }
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   594
1e0ad25c94c8 export constdefs according to defs.ML;
wenzelm
parents: 70913
diff changeset
   595
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   596
  /* HOL typedefs */
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   597
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   598
  sealed case class Typedef(name: String,
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   599
    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
   600
  {
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   601
    def cache(cache: Term.Cache): Typedef =
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   602
      Typedef(cache.string(name),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   603
        cache.typ(rep_type),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   604
        cache.typ(abs_type),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   605
        cache.string(rep_name),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   606
        cache.string(abs_name),
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   607
        cache.string(axiom_name))
6a29709906c6 more scalable JVM memory management;
wenzelm
parents: 68264
diff changeset
   608
  }
68264
bb9a3be6952a more exports;
wenzelm
parents: 68232
diff changeset
   609
68418
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   610
  def read_typedefs(provider: Export.Provider): List[Typedef] =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   611
  {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   612
    val body = provider.uncompressed_yxml(export_prefix + "typedefs")
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   613
    val typedefs =
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   614
    {
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   615
      import XML.Decode._
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   616
      import Term_XML.Decode._
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   617
      list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   618
    }
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   619
    for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   620
    yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
366e43cddd20 more abstract Export.Provider;
wenzelm
parents: 68346
diff changeset
   621
  }
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   622
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   623
71248
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   624
  /* HOL datatypes */
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   625
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   626
  sealed case class Datatype(
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   627
    pos: Position.T,
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   628
    name: String,
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   629
    co: Boolean,
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   630
    typargs: List[(String, Term.Sort)],
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   631
    typ: Term.Typ,
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   632
    constructors: List[(Term.Term, Term.Typ)])
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   633
  {
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   634
    def id: Option[Long] = Position.Id.unapply(pos)
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   635
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   636
    def cache(cache: Term.Cache): Datatype =
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   637
      Datatype(
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   638
        cache.position(pos),
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   639
        cache.string(name),
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   640
        co,
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   641
        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   642
        cache.typ(typ),
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   643
        constructors.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }))
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   644
  }
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   645
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   646
  def read_datatypes(provider: Export.Provider): List[Datatype] =
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   647
  {
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   648
    val body = provider.uncompressed_yxml(export_prefix + "datatypes")
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   649
    val datatypes =
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   650
    {
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   651
      import XML.Decode._
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   652
      import Term_XML.Decode._
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   653
      list(pair(properties, pair(string, pair(bool, pair(list(pair(string, sort)),
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   654
            pair(typ, list(pair(term, typ))))))))(body)
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   655
    }
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   656
    for ((pos, (name, (co, (typargs, (typ, constructors))))) <- datatypes)
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   657
      yield Datatype(pos, name, co, typargs, typ, constructors)
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   658
  }
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   659
adf5e53d2b2b export datatypes;
wenzelm
parents: 71222
diff changeset
   660
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   661
  /* Pure spec rules */
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   662
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   663
  sealed abstract class Recursion
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   664
  {
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   665
    def cache(cache: Term.Cache): Recursion =
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   666
      this match {
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   667
        case Primrec(types) => Primrec(types.map(cache.string))
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   668
        case Primcorec(types) => Primcorec(types.map(cache.string))
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   669
        case _ => this
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   670
      }
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   671
  }
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   672
  case class Primrec(types: List[String]) extends Recursion
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   673
  case object Recdef extends Recursion
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   674
  case class Primcorec(types: List[String]) extends Recursion
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   675
  case object Corec extends Recursion
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   676
  case object Unknown_Recursion extends Recursion
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   677
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   678
  val decode_recursion: XML.Decode.T[Recursion] =
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   679
  {
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   680
    import XML.Decode._
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   681
    variant(List(
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   682
      { case (Nil, a) => Primrec(list(string)(a)) },
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   683
      { case (Nil, Nil) => Recdef },
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   684
      { case (Nil, a) => Primcorec(list(string)(a)) },
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   685
      { case (Nil, Nil) => Corec },
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   686
      { case (Nil, Nil) => Unknown_Recursion }))
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   687
  }
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   688
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   689
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   690
  sealed abstract class Rough_Classification
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   691
  {
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   692
    def is_equational: Boolean = this.isInstanceOf[Equational]
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   693
    def is_inductive: Boolean = this == Inductive
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   694
    def is_co_inductive: Boolean = this == Co_Inductive
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   695
    def is_relational: Boolean = is_inductive || is_co_inductive
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   696
    def is_unknown: Boolean = this == Unknown
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   697
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   698
    def cache(cache: Term.Cache): Rough_Classification =
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   699
      this match {
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   700
        case Equational(recursion) => Equational(recursion.cache(cache))
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   701
        case _ => this
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   702
      }
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   703
  }
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   704
  case class Equational(recursion: Recursion) extends Rough_Classification
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   705
  case object Inductive extends Rough_Classification
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   706
  case object Co_Inductive extends Rough_Classification
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   707
  case object Unknown extends Rough_Classification
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   708
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   709
  val decode_rough_classification: XML.Decode.T[Rough_Classification] =
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   710
  {
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   711
    import XML.Decode._
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   712
    variant(List(
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   713
      { case (Nil, a) => Equational(decode_recursion(a)) },
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   714
      { case (Nil, Nil) => Inductive },
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   715
      { case (Nil, Nil) => Co_Inductive },
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   716
      { case (Nil, Nil) => Unknown }))
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   717
  }
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   718
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   719
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   720
  sealed case class Spec_Rule(
71207
8af82f3e03c9 formal position for spec rule (not significant for equality);
wenzelm
parents: 71202
diff changeset
   721
    pos: Position.T,
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   722
    name: String,
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   723
    rough_classification: Rough_Classification,
71208
5e0050eb64f2 clarified export of spec rules: more like locale;
wenzelm
parents: 71207
diff changeset
   724
    typargs: List[(String, Term.Sort)],
5e0050eb64f2 clarified export of spec rules: more like locale;
wenzelm
parents: 71207
diff changeset
   725
    args: List[(String, Term.Typ)],
71211
7d522732b7f2 more informative export;
wenzelm
parents: 71208
diff changeset
   726
    terms: List[(Term.Term, Term.Typ)],
71208
5e0050eb64f2 clarified export of spec rules: more like locale;
wenzelm
parents: 71207
diff changeset
   727
    rules: List[Term.Term])
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   728
  {
71207
8af82f3e03c9 formal position for spec rule (not significant for equality);
wenzelm
parents: 71202
diff changeset
   729
    def id: Option[Long] = Position.Id.unapply(pos)
8af82f3e03c9 formal position for spec rule (not significant for equality);
wenzelm
parents: 71202
diff changeset
   730
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   731
    def cache(cache: Term.Cache): Spec_Rule =
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   732
      Spec_Rule(
71207
8af82f3e03c9 formal position for spec rule (not significant for equality);
wenzelm
parents: 71202
diff changeset
   733
        cache.position(pos),
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   734
        cache.string(name),
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   735
        rough_classification.cache(cache),
71208
5e0050eb64f2 clarified export of spec rules: more like locale;
wenzelm
parents: 71207
diff changeset
   736
        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
5e0050eb64f2 clarified export of spec rules: more like locale;
wenzelm
parents: 71207
diff changeset
   737
        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
71211
7d522732b7f2 more informative export;
wenzelm
parents: 71208
diff changeset
   738
        terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }),
71208
5e0050eb64f2 clarified export of spec rules: more like locale;
wenzelm
parents: 71207
diff changeset
   739
        rules.map(cache.term(_)))
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   740
  }
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   741
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   742
  def read_spec_rules(provider: Export.Provider): List[Spec_Rule] =
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   743
  {
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   744
    val body = provider.uncompressed_yxml(export_prefix + "spec_rules")
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   745
    val spec_rules =
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   746
    {
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   747
      import XML.Decode._
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   748
      import Term_XML.Decode._
71207
8af82f3e03c9 formal position for spec rule (not significant for equality);
wenzelm
parents: 71202
diff changeset
   749
      list(
8af82f3e03c9 formal position for spec rule (not significant for equality);
wenzelm
parents: 71202
diff changeset
   750
        pair(properties, pair(string, pair(decode_rough_classification,
71208
5e0050eb64f2 clarified export of spec rules: more like locale;
wenzelm
parents: 71207
diff changeset
   751
          pair(list(pair(string, sort)), pair(list(pair(string, typ)),
71211
7d522732b7f2 more informative export;
wenzelm
parents: 71208
diff changeset
   752
            pair(list(pair(term, typ)), list(term))))))))(body)
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   753
    }
71208
5e0050eb64f2 clarified export of spec rules: more like locale;
wenzelm
parents: 71207
diff changeset
   754
    for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules)
5e0050eb64f2 clarified export of spec rules: more like locale;
wenzelm
parents: 71207
diff changeset
   755
      yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules)
71202
785610ad6bfa export spec rules;
wenzelm
parents: 71016
diff changeset
   756
  }
68171
13162bb3a677 export foundational theory content in Scala;
wenzelm
parents:
diff changeset
   757
}