src/Pure/Thy/export_theory.scala
changeset 68862 47e9912c53c3
parent 68835 2e59da922630
child 68864 1dacce27bc25
     1.1 --- a/src/Pure/Thy/export_theory.scala	Fri Aug 31 13:34:31 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.scala	Fri Aug 31 15:48:37 2018 +0200
     1.3 @@ -30,9 +30,10 @@
     1.4      axioms: Boolean = true,
     1.5      facts: Boolean = true,
     1.6      classes: Boolean = true,
     1.7 -    typedefs: Boolean = true,
     1.8 +    locales: Boolean = true,
     1.9      classrel: Boolean = true,
    1.10      arities: Boolean = true,
    1.11 +    typedefs: Boolean = true,
    1.12      cache: Term.Cache = Term.make_cache()): Session =
    1.13    {
    1.14      val thys =
    1.15 @@ -42,7 +43,8 @@
    1.16            Export.read_theory_names(db, session_name).map((theory_name: String) =>
    1.17              read_theory(Export.Provider.database(db, session_name, theory_name),
    1.18                session_name, theory_name, types = types, consts = consts,
    1.19 -              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
    1.20 +              axioms = axioms, facts = facts, classes = classes, locales = locales,
    1.21 +              classrel = classrel, arities = arities, typedefs = typedefs,
    1.22                cache = Some(cache)))
    1.23          }
    1.24        })
    1.25 @@ -69,9 +71,10 @@
    1.26      axioms: List[Fact_Single],
    1.27      facts: List[Fact_Multi],
    1.28      classes: List[Class],
    1.29 -    typedefs: List[Typedef],
    1.30 +    locales: List[Locale],
    1.31      classrel: List[Classrel],
    1.32 -    arities: List[Arity])
    1.33 +    arities: List[Arity],
    1.34 +    typedefs: List[Typedef])
    1.35    {
    1.36      override def toString: String = name
    1.37  
    1.38 @@ -81,7 +84,8 @@
    1.39          consts.iterator.map(_.entity.serial) ++
    1.40          axioms.iterator.map(_.entity.serial) ++
    1.41          facts.iterator.map(_.entity.serial) ++
    1.42 -        classes.iterator.map(_.entity.serial)
    1.43 +        classes.iterator.map(_.entity.serial) ++
    1.44 +        locales.iterator.map(_.entity.serial)
    1.45  
    1.46      def cache(cache: Term.Cache): Theory =
    1.47        Theory(cache.string(name),
    1.48 @@ -91,13 +95,14 @@
    1.49          axioms.map(_.cache(cache)),
    1.50          facts.map(_.cache(cache)),
    1.51          classes.map(_.cache(cache)),
    1.52 -        typedefs.map(_.cache(cache)),
    1.53 +        locales.map(_.cache(cache)),
    1.54          classrel.map(_.cache(cache)),
    1.55 -        arities.map(_.cache(cache)))
    1.56 +        arities.map(_.cache(cache)),
    1.57 +        typedefs.map(_.cache(cache)))
    1.58    }
    1.59  
    1.60    def empty_theory(name: String): Theory =
    1.61 -    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    1.62 +    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    1.63  
    1.64    def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
    1.65      types: Boolean = true,
    1.66 @@ -105,9 +110,10 @@
    1.67      axioms: Boolean = true,
    1.68      facts: Boolean = true,
    1.69      classes: Boolean = true,
    1.70 -    typedefs: Boolean = true,
    1.71 +    locales: Boolean = true,
    1.72      classrel: Boolean = true,
    1.73      arities: Boolean = true,
    1.74 +    typedefs: Boolean = true,
    1.75      cache: Option[Term.Cache] = None): Theory =
    1.76    {
    1.77      val parents =
    1.78 @@ -124,9 +130,10 @@
    1.79          if (axioms) read_axioms(provider) else Nil,
    1.80          if (facts) read_facts(provider) else Nil,
    1.81          if (classes) read_classes(provider) else Nil,
    1.82 -        if (typedefs) read_typedefs(provider) else Nil,
    1.83 +        if (locales) read_locales(provider) else Nil,
    1.84          if (classrel) read_classrel(provider) else Nil,
    1.85 -        if (arities) read_arities(provider) else Nil)
    1.86 +        if (arities) read_arities(provider) else Nil,
    1.87 +        if (typedefs) read_typedefs(provider) else Nil)
    1.88      if (cache.isDefined) theory.cache(cache.get) else theory
    1.89    }
    1.90  
    1.91 @@ -154,6 +161,7 @@
    1.92      val AXIOM = Value("axiom")
    1.93      val FACT = Value("fact")
    1.94      val CLASS = Value("class")
    1.95 +    val LOCALE = Value("locale")
    1.96    }
    1.97  
    1.98    sealed case class Entity(
    1.99 @@ -316,6 +324,36 @@
   1.100        })
   1.101  
   1.102  
   1.103 +  /* locales */
   1.104 +
   1.105 +  sealed case class Locale(
   1.106 +    entity: Entity, type_params: List[(String, Term.Sort)], params: List[(String, Term.Typ)],
   1.107 +      asm: Option[Term.Term], defs: List[Term.Term])
   1.108 +  {
   1.109 +    def cache(cache: Term.Cache): Locale =
   1.110 +      Locale(entity.cache(cache),
   1.111 +        type_params.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   1.112 +        params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   1.113 +        asm.map(cache.term(_)),
   1.114 +        defs.map(cache.term(_)))
   1.115 +  }
   1.116 +
   1.117 +  def read_locales(provider: Export.Provider): List[Locale] =
   1.118 +    provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
   1.119 +      {
   1.120 +        val (entity, body) = decode_entity(Kind.LOCALE, tree)
   1.121 +        val (type_params, (params, (asm, defs))) =
   1.122 +        {
   1.123 +          import XML.Decode._
   1.124 +          import Term_XML.Decode._
   1.125 +          pair(list(pair(string, sort)),
   1.126 +            pair(list(pair(string, typ)),
   1.127 +              pair(option(term), list(term))))(body)
   1.128 +        }
   1.129 +        Locale(entity, type_params, params, asm, defs)
   1.130 +      })
   1.131 +
   1.132 +
   1.133    /* sort algebra */
   1.134  
   1.135    sealed case class Classrel(class_name: String, super_names: List[String])