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