suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
authorwenzelm
Sun Sep 30 12:26:14 2018 +0200 (12 months ago)
changeset 6908706017b2c4552
parent 69086 2859dcdbc849
child 69088 051127c38be8
suppress aux. locales from command 'experiment' -- avoid crash of theory Dict_Construction.Test_Dict_Construction (AFP);
src/Pure/Isar/experiment.ML
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Isar/experiment.ML	Sun Sep 30 11:58:59 2018 +0200
     1.2 +++ b/src/Pure/Isar/experiment.ML	Sun Sep 30 12:26:14 2018 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature EXPERIMENT =
     1.6  sig
     1.7 +  val is_experiment: theory -> string -> bool
     1.8    val experiment: Element.context_i list -> theory -> Binding.scope * local_theory
     1.9    val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory
    1.10  end;
    1.11 @@ -13,10 +14,23 @@
    1.12  structure Experiment: EXPERIMENT =
    1.13  struct
    1.14  
    1.15 +structure Data = Theory_Data
    1.16 +(
    1.17 +  type T = Symtab.set;
    1.18 +  val empty = Symtab.empty;
    1.19 +  val extend = I;
    1.20 +  val merge = Symtab.merge (K true);
    1.21 +);
    1.22 +
    1.23 +fun is_experiment thy name = Symtab.defined (Data.get thy) name;
    1.24 +
    1.25  fun gen_experiment add_locale elems thy =
    1.26    let
    1.27      val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed;
    1.28 -    val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems;
    1.29 +    val lthy =
    1.30 +      thy
    1.31 +      |> add_locale experiment_name Binding.empty ([], []) elems
    1.32 +      |-> (Local_Theory.background_theory o Data.map o Symtab.insert_set);
    1.33      val (scope, naming) =
    1.34        Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
    1.35      val naming' = naming |> Name_Space.private_scope scope;
     2.1 --- a/src/Pure/Thy/export_theory.ML	Sun Sep 30 11:58:59 2018 +0200
     2.2 +++ b/src/Pure/Thy/export_theory.ML	Sun Sep 30 12:26:14 2018 +0200
     2.3 @@ -101,7 +101,7 @@
     2.4    (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
     2.5  
     2.6  
     2.7 -(* locale content *)
     2.8 +(* locales content *)
     2.9  
    2.10  fun locale_content thy loc =
    2.11    let
    2.12 @@ -127,23 +127,31 @@
    2.13      val typargs = rev (fold Term.add_tfrees (map (Free o #1) args @ axioms) []);
    2.14    in {typargs = typargs, args = args, axioms = axioms} end;
    2.15  
    2.16 -fun locale_dependency_subst thy (dep: Locale.locale_dependency) =
    2.17 -  let
    2.18 -    val (type_params, params) = Locale.parameters_of thy (#source dep);
    2.19 -    val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
    2.20 -    val substT =
    2.21 -      typargs |> map_filter (fn v =>
    2.22 -        let
    2.23 -          val T = TFree v;
    2.24 -          val T' = Morphism.typ (#morphism dep) T;
    2.25 -        in if T = T' then NONE else SOME (v, T') end);
    2.26 -    val subst =
    2.27 -      params |> map_filter (fn (v, _) =>
    2.28 -        let
    2.29 -          val t = Free v;
    2.30 -          val t' = Morphism.term (#morphism dep) t;
    2.31 -        in if t aconv t' then NONE else SOME (v, t') end);
    2.32 -  in (substT, subst) end;
    2.33 +fun get_locales thy =
    2.34 +  Locale.get_locales thy |> map_filter (fn loc =>
    2.35 +    if Experiment.is_experiment thy loc then NONE else SOME (loc, ()));
    2.36 +
    2.37 +fun get_dependencies prev_thys thy =
    2.38 +  Locale.dest_dependencies prev_thys thy |> map_filter (fn dep =>
    2.39 +    if Experiment.is_experiment thy (#source dep) orelse
    2.40 +      Experiment.is_experiment thy (#target dep) then NONE
    2.41 +    else
    2.42 +      let
    2.43 +        val (type_params, params) = Locale.parameters_of thy (#source dep);
    2.44 +        val typargs = fold (Term.add_tfreesT o #2 o #1) params type_params;
    2.45 +        val substT =
    2.46 +          typargs |> map_filter (fn v =>
    2.47 +            let
    2.48 +              val T = TFree v;
    2.49 +              val T' = Morphism.typ (#morphism dep) T;
    2.50 +            in if T = T' then NONE else SOME (v, T') end);
    2.51 +        val subst =
    2.52 +          params |> map_filter (fn (v, _) =>
    2.53 +            let
    2.54 +              val t = Free v;
    2.55 +              val t' = Morphism.term (#morphism dep) t;
    2.56 +            in if t aconv t' then NONE else SOME (v, t') end);
    2.57 +      in SOME (dep, (substT, subst)) end);
    2.58  
    2.59  
    2.60  (* general setup *)
    2.61 @@ -330,14 +338,13 @@
    2.62  
    2.63      val _ =
    2.64        export_entities "locales" (fn loc => fn () => SOME (export_locale loc))
    2.65 -        Locale.locale_space
    2.66 -        (map (rpair ()) (Locale.get_locales thy));
    2.67 +        Locale.locale_space (get_locales thy);
    2.68  
    2.69  
    2.70      (* locale dependencies *)
    2.71  
    2.72 -    fun encode_locale_dependency (dep: Locale.locale_dependency) =
    2.73 -      (#source dep, (#target dep, (#prefix dep, locale_dependency_subst thy dep))) |>
    2.74 +    fun encode_locale_dependency (dep: Locale.locale_dependency, subst) =
    2.75 +      (#source dep, (#target dep, (#prefix dep, subst))) |>
    2.76          let
    2.77            open XML.Encode Term_XML.Encode;
    2.78            val encode_subst =
    2.79 @@ -345,15 +352,16 @@
    2.80          in pair string (pair string (pair (list (pair string bool)) encode_subst)) end;
    2.81  
    2.82      val _ =
    2.83 -      (case Locale.dest_dependencies parents thy of
    2.84 +      (case get_dependencies parents thy of
    2.85          [] => ()
    2.86        | deps =>
    2.87            deps |> map_index (fn (i, dep) =>
    2.88              let
    2.89                val xname = string_of_int (i + 1);
    2.90                val name = Long_Name.implode [Context.theory_name thy, xname];
    2.91 +              val markup = make_entity_markup name xname (#pos (#1 dep)) (#serial (#1 dep));
    2.92                val body = encode_locale_dependency dep;
    2.93 -            in XML.Elem (make_entity_markup name xname (#pos dep) (#serial dep), body) end)
    2.94 +            in XML.Elem (markup, body) end)
    2.95            |> export_body thy "locale_dependencies");
    2.96  
    2.97