# HG changeset patch # User blanchet # Date 1380629604 -7200 # Node ID f138452e8265704b771a7dbe459ddab11d2ab110 # Parent b15cfc2864dede0d8b84eb5f11f183d6bad778bc got rid of dead feature diff -r b15cfc2864de -r f138452e8265 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Tue Oct 01 14:05:25 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Tue Oct 01 14:13:24 2013 +0200 @@ -7,7 +7,7 @@ signature BNF_FP_N2M_SUGAR = sig - val mutualize_fp_sugars: bool -> bool -> BNF_FP_Util.fp_kind -> binding list -> typ list -> + val mutualize_fp_sugars: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory -> (BNF_FP_Def_Sugar.fp_sugar list @@ -15,8 +15,8 @@ * local_theory val pad_and_indexify_calls: BNF_FP_Def_Sugar.fp_sugar list -> int -> (term * term list list) list list -> term list list list list - val nested_to_mutual_fps: bool -> BNF_FP_Util.fp_kind -> binding list -> typ list -> - (term -> int list) -> ((term * term list list) list) list -> local_theory -> + val nested_to_mutual_fps: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) -> + (term * term list list) list list -> local_theory -> (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) * local_theory @@ -37,9 +37,7 @@ (* TODO: test with sort constraints on As *) (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables as deads? *) -fun mutualize_fp_sugars lose_co_rec mutualize fp bs fpTs get_indices callssss fp_sugars0 - no_defs_lthy0 = - (* TODO: Also check whether there's any lost recursion? *) +fun mutualize_fp_sugars mutualize fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 = if mutualize orelse has_duplicates (op =) fpTs then let val thy = Proof_Context.theory_of no_defs_lthy0; @@ -79,11 +77,6 @@ |> mk_TFrees nn ||>> variant_tfrees fp_b_names; - (* If "lose_co_rec" is "true", the function "null" on "'a list" gives rise to - 'list = unit + 'a list - instead of - 'list = unit + 'list - resulting in a simpler (co)induction rule and (co)recursor. *) fun freeze_fp_default (T as Type (s, Ts)) = (case find_index (curry (op =) T) fpTs of ~1 => Type (s, map freeze_fp_default Ts) @@ -100,7 +93,7 @@ [] => (case union (op = o pairself fst) (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of - [] => T |> not lose_co_rec ? freeze_fp_default + [] => freeze_fp_default T | [(kk, _)] => nth Xs kk | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2) | callss => @@ -201,7 +194,7 @@ fun pad_and_indexify_calls fp_sugars0 = map2 indexify_callsss fp_sugars0 oo pad_list []; -fun nested_to_mutual_fps lose_co_rec fp actual_bs actual_Ts get_indices actual_callssss0 lthy = +fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy = let val qsoty = quote o Syntax.string_of_typ lthy; val qsotys = space_implode " or " o map qsoty; @@ -264,7 +257,7 @@ val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices; val ((perm_fp_sugars, fp_sugar_thms), lthy) = - mutualize_fp_sugars lose_co_rec mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss + mutualize_fp_sugars mutualize fp perm_bs perm_Ts get_perm_indices perm_callssss perm_fp_sugars0 lthy; val fp_sugars = unpermute perm_fp_sugars; diff -r b15cfc2864de -r f138452e8265 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Tue Oct 01 14:05:25 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Tue Oct 01 14:13:24 2013 +0200 @@ -422,8 +422,6 @@ | NONE => []) | map_thms_of_typ _ _ = []; -val lose_co_rec = false (*FIXME: try true?*); - fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy = let val thy = Proof_Context.theory_of lthy; @@ -431,7 +429,7 @@ val ((missing_arg_Ts, perm0_kks, fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...}, co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy') = - nested_to_mutual_fps lose_co_rec Least_FP bs arg_Ts get_indices callssss0 lthy; + nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy; val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars; @@ -515,7 +513,7 @@ val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...}, co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy') = - nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy; + nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy; val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars; diff -r b15cfc2864de -r f138452e8265 src/HOL/BNF/Tools/bnf_lfp_compat.ML --- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML Tue Oct 01 14:05:25 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML Tue Oct 01 14:13:24 2013 +0200 @@ -95,8 +95,7 @@ val has_nested = nn > nn_fp; val ((fp_sugars, (lfp_sugar_thms, _)), lthy) = - mutualize_fp_sugars false has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0 - lthy; + mutualize_fp_sugars has_nested Least_FP compat_bs Ts get_indices callssss fp_sugars0 lthy; val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ = fp_sugars;