src/Pure/Thy/export_theory.scala
author wenzelm
Thu May 24 21:36:39 2018 +0200 (14 months ago)
changeset 68267 6a29709906c6
parent 68264 bb9a3be6952a
child 68295 781a98696638
permissions -rw-r--r--
more scalable JVM memory management;
     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 {
    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     cache: Term.Cache = Term.make_cache()): Session =
    35   {
    36     val thys =
    37       using(store.open_database(session_name))(db =>
    38       {
    39         db.transaction {
    40           Export.read_theory_names(db, session_name).map((theory_name: String) =>
    41             read_theory(db, session_name, theory_name, types = types, consts = consts,
    42               axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
    43               cache = Some(cache)))
    44         }
    45       })
    46 
    47     val graph0 =
    48       (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) }
    49     val graph1 =
    50       (graph0 /: thys) { case (g0, thy) =>
    51         (g0 /: thy.parents) { case (g1, parent) =>
    52           g1.default_node(parent, empty_theory(parent)).add_edge_acyclic(parent, thy.name) } }
    53 
    54     Session(session_name, graph1)
    55   }
    56 
    57 
    58 
    59   /** theory content **/
    60 
    61   sealed case class Theory(name: String, parents: List[String],
    62     types: List[Type],
    63     consts: List[Const],
    64     axioms: List[Axiom],
    65     facts: List[Fact],
    66     classes: List[Class],
    67     typedefs: List[Typedef])
    68   {
    69     override def toString: String = name
    70 
    71     def cache(cache: Term.Cache): Theory =
    72       Theory(cache.string(name),
    73         parents.map(cache.string(_)),
    74         types.map(_.cache(cache)),
    75         consts.map(_.cache(cache)),
    76         axioms.map(_.cache(cache)),
    77         facts.map(_.cache(cache)),
    78         classes.map(_.cache(cache)),
    79         typedefs.map(_.cache(cache)))
    80   }
    81 
    82   def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    83 
    84   def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    85     types: Boolean = true,
    86     consts: Boolean = true,
    87     axioms: Boolean = true,
    88     facts: Boolean = true,
    89     classes: Boolean = true,
    90     typedefs: Boolean = true,
    91     cache: Option[Term.Cache] = None): Theory =
    92   {
    93     val parents =
    94       Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    95         case Some(entry) => split_lines(entry.uncompressed().text)
    96         case None =>
    97           error("Missing theory export in session " + quote(session_name) + ": " +
    98             quote(theory_name))
    99       }
   100     val theory =
   101       Theory(theory_name, parents,
   102         if (types) read_types(db, session_name, theory_name) else Nil,
   103         if (consts) read_consts(db, session_name, theory_name) else Nil,
   104         if (axioms) read_axioms(db, session_name, theory_name) else Nil,
   105         if (facts) read_facts(db, session_name, theory_name) else Nil,
   106         if (classes) read_classes(db, session_name, theory_name) else Nil,
   107         if (typedefs) read_typedefs(db, session_name, theory_name) else Nil)
   108     if (cache.isDefined) theory.cache(cache.get) else theory
   109   }
   110 
   111 
   112   /* entities */
   113 
   114   sealed case class Entity(name: String, serial: Long, pos: Position.T)
   115   {
   116     override def toString: String = name
   117 
   118     def cache(cache: Term.Cache): Entity =
   119       Entity(cache.string(name), serial, cache.position(pos))
   120   }
   121 
   122   def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
   123   {
   124     def err(): Nothing = throw new XML.XML_Body(List(tree))
   125 
   126     tree match {
   127       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
   128         val name = Markup.Name.unapply(props) getOrElse err()
   129         val serial = Markup.Serial.unapply(props) getOrElse err()
   130         val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
   131         (Entity(name, serial, pos), body)
   132       case _ => err()
   133     }
   134   }
   135 
   136   def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
   137     export_name: String, decode: XML.Body => List[A]): List[A] =
   138   {
   139     Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
   140       case Some(entry) => decode(entry.uncompressed_yxml())
   141       case None => Nil
   142     }
   143   }
   144 
   145   def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
   146     export_name: String, decode: XML.Tree => A): List[A] =
   147   {
   148     read_export(db, session_name, theory_name, export_name,
   149       (body: XML.Body) => body.map(decode(_)))
   150   }
   151 
   152 
   153   /* types */
   154 
   155   sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
   156   {
   157     def cache(cache: Term.Cache): Type =
   158       Type(entity.cache(cache),
   159         args.map(cache.string(_)),
   160         abbrev.map(cache.typ(_)))
   161   }
   162 
   163   def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
   164     read_entities(db, session_name, theory_name, "types",
   165       (tree: XML.Tree) =>
   166         {
   167           val (entity, body) = decode_entity(tree)
   168           val (args, abbrev) =
   169           {
   170             import XML.Decode._
   171             pair(list(string), option(Term_XML.Decode.typ))(body)
   172           }
   173           Type(entity, args, abbrev)
   174         })
   175 
   176 
   177   /* consts */
   178 
   179   sealed case class Const(
   180     entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
   181   {
   182     def cache(cache: Term.Cache): Const =
   183       Const(entity.cache(cache),
   184         typargs.map(cache.string(_)),
   185         cache.typ(typ),
   186         abbrev.map(cache.term(_)))
   187   }
   188 
   189   def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
   190     read_entities(db, session_name, theory_name, "consts",
   191       (tree: XML.Tree) =>
   192         {
   193           val (entity, body) = decode_entity(tree)
   194           val (args, typ, abbrev) =
   195           {
   196             import XML.Decode._
   197             triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   198           }
   199           Const(entity, args, typ, abbrev)
   200         })
   201 
   202 
   203   /* axioms and facts */
   204 
   205   def decode_props(body: XML.Body):
   206     (List[(String, Term.Sort)], List[(String, Term.Typ)], List[Term.Term]) =
   207   {
   208     import XML.Decode._
   209     import Term_XML.Decode._
   210     triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
   211   }
   212 
   213   sealed case class Axiom(
   214     entity: Entity,
   215     typargs: List[(String, Term.Sort)],
   216     args: List[(String, Term.Typ)],
   217     prop: Term.Term)
   218   {
   219     def cache(cache: Term.Cache): Axiom =
   220       Axiom(entity.cache(cache),
   221         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   222         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   223         cache.term(prop))
   224   }
   225 
   226   def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
   227     read_entities(db, session_name, theory_name, "axioms",
   228       (tree: XML.Tree) =>
   229         {
   230           val (entity, body) = decode_entity(tree)
   231           val (typargs, args, List(prop)) = decode_props(body)
   232           Axiom(entity, typargs, args, prop)
   233         })
   234 
   235   sealed case class Fact(
   236     entity: Entity,
   237     typargs: List[(String, Term.Sort)],
   238     args: List[(String, Term.Typ)],
   239     props: List[Term.Term])
   240   {
   241     def cache(cache: Term.Cache): Fact =
   242       Fact(entity.cache(cache),
   243         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   244         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   245         props.map(cache.term(_)))
   246   }
   247 
   248   def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
   249     read_entities(db, session_name, theory_name, "facts",
   250       (tree: XML.Tree) =>
   251         {
   252           val (entity, body) = decode_entity(tree)
   253           val (typargs, args, props) = decode_props(body)
   254           Fact(entity, typargs, args, props)
   255         })
   256 
   257 
   258   /* type classes */
   259 
   260   sealed case class Class(
   261     entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
   262   {
   263     def cache(cache: Term.Cache): Class =
   264       Class(entity.cache(cache),
   265         params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   266         axioms.map(cache.term(_)))
   267   }
   268 
   269   def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
   270     read_entities(db, session_name, theory_name, "classes",
   271       (tree: XML.Tree) =>
   272         {
   273           val (entity, body) = decode_entity(tree)
   274           val (params, axioms) =
   275           {
   276             import XML.Decode._
   277             import Term_XML.Decode._
   278             pair(list(pair(string, typ)), list(term))(body)
   279           }
   280           Class(entity, params, axioms)
   281         })
   282 
   283 
   284   /* HOL typedefs */
   285 
   286   sealed case class Typedef(name: String,
   287     rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
   288   {
   289     def cache(cache: Term.Cache): Typedef =
   290       Typedef(cache.string(name),
   291         cache.typ(rep_type),
   292         cache.typ(abs_type),
   293         cache.string(rep_name),
   294         cache.string(abs_name),
   295         cache.string(axiom_name))
   296   }
   297 
   298   def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
   299     read_export(db, session_name, theory_name, "typedefs",
   300       (body: XML.Body) =>
   301         {
   302           val typedefs =
   303           {
   304             import XML.Decode._
   305             import Term_XML.Decode._
   306             list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   307           }
   308           for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   309           yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   310         })
   311 }