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