# HG changeset patch
# User blanchet
# Date 1459159547 -7200
# Node ID 2ceae1e761bd75ce88d4e67915080fa8c825d458
# Parent  2e05b5ad6ae11dd6b0a67c8c878aecdd2b219f80
generalized ML interface

diff -r 2e05b5ad6ae1 -r 2ceae1e761bd src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -2168,14 +2168,14 @@
       map_filter (fn (A, set_bos) => if exists is_none set_bos then SOME A else NONE)
         (unsorted_As ~~ transpose set_boss);
 
-    val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
+    val (((pre_bnfs, absT_infos), _), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
              dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
              ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels,
              xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
              xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
            lthy)) =
-      fp_bnf (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs
-        (map dest_TFree unsorted_As) (map dest_TFree killed_As) fp_eqs no_defs_lthy
+      fixpoint_bnf (construct_fp mixfixes map_bs rel_bs pred_bs set_bss) fp_bs
+        (map dest_TFree unsorted_As) (map dest_TFree killed_As) fp_eqs empty_comp_cache no_defs_lthy
       handle BAD_DEAD (X, X_backdrop) =>
         (case X_backdrop of
           Type (bad_tc, _) =>
diff -r 2e05b5ad6ae1 -r 2ceae1e761bd src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -31,6 +31,7 @@
 open Ctr_Sugar
 open BNF_Util
 open BNF_Def
+open BNF_Comp
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
 open BNF_FP_N2M
@@ -243,10 +244,10 @@
         val fp_absT_infos = map #absT_info fp_sugars0;
         val indexed_fp_ress = map (apsnd #fp_res o `(#fp_res_index)) fp_sugars0;
 
-        val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
+        val (((pre_bnfs, absT_infos), _), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
                dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
-          fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs indexed_fp_ress) fp_bs
-            unsorted_As' killed_As' fp_eqs no_defs_lthy;
+          fixpoint_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs indexed_fp_ress)
+            fp_bs unsorted_As' killed_As' fp_eqs empty_comp_cache no_defs_lthy;
 
         val time = time lthy;
         val timer = time (Timer.startRealTimer ());
@@ -389,7 +390,6 @@
 fun nested_to_mutual_fps plugins fp actual_bs actual_Ts actual_callers actual_callssss0 lthy =
   let
     val qsoty = quote o Syntax.string_of_typ lthy;
-    val qsotys = space_implode " or " o map qsoty;
 
     fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype");
     fun not_co_datatype (T as Type (s, _)) =
diff -r 2e05b5ad6ae1 -r 2ceae1e761bd src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -197,10 +197,11 @@
   val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list
 
-  val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
+  val fixpoint_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
     binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list ->
-    local_theory -> (BNF_Def.bnf list * BNF_Comp.absT_info list) * 'a
+    BNF_Comp.comp_cache -> local_theory ->
+    ((BNF_Def.bnf list * BNF_Comp.absT_info list) * BNF_Comp.comp_cache) * 'a
   val fp_antiquote_setup: binding -> theory -> theory
 end;
 
@@ -608,7 +609,7 @@
     split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
   end;
 
-fun fp_bnf construct_fp bs resBs Ds0 fp_eqs lthy =
+fun fixpoint_bnf construct_fp bs resBs Ds0 fp_eqs comp_cache0 lthy =
   let
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
@@ -629,11 +630,11 @@
         #> Binding.concealed
       end;
 
-    val ((bnfs, (deadss, livess)), accum) =
+    val ((bnfs, (deadss, livess)), (comp_cache, unfold_set)) =
       apfst (apsnd split_list o split_list)
         (@{fold_map 2}
           (fn b => bnf_of_typ true Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
-          ((empty_comp_cache, empty_unfolds), lthy));
+          ((comp_cache0, empty_unfolds), lthy));
 
     fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
       #> Binding.concealed;
@@ -647,8 +648,8 @@
 
     val timer = time (timer "Construction of BNFs");
 
-    val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) =
-      normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum;
+    val ((kill_poss, _), (bnfs', ((comp_cache', unfold_set'), lthy'))) =
+      normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs (comp_cache, unfold_set);
 
     val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
 
@@ -667,7 +668,7 @@
 
     val timer = time (timer "FP construction in total");
   in
-    ((pre_bnfs, absT_infos), res)
+    (((pre_bnfs, absT_infos), comp_cache'), res)
   end;
 
 fun fp_antiquote_setup binding =