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