export locale dependencies, with approx. morphism as type/term substitution;

--- a/src/Pure/Thy/export_theory.ML	Tue Sep 25 20:27:39 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Tue Sep 25 20:41:27 2018 +0200
@@ -94,6 +94,25 @@
     val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) []);
   in {typargs = typargs, args = args, axioms = axioms} end;
 
+fun locale_dependency_subst thy (dep: Locale.locale_dependency) =
+  let
+    val (type_params, params) = Locale.parameters_of thy (#source dep);
+    (* FIXME proper type_params wrt. locale_content (!?!) *)
+    val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
+    val substT =
+      typargs |> map_filter (fn v =>
+        let
+          val T = TFree v;
+          val T' = Morphism.typ (#morphism dep) T;
+        in if T = T' then NONE else SOME (v, T') end);
+    val subst =
+      params |> map_filter (fn (v, _) =>
+        let
+          val t = Free v;
+          val t' = Morphism.term (#morphism dep) t;
+        in if t aconv t' then NONE else SOME (v, t') end);
+  in (substT, subst) end;
+
 
 (* general setup *)
 
@@ -117,16 +136,20 @@
 
     (* entities *)
 
-    fun entity_markup space name =
+    fun make_entity_markup name xname pos serial =
       let
-        val xname = Name_Space.extern_shortest thy_ctxt space name;
-        val {serial, pos, ...} = Name_Space.the_entry space name;
         val props =
           Position.offset_properties_of (adjust_pos pos) @
           Position.id_properties_of pos @
           Markup.serial_properties serial;
       in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
 
+    fun entity_markup space name =
+      let
+        val xname = Name_Space.extern_shortest thy_ctxt space name;
+        val {serial, pos, ...} = Name_Space.the_entry space name;
+      in make_entity_markup name xname pos serial end;
+
     fun export_entities export_name export get_space decls =
       let val elems =
         let
@@ -293,6 +316,29 @@
         (map (rpair ()) (Locale.get_locales thy));
 
 
+    (* locale dependencies *)
+
+    fun encode_locale_dependency (dep: Locale.locale_dependency) =
+      (#source dep, (#target dep, (#prefix dep, locale_dependency_subst thy dep))) |>
+        let
+          open XML.Encode Term_XML.Encode;
+          val encode_subst =
+            pair (list (pair (pair string sort) typ)) (list (pair (pair string typ) term));
+        in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
+
+    val _ =
+      (case Locale.dest_dependencies parents thy of
+        [] => ()
+      | deps =>
+          deps |> map_index (fn (i, dep) =>
+            let
+              val xname = string_of_int (i + 1);
+              val name = Long_Name.implode [Context.theory_name thy, xname];
+              val body = encode_locale_dependency dep;
+            in XML.Elem (make_entity_markup name xname (#pos dep) (#serial dep), body) end)
+          |> export_body thy "locale_dependencies");
+
+
     (* parents *)
 
     val _ =

--- a/src/Pure/Thy/export_theory.scala	Tue Sep 25 20:27:39 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Sep 25 20:41:27 2018 +0200
@@ -31,6 +31,7 @@
     facts: Boolean = true,
     classes: Boolean = true,
     locales: Boolean = true,
+    locale_dependencies: Boolean = true,
     classrel: Boolean = true,
     arities: Boolean = true,
     typedefs: Boolean = true,
@@ -44,8 +45,8 @@
             read_theory(Export.Provider.database(db, session_name, theory_name),
               session_name, theory_name, types = types, consts = consts,
               axioms = axioms, facts = facts, classes = classes, locales = locales,
-              classrel = classrel, arities = arities, typedefs = typedefs,
-              cache = Some(cache)))
+              locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
+              typedefs = typedefs, cache = Some(cache)))
         }
       })
 
@@ -72,6 +73,7 @@
     facts: List[Fact_Multi],
     classes: List[Class],
     locales: List[Locale],
+    locale_dependencies: List[Locale_Dependency],
     classrel: List[Classrel],
     arities: List[Arity],
     typedefs: List[Typedef])
@@ -85,7 +87,8 @@
         axioms.iterator.map(_.entity.serial) ++
         facts.iterator.map(_.entity.serial) ++
         classes.iterator.map(_.entity.serial) ++
-        locales.iterator.map(_.entity.serial)
+        locales.iterator.map(_.entity.serial) ++
+        locale_dependencies.iterator.map(_.entity.serial)
 
     def cache(cache: Term.Cache): Theory =
       Theory(cache.string(name),
@@ -96,13 +99,14 @@
         facts.map(_.cache(cache)),
         classes.map(_.cache(cache)),
         locales.map(_.cache(cache)),
+        locale_dependencies.map(_.cache(cache)),
         classrel.map(_.cache(cache)),
         arities.map(_.cache(cache)),
         typedefs.map(_.cache(cache)))
   }
 
   def empty_theory(name: String): Theory =
-    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
+    Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
 
   def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
     types: Boolean = true,
@@ -111,6 +115,7 @@
     facts: Boolean = true,
     classes: Boolean = true,
     locales: Boolean = true,
+    locale_dependencies: Boolean = true,
     classrel: Boolean = true,
     arities: Boolean = true,
     typedefs: Boolean = true,
@@ -131,6 +136,7 @@
         if (facts) read_facts(provider) else Nil,
         if (classes) read_classes(provider) else Nil,
         if (locales) read_locales(provider) else Nil,
+        if (locale_dependencies) read_locale_dependencies(provider) else Nil,
         if (classrel) read_classrel(provider) else Nil,
         if (arities) read_arities(provider) else Nil,
         if (typedefs) read_typedefs(provider) else Nil)
@@ -162,6 +168,7 @@
     val FACT = Value("fact")
     val CLASS = Value("class")
     val LOCALE = Value("locale")
+    val LOCALE_DEPENDENCY = Value("locale_dependency")
   }
 
   sealed case class Entity(
@@ -379,6 +386,43 @@
       })
 
 
+  /* locale dependencies */
+
+  sealed case class Locale_Dependency(
+    entity: Entity,
+    source: String,
+    target: String,
+    prefix: List[(String, Boolean)],
+    subst_types: List[((String, Term.Sort), Term.Typ)],
+    subst_terms: List[((String, Term.Typ), Term.Term)])
+  {
+    def cache(cache: Term.Cache): Locale_Dependency =
+      Locale_Dependency(entity.cache(cache),
+        cache.string(source),
+        cache.string(target),
+        prefix.map({ case (name, mandatory) => (cache.string(name), mandatory) }),
+        subst_types.map({ case ((a, s), ty) => ((cache.string(a), cache.sort(s)), cache.typ(ty)) }),
+        subst_terms.map({ case ((x, ty), t) => ((cache.string(x), cache.typ(ty)), cache.term(t)) }))
+
+    def is_inclusion: Boolean =
+      subst_types.isEmpty && subst_terms.isEmpty
+  }
+
+  def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] =
+    provider.uncompressed_yxml(export_prefix + "locale_dependencies").map((tree: XML.Tree) =>
+      {
+        val (entity, body) = decode_entity(Kind.LOCALE_DEPENDENCY, tree)
+        val (source, (target, (prefix, (subst_types, subst_terms)))) =
+        {
+          import XML.Decode._
+          import Term_XML.Decode._
+          pair(string, pair(string, pair(list(pair(string, bool)),
+            pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body)
+        }
+        Locale_Dependency(entity, source, target, prefix, subst_types, subst_terms)
+      })
+
+
   /* sort algebra */
 
   sealed case class Classrel(class_name: String, super_names: List[String])