src/Pure/Thy/export_theory.scala
author wenzelm
Thu May 17 14:50:48 2018 +0200 (14 months ago)
changeset 68203 cda4f24331d5
parent 68173 7ed88a534bb6
child 68206 dedf1a70d1fa
permissions -rw-r--r--
read theory content from session database;
     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   /** theory content **/
    13 
    14   sealed case class Theory(types: List[Type], consts: List[Const])
    15 
    16   def read_theory(db: SQL.Database, session_name: String, theory_name: String,
    17     types: Boolean = true,
    18     consts: Boolean = true): Theory =
    19   {
    20     Theory(
    21       if (types) read_types(db, session_name, theory_name) else Nil,
    22       if (consts) read_consts(db, session_name, theory_name) else Nil)
    23   }
    24 
    25 
    26   /* entities */
    27 
    28   sealed case class Entity(name: String, serial: Long, pos: Position.T)
    29   {
    30     override def toString: String = name
    31   }
    32 
    33   def decode_entity(tree: XML.Tree): (Entity, XML.Body) =
    34   {
    35     def err(): Nothing = throw new XML.XML_Body(List(tree))
    36 
    37     tree match {
    38       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
    39         val name = Markup.Name.unapply(props) getOrElse err()
    40         val serial = Markup.Serial.unapply(props) getOrElse err()
    41         val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) })
    42         (Entity(name, serial, pos), body)
    43       case _ => err()
    44     }
    45   }
    46 
    47   def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
    48     export_name: String, decode: XML.Tree => A): List[A] =
    49   {
    50     Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
    51       case Some(entry) => entry.uncompressed_yxml().map(decode(_))
    52       case None => Nil
    53     }
    54   }
    55 
    56 
    57   /* types */
    58 
    59   sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
    60 
    61   def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
    62     read_entities(db, session_name, theory_name, "types",
    63       (tree: XML.Tree) =>
    64         {
    65           val (entity, body) = decode_entity(tree)
    66           val (args, abbrev) =
    67           {
    68             import XML.Decode._
    69             pair(list(string), option(Term_XML.Decode.typ))(body)
    70           }
    71           Type(entity, args, abbrev)
    72         })
    73 
    74 
    75   /* consts */
    76 
    77   sealed case class Const(
    78     entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
    79 
    80   def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
    81     read_entities(db, session_name, theory_name, "consts",
    82       (tree: XML.Tree) =>
    83         {
    84           val (entity, body) = decode_entity(tree)
    85           val (args, typ, abbrev) =
    86           {
    87             import XML.Decode._
    88             triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
    89           }
    90           Const(entity, args, typ, abbrev)
    91         })
    92 }