src/Pure/Thy/export_theory.scala
author wenzelm
Sat Jul 20 12:52:29 2019 +0200 (4 months ago)
changeset 70384 8ce08b154aa1
parent 69996 8f2d3a27aff0
child 70534 fb876ebbf5a7
permissions -rw-r--r--
clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
     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     locale_dependencies: Boolean = true,
    35     classrel: Boolean = true,
    36     arities: Boolean = true,
    37     typedefs: Boolean = true,
    38     cache: Term.Cache = Term.make_cache()): Session =
    39   {
    40     val thys =
    41       using(store.open_database(session_name))(db =>
    42       {
    43         db.transaction {
    44           Export.read_theory_names(db, session_name).map((theory_name: String) =>
    45             read_theory(Export.Provider.database(db, session_name, theory_name),
    46               session_name, theory_name, types = types, consts = consts,
    47               axioms = axioms, facts = facts, classes = classes, locales = locales,
    48               locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
    49               typedefs = typedefs, cache = Some(cache)))
    50         }
    51       })
    52 
    53     val graph0 =
    54       (Graph.string[Theory] /: thys) { case (g, thy) => g.new_node(thy.name, thy) }
    55     val graph1 =
    56       (graph0 /: thys) { case (g0, thy) =>
    57         (g0 /: thy.parents) { case (g1, parent) =>
    58           g1.default_node(parent, empty_theory(parent)).add_edge_acyclic(parent, thy.name) } }
    59 
    60     Session(session_name, graph1)
    61   }
    62 
    63 
    64 
    65   /** theory content **/
    66 
    67   val export_prefix: String = "theory/"
    68 
    69   sealed case class Theory(name: String, parents: List[String],
    70     types: List[Type],
    71     consts: List[Const],
    72     axioms: List[Fact_Single],
    73     facts: List[Fact_Multi],
    74     classes: List[Class],
    75     locales: List[Locale],
    76     locale_dependencies: List[Locale_Dependency],
    77     classrel: List[Classrel],
    78     arities: List[Arity],
    79     typedefs: List[Typedef])
    80   {
    81     override def toString: String = name
    82 
    83     lazy val entities: Set[Long] =
    84       Set.empty[Long] ++
    85         types.iterator.map(_.entity.serial) ++
    86         consts.iterator.map(_.entity.serial) ++
    87         axioms.iterator.map(_.entity.serial) ++
    88         facts.iterator.map(_.entity.serial) ++
    89         classes.iterator.map(_.entity.serial) ++
    90         locales.iterator.map(_.entity.serial) ++
    91         locale_dependencies.iterator.map(_.entity.serial)
    92 
    93     def cache(cache: Term.Cache): Theory =
    94       Theory(cache.string(name),
    95         parents.map(cache.string(_)),
    96         types.map(_.cache(cache)),
    97         consts.map(_.cache(cache)),
    98         axioms.map(_.cache(cache)),
    99         facts.map(_.cache(cache)),
   100         classes.map(_.cache(cache)),
   101         locales.map(_.cache(cache)),
   102         locale_dependencies.map(_.cache(cache)),
   103         classrel.map(_.cache(cache)),
   104         arities.map(_.cache(cache)),
   105         typedefs.map(_.cache(cache)))
   106   }
   107 
   108   def empty_theory(name: String): Theory =
   109     Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
   110 
   111   def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
   112     types: Boolean = true,
   113     consts: Boolean = true,
   114     axioms: Boolean = true,
   115     facts: Boolean = true,
   116     classes: Boolean = true,
   117     locales: Boolean = true,
   118     locale_dependencies: Boolean = true,
   119     classrel: Boolean = true,
   120     arities: Boolean = true,
   121     typedefs: Boolean = true,
   122     cache: Option[Term.Cache] = None): Theory =
   123   {
   124     val parents =
   125       provider(export_prefix + "parents") match {
   126         case Some(entry) => split_lines(entry.uncompressed().text)
   127         case None =>
   128           error("Missing theory export in session " + quote(session_name) + ": " +
   129             quote(theory_name))
   130       }
   131     val theory =
   132       Theory(theory_name, parents,
   133         if (types) read_types(provider) else Nil,
   134         if (consts) read_consts(provider) else Nil,
   135         if (axioms) read_axioms(provider) else Nil,
   136         if (facts) read_facts(provider) else Nil,
   137         if (classes) read_classes(provider) else Nil,
   138         if (locales) read_locales(provider) else Nil,
   139         if (locale_dependencies) read_locale_dependencies(provider) else Nil,
   140         if (classrel) read_classrel(provider) else Nil,
   141         if (arities) read_arities(provider) else Nil,
   142         if (typedefs) read_typedefs(provider) else Nil)
   143     if (cache.isDefined) theory.cache(cache.get) else theory
   144   }
   145 
   146   def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
   147   {
   148     val session_name = Thy_Header.PURE
   149     val theory_name = Thy_Header.PURE
   150 
   151     using(store.open_database(session_name))(db =>
   152     {
   153       db.transaction {
   154         read_theory(Export.Provider.database(db, session_name, theory_name),
   155           session_name, theory_name, cache = cache)
   156       }
   157     })
   158   }
   159 
   160 
   161   /* entities */
   162 
   163   object Kind extends Enumeration
   164   {
   165     val TYPE = Value("type")
   166     val CONST = Value("const")
   167     val AXIOM = Value("axiom")
   168     val FACT = Value("fact")
   169     val CLASS = Value("class")
   170     val LOCALE = Value("locale")
   171     val LOCALE_DEPENDENCY = Value("locale_dependency")
   172   }
   173 
   174   sealed case class Entity(
   175     kind: Kind.Value, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long)
   176   {
   177     override def toString: String = kind.toString + " " + quote(name)
   178 
   179     def cache(cache: Term.Cache): Entity =
   180       Entity(kind, cache.string(name), cache.string(xname), cache.position(pos), id, serial)
   181   }
   182 
   183   def decode_entity(kind: Kind.Value, tree: XML.Tree): (Entity, XML.Body) =
   184   {
   185     def err(): Nothing = throw new XML.XML_Body(List(tree))
   186 
   187     tree match {
   188       case XML.Elem(Markup(Markup.ENTITY, props), body) =>
   189         val name = Markup.Name.unapply(props) getOrElse err()
   190         val xname = Markup.XName.unapply(props) getOrElse err()
   191         val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
   192         val id = Position.Id.unapply(props)
   193         val serial = Markup.Serial.unapply(props) getOrElse err()
   194         (Entity(kind, name, xname, pos, id, serial), body)
   195       case _ => err()
   196     }
   197   }
   198 
   199 
   200   /* approximative syntax */
   201 
   202   object Assoc extends Enumeration
   203   {
   204     val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
   205   }
   206 
   207   sealed abstract class Syntax
   208   case object No_Syntax extends Syntax
   209   case class Prefix(delim: String) extends Syntax
   210   case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax
   211 
   212   def decode_syntax: XML.Decode.T[Syntax] =
   213     XML.Decode.variant(List(
   214       { case (Nil, Nil) => No_Syntax },
   215       { case (List(delim), Nil) => Prefix(delim) },
   216       { case (Nil, body) =>
   217           import XML.Decode._
   218           val (ass, delim, pri) = triple(int, string, int)(body)
   219           Infix(Assoc(ass), delim, pri) }))
   220 
   221 
   222   /* types */
   223 
   224   sealed case class Type(
   225     entity: Entity, syntax: Syntax, args: List[String], abbrev: Option[Term.Typ])
   226   {
   227     def cache(cache: Term.Cache): Type =
   228       Type(entity.cache(cache),
   229         syntax,
   230         args.map(cache.string(_)),
   231         abbrev.map(cache.typ(_)))
   232   }
   233 
   234   def read_types(provider: Export.Provider): List[Type] =
   235     provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
   236       {
   237         val (entity, body) = decode_entity(Kind.TYPE, tree)
   238         val (syntax, args, abbrev) =
   239         {
   240           import XML.Decode._
   241           triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body)
   242         }
   243         Type(entity, syntax, args, abbrev)
   244       })
   245 
   246 
   247   /* consts */
   248 
   249   sealed case class Const(
   250     entity: Entity,
   251     syntax: Syntax,
   252     typargs: List[String],
   253     typ: Term.Typ,
   254     abbrev: Option[Term.Term],
   255     propositional: Boolean,
   256     primrec_types: List[String],
   257     corecursive: Boolean)
   258   {
   259     def cache(cache: Term.Cache): Const =
   260       Const(entity.cache(cache),
   261         syntax,
   262         typargs.map(cache.string(_)),
   263         cache.typ(typ),
   264         abbrev.map(cache.term(_)),
   265         propositional,
   266         primrec_types.map(cache.string(_)),
   267         corecursive)
   268   }
   269 
   270   def read_consts(provider: Export.Provider): List[Const] =
   271     provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
   272       {
   273         val (entity, body) = decode_entity(Kind.CONST, tree)
   274         val (syntax, (args, (typ, (abbrev, (propositional, (primrec_types, corecursive)))))) =
   275         {
   276           import XML.Decode._
   277           pair(decode_syntax,
   278             pair(list(string),
   279               pair(Term_XML.Decode.typ,
   280                 pair(option(Term_XML.Decode.term), pair(bool,
   281                   pair(list(string), bool))))))(body)
   282         }
   283         Const(entity, syntax, args, typ, abbrev, propositional, primrec_types, corecursive)
   284       })
   285 
   286 
   287   /* facts */
   288 
   289   sealed case class Prop(
   290     typargs: List[(String, Term.Sort)],
   291     args: List[(String, Term.Typ)],
   292     term: Term.Term)
   293   {
   294     def cache(cache: Term.Cache): Prop =
   295       Prop(
   296         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   297         args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   298         cache.term(term))
   299   }
   300 
   301   def decode_prop(body: XML.Body): Prop =
   302   {
   303     val (typargs, args, t) =
   304     {
   305       import XML.Decode._
   306       import Term_XML.Decode._
   307       triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
   308     }
   309     Prop(typargs, args, t)
   310   }
   311 
   312   sealed case class Fact_Single(entity: Entity, prop: Prop)
   313   {
   314     def cache(cache: Term.Cache): Fact_Single =
   315       Fact_Single(entity.cache(cache), prop.cache(cache))
   316   }
   317 
   318   sealed case class Fact_Multi(entity: Entity, props: List[Prop])
   319   {
   320     def cache(cache: Term.Cache): Fact_Multi =
   321       Fact_Multi(entity.cache(cache), props.map(_.cache(cache)))
   322 
   323     def split: List[Fact_Single] =
   324       props match {
   325         case List(prop) => List(Fact_Single(entity, prop))
   326         case _ =>
   327           for ((prop, i) <- props.zipWithIndex)
   328           yield Fact_Single(entity.copy(name = entity.name + "(" + (i + 1) + ")"), prop)
   329       }
   330   }
   331 
   332   def read_axioms(provider: Export.Provider): List[Fact_Single] =
   333     provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
   334       {
   335         val (entity, body) = decode_entity(Kind.AXIOM, tree)
   336         val prop = decode_prop(body)
   337         Fact_Single(entity, prop)
   338       })
   339 
   340   def read_facts(provider: Export.Provider): List[Fact_Multi] =
   341     provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
   342       {
   343         val (entity, body) = decode_entity(Kind.FACT, tree)
   344         val props = XML.Decode.list(decode_prop)(body)
   345         Fact_Multi(entity, props)
   346       })
   347 
   348 
   349   /* type classes */
   350 
   351   sealed case class Class(
   352     entity: Entity, params: List[(String, Term.Typ)], axioms: List[Prop])
   353   {
   354     def cache(cache: Term.Cache): Class =
   355       Class(entity.cache(cache),
   356         params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   357         axioms.map(_.cache(cache)))
   358   }
   359 
   360   def read_classes(provider: Export.Provider): List[Class] =
   361     provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
   362       {
   363         val (entity, body) = decode_entity(Kind.CLASS, tree)
   364         val (params, axioms) =
   365         {
   366           import XML.Decode._
   367           import Term_XML.Decode._
   368           pair(list(pair(string, typ)), list(decode_prop))(body)
   369         }
   370         Class(entity, params, axioms)
   371       })
   372 
   373 
   374   /* locales */
   375 
   376   sealed case class Locale(
   377     entity: Entity,
   378     typargs: List[(String, Term.Sort)],
   379     args: List[((String, Term.Typ), Syntax)],
   380     axioms: List[Prop])
   381   {
   382     def cache(cache: Term.Cache): Locale =
   383       Locale(entity.cache(cache),
   384         typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   385         args.map({ case ((name, typ), syntax) => ((cache.string(name), cache.typ(typ)), syntax) }),
   386         axioms.map(_.cache(cache)))
   387   }
   388 
   389   def read_locales(provider: Export.Provider): List[Locale] =
   390     provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
   391       {
   392         val (entity, body) = decode_entity(Kind.LOCALE, tree)
   393         val (typargs, args, axioms) =
   394         {
   395           import XML.Decode._
   396           import Term_XML.Decode._
   397           triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)),
   398             list(decode_prop))(body)
   399         }
   400         Locale(entity, typargs, args, axioms)
   401       })
   402 
   403 
   404   /* locale dependencies */
   405 
   406   sealed case class Locale_Dependency(
   407     entity: Entity,
   408     source: String,
   409     target: String,
   410     prefix: List[(String, Boolean)],
   411     subst_types: List[((String, Term.Sort), Term.Typ)],
   412     subst_terms: List[((String, Term.Typ), Term.Term)])
   413   {
   414     def cache(cache: Term.Cache): Locale_Dependency =
   415       Locale_Dependency(entity.cache(cache),
   416         cache.string(source),
   417         cache.string(target),
   418         prefix.map({ case (name, mandatory) => (cache.string(name), mandatory) }),
   419         subst_types.map({ case ((a, s), ty) => ((cache.string(a), cache.sort(s)), cache.typ(ty)) }),
   420         subst_terms.map({ case ((x, ty), t) => ((cache.string(x), cache.typ(ty)), cache.term(t)) }))
   421 
   422     def is_inclusion: Boolean =
   423       subst_types.isEmpty && subst_terms.isEmpty
   424   }
   425 
   426   def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] =
   427     provider.uncompressed_yxml(export_prefix + "locale_dependencies").map((tree: XML.Tree) =>
   428       {
   429         val (entity, body) = decode_entity(Kind.LOCALE_DEPENDENCY, tree)
   430         val (source, (target, (prefix, (subst_types, subst_terms)))) =
   431         {
   432           import XML.Decode._
   433           import Term_XML.Decode._
   434           pair(string, pair(string, pair(list(pair(string, bool)),
   435             pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body)
   436         }
   437         Locale_Dependency(entity, source, target, prefix, subst_types, subst_terms)
   438       })
   439 
   440 
   441   /* sort algebra */
   442 
   443   sealed case class Classrel(class1: String, class2: String, prop: Prop)
   444   {
   445     def cache(cache: Term.Cache): Classrel =
   446       Classrel(cache.string(class1), cache.string(class2), prop.cache(cache))
   447   }
   448 
   449   def read_classrel(provider: Export.Provider): List[Classrel] =
   450   {
   451     val body = provider.uncompressed_yxml(export_prefix + "classrel")
   452     val classrel =
   453     {
   454       import XML.Decode._
   455       list(pair(decode_prop, pair(string, string)))(body)
   456     }
   457     for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop)
   458   }
   459 
   460   sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String, prop: Prop)
   461   {
   462     def cache(cache: Term.Cache): Arity =
   463       Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain),
   464         prop.cache(cache))
   465   }
   466 
   467   def read_arities(provider: Export.Provider): List[Arity] =
   468   {
   469     val body = provider.uncompressed_yxml(export_prefix + "arities")
   470     val arities =
   471     {
   472       import XML.Decode._
   473       import Term_XML.Decode._
   474       list(pair(decode_prop, triple(string, list(sort), string)))(body)
   475     }
   476     for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop)
   477   }
   478 
   479 
   480   /* HOL typedefs */
   481 
   482   sealed case class Typedef(name: String,
   483     rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String)
   484   {
   485     def cache(cache: Term.Cache): Typedef =
   486       Typedef(cache.string(name),
   487         cache.typ(rep_type),
   488         cache.typ(abs_type),
   489         cache.string(rep_name),
   490         cache.string(abs_name),
   491         cache.string(axiom_name))
   492   }
   493 
   494   def read_typedefs(provider: Export.Provider): List[Typedef] =
   495   {
   496     val body = provider.uncompressed_yxml(export_prefix + "typedefs")
   497     val typedefs =
   498     {
   499       import XML.Decode._
   500       import Term_XML.Decode._
   501       list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
   502     }
   503     for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
   504     yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
   505   }
   506 }