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