introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales

--- a/src/HOL/Ctr_Sugar.thy	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Ctr_Sugar.thy	Wed Sep 03 22:49:05 2014 +0200
@@ -37,6 +37,7 @@
 "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
 by blast+
 
+ML_file "Tools/Ctr_Sugar/local_interpretation.ML"
 ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
 ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
 ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"

--- a/src/HOL/Lifting.thy	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Lifting.thy	Wed Sep 03 22:49:05 2014 +0200
@@ -556,11 +556,8 @@
 lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
 
 ML_file "Tools/Lifting/lifting_bnf.ML"
-
 ML_file "Tools/Lifting/lifting_term.ML"
-
 ML_file "Tools/Lifting/lifting_def.ML"
-
 ML_file "Tools/Lifting/lifting_setup.ML"
                            
 hide_const (open) POS NEG

--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -17,7 +17,10 @@
   val transfer_bnf: theory -> bnf -> bnf
   val bnf_of: Proof.context -> string -> bnf option
   val bnf_of_global: theory -> string -> bnf option
-  val bnf_interpretation: (bnf -> theory -> theory) -> theory -> theory
+  val bnf_interpretation: (bnf -> theory -> theory) -> (bnf -> local_theory -> local_theory) ->
+    theory -> theory
+  val interpret_bnf: bnf -> local_theory -> local_theory
+  val register_bnf_raw: string -> bnf -> local_theory -> local_theory
   val register_bnf: string -> bnf -> local_theory -> local_theory
 
   val name_of_bnf: bnf -> binding
@@ -1512,7 +1515,7 @@
     (key, goals, wit_goalss, after_qed, lthy, one_step_defs)
   end;
 
-structure BNF_Interpretation = Interpretation
+structure BNF_Interpretation = Local_Interpretation
 (
   type T = bnf;
   val eq: T * T -> bool = op = o pairself T_of_bnf;
@@ -1533,13 +1536,14 @@
     |> Sign.restore_naming thy
   end;
 
-fun bnf_interpretation f = BNF_Interpretation.interpretation (with_repaired_path f);
+val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path;
+val interpret_bnf = BNF_Interpretation.data;
 
-fun register_bnf key bnf =
+fun register_bnf_raw key bnf =
   Local_Theory.declaration {syntax = false, pervasive = true}
-    (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)))
-  #> Local_Theory.background_theory
-    (fn thy => BNF_Interpretation.data (the (bnf_of_global thy key)) thy);
+    (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
+
+fun register_bnf key bnf = register_bnf_raw key bnf #> interpret_bnf bnf;
 
 fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
   (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -12,7 +12,8 @@
   val fp_sugar_of_global: theory -> string -> BNF_FP_Util.fp_sugar option
   val fp_sugars_of: Proof.context -> BNF_FP_Util.fp_sugar list
   val fp_sugars_of_global: theory -> BNF_FP_Util.fp_sugar list
-  val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) -> theory -> theory
+  val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) ->
+    (BNF_FP_Util.fp_sugar list -> local_theory -> local_theory)-> theory -> theory
   val register_fp_sugars: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory
 
   val co_induct_of: 'a list -> 'a
@@ -158,7 +159,7 @@
 fun co_induct_of (i :: _) = i;
 fun strong_co_induct_of [_, s] = s;
 
