# HG changeset patch # User traytel # Date 1458627516 -3600 # Node ID cb20e88281960b62fb3b0a7fa1a13edd13b136c2 # Parent ddd1c864408b462949458fe14cd609c86f86c5b3 document that n2m does not depend on most things in fp_sugar in its type diff -r ddd1c864408b -r cb20e8828196 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 21 21:18:08 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Tue Mar 22 07:18:36 2016 +0100 @@ -779,8 +779,8 @@ (case (absT, absU) of (Type (C, Ts), Type (C', Us)) => if C = C' then Term.typ_subst_atomic (Ts ~~ Us) repT - else raise Term.TYPE ("mk_repT", [absT, repT, absT], []) - | _ => raise Term.TYPE ("mk_repT", [absT, repT, absT], [])); + else raise Term.TYPE ("mk_repT", [absT, repT, absU], []) + | _ => raise Term.TYPE ("mk_repT", [absT, repT, absU], [])); fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf}, _)) = Const (@{const_name id_bnf}, absU --> absU) diff -r ddd1c864408b -r cb20e8828196 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Mar 21 21:18:08 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Mar 22 07:18:36 2016 +0100 @@ -8,7 +8,7 @@ signature BNF_FP_N2M = sig val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list -> - BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list -> + (int * BNF_FP_Util.fp_result) list -> binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory end; @@ -47,12 +47,10 @@ Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g end; -fun construct_mutualized_fp fp mutual_cliques fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) - bnfs (absT_infos : absT_info list) lthy = +fun construct_mutualized_fp fp mutual_cliques fpTs (fp_results : (int * fp_result) list) bs resBs + (resDs, Dss) bnfs (absT_infos : absT_info list) lthy = let - fun of_fp_res get = - map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars; - + fun of_fp_res get = map (uncurry nth o swap o apsnd get) fp_results; fun mk_co_algT T U = case_fp fp (T --> U) (U --> T); fun co_swap pair = case_fp fp I swap pair; val mk_co_comp = HOLogic.mk_comp o co_swap; @@ -68,13 +66,9 @@ val dest_co_productT = case_fp fp HOLogic.dest_prodT dest_sumT; val rewrite_comp_comp = case_fp fp @{thm rewriteL_comp_comp} @{thm rewriteR_comp_comp}; - val fp_absT_infos = map #absT_info fp_sugars; + val fp_absT_infos = of_fp_res #absT_infos; val fp_bnfs = of_fp_res #bnfs; - val pre_bnfs = map #pre_bnf fp_sugars; - val nesting_bnfss = - map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars; - val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss; - val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (flat fp_or_nesting_bnfss); + val pre_bnfs = of_fp_res #pre_bnfs; val fp_absTs = map #absT fp_absT_infos; val fp_repTs = map #repT fp_absT_infos; @@ -130,6 +124,15 @@ val fp_repAs = map2 mk_rep absATs fp_reps; val fp_repBs = map2 mk_rep absBTs fp_reps; + val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single); + val sorted_theta = sort (int_ord o apply2 (Term.size_of_typ o fst)) (fpTs ~~ Xs) + val sorted_fpTs = map fst sorted_theta; + + val nesting_bnfs = nesting_bnfs lthy + [[map (typ_subst_nonatomic_sorted (rev sorted_theta) o range_type o fastype_of) fp_repAs]] + allAs; + val fp_or_nesting_bnfs = distinct (op = o apply2 T_of_bnf) (fp_bnfs @ nesting_bnfs); + val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy |> mk_Frees' "R" phiTs ||>> mk_Frees "S" pre_phiTs @@ -138,9 +141,9 @@ val rels = let - fun find_rel T As Bs = fp_or_nesting_bnfss - |> map (filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf)) - |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T))) + fun find_rel T As Bs = fp_or_nesting_bnfs + |> filter_out (curry (op = o apply2 name_of_bnf) BNF_Comp.DEADID_bnf) + |> find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)) |> Option.map (fn bnf => let val live = live_of_bnf bnf; in (mk_rel live As Bs (rel_of_bnf bnf), live) end) @@ -258,9 +261,7 @@ |> mk_Frees' "s" rec_strTs; val co_recs = of_fp_res #xtor_co_recs; - val ns = map (length o #Ts o #fp_res) fp_sugars; - - val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single); + val ns = map (length o #Ts o snd) fp_results; fun foldT_of_recT recT = let @@ -288,8 +289,7 @@ val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs); val fold_pre_deads_only_Ts = - map (typ_subst_nonatomic_sorted (map (rpair dummyT) - (As @ sort (int_ord o apply2 Term.size_of_typ) fpTs))) fold_preTs'; + map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ sorted_fpTs))) fold_preTs'; val (mutual_clique, TUs) = map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec))) @@ -481,7 +481,8 @@ (* These results are half broken. This is deliberate. We care only about those fields that are used by "primrec", "primcorecursive", and "datatype_compat". *) val fp_res = - ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors, + ({Ts = fpTs, bnfs = of_fp_res #bnfs, pre_bnfs = bnfs, absT_infos = absT_infos, + dtors = dtors, ctors = ctors, xtor_un_folds = co_recs (*wrong*), xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm, dtor_ctors = of_fp_res #dtor_ctors (*too general types*), diff -r ddd1c864408b -r cb20e8828196 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 21 21:18:08 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Mar 22 07:18:36 2016 +0100 @@ -242,9 +242,11 @@ val fp_absT_infos = map #absT_info fp_sugars0; + val fp_results = 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, dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) = - fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_sugars0) fp_bs + fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_results) fp_bs unsorted_As' killed_As' fp_eqs no_defs_lthy; val fp_abs_inverses = map #abs_inverse fp_absT_infos; diff -r ddd1c864408b -r cb20e8828196 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 21 21:18:08 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 22 07:18:36 2016 +0100 @@ -13,6 +13,8 @@ type fp_result = {Ts: typ list, bnfs: BNF_Def.bnf list, + pre_bnfs: BNF_Def.bnf list, + absT_infos: BNF_Comp.absT_info list, ctors: term list, dtors: term list, xtor_un_folds: term list, @@ -213,6 +215,8 @@ type fp_result = {Ts: typ list, bnfs: bnf list, + pre_bnfs: BNF_Def.bnf list, + absT_infos: BNF_Comp.absT_info list, ctors: term list, dtors: term list, xtor_un_folds: term list, @@ -237,13 +241,15 @@ xtor_rel_co_induct: thm, dtor_set_inducts: thm list}; -fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct, - dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_map_uniques, xtor_setss, - xtor_rels, xtor_un_fold_thms, xtor_co_rec_thms, xtor_un_fold_uniques, xtor_co_rec_uniques, - xtor_un_fold_o_maps, xtor_co_rec_o_maps, xtor_un_fold_transfers, xtor_co_rec_transfers, - xtor_rel_co_induct, dtor_set_inducts} = +fun morph_fp_result phi {Ts, bnfs, pre_bnfs, absT_infos, ctors, dtors, xtor_un_folds, xtor_co_recs, + xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_map_uniques, + xtor_setss, xtor_rels, xtor_un_fold_thms, xtor_co_rec_thms, xtor_un_fold_uniques, + xtor_co_rec_uniques, xtor_un_fold_o_maps, xtor_co_rec_o_maps, xtor_un_fold_transfers, + xtor_co_rec_transfers, xtor_rel_co_induct, dtor_set_inducts} = {Ts = map (Morphism.typ phi) Ts, bnfs = map (morph_bnf phi) bnfs, + pre_bnfs = map (morph_bnf phi) pre_bnfs, + absT_infos = map (morph_absT_info phi) absT_infos, ctors = map (Morphism.term phi) ctors, dtors = map (Morphism.term phi) dtors, xtor_un_folds = map (Morphism.term phi) xtor_un_folds, diff -r ddd1c864408b -r cb20e8828196 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 21 21:18:08 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 22 07:18:36 2016 +0100 @@ -56,7 +56,8 @@ ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees; (*all BNFs have the same lives*) -fun construct_gfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs _ lthy = +fun construct_gfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs absT_infos + lthy = let val time = time lthy; val timer = time (Timer.startRealTimer ()); @@ -2691,10 +2692,10 @@ val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Jbnf_notes); val fp_res = - {Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, - xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, - ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, - dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms, + {Ts = Ts, bnfs = Jbnfs, pre_bnfs = bnfs, absT_infos = absT_infos, + ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, xtor_co_recs = corecs, + xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, + ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms, xtor_map_uniques = dtor_Jmap_unique_thms, xtor_setss = dtor_Jset_thmss', xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms = dtor_unfold_thms, xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_uniques = dtor_unfold_unique_thms, diff -r ddd1c864408b -r cb20e8828196 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 21 21:18:08 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 22 07:18:36 2016 +0100 @@ -27,7 +27,8 @@ open BNF_LFP_Tactics (*all BNFs have the same lives*) -fun construct_lfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs _ lthy = +fun construct_lfp mixfixes map_bs rel_bs pred_bs set_bss0 bs resBs (resDs, Dss) bnfs absT_infos + lthy = let val time = time lthy; val timer = time (Timer.startRealTimer ()); @@ -1951,8 +1952,9 @@ val lthy' = lthy |> internals ? snd o Local_Theory.notes (common_notes @ notes @ Ibnf_notes); val fp_res = - {Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds, - xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, + {Ts = Ts, bnfs = Ibnfs, pre_bnfs = bnfs, absT_infos = absT_infos, + ctors = ctors, dtors = dtors, xtor_un_folds = folds, xtor_co_recs = recs, + xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms, xtor_map_uniques = ctor_Imap_unique_thms, xtor_setss = ctor_Iset_thmss', diff -r ddd1c864408b -r cb20e8828196 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Mar 21 21:18:08 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Mar 22 07:18:36 2016 +0100 @@ -34,7 +34,8 @@ val co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))]; val co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}]; in - {Ts = [fpT], bnfs = [fp_bnf], ctors = xtors, dtors = xtors, xtor_un_folds = co_recs, + {Ts = [fpT], bnfs = [fp_bnf], pre_bnfs = [ID_bnf], absT_infos = [trivial_absT_info_of fpT], + ctors = xtors, dtors = xtors, xtor_un_folds = co_recs, xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor}, ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject}, dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], xtor_map_uniques = [],