# HG changeset patch # User blanchet # Date 1367915370 -7200 # Node ID 83e8f0bf1eac34084a12c357d3b7ff4af5705094 # Parent 1cbcc0cc6bdf72cfee5c8154addffa64f0b47813 tuning diff -r 1cbcc0cc6bdf -r 83e8f0bf1eac src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue May 07 10:18:59 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue May 07 10:29:30 2013 +0200 @@ -231,7 +231,7 @@ val massage_rec_fun_arg_typesss = map o map o flat_rec o unzip_recT; -val mk_fold_fun_typess = map2 (map2 (curry (op --->))); +fun mk_fold_fun_typess y_Tsss Cs = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss; val mk_rec_fun_typess = mk_fold_fun_typess oo massage_rec_fun_arg_typesss; fun mk_fun_arg_typess n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type; @@ -241,10 +241,10 @@ #> map3 mk_fun_arg_typess ns mss #> map (map (map (unzip_recT fpTs))); -fun mk_fold_rec_args_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy = +fun mk_fold_rec_args_types fpTs Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy = let val y_Tsss = map3 mk_fun_arg_typess ns mss ctor_fold_fun_Ts; - val g_Tss = mk_fold_fun_typess y_Tsss Css; + val g_Tss = mk_fold_fun_typess y_Tsss Cs; val ((gss, ysss), lthy) = lthy @@ -252,7 +252,7 @@ ||>> mk_Freesss "x" y_Tsss; val z_Tsss = map3 mk_fun_arg_typess ns mss ctor_rec_fun_Ts; - val h_Tss = mk_rec_fun_typess fpTs z_Tsss Css; + val h_Tss = mk_rec_fun_typess fpTs z_Tsss Cs; val hss = map2 (map2 retype_free) h_Tss gss; val zsss = map2 (map2 (map2 retype_free)) z_Tsss ysss; @@ -284,15 +284,14 @@ val f_sum_prod_Ts = map range_type fun_Ts; val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts; val f_Tsss = map2 (map2 dest_tupleT o repair_arity) mss f_prod_Tss; - val f_Tssss = - map2 (fn C => map (map (map (curry (op -->) C) o maybe_unzipT))) Cs f_Tsss; + val f_Tssss = map2 (fn C => map (map (map (curry (op -->) C) o maybe_unzipT))) Cs f_Tsss; val q_Tssss = map (map (map (fn [_] => [] | [_, C] => [mk_pred1T (domain_type C)]))) f_Tssss; val pf_Tss = map3 flat_preds_predsss_gettersss p_Tss q_Tssss f_Tssss; - in (q_Tssss, f_sum_prod_Ts, f_Tsss, f_Tssss, pf_Tss) end; + in (q_Tssss, f_Tssss, (f_sum_prod_Ts, f_Tsss, pf_Tss)) end; - val (r_Tssss, g_sum_prod_Ts, g_Tsss, g_Tssss, pg_Tss) = mk_types single dtor_unfold_fun_Ts; - val (s_Tssss, h_sum_prod_Ts, h_Tsss, h_Tssss, ph_Tss) = mk_types unzip_corecT dtor_corec_fun_Ts; + val (r_Tssss, g_Tssss, unfold_types) = mk_types single dtor_unfold_fun_Ts; + val (s_Tssss, h_Tssss, corec_types) = mk_types unzip_corecT dtor_corec_fun_Ts; val (((cs, pss), gssss), lthy) = lthy @@ -310,18 +309,17 @@ val cpss = map2 (map o rapp) cs pss; - fun mk_terms qssss fssss = + fun mk_args qssss fssss = let val pfss = map3 flat_preds_predsss_gettersss pss qssss fssss; val cqssss = map2 (map o map o map o rapp) cs qssss; val cfssss = map2 (map o map o map o rapp) cs fssss; in (pfss, cqssss, cfssss) end; - val unfold_terms = mk_terms rssss gssss; - val corec_terms = mk_terms sssss hssss; + val unfold_args = mk_args rssss gssss; + val corec_args = mk_args sssss hssss; in - ((cs, cpss, (unfold_terms, (g_sum_prod_Ts, g_Tsss, pg_Tss)), - (corec_terms, (h_sum_prod_Ts, h_Tsss, ph_Tss))), lthy) + ((cs, cpss, (unfold_args, unfold_types), (corec_args, corec_types)), lthy) end; fun mk_map live Ts Us t = @@ -409,19 +407,16 @@ fun mk_fold_recs lthy fpTs As Cs ns mss ctor_folds ctor_recs = let - val Css = map2 replicate ns Cs; - val (_, ctor_fold_fun_Ts) = mk_fp_iter true As Cs ctor_folds; val (_, ctor_rec_fun_Ts) = mk_fp_iter true As Cs ctor_recs; val (((gss, _, ysss), (hss, _, zsss)), _) = - mk_fold_rec_args_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy; + mk_fold_rec_args_types fpTs Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy; fun mk_term ctor_iter fss xsss = fold_rev (fold_rev Term.lambda) fss (mk_iter_body lthy fpTs ctor_iter fss xsss); - fun mk_terms ctor_fold ctor_rec = - (mk_term ctor_fold gss ysss, mk_term ctor_rec hss zsss) + fun mk_terms ctor_fold ctor_rec = (mk_term ctor_fold gss ysss, mk_term ctor_rec hss zsss); in map2 mk_terms ctor_folds ctor_recs |> split_list end; @@ -471,7 +466,6 @@ val nn = length pre_bnfs; val ns = map length ctr_Tsss; val mss = map (map length) ctr_Tsss; - val Css = map2 replicate ns Cs; val pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_set_defss = map set_defs_of_bnf pre_bnfs; @@ -486,7 +480,7 @@ val (_, ctor_rec_fun_Ts) = mk_fp_iter true As Cs ctor_recs0; val (((gss, _, _), (hss, _, _)), names_lthy0) = - mk_fold_rec_args_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy; + mk_fold_rec_args_types fpTs Cs ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy; val ((((ps, ps'), xsss), us'), names_lthy) = names_lthy0 @@ -1054,14 +1048,13 @@ val ns = map length ctr_Tsss; val kss = map (fn n => 1 upto n) ns; val mss = map (map length) ctr_Tsss; - val Css = map2 replicate ns Cs; val (fp_folds, fp_fold_fun_Ts) = mk_fp_iter lfp As Cs fp_folds0; val (fp_recs, fp_rec_fun_Ts) = mk_fp_iter lfp As Cs fp_recs0; val (((fold_only, rec_only), (cs, cpss, unfold_only, corec_only)), _) = if lfp then - mk_fold_rec_args_types fpTs Css ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy + mk_fold_rec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy |>> rpair ([], [], (([], [], []), ([], [], [])), (([], [], []), ([], [], []))) else mk_unfold_corec_args_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy