export locale dependencies, with approx. morphism as type/term substitution;
authorwenzelm
Tue Sep 25 20:41:27 2018 +0200 (13 months ago)
changeset 69069b9aca3b9619f
parent 69068 6ce325825ad7
child 69070 a74b09822d79
export locale dependencies, with approx. morphism as type/term substitution;
src/Pure/Thy/export_theory.ML
src/Pure/Thy/export_theory.scala
     1.1 --- a/src/Pure/Thy/export_theory.ML	Tue Sep 25 20:27:39 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Tue Sep 25 20:41:27 2018 +0200
     1.3 @@ -94,6 +94,25 @@
     1.4      val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) []);
     1.5    in {typargs = typargs, args = args, axioms = axioms} end;
     1.6  
     1.7 +fun locale_dependency_subst thy (dep: Locale.locale_dependency) =
     1.8 +  let
     1.9 +    val (type_params, params) = Locale.parameters_of thy (#source dep);
    1.10 +    (* FIXME proper type_params wrt. locale_content (!?!) *)
    1.11 +    val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
    1.12 +    val substT =
    1.13 +      typargs |> map_filter (fn v =>
    1.14 +        let
    1.15 +          val T = TFree v;
    1.16 +          val T' = Morphism.typ (#morphism dep) T;
    1.17 +        in if T = T' then NONE else SOME (v, T') end);
    1.18 +    val subst =
    1.19 +      params |> map_filter (fn (v, _) =>
    1.20 +        let
    1.21 +          val t = Free v;
    1.22 +          val t' = Morphism.term (#morphism dep) t;
    1.23 +        in if t aconv t' then NONE else SOME (v, t') end);
    1.24 +  in (substT, subst) end;
    1.25 +
    1.26  
    1.27  (* general setup *)
    1.28  
    1.29 @@ -117,16 +136,20 @@
    1.30  
    1.31      (* entities *)
    1.32  
    1.33 -    fun entity_markup space name =
    1.34 +    fun make_entity_markup name xname pos serial =
    1.35        let
    1.36 -        val xname = Name_Space.extern_shortest thy_ctxt space name;
    1.37 -        val {serial, pos, ...} = Name_Space.the_entry space name;
    1.38          val props =
    1.39            Position.offset_properties_of (adjust_pos pos) @
    1.40            Position.id_properties_of pos @
    1.41            Markup.serial_properties serial;
    1.42        in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
    1.43  
    1.44 +    fun entity_markup space name =
    1.45 +      let
    1.46 +        val xname = Name_Space.extern_shortest thy_ctxt space name;
    1.47 +        val {serial, pos, ...} = Name_Space.the_entry space name;
    1.48 +      in make_entity_markup name xname pos serial end;
    1.49 +
    1.50      fun export_entities export_name export get_space decls =
    1.51        let val elems =
    1.52          let
    1.53 @@ -293,6 +316,29 @@
    1.54          (map (rpair ()) (Locale.get_locales thy));
    1.55  
    1.56  
    1.57 +    (* locale dependencies *)
    1.58 +
    1.59 +    fun encode_locale_dependency (dep: Locale.locale_dependency) =
    1.60 +      (#source dep, (#target dep, (#prefix dep, locale_dependency_subst thy dep))) |>
    1.61 +        let
    1.62 +          open XML.Encode Term_XML.Encode;
    1.63 +          val encode_subst =
    1.64 +            pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) term));
    1.65 +        in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
    1.66 +
    1.67 +    val _ =
    1.68 +      (case Locale.dest_dependencies parents thy of
    1.69 +        [] => ()
    1.70 +      | deps =>
    1.71 +          deps |> map_index (fn (i, dep) =>
    1.72 +            let
    1.73 +              val xname = string_of_int (i + 1);
    1.74 +              val name = Long_Name.implode [Context.theory_name thy, xname];
    1.75 +              val body = encode_locale_dependency dep;
    1.76 +            in XML.Elem (make_entity_markup name xname (#pos dep) (#serial dep), body) end)
    1.77 +          |> export_body thy "locale_dependencies");
    1.78 +
    1.79 +
    1.80      (* parents *)
    1.81  
    1.82      val _ =
     2.1 --- a/src/Pure/Thy/export_theory.scala	Tue Sep 25 20:27:39 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.scala	Tue Sep 25 20:41:27 2018 +0200
     2.3 @@ -31,6 +31,7 @@
     2.4      facts: Boolean = true,
     2.5      classes: Boolean = true,
     2.6      locales: Boolean = true,
     2.7 +    locale_dependencies: Boolean = true,
     2.8      classrel: Boolean = true,
     2.9      arities: Boolean = true,
    2.10      typedefs: Boolean = true,
    2.11 @@ -44,8 +45,8 @@
    2.12              read_theory(Export.Provider.database(db, session_name, theory_name),
    2.13                session_name, theory_name, types = types, consts = consts,
    2.14                axioms = axioms, facts = facts, classes = classes, locales = locales,
    2.15 -              classrel = classrel, arities = arities, typedefs = typedefs,
    2.16 -              cache = Some(cache)))
    2.17 +              locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
    2.18 +              typedefs = typedefs, cache = Some(cache)))
    2.19          }
    2.20        })
    2.21  
    2.22 @@ -72,6 +73,7 @@
    2.23      facts: List[Fact_Multi],
    2.24      classes: List[Class],
    2.25      locales: List[Locale],
    2.26 +    locale_dependencies: List[Locale_Dependency],
    2.27      classrel: List[Classrel],
    2.28      arities: List[Arity],
    2.29      typedefs: List[Typedef])
    2.30 @@ -85,7 +87,8 @@
    2.31          axioms.iterator.map(_.entity.serial) ++
    2.32          facts.iterator.map(_.entity.serial) ++
    2.33          classes.iterator.map(_.entity.serial) ++
    2.34 -        locales.iterator.map(_.entity.serial)
    2.35 +        locales.iterator.map(_.entity.serial) ++
    2.36 +        locale_dependencies.iterator.map(_.entity.serial)
    2.37  
    2.38      def cache(cache: Term.Cache): Theory =
    2.39        Theory(cache.string(name),
    2.40 @@ -96,13 +99,14 @@
    2.41          facts.map(_.cache(cache)),
    2.42          classes.map(_.cache(cache)),
    2.43          locales.map(_.cache(cache)),
    2.44 +        locale_dependencies.map(_.cache(cache)),
    2.45          classrel.map(_.cache(cache)),
    2.46          arities.map(_.cache(cache)),
    2.47          typedefs.map(_.cache(cache)))
    2.48    }
    2.49  
    2.50    def empty_theory(name: String): Theory =
    2.51 -    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    2.52 +    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
    2.53  
    2.54    def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
    2.55      types: Boolean = true,
    2.56 @@ -111,6 +115,7 @@
    2.57      facts: Boolean = true,
    2.58      classes: Boolean = true,
    2.59      locales: Boolean = true,
    2.60 +    locale_dependencies: Boolean = true,
    2.61      classrel: Boolean = true,
    2.62      arities: Boolean = true,
    2.63      typedefs: Boolean = true,
    2.64 @@ -131,6 +136,7 @@
    2.65          if (facts) read_facts(provider) else Nil,
    2.66          if (classes) read_classes(provider) else Nil,
    2.67          if (locales) read_locales(provider) else Nil,
    2.68 +        if (locale_dependencies) read_locale_dependencies(provider) else Nil,
    2.69          if (classrel) read_classrel(provider) else Nil,
    2.70          if (arities) read_arities(provider) else Nil,
    2.71          if (typedefs) read_typedefs(provider) else Nil)
    2.72 @@ -162,6 +168,7 @@
    2.73      val FACT = Value("fact")
    2.74      val CLASS = Value("class")
    2.75      val LOCALE = Value("locale")
    2.76 +    val LOCALE_DEPENDENCY = Value("locale_dependency")
    2.77    }
    2.78  
    2.79    sealed case class Entity(
    2.80 @@ -379,6 +386,43 @@
    2.81        })
    2.82  
    2.83  
    2.84 +  /* locale dependencies */
    2.85 +
    2.86 +  sealed case class Locale_Dependency(
    2.87 +    entity: Entity,
    2.88 +    source: String,
    2.89 +    target: String,
    2.90 +    prefix: List[(String, Boolean)],
    2.91 +    subst_types: List[((String, Term.Sort), Term.Typ)],
    2.92 +    subst_terms: List[((String, Term.Typ), Term.Term)])
    2.93 +  {
    2.94 +    def cache(cache: Term.Cache): Locale_Dependency =
    2.95 +      Locale_Dependency(entity.cache(cache),
    2.96 +        cache.string(source),
    2.97 +        cache.string(target),
    2.98 +        prefix.map({ case (name, mandatory) => (cache.string(name), mandatory) }),
    2.99 +        subst_types.map({ case ((a, s), ty) => ((cache.string(a), cache.sort(s)), cache.typ(ty)) }),
   2.100 +        subst_terms.map({ case ((x, ty), t) => ((cache.string(x), cache.typ(ty)), cache.term(t)) }))
   2.101 +
   2.102 +    def is_inclusion: Boolean =
   2.103 +      subst_types.isEmpty && subst_terms.isEmpty
   2.104 +  }
   2.105 +
   2.106 +  def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] =
   2.107 +    provider.uncompressed_yxml(export_prefix + "locale_dependencies").map((tree: XML.Tree) =>
   2.108 +      {
   2.109 +        val (entity, body) = decode_entity(Kind.LOCALE_DEPENDENCY, tree)
   2.110 +        val (source, (target, (prefix, (subst_types, subst_terms)))) =
   2.111 +        {
   2.112 +          import XML.Decode._
   2.113 +          import Term_XML.Decode._
   2.114 +          pair(string, pair(string, pair(list(pair(string, bool)),
   2.115 +            pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body)
   2.116 +        }
   2.117 +        Locale_Dependency(entity, source, target, prefix, subst_types, subst_terms)
   2.118 +      })
   2.119 +
   2.120 +
   2.121    /* sort algebra */
   2.122  
   2.123    sealed case class Classrel(class_name: String, super_names: List[String])