src/Pure/Thy/export_theory.scala
author wenzelm
Fri May 18 16:30:20 2018 +0200 (14 months ago)
changeset 68208 d9f2cf4fc002
parent 68206 dedf1a70d1fa
child 68209 aeffd8f1f079
permissions -rw-r--r--
more exports;
     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(session_name: String,
    27     system_mode: Boolean = false,
    28     types: Boolean = true,
    29     consts: Boolean = true): Session =
    30   {
    31     val store = Sessions.store(system_mode)
    32 
    33     val thys =
    34       using(SQLite.open_database(store.the_database(session_name)))(db =>
    35       {
    36         db.transaction {
    37           Export.read_theory_names(db, session_name).iterator.map(_._1).toSet.iterator.
    38             map((theory_name: String) =>
    39               read_theory(db, session_name, theory_name, types = types, consts = consts)).toList
    40         }
    41       })
    42 
    43     val graph0 =
    44       (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) }
    45     val graph1 =
    46       (graph0 /: thys) { case (g0, thy) =>
    47         (g0 /: thy.parents) { case (g1, parent) =>
    48           g1.default_node(parent, empty_theory(parent)).add_edge_acyclic(parent, thy.name) } }
    49 
    50     Session(session_name, graph1)
    51   }
    52 
    53 
    54 
    55   /** theory content **/
    56 
    57   sealed case class Theory(name: String, parents: List[String],
    58     types: List[Type],
    59     consts: List[Const],
    60     axioms: List[Axiom])
    61   {
    62     override def toString: String = name
    63   }
    64 
    65   def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil)
    66 
    67   def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    68     types: Boolean = true,
    69     consts: Boolean = true,
    70     axioms: Boolean = true): Theory =
    71   {
    72     val parents =
    73       Export.read_entry(db, session_name, theory_name, "theory/parents") match {
    74         case Some(entry) =>
    75           import XML.Decode._
    76           list(string)(entry.uncompressed_yxml())
    77         case None =>
    78           error("Missing theory export in session " + quote(session_name) + ": " +
    79             quote(theory_name))
    80       }
    81     Theory(theory_name, parents,
    82       if (types) read_types(db, session_name, theory_name) else Nil,
    83       if (consts) read_consts(db, session_name, theory_name) else Nil,
    84       if (axioms) read_axioms(db, session_name, theory_name) else Nil)
    85   }
    86 
    87 
    88   /* entities */
    89 
    90   sealed case class Entity(name: String, serial: Long, pos: Position.T)
    91   {
    92     override def toString: String = name
    93   }
    94 
    95   def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
    96   {
    97     def err(): Nothing = throw new XML.XML_Body(List(tree))
    98 
    99     tree match {
   100       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
   101         val name = Markup.Name.unapply(props) getOrElse err()
   102         val serial = Markup.Serial.unapply(props) getOrElse err()
   103         val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
   104         (Entity(name, serial, pos), body)
   105       case _ => err()
   106     }
   107   }
   108 
   109   def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
   110     export_name: String, decode: XML.Tree => A): List[A] =
   111   {
   112     Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
   113       case Some(entry) => entry.uncompressed_yxml().map(decode(_))
   114       case None => Nil
   115     }
   116   }
   117 
   118 
   119   /* types */
   120 
   121   sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
   122 
   123   def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
   124     read_entities(db, session_name, theory_name, "types",
   125       (tree: XML.Tree) =>
   126         {
   127           val (entity, body) = decode_entity(tree)
   128           val (args, abbrev) =
   129           {
   130             import XML.Decode._
   131             pair(list(string), option(Term_XML.Decode.typ))(body)
   132           }
   133           Type(entity, args, abbrev)
   134         })
   135 
   136 
   137   /* consts */
   138 
   139   sealed case class Const(
   140     entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
   141 
   142   def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
   143     read_entities(db, session_name, theory_name, "consts",
   144       (tree: XML.Tree) =>
   145         {
   146           val (entity, body) = decode_entity(tree)
   147           val (args, typ, abbrev) =
   148           {
   149             import XML.Decode._
   150             triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   151           }
   152           Const(entity, args, typ, abbrev)
   153         })
   154 
   155 
   156   /* axioms */
   157 
   158   sealed case class Axiom(
   159     entity: Entity,
   160     typargs: List[(String, Term.Sort)],
   161     args: List[(String, Term.Typ)],
   162     prop: Term.Term)
   163 
   164   def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
   165     read_entities(db, session_name, theory_name, "axioms",
   166       (tree: XML.Tree) =>
   167         {
   168           val (entity, body) = decode_entity(tree)
   169           val (typargs, args, prop) =
   170           {
   171             import XML.Decode._
   172             import Term_XML.Decode._
   173             triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
   174           }
   175           Axiom(entity, typargs, args, prop)
   176         })
   177 }