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