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