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