clarified signature: proper typargs;
authorwenzelm
Fri Aug 31 16:17:30 2018 +0200 (10 months ago)
changeset 688641dacce27bc25
parent 68863 a0769c7f51b4
child 68865 dd44e31ca2c6
clarified signature: proper typargs;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.ML	Fri Aug 31 15:57:21 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Fri Aug 31 16:17:30 2018 +0200
     1.3 @@ -198,13 +198,17 @@
     1.4  
     1.5      (* locales *)
     1.6  
     1.7 -    fun encode_locale {type_params, params, asm, defs} =
     1.8 -      (type_params, (map #1 params, (asm, defs))) |>
     1.9 -        let open XML.Encode Term_XML.Encode in
    1.10 -          pair (list (pair string sort))
    1.11 -            (pair (list (pair string typ))
    1.12 -              (pair (option term) (list term)))
    1.13 -        end;
    1.14 +    fun encode_locale ({type_params, params, asm, defs}: Locale.content) =
    1.15 +      let
    1.16 +        val args = map #1 params;
    1.17 +        val typargs = type_params @ rev (fold Term.add_tfrees (map Free args @ the_list asm) []);
    1.18 +        val encode =
    1.19 +          let open XML.Encode Term_XML.Encode in
    1.20 +            pair (list (pair string sort))
    1.21 +              (pair (list (pair string typ))
    1.22 +                (pair (option term) (list term)))
    1.23 +          end;
    1.24 +      in encode (typargs, (args, (asm, defs))) end;
    1.25  
    1.26      val _ =
    1.27        export_entities "locales" (fn _ => SOME o encode_locale) Locale.locale_space
     2.1 --- a/src/Pure/Thy/export_theory.scala	Fri Aug 31 15:57:21 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Fri Aug 31 16:17:30 2018 +0200
     2.3 @@ -327,13 +327,13 @@
     2.4    /* locales */
     2.5  
     2.6    sealed case class Locale(
     2.7 -    entity: Entity, type_params: List[(String, Term.Sort)], params: List[(String, Term.Typ)],
     2.8 +    entity: Entity, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)],
     2.9        asm: Option[Term.Term], defs: List[Term.Term])
    2.10    {
    2.11      def cache(cache: Term.Cache): Locale =
    2.12        Locale(entity.cache(cache),
    2.13 -        type_params.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
    2.14 -        params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
    2.15 +        typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
    2.16 +        args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }),
    2.17          asm.map(cache.term(_)),
    2.18          defs.map(cache.term(_)))
    2.19    }
    2.20 @@ -342,7 +342,7 @@
    2.21      provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
    2.22        {
    2.23          val (entity, body) = decode_entity(Kind.LOCALE, tree)
    2.24 -        val (type_params, (params, (asm, defs))) =
    2.25 +        val (typargs, (args, (asm, defs))) =
    2.26          {
    2.27            import XML.Decode._
    2.28            import Term_XML.Decode._
    2.29 @@ -350,7 +350,7 @@
    2.30              pair(list(pair(string, typ)),
    2.31                pair(option(term), list(term))))(body)
    2.32          }
    2.33 -        Locale(entity, type_params, params, asm, defs)
    2.34 +        Locale(entity, typargs, args, asm, defs)
    2.35        })
    2.36  
    2.37