1/* Title: Pure/Thy/export_theory.scala 2 Author: Makarius 3 4Export foundational theory content. 5*/ 6 7package isabelle 8 9 10object Export_Theory 11{ 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 26 def read_session(store: Sessions.Store, 27 session_name: String, 28 types: Boolean = true, 29 consts: Boolean = true, 30 axioms: Boolean = true, 31 facts: Boolean = true, 32 classes: Boolean = true, 33 typedefs: Boolean = true, 34 classrel: Boolean = true, 35 arities: Boolean = true, 36 cache: Term.Cache = Term.make_cache()): Session = 37 { 38 val thys = 39 using(store.open_database(session_name))(db => 40 { 41 db.transaction { 42 Export.read_theory_names(db, session_name).map((theory_name: String) => 43 read_theory(Export.Provider.database(db, session_name, theory_name), 44 session_name, theory_name, types = types, consts = consts, 45 axioms = axioms, facts = facts, classes = classes, typedefs = typedefs, 46 cache = Some(cache))) 47 } 48 }) 49 50 val graph0 = 51 (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) } 52 val graph1 = 53 (graph0 /: thys) { case (g0, thy) => 54 (g0 /: thy.parents) { case (g1, parent) => 55 g1.default_node(parent, empty_theory(parent)).add_edge_acyclic(parent, thy.name) } } 56 57 Session(session_name, graph1) 58 } 59 60 61 62 /** theory content **/ 63 64 val export_prefix: String = "theory/" 65 66 sealed case class Theory(name: String, parents: List[String], 67 types: List[Type], 68 consts: List[Const], 69 axioms: List[Axiom], 70 facts: List[Fact], 71 classes: List[Class], 72 typedefs: List[Typedef], 73 classrel: List[Classrel], 74 arities: List[Arity]) 75 { 76 override def toString: String = name 77 78 def cache(cache: Term.Cache): Theory = 79 Theory(cache.string(name), 80 parents.map(cache.string(_)), 81 types.map(_.cache(cache)), 82 consts.map(_.cache(cache)), 83 axioms.map(_.cache(cache)), 84 facts.map(_.cache(cache)), 85 classes.map(_.cache(cache)), 86 typedefs.map(_.cache(cache)), 87 classrel.map(_.cache(cache)), 88 arities.map(_.cache(cache))) 89 } 90 91 def empty_theory(name: String): Theory = 92 Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil) 93 94 def read_theory(provider: Export.Provider, session_name: String, theory_name: String, 95 types: Boolean = true, 96 consts: Boolean = true, 97 axioms: Boolean = true, 98 facts: Boolean = true, 99 classes: Boolean = true, 100 typedefs: Boolean = true, 101 classrel: Boolean = true, 102 arities: Boolean = true, 103 cache: Option[Term.Cache] = None): Theory = 104 { 105 val parents = 106 provider(export_prefix + "parents") match { 107 case Some(entry) => split_lines(entry.uncompressed().text) 108 case None => 109 error("Missing theory export in session " + quote(session_name) + ": " + 110 quote(theory_name)) 111 } 112 val theory = 113 Theory(theory_name, parents, 114 if (types) read_types(provider) else Nil, 115 if (consts) read_consts(provider) else Nil, 116 if (axioms) read_axioms(provider) else Nil, 117 if (facts) read_facts(provider) else Nil, 118 if (classes) read_classes(provider) else Nil, 119 if (typedefs) read_typedefs(provider) else Nil, 120 if (classrel) read_classrel(provider) else Nil, 121 if (arities) read_arities(provider) else Nil) 122 if (cache.isDefined) theory.cache(cache.get) else theory 123 } 124 125 126 /* entities */ 127 128 sealed case class Entity(name: String, serial: Long, pos: Position.T) 129 { 130 override def toString: String = name 131 132 def cache(cache: Term.Cache): Entity = 133 Entity(cache.string(name), serial, cache.position(pos)) 134 } 135 136 def decode_entity(tree: XML.Tree): (Entity, XML.Body) = 137 { 138 def err(): Nothing = throw new XML.XML_Body(List(tree)) 139 140 tree match { 141 case XML.Elem(Markup(Markup.ENTITY, props), body) => 142 val name = Markup.Name.unapply(props) getOrElse err() 143 val serial = Markup.Serial.unapply(props) getOrElse err() 144 val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) 145 (Entity(name, serial, pos), body) 146 case _ => err() 147 } 148 } 149 150 151 /* types */ 152 153 sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ]) 154 { 155 def cache(cache: Term.Cache): Type = 156 Type(entity.cache(cache), 157 args.map(cache.string(_)), 158 abbrev.map(cache.typ(_))) 159 } 160 161 def read_types(provider: Export.Provider): List[Type] = 162 provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) => 163 { 164 val (entity, body) = decode_entity(tree) 165 val (args, abbrev) = 166 { 167 import XML.Decode._ 168 pair(list(string), option(Term_XML.Decode.typ))(body) 169 } 170 Type(entity, args, abbrev) 171 }) 172 173 174 /* consts */ 175 176 sealed case class Const( 177 entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term]) 178 { 179 def cache(cache: Term.Cache): Const = 180 Const(entity.cache(cache), 181 typargs.map(cache.string(_)), 182 cache.typ(typ), 183 abbrev.map(cache.term(_))) 184 } 185 186 def read_consts(provider: Export.Provider): List[Const] = 187 provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) => 188 { 189 val (entity, body) = decode_entity(tree) 190 val (args, typ, abbrev) = 191 { 192 import XML.Decode._ 193 triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body) 194 } 195 Const(entity, args, typ, abbrev) 196 }) 197 198 199 /* axioms and facts */ 200 201 def decode_props(body: XML.Body): 202 (List[(String, Term.Sort)], List[(String, Term.Typ)], List[Term.Term]) = 203 { 204 import XML.Decode._ 205 import Term_XML.Decode._ 206 triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body) 207 } 208 209 sealed case class Axiom( 210 entity: Entity, 211 typargs: List[(String, Term.Sort)], 212 args: List[(String, Term.Typ)], 213 prop: Term.Term) 214 { 215 def cache(cache: Term.Cache): Axiom = 216 Axiom(entity.cache(cache), 217 typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), 218 args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), 219 cache.term(prop)) 220 } 221 222 def read_axioms(provider: Export.Provider): List[Axiom] = 223 provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) => 224 { 225 val (entity, body) = decode_entity(tree) 226 val (typargs, args, List(prop)) = decode_props(body) 227 Axiom(entity, typargs, args, prop) 228 }) 229 230 sealed case class Fact( 231 entity: Entity, 232 typargs: List[(String, Term.Sort)], 233 args: List[(String, Term.Typ)], 234 props: List[Term.Term]) 235 { 236 def cache(cache: Term.Cache): Fact = 237 Fact(entity.cache(cache), 238 typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), 239 args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), 240 props.map(cache.term(_))) 241 } 242 243 def read_facts(provider: Export.Provider): List[Fact] = 244 provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) => 245 { 246 val (entity, body) = decode_entity(tree) 247 val (typargs, args, props) = decode_props(body) 248 Fact(entity, typargs, args, props) 249 }) 250 251 252 /* type classes */ 253 254 sealed case class Class( 255 entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term]) 256 { 257 def cache(cache: Term.Cache): Class = 258 Class(entity.cache(cache), 259 params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), 260 axioms.map(cache.term(_))) 261 } 262 263 def read_classes(provider: Export.Provider): List[Class] = 264 provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) => 265 { 266 val (entity, body) = decode_entity(tree) 267 val (params, axioms) = 268 { 269 import XML.Decode._ 270 import Term_XML.Decode._ 271 pair(list(pair(string, typ)), list(term))(body) 272 } 273 Class(entity, params, axioms) 274 }) 275 276 277 /* sort algebra */ 278 279 sealed case class Classrel(class_name: String, super_names: List[String]) 280 { 281 def cache(cache: Term.Cache): Classrel = 282 Classrel(cache.string(class_name), super_names.map(cache.string(_))) 283 } 284 285 def read_classrel(provider: Export.Provider): List[Classrel] = 286 { 287 val body = provider.uncompressed_yxml(export_prefix + "classrel") 288 val classrel = 289 { 290 import XML.Decode._ 291 list(pair(string, list(string)))(body) 292 } 293 for ((c, cs) <- classrel) yield Classrel(c, cs) 294 } 295 296 sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String) 297 { 298 def cache(cache: Term.Cache): Arity = 299 Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain)) 300 } 301 302 def read_arities(provider: Export.Provider): List[Arity] = 303 { 304 val body = provider.uncompressed_yxml(export_prefix + "arities") 305 val arities = 306 { 307 import XML.Decode._ 308 import Term_XML.Decode._ 309 list(triple(string, list(sort), string))(body) 310 } 311 for ((a, b, c) <- arities) yield Arity(a, b, c) 312 } 313 314 315 /* HOL typedefs */ 316 317 sealed case class Typedef(name: String, 318 rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String) 319 { 320 def cache(cache: Term.Cache): Typedef = 321 Typedef(cache.string(name), 322 cache.typ(rep_type), 323 cache.typ(abs_type), 324 cache.string(rep_name), 325 cache.string(abs_name), 326 cache.string(axiom_name)) 327 } 328 329 def read_typedefs(provider: Export.Provider): List[Typedef] = 330 { 331 val body = provider.uncompressed_yxml(export_prefix + "typedefs") 332 val typedefs = 333 { 334 import XML.Decode._ 335 import Term_XML.Decode._ 336 list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body) 337 } 338 for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs } 339 yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name) 340 } 341} 342