merged
authorwenzelm
Fri Aug 31 15:57:21 2018 +0200 (13 months ago)
changeset 68863a0769c7f51b4
parent 68860 f443ec10447d
parent 68862 47e9912c53c3
child 68864 1dacce27bc25
merged
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Aug 30 17:20:54 2018 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Aug 31 15:57:21 2018 +0200
     1.3 @@ -531,12 +531,8 @@
     1.4  local
     1.5  
     1.6  fun props_of thy (name, morph) =
     1.7 -  let
     1.8 -    val (asm, defs) = Locale.specification_of thy name;
     1.9 -  in
    1.10 -    (case asm of NONE => defs | SOME asm => asm :: defs)
    1.11 -    |> map (Morphism.term morph)
    1.12 -  end;
    1.13 +  let val (asm, defs) = Locale.specification_of thy name
    1.14 +  in map (Morphism.term morph) (the_list asm @ defs) end;
    1.15  
    1.16  fun prep_goal_expression prep expression ctxt =
    1.17    let
     2.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 30 17:20:54 2018 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Fri Aug 31 15:57:21 2018 +0200
     2.3 @@ -42,6 +42,7 @@
     2.4      declaration list ->
     2.5      (string * Attrib.fact list) list ->
     2.6      (string * morphism) list -> theory -> theory
     2.7 +  val locale_space: theory -> Name_Space.T
     2.8    val intern: theory -> xstring -> string
     2.9    val check: theory -> xstring * Position.T -> string
    2.10    val extern: theory -> string -> xstring
    2.11 @@ -53,6 +54,14 @@
    2.12    val axioms_of: theory -> string -> thm list
    2.13    val instance_of: theory -> string -> morphism -> term list
    2.14    val specification_of: theory -> string -> term option * term list
    2.15 +  val hyp_spec_of: theory -> string -> Element.context_i list
    2.16 +
    2.17 +  type content =
    2.18 +   {type_params: (string * sort) list,
    2.19 +    params: ((string * typ) * mixfix) list,
    2.20 +    asm: term option,
    2.21 +    defs: term list}
    2.22 +  val dest_locales: theory -> (string * content) list
    2.23  
    2.24    (* Storing results *)
    2.25    val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
    2.26 @@ -84,7 +93,6 @@
    2.27    val add_dependency: string -> registration -> theory -> theory
    2.28  
    2.29    (* Diagnostic *)
    2.30 -  val hyp_spec_of: theory -> string -> Element.context_i list
    2.31    val print_locales: bool -> theory -> unit
    2.32    val print_locale: theory -> bool -> xstring * Position.T -> unit
    2.33    val print_registrations: Proof.context -> xstring * Position.T -> unit
    2.34 @@ -207,6 +215,20 @@
    2.35    Locales.map o Name_Space.map_table_entry name o map_locale o apsnd;
    2.36  
    2.37  
    2.38 +(* content *)
    2.39 +
    2.40 +type content =
    2.41 + {type_params: (string * sort) list,
    2.42 +  params: ((string * typ) * mixfix) list,
    2.43 +  asm: term option,
    2.44 +  defs: term list};
    2.45 +
    2.46 +fun dest_locales thy =
    2.47 +  (Locales.get thy, []) |-> Name_Space.fold_table
    2.48 +    (fn (name, Loc {parameters = (type_params, params), spec = (asm, defs), ...}) =>
    2.49 +      cons (name, {type_params = type_params, params = params, asm = asm, defs = defs}));
    2.50 +
    2.51 +
    2.52  (** Primitive operations **)
    2.53  
    2.54  fun params_of thy = snd o #parameters o the_locale thy;
    2.55 @@ -220,8 +242,9 @@
    2.56  
    2.57  fun specification_of thy = #spec o the_locale thy;
    2.58  
    2.59 -fun dependencies_of thy name = the_locale thy name |>
    2.60 -  #dependencies;
    2.61 +fun hyp_spec_of thy = #hyp_spec o the_locale thy;
    2.62 +
    2.63 +fun dependencies_of thy = #dependencies o the_locale thy;
    2.64  
    2.65  fun mixins_of thy name serial = the_locale thy name |>
    2.66    #mixins |> lookup_mixins serial;
    2.67 @@ -693,8 +716,6 @@
    2.68  
    2.69  (*** diagnostic commands and interfaces ***)
    2.70  
    2.71 -fun hyp_spec_of thy = #hyp_spec o the_locale thy;
    2.72 -
    2.73  fun print_locales verbose thy =
    2.74    Pretty.block
    2.75      (Pretty.breaks
     3.1 --- a/src/Pure/Thy/export_theory.ML	Thu Aug 30 17:20:54 2018 +0200
     3.2 +++ b/src/Pure/Thy/export_theory.ML	Fri Aug 31 15:57:21 2018 +0200
     3.3 @@ -87,7 +87,6 @@
     3.4                      XML.Elem (entity_markup space name, body))))
     3.5            |> sort (int_ord o apply2 #1) |> map #2
     3.6          end;
     3.7 -
     3.8        in if null elems then () else export_body thy export_name elems end;
     3.9  
    3.10  
    3.11 @@ -196,6 +195,21 @@
    3.12      val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel);
    3.13      val _ = if null arities then () else export_body thy "arities" (encode_arities arities);
    3.14  
    3.15 +
    3.16 +    (* locales *)
    3.17 +
    3.18 +    fun encode_locale {type_params, params, asm, defs} =
    3.19 +      (type_params, (map #1 params, (asm, defs))) |>
    3.20 +        let open XML.Encode Term_XML.Encode in
    3.21 +          pair (list (pair string sort))
    3.22 +            (pair (list (pair string typ))
    3.23 +              (pair (option term) (list term)))
    3.24 +        end;
    3.25 +
    3.26 +    val _ =
    3.27 +      export_entities "locales" (fn _ => SOME o encode_locale) Locale.locale_space
    3.28 +        (Locale.dest_locales thy);
    3.29 +
    3.30    in () end);
    3.31  
    3.32  end;
     4.1 --- a/src/Pure/Thy/export_theory.scala	Thu Aug 30 17:20:54 2018 +0200
     4.2 +++ b/src/Pure/Thy/export_theory.scala	Fri Aug 31 15:57:21 2018 +0200
     4.3 @@ -30,9 +30,10 @@
     4.4      axioms: Boolean = true,
     4.5      facts: Boolean = true,
     4.6      classes: Boolean = true,
     4.7 -    typedefs: Boolean = true,
     4.8 +    locales: Boolean = true,
     4.9      classrel: Boolean = true,
    4.10      arities: Boolean = true,
    4.11 +    typedefs: Boolean = true,
    4.12      cache: Term.Cache = Term.make_cache()): Session =
    4.13    {
    4.14      val thys =
    4.15 @@ -42,7 +43,8 @@
    4.16            Export.read_theory_names(db, session_name).map((theory_name: String) =>
    4.17              read_theory(Export.Provider.database(db, session_name, theory_name),
    4.18                session_name, theory_name, types = types, consts = consts,
    4.19 -              axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
    4.20 +              axioms = axioms, facts = facts, classes = classes, locales = locales,
    4.21 +              classrel = classrel, arities = arities, typedefs = typedefs,
    4.22                cache = Some(cache)))
    4.23          }
    4.24        })
    4.25 @@ -69,9 +71,10 @@
    4.26      axioms: List[Fact_Single],
    4.27      facts: List[Fact_Multi],
    4.28      classes: List[Class],
    4.29 -    typedefs: List[Typedef],
    4.30 +    locales: List[Locale],
    4.31      classrel: List[Classrel],
    4.32 -    arities: List[Arity])
    4.33 +    arities: List[Arity],
    4.34 +    typedefs: List[Typedef])
    4.35    {
    4.36      override def toString: String = name
    4.37  
    4.38 @@ -81,7 +84,8 @@
    4.39          consts.iterator.map(_.entity.serial) ++
    4.40          axioms.iterator.map(_.entity.serial) ++
    4.41          facts.iterator.map(_.entity.serial) ++
    4.42 -        classes.iterator.map(_.entity.serial)
    4.43 +        classes.iterator.map(_.entity.serial) ++
    4.44 +        locales.iterator.map(_.entity.serial)
    4.45  
    4.46      def cache(cache: Term.Cache): Theory =
    4.47        Theory(cache.string(name),
    4.48 @@ -91,13 +95,14 @@
    4.49          axioms.map(_.cache(cache)),
    4.50          facts.map(_.cache(cache)),
    4.51          classes.map(_.cache(cache)),
    4.52 -        typedefs.map(_.cache(cache)),
    4.53 +        locales.map(_.cache(cache)),
    4.54          classrel.map(_.cache(cache)),
    4.55 -        arities.map(_.cache(cache)))
    4.56 +        arities.map(_.cache(cache)),
    4.57 +        typedefs.map(_.cache(cache)))
    4.58    }
    4.59  
    4.60    def empty_theory(name: String): Theory =
    4.61 -    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    4.62 +    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    4.63  
    4.64    def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
    4.65      types: Boolean = true,
    4.66 @@ -105,9 +110,10 @@
    4.67      axioms: Boolean = true,
    4.68      facts: Boolean = true,
    4.69      classes: Boolean = true,
    4.70 -    typedefs: Boolean = true,
    4.71 +    locales: Boolean = true,
    4.72      classrel: Boolean = true,
    4.73      arities: Boolean = true,
    4.74 +    typedefs: Boolean = true,
    4.75      cache: Option[Term.Cache] = None): Theory =
    4.76    {
    4.77      val parents =
    4.78 @@ -124,9 +130,10 @@
    4.79          if (axioms) read_axioms(provider) else Nil,
    4.80          if (facts) read_facts(provider) else Nil,
    4.81          if (classes) read_classes(provider) else Nil,
    4.82 -        if (typedefs) read_typedefs(provider) else Nil,
    4.83 +        if (locales) read_locales(provider) else Nil,
    4.84          if (classrel) read_classrel(provider) else Nil,
    4.85 -        if (arities) read_arities(provider) else Nil)
    4.86 +        if (arities) read_arities(provider) else Nil,
    4.87 +        if (typedefs) read_typedefs(provider) else Nil)
    4.88      if (cache.isDefined) theory.cache(cache.get) else theory
    4.89    }
    4.90  
    4.91 @@ -154,6 +161,7 @@
    4.92      val AXIOM = Value("axiom")
    4.93      val FACT = Value("fact")
    4.94      val CLASS = Value("class")
    4.95 +    val LOCALE = Value("locale")
    4.96    }
    4.97  
    4.98    sealed case class Entity(
    4.99 @@ -316,6 +324,36 @@
   4.100        })
   4.101  
   4.102  
   4.103 +  /* locales */
   4.104 +
   4.105 +  sealed case class Locale(
   4.106 +    entity: Entity, type_params: List[(String, Term.Sort)], params: List[(String, Term.Typ)],
   4.107 +      asm: Option[Term.Term], defs: List[Term.Term])
   4.108 +  {
   4.109 +    def cache(cache: Term.Cache): Locale =
   4.110 +      Locale(entity.cache(cache),
   4.111 +        type_params.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
   4.112 +        params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
   4.113 +        asm.map(cache.term(_)),
   4.114 +        defs.map(cache.term(_)))
   4.115 +  }
   4.116 +
   4.117 +  def read_locales(provider: Export.Provider): List[Locale] =
   4.118 +    provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
   4.119 +      {
   4.120 +        val (entity, body) = decode_entity(Kind.LOCALE, tree)
   4.121 +        val (type_params, (params, (asm, defs))) =
   4.122 +        {
   4.123 +          import XML.Decode._
   4.124 +          import Term_XML.Decode._
   4.125 +          pair(list(pair(string, sort)),
   4.126 +            pair(list(pair(string, typ)),
   4.127 +              pair(option(term), list(term))))(body)
   4.128 +        }
   4.129 +        Locale(entity, type_params, params, asm, defs)
   4.130 +      })
   4.131 +
   4.132 +
   4.133    /* sort algebra */
   4.134  
   4.135    sealed case class Classrel(class_name: String, super_names: List[String])