-structure FP_Sugar_Interpretation = Interpretation
+structure FP_Sugar_Interpretation = Local_Interpretation
 (
   type T = fp_sugar list;
   val eq: T * T -> bool = op = o pairself (map #T);
@@ -171,7 +172,7 @@
   |> f (map (transfer_fp_sugar thy) fp_sugars)
   |> Sign.restore_naming thy;
 
-fun fp_sugar_interpretation f = FP_Sugar_Interpretation.interpretation (with_repaired_path f);
+val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
 
 fun register_fp_sugars (fp_sugars as {fp, ...} :: _) =
   fold (fn fp_sugar as {T = Type (s, _), ...} =>
@@ -179,12 +180,12 @@
         (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
     fp_sugars
   #> fp = Least_FP ? generate_lfp_size fp_sugars
-  #> Local_Theory.background_theory (fn thy => FP_Sugar_Interpretation.data
-    (map (the o fp_sugar_of_global thy o fst o dest_Type o #T) fp_sugars) thy);
+  #> FP_Sugar_Interpretation.data fp_sugars;
 
-fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res
-    ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss
-    co_rec_thmss co_rec_discss co_rec_selsss rel_injectss rel_distinctss noted =
+fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
+    live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss
+    common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
+    rel_distinctss noted =
   let
     val fp_sugars =
       map_index (fn (kk, T) =>
@@ -199,7 +200,8 @@
          rel_distincts = nth rel_distinctss kk}
         |> morph_fp_sugar (substitute_noted_thm noted)) Ts;
   in
-    register_fp_sugars fp_sugars
+    fold interpret_bnf (#bnfs fp_res)
+    #> register_fp_sugars fp_sugars
   end;
 
 (* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A",
@@ -1972,10 +1974,10 @@
         (* for "datatype_realizer.ML": *)
         |>> name_noted_thms
           (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN
-        |-> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs
-          live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
-          (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss
-          rel_distinctss
+        |-> interpret_bnfs_register_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
+          fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
+          mapss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn [])
+          rel_injectss rel_distinctss
       end;
 
     fun derive_note_coinduct_corecs_thms_for_types
@@ -2064,13 +2066,15 @@
         |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
           [flat corec_sel_thmss, flat corec_thmss]
         |> Local_Theory.notes (common_notes @ notes)
-        |-> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs
-          live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
-          [coinduct_thm, coinduct_strong_thm] (transpose [coinduct_thms, coinduct_strong_thms])
-          corec_thmss corec_disc_thmss corec_sel_thmsss rel_injectss rel_distinctss
+        |-> interpret_bnfs_register_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos
+          fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs
+          mapss [coinduct_thm, coinduct_strong_thm]
+          (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
+          corec_sel_thmsss rel_injectss rel_distinctss
       end;
 
     val lthy'' = lthy'
+      |> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
       |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
         xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
         pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -2435,8 +2435,7 @@
           fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
               fn consts =>
             bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms)
-              (SOME deads) map_b rel_b set_bs consts
-            #> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
+              (SOME deads) map_b rel_b set_bs consts)
           bs tacss map_bs rel_bs set_bss wit_thmss
           ((((((replicate n Binding.empty ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~
             all_witss) ~~ map SOME Jrels)

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -1722,8 +1722,7 @@
         val (Ibnfs, lthy) =
           fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts =>
             bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads)
-              map_b rel_b set_bs consts
-            #> (fn (bnf, lthy) => (bnf, register_bnf (Local_Theory.full_name lthy b) bnf lthy)))
+              map_b rel_b set_bs consts)
           bs tacss map_bs rel_bs set_bss
             ((((((replicate n Binding.empty ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~
               Iwitss) ~~ map SOME Irels) lthy;

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -281,8 +281,10 @@
   end;
 
 fun interpretation nesting_pref f =
-  Old_Datatype_Data.interpretation (old_interpretation_of nesting_pref f)
-  #> fp_sugar_interpretation (new_interpretation_of nesting_pref f);
+  let val new_f = new_interpretation_of nesting_pref f in
+    Old_Datatype_Data.interpretation (old_interpretation_of nesting_pref f)
+    #> fp_sugar_interpretation new_f (Local_Theory.background_theory o new_f)
+  end;
 
 val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
 

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -43,7 +43,8 @@
   val ctr_sugars_of_global: theory -> ctr_sugar list
   val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
   val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
-  val ctr_sugar_interpretation: (ctr_sugar -> theory -> theory) -> theory -> theory
+  val ctr_sugar_interpretation: (ctr_sugar -> theory -> theory) ->
+    (ctr_sugar -> local_theory -> local_theory) -> theory -> theory
   val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
   val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
 
@@ -170,26 +171,25 @@
 val ctr_sugar_of_case = ctr_sugar_of_case_generic o Context.Proof;
 val ctr_sugar_of_case_global = ctr_sugar_of_case_generic o Context.Theory;
 
-structure Ctr_Sugar_Interpretation = Interpretation
+structure Ctr_Sugar_Interpretation = Local_Interpretation
 (
   type T = ctr_sugar;
   val eq: T * T -> bool = op = o pairself #ctrs;
 );
 
-fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy =
+fun with_repaired_path g (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy =
   thy
   |> Sign.root_path
   |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
-  |> (fn thy => f (transfer_ctr_sugar thy ctr_sugar) thy)
+  |> (fn thy => g (transfer_ctr_sugar thy ctr_sugar) thy)
   |> Sign.restore_naming thy;
 
-fun ctr_sugar_interpretation f = Ctr_Sugar_Interpretation.interpretation (with_repaired_path f);
+val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
 
 fun register_ctr_sugar key ctr_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)))
-  #> Local_Theory.background_theory
-    (fn thy => Ctr_Sugar_Interpretation.data (the (ctr_sugar_of_global thy key)) thy);
+  #> Ctr_Sugar_Interpretation.data ctr_sugar;
 
 fun default_register_ctr_sugar_global key ctr_sugar thy =
   let val tab = Data.get (Context.Theory thy) in
@@ -198,7 +198,7 @@
     else
       thy
       |> Context.theory_map (Data.put (Symtab.update_new (key, ctr_sugar) tab))
-      |> Ctr_Sugar_Interpretation.data ctr_sugar
+      |> Ctr_Sugar_Interpretation.data_global ctr_sugar
   end;
 
 val isN = "is_";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -0,0 +1,72 @@
+(*  Title:      HOL/Tools/Ctr_Sugar/local_interpretation.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Generic interpretation of local theory data -- ad hoc. Based on
+
+    Title:      Pure/interpretation.ML
+    Author:     Florian Haftmann and Makarius
+*)
+
+signature LOCAL_INTERPRETATION =
+sig
+  type T
+  val result: theory -> T list
+  val interpretation: (T -> theory -> theory) -> (T -> local_theory -> local_theory) -> theory ->
+    theory
+  val data: T -> local_theory -> local_theory
+  val data_global: T -> theory -> theory
+  val init: theory -> theory
+end;
+
+functor Local_Interpretation(type T val eq: T * T -> bool): LOCAL_INTERPRETATION =
+struct
+
+type T = T;
+
+structure Interp = Theory_Data
+(
+  type T =
+    T list
+    * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * stamp) * T list) list;
+  val empty = ([], []);
+  val extend = I;
+  fun merge ((data1, interps1), (data2, interps2)) : T =
+    (Library.merge eq (data1, data2),
+     AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
+);
+
+val result = #1 o Interp.get;
+
+fun consolidate lthy =
+  let
+    val thy = Proof_Context.theory_of lthy;
+    val (data, interps) = Interp.get thy;
+    val unfinished = interps |> map (fn (((_, f), _), xs) =>
+      (f, if eq_list eq (xs, data) then [] else subtract eq xs data));
+    val finished = interps |> map (fn (interp, _) => (interp, data));
+  in
+    if forall (null o #2) unfinished then NONE
+    else SOME (lthy |> fold_rev (uncurry fold_rev) unfinished
+      |> Local_Theory.background_theory (Interp.put (data, finished)))
+  end;
+
+fun consolidate_global thy =
+  let
+    val (data, interps) = Interp.get thy;
+    val unfinished = interps |> map (fn (((g, _), _), xs) =>
+      (g, if eq_list eq (xs, data) then [] else subtract eq xs data));
+    val finished = interps |> map (fn (interp, _) => (interp, data));
+  in
+    if forall (null o #2) unfinished then NONE
+    else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))
+  end;
+
+fun interpretation g f =
+  Interp.map (apsnd (cons (((g, f), stamp ()), []))) #> perhaps consolidate_global;
+
+fun data x = Local_Theory.background_theory (Interp.map (apfst (cons x))) #> perhaps consolidate;
+fun data_global x = Interp.map (apfst (cons x)) #> perhaps consolidate_global;
+
+val init = Theory.at_begin consolidate_global;
+
+end;

--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -116,6 +116,7 @@
     end
 
 val _ = Context.>> (Context.map_theory (bnf_interpretation
-  (bnf_only_type_ctr (fn bnf => map_local_theory (lifting_bnf_interpretation bnf)))))
+  (bnf_only_type_ctr (map_local_theory o lifting_bnf_interpretation))
+  (bnf_only_type_ctr lifting_bnf_interpretation)))
 
 end

--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -291,7 +291,8 @@
   end
 
 val _ = Context.>> (Context.map_theory (bnf_interpretation
-  (bnf_only_type_ctr (fn bnf => map_local_theory (transfer_bnf_interpretation bnf)))))
+  (bnf_only_type_ctr (map_local_theory o transfer_bnf_interpretation))
+  (bnf_only_type_ctr (transfer_bnf_interpretation))))
 
 (* simplification rules for the predicator *)
 
@@ -360,7 +361,8 @@
     snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
   end
 
-val _ = Context.>> (Context.map_theory (fp_sugar_interpretation (fp_sugar_only_type_ctr
-  (fn fp_sugars => map_local_theory (fold transfer_fp_sugar_interpretation fp_sugars)))))
+val _ = Context.>> (Context.map_theory (fp_sugar_interpretation
+  (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugar_interpretation))
+  (fp_sugar_only_type_ctr (fold transfer_fp_sugar_interpretation))))
 
 end

--- a/src/Pure/interpretation.ML	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/Pure/interpretation.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -47,4 +47,3 @@
 val init = Theory.at_begin consolidate;
 
 end;
-