diff --git a/src/Pure/PIDE/xml.scala b/src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala +++ b/src/Pure/PIDE/xml.scala @@ -1,433 +1,433 @@ /* Title: Pure/PIDE/xml.scala Author: Makarius Untyped XML trees and basic data representation. */ package isabelle object XML { /** XML trees **/ /* datatype representation */ type Attribute = Properties.Entry type Attributes = Properties.T sealed abstract class Tree { override def toString: String = string_of_tree(this) } type Body = List[Tree] case class Elem(markup: Markup, body: Body) extends Tree { private lazy val hash: Int = (markup, body).hashCode() override def hashCode(): Int = hash def name: String = markup.name def update_attributes(more_attributes: Attributes): Elem = if (more_attributes.isEmpty) this else Elem(markup.update_properties(more_attributes), body) def + (att: Attribute): Elem = Elem(markup + att, body) } case class Text(content: String) extends Tree { private lazy val hash: Int = content.hashCode() override def hashCode(): Int = hash } def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil) def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body) def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil) val no_text: Text = Text("") val newline: Text = Text("\n") def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s)) def enclose(bg: String, en:String, body: Body): Body = string(bg) ::: body ::: string(en) /* name space */ object Namespace { def apply(prefix: String, target: String): Namespace = new Namespace(prefix, target) } final class Namespace private(prefix: String, target: String) { def apply(name: String): String = prefix + ":" + name val attribute: XML.Attribute = ("xmlns:" + prefix, target) override def toString: String = attribute.toString } /* wrapped elements */ val XML_ELEM = "xml_elem" val XML_NAME = "xml_name" val XML_BODY = "xml_body" object Wrapped_Elem { def apply(markup: Markup, body1: Body, body2: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties), XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) def unapply(tree: Tree): Option[(Markup, Body, Body)] = tree match { case XML.Elem(Markup(XML_ELEM, (XML_NAME, name) :: props), XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) => Some(Markup(name, props), body1, body2) case _ => None } } object Root_Elem { def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body) def unapply(tree: Tree): Option[Body] = tree match { case XML.Elem(Markup(XML_ELEM, Nil), body) => Some(body) case _ => None } } /* traverse text */ def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = { def traverse(x: A, t: Tree): A = t match { case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse) case XML.Elem(_, ts) => ts.foldLeft(x)(traverse) case XML.Text(s) => op(x, s) } body.foldLeft(a)(traverse) } def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length } def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) } /* text content */ def content(body: Body): String = { val text = new StringBuilder(text_length(body)) traverse_text(body)(()) { case (_, s) => text.append(s) } text.toString } def content(tree: Tree): String = content(List(tree)) /** string representation **/ val header: String = "\n" def output_char(s: StringBuilder, c: Char, permissive: Boolean = false): Unit = { c match { case '<' => s ++= "<" case '>' => s ++= ">" case '&' => s ++= "&" case '"' if !permissive => s ++= """ case '\'' if !permissive => s ++= "'" case _ => s += c } } def output_string(s: StringBuilder, str: String, permissive: Boolean = false): Unit = { if (str == null) s ++= str else str.iterator.foreach(output_char(s, _, permissive = permissive)) } def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false): Unit = { s += '<' s ++= markup.name for ((a, b) <- markup.properties) { s += ' ' s ++= a s += '=' s += '"' output_string(s, b) s += '"' } if (end) s += '/' s += '>' } def output_elem_end(s: StringBuilder, name: String): Unit = { s += '<' s += '/' s ++= name s += '>' } def string_of_body(body: Body): String = { val s = new StringBuilder def tree(t: Tree): Unit = t match { case XML.Elem(markup, Nil) => output_elem(s, markup, end = true) case XML.Elem(markup, ts) => output_elem(s, markup) ts.foreach(tree) output_elem_end(s, markup.name) case XML.Text(txt) => output_string(s, txt) } body.foreach(tree) s.toString } def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) def text(s: String): String = string_of_tree(XML.Text(s)) /** cache **/ object Cache { def make( xz: XZ.Cache = XZ.Cache.make(), max_string: Int = isabelle.Cache.default_max_string, initial_size: Int = isabelle.Cache.default_initial_size): Cache = new Cache(xz, max_string, initial_size) val none: Cache = make(XZ.Cache.none, max_string = 0) } class Cache(val xz: XZ.Cache, max_string: Int, initial_size: Int) extends isabelle.Cache(max_string, initial_size) { protected def cache_props(x: Properties.T): Properties.T = { if (x.isEmpty) x else lookup(x) match { case Some(y) => y case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2)))) } } protected def cache_markup(x: Markup): Markup = { lookup(x) match { case Some(y) => y case None => x match { case Markup(name, props) => store(Markup(cache_string(name), cache_props(props))) } } } protected def cache_tree(x: XML.Tree): XML.Tree = { lookup(x) match { case Some(y) => y case None => x match { case XML.Elem(markup, body) => store(XML.Elem(cache_markup(markup), cache_body(body))) case XML.Text(text) => store(XML.Text(cache_string(text))) } } } protected def cache_body(x: XML.Body): XML.Body = { if (x.isEmpty) x else lookup(x) match { case Some(y) => y case None => x.map(cache_tree) } } // support hash-consing def tree0(x: XML.Tree): XML.Tree = if (no_cache) x else synchronized { lookup(x) getOrElse store(x) } // main methods def props(x: Properties.T): Properties.T = if (no_cache) x else synchronized { cache_props(x) } def markup(x: Markup): Markup = if (no_cache) x else synchronized { cache_markup(x) } def tree(x: XML.Tree): XML.Tree = if (no_cache) x else synchronized { cache_tree(x) } def body(x: XML.Body): XML.Body = if (no_cache) x else synchronized { cache_body(x) } def elem(x: XML.Elem): XML.Elem = if (no_cache) x else synchronized { cache_tree(x).asInstanceOf[XML.Elem] } } /** XML as data representation language **/ abstract class Error(s: String) extends Exception(s) class XML_Atom(s: String) extends Error(s) class XML_Body(body: XML.Body) extends Error("") object Encode { type T[A] = A => XML.Body type V[A] = PartialFunction[A, (List[String], XML.Body)] type P[A] = PartialFunction[A, List[String]] /* atomic values */ def long_atom(i: Long): String = Library.signed_string_of_long(i) def int_atom(i: Int): String = Library.signed_string_of_int(i) def bool_atom(b: Boolean): String = if (b) "1" else "0" def unit_atom(u: Unit) = "" /* structural nodes */ private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts) private def vector(xs: List[String]): XML.Attributes = xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) }) private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree = XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2) /* representation of standard types */ val tree: T[XML.Tree] = (t => List(t)) val properties: T[Properties.T] = (props => List(XML.Elem(Markup(":", props), Nil))) val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s))) val long: T[Long] = (x => string(long_atom(x))) val int: T[Int] = (x => string(int_atom(x))) val bool: T[Boolean] = (x => string(bool_atom(x))) val unit: T[Unit] = (x => string(unit_atom(x))) def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = (x => List(node(f(x._1)), node(g(x._2)))) def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3)))) def list[A](f: T[A]): T[List[A]] = (xs => xs.map((x: A) => node(f(x)))) def option[A](f: T[A]): T[Option[A]] = { case None => Nil case Some(x) => List(node(f(x))) } def variant[A](fs: List[V[A]]): T[A] = { case x => val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get List(tagged(tag, f(x))) } } object Decode { type T[A] = XML.Body => A - type V[A] = (List[String], XML.Body) => A + type V[A] = PartialFunction[(List[String], XML.Body), A] type P[A] = PartialFunction[List[String], A] /* atomic values */ def long_atom(s: String): Long = try { java.lang.Long.parseLong(s) } catch { case e: NumberFormatException => throw new XML_Atom(s) } def int_atom(s: String): Int = try { Integer.parseInt(s) } catch { case e: NumberFormatException => throw new XML_Atom(s) } def bool_atom(s: String): Boolean = if (s == "1") true else if (s == "0") false else throw new XML_Atom(s) def unit_atom(s: String): Unit = if (s == "") () else throw new XML_Atom(s) /* structural nodes */ private def node(t: XML.Tree): XML.Body = t match { case XML.Elem(Markup(":", Nil), ts) => ts case _ => throw new XML_Body(List(t)) } private def vector(atts: XML.Attributes): List[String] = atts.iterator.zipWithIndex.map( { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) = t match { case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts)) case _ => throw new XML_Body(List(t)) } /* representation of standard types */ val tree: T[XML.Tree] = { case List(t) => t case ts => throw new XML_Body(ts) } val properties: T[Properties.T] = { case List(XML.Elem(Markup(":", props), Nil)) => props case ts => throw new XML_Body(ts) } val string: T[String] = { case Nil => "" case List(XML.Text(s)) => s case ts => throw new XML_Body(ts) } val long: T[Long] = (x => long_atom(string(x))) val int: T[Int] = (x => int_atom(string(x))) val bool: T[Boolean] = (x => bool_atom(string(x))) val unit: T[Unit] = (x => unit_atom(string(x))) def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = { case List(t1, t2) => (f(node(t1)), g(node(t2))) case ts => throw new XML_Body(ts) } def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = { case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3))) case ts => throw new XML_Body(ts) } def list[A](f: T[A]): T[List[A]] = (ts => ts.map(t => f(node(t)))) def option[A](f: T[A]): T[Option[A]] = { case Nil => None case List(t) => Some(f(node(t))) case ts => throw new XML_Body(ts) } def variant[A](fs: List[V[A]]): T[A] = { case List(t) => val (tag, (xs, ts)) = tagged(t) val f = try { fs(tag) } catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) } f(xs, ts) case ts => throw new XML_Body(ts) } } } diff --git a/src/Pure/Thy/export_theory.scala b/src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala +++ b/src/Pure/Thy/export_theory.scala @@ -1,779 +1,778 @@ /* Title: Pure/Thy/export_theory.scala Author: Makarius Export foundational theory content. */ package isabelle import scala.collection.immutable.SortedMap object Export_Theory { /** session content **/ sealed case class Session(name: String, theory_graph: Graph[String, Option[Theory]]) { override def toString: String = name def theory(theory_name: String): Option[Theory] = if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name) else None def theories: List[Theory] = theory_graph.topological_order.flatMap(theory) } def read_session( store: Sessions.Store, sessions_structure: Sessions.Structure, session_name: String, progress: Progress = new Progress, cache: Term.Cache = Term.Cache.make()): Session = { val thys = sessions_structure.build_requirements(List(session_name)).flatMap(session => using(store.open_database(session)) { db => db.transaction { for (theory <- Export.read_theory_names(db, session)) yield { progress.echo("Reading theory " + theory) val provider = Export.Provider.database(db, store.cache, session, theory) read_theory(provider, session, theory, cache = cache) } } }) val graph0 = thys.foldLeft(Graph.string[Option[Theory]]) { case (g, thy) => g.default_node(thy.name, Some(thy)) } val graph1 = thys.foldLeft(graph0) { case (g0, thy) => thy.parents.foldLeft(g0) { case (g1, parent) => g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) } } Session(session_name, graph1) } /** theory content **/ sealed case class Theory(name: String, parents: List[String], types: List[Entity[Type]], consts: List[Entity[Const]], axioms: List[Entity[Axiom]], thms: List[Entity[Thm]], classes: List[Entity[Class]], locales: List[Entity[Locale]], locale_dependencies: List[Entity[Locale_Dependency]], classrel: List[Classrel], arities: List[Arity], constdefs: List[Constdef], typedefs: List[Typedef], datatypes: List[Datatype], spec_rules: List[Spec_Rule], others: Map[String, List[Entity[Other]]] ) { override def toString: String = name def entity_iterator: Iterator[Entity[No_Content]] = types.iterator.map(_.no_content) ++ consts.iterator.map(_.no_content) ++ axioms.iterator.map(_.no_content) ++ thms.iterator.map(_.no_content) ++ classes.iterator.map(_.no_content) ++ locales.iterator.map(_.no_content) ++ locale_dependencies.iterator.map(_.no_content) ++ (for { (_, xs) <- others; x <- xs.iterator } yield x.no_content) def cache(cache: Term.Cache): Theory = Theory(cache.string(name), parents.map(cache.string), types.map(_.cache(cache)), consts.map(_.cache(cache)), axioms.map(_.cache(cache)), thms.map(_.cache(cache)), classes.map(_.cache(cache)), locales.map(_.cache(cache)), locale_dependencies.map(_.cache(cache)), classrel.map(_.cache(cache)), arities.map(_.cache(cache)), constdefs.map(_.cache(cache)), typedefs.map(_.cache(cache)), datatypes.map(_.cache(cache)), spec_rules.map(_.cache(cache)), (for ((k, xs) <- others.iterator) yield cache.string(k) -> xs.map(_.cache(cache))).toMap) } def read_theory_parents(provider: Export.Provider, theory_name: String): Option[List[String]] = { if (theory_name == Thy_Header.PURE) Some(Nil) else { provider(Export.THEORY_PREFIX + "parents") .map(entry => split_lines(entry.uncompressed.text)) } } def no_theory: Theory = Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty) def read_theory( provider: Export.Provider, session_name: String, theory_name: String, cache: Term.Cache = Term.Cache.none ): Theory = { val parents = read_theory_parents(provider, theory_name) getOrElse error("Missing theory export in session " + quote(session_name) + ": " + quote(theory_name)) val theory = Theory(theory_name, parents, read_types(provider), read_consts(provider), read_axioms(provider), read_thms(provider), read_classes(provider), read_locales(provider), read_locale_dependencies(provider), read_classrel(provider), read_arities(provider), read_constdefs(provider), read_typedefs(provider), read_datatypes(provider), read_spec_rules(provider), read_others(provider)) if (cache.no_cache) theory else theory.cache(cache) } def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A = { val session_name = Thy_Header.PURE val theory_name = Thy_Header.PURE using(store.open_database(session_name)) { db => db.transaction { val provider = Export.Provider.database(db, store.cache, session_name, theory_name) read(provider, session_name, theory_name) } } } def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.Cache.none): Theory = read_pure(store, read_theory(_, _, _, cache = cache)) def read_pure_proof( store: Sessions.Store, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] = read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache)) /* entities */ object Kind { val TYPE = "type" val CONST = "const" val THM = "thm" val PROOF = "proof" val LOCALE_DEPENDENCY = "locale_dependency" val DOCUMENT_HEADING = "document_heading" val DOCUMENT_TEXT = "document_text" val PROOF_TEXT = "proof_text" } def export_kind(kind: String): String = if (kind == Markup.TYPE_NAME) Kind.TYPE else if (kind == Markup.CONSTANT) Kind.CONST else kind def export_kind_name(kind: String, name: String): String = name + "|" + export_kind(kind) abstract class Content[T] { def cache(cache: Term.Cache): T } sealed case class No_Content() extends Content[No_Content] { def cache(cache: Term.Cache): No_Content = this } sealed case class Entity[A <: Content[A]]( kind: String, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long, content: Option[A] ) { val kname: String = export_kind_name(kind, name) val range: Symbol.Range = Position.Range.unapply(pos).getOrElse(Text.Range.offside) def export_kind: String = Export_Theory.export_kind(kind) override def toString: String = export_kind + " " + quote(name) def the_content: A = if (content.isDefined) content.get else error("No content for " + toString) def no_content: Entity[No_Content] = copy(content = None) def cache(cache: Term.Cache): Entity[A] = Entity( cache.string(kind), cache.string(name), cache.string(xname), cache.position(pos), id, serial, content.map(_.cache(cache))) } def read_entities[A <: Content[A]]( provider: Export.Provider, export_name: String, kind: String, decode: XML.Decode.T[A] ): List[Entity[A]] = { def decode_entity(tree: XML.Tree): Entity[A] = { def err(): Nothing = throw new XML.XML_Body(List(tree)) tree match { case XML.Elem(Markup(Markup.ENTITY, props), body) => val name = Markup.Name.unapply(props) getOrElse err() val xname = Markup.XName.unapply(props) getOrElse err() val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID) val id = Position.Id.unapply(props) val serial = Markup.Serial.unapply(props) getOrElse err() val content = if (body.isEmpty) None else Some(decode(body)) Entity(kind, name, xname, pos, id, serial, content) case _ => err() } } provider.uncompressed_yxml(export_name).map(decode_entity) } /* approximative syntax */ object Assoc extends Enumeration { val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value } sealed abstract class Syntax case object No_Syntax extends Syntax case class Prefix(delim: String) extends Syntax case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax def decode_syntax: XML.Decode.T[Syntax] = XML.Decode.variant(List( - { case (Nil, Nil) => No_Syntax case _ => ??? }, - { case (List(delim), Nil) => Prefix(delim) case _ => ??? }, + { case (Nil, Nil) => No_Syntax }, + { case (List(delim), Nil) => Prefix(delim) }, { case (Nil, body) => import XML.Decode._ val (ass, delim, pri) = triple(int, string, int)(body) - Infix(Assoc(ass), delim, pri) - case _ => ??? })) + Infix(Assoc(ass), delim, pri) })) /* types */ sealed case class Type(syntax: Syntax, args: List[String], abbrev: Option[Term.Typ]) extends Content[Type] { override def cache(cache: Term.Cache): Type = Type( syntax, args.map(cache.string), abbrev.map(cache.typ)) } def read_types(provider: Export.Provider): List[Entity[Type]] = read_entities(provider, Export.THEORY_PREFIX + "types", Markup.TYPE_NAME, { body => import XML.Decode._ val (syntax, args, abbrev) = triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body) Type(syntax, args, abbrev) }) /* consts */ sealed case class Const( syntax: Syntax, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term], propositional: Boolean ) extends Content[Const] { override def cache(cache: Term.Cache): Const = Const( syntax, typargs.map(cache.string), cache.typ(typ), abbrev.map(cache.term), propositional) } def read_consts(provider: Export.Provider): List[Entity[Const]] = read_entities(provider, Export.THEORY_PREFIX + "consts", Markup.CONSTANT, { body => import XML.Decode._ val (syntax, (typargs, (typ, (abbrev, propositional)))) = pair(decode_syntax, pair(list(string), pair(Term_XML.Decode.typ, pair(option(Term_XML.Decode.term), bool))))(body) Const(syntax, typargs, typ, abbrev, propositional) }) /* axioms */ sealed case class Prop( typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], term: Term.Term ) extends Content[Prop] { override def cache(cache: Term.Cache): Prop = Prop( typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), cache.term(term)) } def decode_prop(body: XML.Body): Prop = { val (typargs, args, t) = { import XML.Decode._ import Term_XML.Decode._ triple(list(pair(string, sort)), list(pair(string, typ)), term)(body) } Prop(typargs, args, t) } sealed case class Axiom(prop: Prop) extends Content[Axiom] { override def cache(cache: Term.Cache): Axiom = Axiom(prop.cache(cache)) } def read_axioms(provider: Export.Provider): List[Entity[Axiom]] = read_entities(provider, Export.THEORY_PREFIX + "axioms", Markup.AXIOM, body => Axiom(decode_prop(body))) /* theorems */ sealed case class Thm_Id(serial: Long, theory_name: String) { def pure: Boolean = theory_name == Thy_Header.PURE } sealed case class Thm( prop: Prop, deps: List[String], proof: Term.Proof) extends Content[Thm] { override def cache(cache: Term.Cache): Thm = Thm( prop.cache(cache), deps.map(cache.string), cache.proof(proof)) } def read_thms(provider: Export.Provider): List[Entity[Thm]] = read_entities(provider, Export.THEORY_PREFIX + "thms", Kind.THM, { body => import XML.Decode._ import Term_XML.Decode._ val (prop, deps, prf) = triple(decode_prop, list(string), proof)(body) Thm(prop, deps, prf) }) sealed case class Proof( typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], term: Term.Term, proof: Term.Proof ) { def prop: Prop = Prop(typargs, args, term) def cache(cache: Term.Cache): Proof = Proof( typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), cache.term(term), cache.proof(proof)) } def read_proof( provider: Export.Provider, id: Thm_Id, cache: Term.Cache = Term.Cache.none ): Option[Proof] = { for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) } yield { val body = entry.uncompressed_yxml val (typargs, (args, (prop_body, proof_body))) = { import XML.Decode._ import Term_XML.Decode._ pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(x => x, x => x)))(body) } val env = args.toMap val prop = Term_XML.Decode.term_env(env)(prop_body) val proof = Term_XML.Decode.proof_env(env)(proof_body) val result = Proof(typargs, args, prop, proof) if (cache.no_cache) result else result.cache(cache) } } def read_proof_boxes( store: Sessions.Store, provider: Export.Provider, proof: Term.Proof, suppress: Thm_Id => Boolean = _ => false, cache: Term.Cache = Term.Cache.none ): List[(Thm_Id, Proof)] = { var seen = Set.empty[Long] var result = SortedMap.empty[Long, (Thm_Id, Proof)] def boxes(context: Option[(Long, Term.Proof)], prf: Term.Proof): Unit = { prf match { case Term.Abst(_, _, p) => boxes(context, p) case Term.AbsP(_, _, p) => boxes(context, p) case Term.Appt(p, _) => boxes(context, p) case Term.AppP(p, q) => boxes(context, p); boxes(context, q) case thm: Term.PThm if !seen(thm.serial) => seen += thm.serial val id = Thm_Id(thm.serial, thm.theory_name) if (!suppress(id)) { val read = if (id.pure) Export_Theory.read_pure_proof(store, id, cache = cache) else Export_Theory.read_proof(provider, id, cache = cache) read match { case Some(p) => result += (thm.serial -> (id -> p)) boxes(Some((thm.serial, p.proof)), p.proof) case None => error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")" + (context match { case None => "" case Some((i, p)) => " in proof " + i + ":\n" + p })) } } case _ => } } boxes(None, proof) result.iterator.map(_._2).toList } /* type classes */ sealed case class Class(params: List[(String, Term.Typ)], axioms: List[Prop]) extends Content[Class] { override def cache(cache: Term.Cache): Class = Class( params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), axioms.map(_.cache(cache))) } def read_classes(provider: Export.Provider): List[Entity[Class]] = read_entities(provider, Export.THEORY_PREFIX + "classes", Markup.CLASS, { body => import XML.Decode._ import Term_XML.Decode._ val (params, axioms) = pair(list(pair(string, typ)), list(decode_prop))(body) Class(params, axioms) }) /* locales */ sealed case class Locale( typargs: List[(String, Term.Sort)], args: List[((String, Term.Typ), Syntax)], axioms: List[Prop] ) extends Content[Locale] { override def cache(cache: Term.Cache): Locale = Locale( typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case ((name, typ), syntax) => ((cache.string(name), cache.typ(typ)), syntax) }), axioms.map(_.cache(cache))) } def read_locales(provider: Export.Provider): List[Entity[Locale]] = read_entities(provider, Export.THEORY_PREFIX + "locales", Markup.LOCALE, { body => import XML.Decode._ import Term_XML.Decode._ val (typargs, args, axioms) = triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)), list(decode_prop))(body) Locale(typargs, args, axioms) }) /* locale dependencies */ sealed case class Locale_Dependency( source: String, target: String, prefix: List[(String, Boolean)], subst_types: List[((String, Term.Sort), Term.Typ)], subst_terms: List[((String, Term.Typ), Term.Term)] ) extends Content[Locale_Dependency] { override def cache(cache: Term.Cache): Locale_Dependency = Locale_Dependency( cache.string(source), cache.string(target), prefix.map({ case (name, mandatory) => (cache.string(name), mandatory) }), subst_types.map({ case ((a, s), ty) => ((cache.string(a), cache.sort(s)), cache.typ(ty)) }), subst_terms.map({ case ((x, ty), t) => ((cache.string(x), cache.typ(ty)), cache.term(t)) })) def is_inclusion: Boolean = subst_types.isEmpty && subst_terms.isEmpty } def read_locale_dependencies(provider: Export.Provider): List[Entity[Locale_Dependency]] = read_entities(provider, Export.THEORY_PREFIX + "locale_dependencies", Kind.LOCALE_DEPENDENCY, { body => import XML.Decode._ import Term_XML.Decode._ val (source, (target, (prefix, (subst_types, subst_terms)))) = pair(string, pair(string, pair(list(pair(string, bool)), pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body) Locale_Dependency(source, target, prefix, subst_types, subst_terms) }) /* sort algebra */ sealed case class Classrel(class1: String, class2: String, prop: Prop) { def cache(cache: Term.Cache): Classrel = Classrel(cache.string(class1), cache.string(class2), prop.cache(cache)) } def read_classrel(provider: Export.Provider): List[Classrel] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "classrel") val classrel = { import XML.Decode._ list(pair(decode_prop, pair(string, string)))(body) } for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop) } sealed case class Arity( type_name: String, domain: List[Term.Sort], codomain: String, prop: Prop ) { def cache(cache: Term.Cache): Arity = Arity(cache.string(type_name), domain.map(cache.sort), cache.string(codomain), prop.cache(cache)) } def read_arities(provider: Export.Provider): List[Arity] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "arities") val arities = { import XML.Decode._ import Term_XML.Decode._ list(pair(decode_prop, triple(string, list(sort), string)))(body) } for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop) } /* Pure constdefs */ sealed case class Constdef(name: String, axiom_name: String) { def cache(cache: Term.Cache): Constdef = Constdef(cache.string(name), cache.string(axiom_name)) } def read_constdefs(provider: Export.Provider): List[Constdef] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs") val constdefs = { import XML.Decode._ list(pair(string, string))(body) } for ((name, axiom_name) <- constdefs) yield Constdef(name, axiom_name) } /* HOL typedefs */ sealed case class Typedef( name: String, rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String ) { def cache(cache: Term.Cache): Typedef = Typedef(cache.string(name), cache.typ(rep_type), cache.typ(abs_type), cache.string(rep_name), cache.string(abs_name), cache.string(axiom_name)) } def read_typedefs(provider: Export.Provider): List[Typedef] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs") val typedefs = { import XML.Decode._ import Term_XML.Decode._ list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body) } for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs } yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name) } /* HOL datatypes */ sealed case class Datatype( pos: Position.T, name: String, co: Boolean, typargs: List[(String, Term.Sort)], typ: Term.Typ, constructors: List[(Term.Term, Term.Typ)] ) { def id: Option[Long] = Position.Id.unapply(pos) def cache(cache: Term.Cache): Datatype = Datatype( cache.position(pos), cache.string(name), co, typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), cache.typ(typ), constructors.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) })) } def read_datatypes(provider: Export.Provider): List[Datatype] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes") val datatypes = { import XML.Decode._ import Term_XML.Decode._ list(pair(properties, pair(string, pair(bool, pair(list(pair(string, sort)), pair(typ, list(pair(term, typ))))))))(body) } for ((pos, (name, (co, (typargs, (typ, constructors))))) <- datatypes) yield Datatype(pos, name, co, typargs, typ, constructors) } /* Pure spec rules */ sealed abstract class Recursion { def cache(cache: Term.Cache): Recursion = this match { case Primrec(types) => Primrec(types.map(cache.string)) case Primcorec(types) => Primcorec(types.map(cache.string)) case _ => this } } case class Primrec(types: List[String]) extends Recursion case object Recdef extends Recursion case class Primcorec(types: List[String]) extends Recursion case object Corec extends Recursion case object Unknown_Recursion extends Recursion val decode_recursion: XML.Decode.T[Recursion] = { import XML.Decode._ variant(List( - { case (Nil, a) => Primrec(list(string)(a)) case _ => ??? }, - { case (Nil, Nil) => Recdef case _ => ??? }, - { case (Nil, a) => Primcorec(list(string)(a)) case _ => ??? }, - { case (Nil, Nil) => Corec case _ => ??? }, - { case (Nil, Nil) => Unknown_Recursion case _ => ??? })) + { case (Nil, a) => Primrec(list(string)(a)) }, + { case (Nil, Nil) => Recdef }, + { case (Nil, a) => Primcorec(list(string)(a)) }, + { case (Nil, Nil) => Corec }, + { case (Nil, Nil) => Unknown_Recursion })) } sealed abstract class Rough_Classification { def is_equational: Boolean = this.isInstanceOf[Equational] def is_inductive: Boolean = this == Inductive def is_co_inductive: Boolean = this == Co_Inductive def is_relational: Boolean = is_inductive || is_co_inductive def is_unknown: Boolean = this == Unknown def cache(cache: Term.Cache): Rough_Classification = this match { case Equational(recursion) => Equational(recursion.cache(cache)) case _ => this } } case class Equational(recursion: Recursion) extends Rough_Classification case object Inductive extends Rough_Classification case object Co_Inductive extends Rough_Classification case object Unknown extends Rough_Classification val decode_rough_classification: XML.Decode.T[Rough_Classification] = { import XML.Decode._ variant(List( - { case (Nil, a) => Equational(decode_recursion(a)) case _ => ??? }, - { case (Nil, Nil) => Inductive case _ => ??? }, - { case (Nil, Nil) => Co_Inductive case _ => ??? }, - { case (Nil, Nil) => Unknown case _ => ??? })) + { case (Nil, a) => Equational(decode_recursion(a)) }, + { case (Nil, Nil) => Inductive }, + { case (Nil, Nil) => Co_Inductive }, + { case (Nil, Nil) => Unknown })) } sealed case class Spec_Rule( pos: Position.T, name: String, rough_classification: Rough_Classification, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], terms: List[(Term.Term, Term.Typ)], rules: List[Term.Term] ) { def id: Option[Long] = Position.Id.unapply(pos) def cache(cache: Term.Cache): Spec_Rule = Spec_Rule( cache.position(pos), cache.string(name), rough_classification.cache(cache), typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }), rules.map(cache.term)) } def read_spec_rules(provider: Export.Provider): List[Spec_Rule] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules") val spec_rules = { import XML.Decode._ import Term_XML.Decode._ list( pair(properties, pair(string, pair(decode_rough_classification, pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(list(pair(term, typ)), list(term))))))))(body) } for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules) yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules) } /* other entities */ sealed case class Other() extends Content[Other] { override def cache(cache: Term.Cache): Other = this } def read_others(provider: Export.Provider): Map[String, List[Entity[Other]]] = { val kinds = provider(Export.THEORY_PREFIX + "other_kinds") match { case Some(entry) => split_lines(entry.uncompressed.text) case None => Nil } val other = Other() def read_other(kind: String): List[Entity[Other]] = read_entities(provider, Export.THEORY_PREFIX + "other/" + kind, kind, _ => other) kinds.map(kind => kind -> read_other(kind)).toMap } } diff --git a/src/Pure/term_xml.scala b/src/Pure/term_xml.scala --- a/src/Pure/term_xml.scala +++ b/src/Pure/term_xml.scala @@ -1,101 +1,101 @@ /* Title: Pure/term_xml.scala Author: Makarius XML data representation of lambda terms. */ package isabelle object Term_XML { import Term._ object Encode { import XML.Encode._ val indexname: P[Indexname] = { case Indexname(a, 0) => List(a) case Indexname(a, b) => List(a, int_atom(b)) } val sort: T[Sort] = list(string) def typ: T[Typ] = variant[Typ](List( { case Type(a, b) => (List(a), list(typ)(b)) }, { case TFree(a, b) => (List(a), sort(b)) }, { case TVar(a, b) => (indexname(a), sort(b)) })) val typ_body: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t) def term: T[Term] = variant[Term](List( { case Const(a, b) => (List(a), list(typ)(b)) }, { case Free(a, b) => (List(a), typ_body(b)) }, { case Var(a, b) => (indexname(a), typ_body(b)) }, { case Bound(a) => (Nil, int(a)) }, { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) }, { case App(a, b) => (Nil, pair(term, term)(a, b)) })) } object Decode { import XML.Decode._ val indexname: P[Indexname] = { case List(a) => Indexname(a, 0) case List(a, b) => Indexname(a, int_atom(b)) } val sort: T[Sort] = list(string) def typ: T[Typ] = variant[Typ](List( - { case (List(a), b) => Type(a, list(typ)(b)) case _ => ??? }, - { case (List(a), b) => TFree(a, sort(b)) case _ => ??? }, + { case (List(a), b) => Type(a, list(typ)(b)) }, + { case (List(a), b) => TFree(a, sort(b)) }, { case (a, b) => TVar(indexname(a), sort(b)) })) val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) } def term: T[Term] = variant[Term](List( - { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? }, - { case (List(a), b) => Free(a, typ_body(b)) case _ => ??? }, + { case (List(a), b) => Const(a, list(typ)(b)) }, + { case (List(a), b) => Free(a, typ_body(b)) }, { case (a, b) => Var(indexname(a), typ_body(b)) }, - { case (Nil, a) => Bound(int(a)) case _ => ??? }, - { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? }, - { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? })) + { case (Nil, a) => Bound(int(a)) }, + { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, + { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) def term_env(env: Map[String, Typ]): T[Term] = { def env_type(x: String, t: Typ): Typ = if (t == dummyT && env.isDefinedAt(x)) env(x) else t def term: T[Term] = variant[Term](List( - { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? }, - { case (List(a), b) => Free(a, env_type(a, typ_body(b))) case _ => ??? }, + { case (List(a), b) => Const(a, list(typ)(b)) }, + { case (List(a), b) => Free(a, env_type(a, typ_body(b))) }, { case (a, b) => Var(indexname(a), typ_body(b)) }, - { case (Nil, a) => Bound(int(a)) case _ => ??? }, - { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? }, - { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? })) + { case (Nil, a) => Bound(int(a)) }, + { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, + { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) term } def proof_env(env: Map[String, Typ]): T[Proof] = { val term = term_env(env) def proof: T[Proof] = variant[Proof](List( - { case (Nil, Nil) => MinProof case _ => ??? }, - { case (Nil, a) => PBound(int(a)) case _ => ??? }, - { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) case _ => ??? }, - { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) case _ => ??? }, - { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) case _ => ??? }, - { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) case _ => ??? }, - { case (Nil, a) => Hyp(term(a)) case _ => ??? }, - { case (List(a), b) => PAxm(a, list(typ)(b)) case _ => ??? }, - { case (List(a), b) => PClass(typ(b), a) case _ => ??? }, - { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) case _ => ??? }, - { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) case _ => ??? })) + { case (Nil, Nil) => MinProof }, + { case (Nil, a) => PBound(int(a)) }, + { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) }, + { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) }, + { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) }, + { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) }, + { case (Nil, a) => Hyp(term(a)) }, + { case (List(a), b) => PAxm(a, list(typ)(b)) }, + { case (List(a), b) => PClass(typ(b), a) }, + { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) }, + { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) })) proof } val proof: T[Proof] = proof_env(Map.empty) } }