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