src/Pure/Thy/export_theory.scala
author wenzelm
Sat Sep 15 23:35:46 2018 +0200 (10 months ago)
changeset 68997 4278947ba336
parent 68864 1dacce27bc25
child 69003 a015f1d3ba0c
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(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     locales: Boolean = true,
    34     classrel: Boolean = true,
    35     arities: Boolean = true,
    36     typedefs: Boolean = true,
    37     cache: Term.Cache = Term.make_cache()): Session =
    38   {
    39     val thys =
    40       using(store.open_database(session_name))(db =>
    41       {
    42         db.transaction {
    43           Export.read_theory_names(db, session_name).map((theory_name: String) =>
    44             read_theory(Export.Provider.database(db, session_name, theory_name),
    45               session_name, theory_name, types = types, consts = consts,
    46               axioms = axioms, facts = facts, classes = classes, locales = locales,
    47               classrel = classrel, arities = arities, typedefs = typedefs,
    48               cache = Some(cache)))
    49         }
    50       })
    51 
    52     val graph0 =
    53       (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) }
    54     val graph1 =
    55       (graph0 /: thys) { case (g0, thy) =>
    56         (g0 /: thy.parents) { case (g1, parent) =>
    57           g1.default_node(parent, empty_theory(parent)).add_edge_acyclic(parent, thy.name) } }
    58 
    59     Session(session_name, graph1)
    60   }
    61 
    62 
    63 
    64   /** theory content **/
    65 
    66   val export_prefix: String = "theory/"
    67 
    68   sealed case class Theory(name: String, parents: List[String],
    69     types: List[Type],
    70     consts: List[Const],
    71     axioms: List[Fact_Single],
    72     facts: List[Fact_Multi],
    73     classes: List[Class],
    74     locales: List[Locale],
    75     classrel: List[Classrel],
    76     arities: List[Arity],
    77     typedefs: List[Typedef])
    78   {
    79     override def toString: String = name
    80 
    81     lazy val entities: Set[Long] =
    82       Set.empty[Long] ++
    83         types.iterator.map(_.entity.serial) ++
    84         consts.iterator.map(_.entity.serial) ++
    85         axioms.iterator.map(_.entity.serial) ++
    86         facts.iterator.map(_.entity.serial) ++
    87         classes.iterator.map(_.entity.serial) ++
    88         locales.iterator.map(_.entity.serial)
    89 
    90     def cache(cache: Term.Cache): Theory =
    91       Theory(cache.string(name),
    92         parents.map(cache.string(_)),
    93         types.map(_.cache(cache)),
    94         consts.map(_.cache(cache)),
    95         axioms.map(_.cache(cache)),
    96         facts.map(_.cache(cache)),
    97         classes.map(_.cache(cache)),
    98         locales.map(_.cache(cache)),
    99         classrel.map(_.cache(cache)),
   100         arities.map(_.cache(cache)),
   101         typedefs.map(_.cache(cache)))
   102   }
   103 
   104   def empty_theory(name: String): Theory =
   105     Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
   106 
   107   def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
   108     types: Boolean = true,
   109     consts: Boolean = true,
   110     axioms: Boolean = true,
   111     facts: Boolean = true,
   112     classes: Boolean = true,
   113     locales: Boolean = true,
   114     classrel: Boolean = true,
   115     arities: Boolean = true,
   116     typedefs: Boolean = true,
   117     cache: Option[Term.Cache] = None): Theory =
   118   {
   119     val parents =
   120       provider(export_prefix + "parents") match {
   121         case Some(entry) => split_lines(entry.uncompressed().text)
   122         case None =>
   123           error("Missing theory export in session " + quote(session_name) + ": " +
   124             quote(theory_name))
   125       }
   126     val theory =
   127       Theory(theory_name, parents,
   128         if (types) read_types(provider) else Nil,
   129         if (consts) read_consts(provider) else Nil,
   130         if (axioms) read_axioms(provider) else Nil,
   131         if (facts) read_facts(provider) else Nil,
   132         if (classes) read_classes(provider) else Nil,
   133         if (locales) read_locales(provider) else Nil,
   134         if (classrel) read_classrel(provider) else Nil,
   135         if (arities) read_arities(provider) else Nil,
   136         if (typedefs) read_typedefs(provider) else Nil)
   137     if (cache.isDefined) theory.cache(cache.get) else theory
   138   }
   139 
   140   def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
   141   {
   142     val session_name = Thy_Header.PURE
   143     val theory_name = Thy_Header.PURE
   144 
   145     using(store.open_database(session_name))(db =>
   146     {
   147       db.transaction {
   148         read_theory(Export.Provider.database(db, session_name, theory_name),
   149           session_name, theory_name, cache = cache)
   150       }
   151     })
   152   }
   153 
   154 
   155   /* entities */
   156 
   157   object Kind extends Enumeration
   158   {
   159     val TYPE = Value("type")
   160     val CONST = Value("const")
   161     val AXIOM = Value("axiom")
   162     val FACT = Value("fact")
   163     val CLASS = Value("class")
   164     val LOCALE = Value("locale")
   165   }
   166 
   167   sealed case class Entity(
   168     kind: Kind.Value, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long)
   169   {
   170     override def toString: String = kind.toString + " " + quote(name)
   171 
   172     def cache(cache: Term.Cache): Entity =
   173       Entity(kind, cache.string(name), cache.string(xname), cache.position(pos), id, serial)
   174   }
   175 
   176   def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
   177   {
   178     def err(): Nothing = throw new XML.XML_Body(List(tree))
   179 
   180     tree match {
   181       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
   182         val name = Markup.Name.unapply(props) getOrElse err()
   183         val xname = Markup.XName.unapply(props) getOrElse err()
   184         val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
   185         val id = Position.Id.unapply(props)
   186         val serial = Markup.Serial.unapply(props) getOrElse err()
   187         (Entity(kind, name, xname, pos, id, serial), body)
   188       case _ => err()
   189     }
   190   }
   191 
   192 
   193   /* types */
   194 
   195   sealed case class Type(entity: Entity, args: List[String], abbrev: Option[Term.Typ])
   196   {
   197     def cache(cache: Term.Cache): Type =
   198       Type(entity.cache(cache),
   199         args.map(cache.string(_)),
   200         abbrev.map(cache.typ(_)))
   201   }
   202 
   203   def read_types(provider: Export.Provider): List[Type] =
   204     provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
   205       {
   206         val (entity, body) = decode_entity(Kind.TYPE, tree)
   207         val (args, abbrev) =
   208         {
   209           import XML.Decode._
   210           pair(list(string), option(Term_XML.Decode.typ))(body)
   211         }
   212         Type(entity, args, abbrev)
   213       })
   214 
   215 
   216   /* consts */
   217 
   218   sealed case class Const(
   219     entity: Entity, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term])
   220   {
   221     def cache(cache: Term.Cache): Const =
   222       Const(entity.cache(cache),
   223         typargs.map(cache.string(_)),
   224         cache.typ(typ),
   225         abbrev.map(cache.term(_)))
   226   }
   227 
   228   def read_consts(provider: Export.Provider): List[Const] =
   229     provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
   230       {
   231         val (entity, body) = decode_entity(Kind.CONST, tree)
   232         val (args, typ, abbrev) =
   233         {
   234           import XML.Decode._
   235           triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
   236         }
   237         Const(entity, args, typ, abbrev)
   238       })
   239 
   240 
   241   /* facts */
   242 
   243   sealed case class Prop(
   244     typargs: List[(String, Term.Sort)],
   245     args: List[(String, Term.Typ)],
   246     term: Term.Term)
   247   {
   248     def cache(cache: Term.Cache): Prop =
   249       Prop(
   250         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   251         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   252         cache.term(term))
   253   }
   254 
   255   def decode_prop(body: XML.Body): Prop =
   256   {
   257     val (typargs, args, t) =
   258     {
   259       import XML.Decode._
   260       import Term_XML.Decode._
   261       triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
   262     }
   263     Prop(typargs, args, t)
   264   }
   265 
   266   sealed case class Fact_Single(entity: Entity, prop: Prop)
   267   {
   268     def cache(cache: Term.Cache): Fact_Single =
   269       Fact_Single(entity.cache(cache), prop.cache(cache))
   270   }
   271 
   272   sealed case class Fact_Multi(entity: Entity, props: List[Prop])
   273   {
   274     def cache(cache: Term.Cache): Fact_Multi =
   275       Fact_Multi(entity.cache(cache), props.map(_.cache(cache)))
   276 
   277     def split: List[Fact_Single] =
   278       props match {
   279         case List(prop) => List(Fact_Single(entity, prop))
   280         case _ =>
   281           for ((prop, i) <- props.zipWithIndex)
   282           yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), prop)
   283       }
   284   }
   285 
   286   def read_axioms(provider: Export.Provider): List[Fact_Single] =
   287     provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
   288       {
   289         val (entity, body) = decode_entity(Kind.AXIOM, tree)
   290         val prop = decode_prop(body)
   291         Fact_Single(entity, prop)
   292       })
   293 
   294   def read_facts(provider: Export.Provider): List[Fact_Multi] =
   295     provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
   296       {
   297         val (entity, body) = decode_entity(Kind.FACT, tree)
   298         val props = XML.Decode.list(decode_prop)(body)
   299         Fact_Multi(entity, props)
   300       })
   301 
   302 
   303   /* type classes */
   304 
   305   sealed case class Class(
   306     entity: Entity, params: List[(String, Term.Typ)], axioms: List[Term.Term])
   307   {
   308     def cache(cache: Term.Cache): Class =
   309       Class(entity.cache(cache),
   310         params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   311         axioms.map(cache.term(_)))
   312   }
   313 
   314   def read_classes(provider: Export.Provider): List[Class] =
   315     provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
   316       {
   317         val (entity, body) = decode_entity(Kind.CLASS, tree)
   318         val (params, axioms) =
   319         {
   320           import XML.Decode._
   321           import Term_XML.Decode._
   322           pair(list(pair(string, typ)), list(term))(body)
   323         }
   324         Class(entity, params, axioms)
   325       })
   326 
   327 
   328   /* locales */
   329 
   330   sealed case class Locale(
   331     entity: Entity, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)],
   332       asm: Option[Term.Term], defs: List[Term.Term])
   333   {
   334     def cache(cache: Term.Cache): Locale =
   335       Locale(entity.cache(cache),
   336         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   337         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   338         asm.map(cache.term(_)),
   339         defs.map(cache.term(_)))
   340   }
   341 
   342   def read_locales(provider: Export.Provider): List[Locale] =
   343     provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
   344       {
   345         val (entity, body) = decode_entity(Kind.LOCALE, tree)
   346         val (typargs, (args, (asm, defs))) =
   347         {
   348           import XML.Decode._
   349           import Term_XML.Decode._
   350           pair(list(pair(string, sort)),
   351             pair(list(pair(string, typ)),
   352               pair(option(term), list(term))))(body)
   353         }
   354         Locale(entity, typargs, args, asm, defs)
   355       })
   356 
   357 
   358   /* sort algebra */
   359 
   360   sealed case class Classrel(class_name: String, super_names: List[String])
   361   {
   362     def cache(cache: Term.Cache): Classrel =
   363       Classrel(cache.string(class_name), super_names.map(cache.string(_)))
   364   }
   365 
   366   def read_classrel(provider: Export.Provider): List[Classrel] =
   367   {
   368     val body = provider.uncompressed_yxml(export_prefix + "classrel")
   369     val classrel =
   370     {
   371       import XML.Decode._
   372       list(pair(string, list(string)))(body)
   373     }
   374     for ((c, cs) <- classrel) yield Classrel(c, cs)
   375   }
   376 
   377   sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
   378   {
   379     def cache(cache: Term.Cache): Arity =
   380       Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
   381   }
   382 
   383   def read_arities(provider: Export.Provider): List[Arity] =
   384   {
   385     val body = provider.uncompressed_yxml(export_prefix + "arities")
   386     val arities =
   387     {
   388       import XML.Decode._
   389       import Term_XML.Decode._
   390       list(triple(string, list(sort), string))(body)
   391     }
   392     for ((a, b, c) <- arities) yield Arity(a, b, c)
   393   }
   394 
   395 
   396   /* HOL typedefs */
   397 
   398   sealed case class Typedef(name: String,
   399     rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
   400   {
   401     def cache(cache: Term.Cache): Typedef =
   402       Typedef(cache.string(name),
   403         cache.typ(rep_type),
   404         cache.typ(abs_type),
   405         cache.string(rep_name),
   406         cache.string(abs_name),
   407         cache.string(axiom_name))
   408   }
   409 
   410   def read_typedefs(provider: Export.Provider): List[Typedef] =
   411   {
   412     val body = provider.uncompressed_yxml(export_prefix + "typedefs")
   413     val typedefs =
   414     {
   415       import XML.Decode._
   416       import Term_XML.Decode._
   417       list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   418     }
   419     for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   420     yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   421   }
   422 }