added BNF cache (within one definition)

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Feb 24 00:04:48 2014 +0100
@@ -11,15 +11,18 @@
   val ID_bnf: BNF_Def.bnf
   val DEADID_bnf: BNF_Def.bnf
 
+  type comp_cache
   type unfold_set
+
+  val empty_comp_cache: comp_cache
   val empty_unfolds: unfold_set
 
   exception BAD_DEAD of typ * typ
 
   val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
     ((string * sort) list list -> (string * sort) list) -> (string * sort) list ->
-    (string * sort) list -> typ -> unfold_set * Proof.context ->
-    (BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context)
+    (string * sort) list -> typ -> (comp_cache * unfold_set) * Proof.context ->
+    (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * Proof.context)
   val default_comp_sort: (string * sort) list list -> (string * sort) list
   val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
     (''a list list -> ''a list) -> BNF_Def.bnf list -> unfold_set -> Proof.context ->
@@ -39,13 +42,16 @@
 val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
 val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
 
-(* TODO: Replace by "BNF_Defs.defs list" *)
+type comp_cache = (bnf * (typ list * typ list)) Typtab.table;
+
+(* TODO: Replace by "BNF_Defs.defs list"? *)
 type unfold_set = {
   map_unfolds: thm list,
   set_unfoldss: thm list list,
   rel_unfolds: thm list
 };
 
+val empty_comp_cache = Typtab.empty;
 val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = []};
 
 fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new;
@@ -650,12 +656,19 @@
     ((bnf', deads), lthy')
   end;
 
+fun key_of_types Ts = Type ("", Ts);
+val key_of_typess = key_of_types o map key_of_types;
+fun key_of_comp oDs Dss Ass T = key_of_types (map key_of_typess [[oDs], Dss, Ass, [[T]]]);
+
+fun cache_comp key cache (bnf_dead_lives, (unfold_set, lthy)) =
+  (bnf_dead_lives, ((Typtab.update (key, bnf_dead_lives) cache, unfold_set), lthy));
+
 exception BAD_DEAD of typ * typ;
 
 fun bnf_of_typ _ _ _ _ Ds0 (T as TFree T') accum =
     (if member (op =) Ds0 T' then (DEADID_bnf, ([T], [])) else (ID_bnf, ([], [T])), accum)
   | bnf_of_typ _ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
-  | bnf_of_typ const_policy qualify' sort Xs Ds0 (T as Type (C, Ts)) (accum as (unfold_set, lthy)) =
+  | bnf_of_typ const_policy qualify' sort Xs Ds0 (T as Type (C, Ts)) (accum as (_, lthy)) =
     let
       fun check_bad_dead ((_, (deads, _)), _) =
         let val Ds = fold Term.add_tfreesT deads [] in
@@ -678,7 +691,7 @@
             val deads_lives =
               pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
                 (deads, lives);
-          in ((bnf, deads_lives), (unfold_set, lthy)) end
+          in ((bnf, deads_lives), accum) end
         else
           let
             val name = Long_Name.base_name C;
@@ -691,12 +704,18 @@
               (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf)));
             val oDs = map (nth Ts) oDs_pos;
             val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
-            val ((inners, (Dss, Ass)), (unfold_set', lthy')) =
+            val ((inners, (Dss, Ass)), ((cache', unfold_set'), lthy')) =
               apfst (apsnd split_list o split_list)
                 (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort Xs Ds0)
-                (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy));
+                (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' accum);
+            val key = key_of_comp oDs Dss Ass T;
           in
-            compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy')
+            (case Typtab.lookup cache' key of
+              SOME bnf_deads_lives => (bnf_deads_lives, accum)
+            | NONE =>
+              (unfold_set', lthy')
+              |> compose_bnf const_policy qualify sort bnf inners oDs Dss Ass
+              |> cache_comp key cache')
           end)
       |> tap check_bad_dead
     end;

--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Feb 24 00:04:48 2014 +0100
@@ -581,9 +581,10 @@
         #> Binding.conceal
       end;
 
-    val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
-      (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs Ds0) bs rhsXs
-        (empty_unfolds, lthy));
+    val ((bnfs, (deadss, livess)), ((_, unfold_set), lthy)) =
+      apfst (apsnd split_list o split_list)
+        (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs Ds0) bs rhsXs
+          ((empty_comp_cache, empty_unfolds), lthy));
 
     fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
       #> Binding.conceal;