src/Pure/Thy/export_theory.ML
changeset 69069 b9aca3b9619f
parent 69034 855c3c501b09
child 69071 3ef82592dc22
     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 _ =