added some N2M caching
authorblanchet
Tue Nov 05 05:48:08 2013 +0100 (2013-11-05)
changeset 542564843082be7ef
parent 54255 4f7c016d5bc6
child 54257 5c7a3b6b05a9
added some N2M caching
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML
src/HOL/BNF/Tools/ctr_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     1.3 @@ -25,7 +25,9 @@
     1.4       sel_co_iterssss: thm list list list list};
     1.5  
     1.6    val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
     1.7 +  val eq_fp_sugar: fp_sugar * fp_sugar -> bool
     1.8    val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
     1.9 +  val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
    1.10    val fp_sugar_of: Proof.context -> string -> fp_sugar option
    1.11    val fp_sugars_of: Proof.context -> fp_sugar list
    1.12  
    1.13 @@ -44,6 +46,9 @@
    1.14      (thm list * thm * Args.src list)
    1.15      * (thm list list * thm list list * Args.src list)
    1.16  
    1.17 +  val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms
    1.18 +  val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
    1.19 +
    1.20    type gfp_sugar_thms =
    1.21      ((thm list * thm) list * Args.src list)
    1.22      * (thm list list * thm list list * Args.src list)
    1.23 @@ -51,6 +56,9 @@
    1.24      * (thm list list * thm list list * Args.src list)
    1.25      * (thm list list list * thm list list list * Args.src list)
    1.26  
    1.27 +  val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
    1.28 +  val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms
    1.29 +
    1.30    val mk_co_iters_prelims: BNF_FP_Util.fp_kind -> typ list list list -> typ list -> typ list ->
    1.31      int list -> int list list -> term list list -> Proof.context ->
    1.32      (term list list
    1.33 @@ -331,6 +339,13 @@
    1.34    (thm list * thm * Args.src list)
    1.35    * (thm list list * thm list list * Args.src list)
    1.36  
    1.37 +fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (foldss, recss, iter_attrs)) =
    1.38 +  ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
    1.39 +   (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs));
    1.40 +
    1.41 +val transfer_lfp_sugar_thms =
    1.42 +  morph_lfp_sugar_thms o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
    1.43 +
    1.44  type gfp_sugar_thms =
    1.45    ((thm list * thm) list * Args.src list)
    1.46    * (thm list list * thm list list * Args.src list)
    1.47 @@ -338,6 +353,23 @@
    1.48    * (thm list list * thm list list * Args.src list)
    1.49    * (thm list list list * thm list list list * Args.src list);
    1.50  
    1.51 +fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs),
    1.52 +    (unfoldss, corecss, coiter_attrs), (disc_unfoldss, disc_corecss, disc_iter_attrs),
    1.53 +    (disc_unfold_iffss, disc_corec_iffss, disc_iter_iff_attrs),
    1.54 +    (sel_unfoldsss, sel_corecsss, sel_iter_attrs)) =
    1.55 +  ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
    1.56 +    coinduct_attrs),
    1.57 +   (map (map (Morphism.thm phi)) unfoldss, map (map (Morphism.thm phi)) corecss, coiter_attrs),
    1.58 +   (map (map (Morphism.thm phi)) disc_unfoldss, map (map (Morphism.thm phi)) disc_corecss,
    1.59 +    disc_iter_attrs),
    1.60 +   (map (map (Morphism.thm phi)) disc_unfold_iffss, map (map (Morphism.thm phi)) disc_corec_iffss,
    1.61 +    disc_iter_iff_attrs),
    1.62 +   (map (map (map (Morphism.thm phi))) sel_unfoldsss,
    1.63 +    map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs));
    1.64 +
    1.65 +val transfer_gfp_sugar_thms =
    1.66 +  morph_gfp_sugar_thms o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
    1.67 +
    1.68  fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
    1.69  
    1.70  fun mk_iter_fun_arg_types ctr_Tsss ns mss =
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     2.3 @@ -37,6 +37,32 @@
     2.4  
     2.5  val n2mN = "n2m_"
     2.6  
     2.7 +type n2m_sugar = fp_sugar list * (lfp_sugar_thms option * gfp_sugar_thms option);
     2.8 +
     2.9 +structure Data = Generic_Data
    2.10 +(
    2.11 +  type T = n2m_sugar Typtab.table;
    2.12 +  val empty = Typtab.empty;
    2.13 +  val extend = I;
    2.14 +  val merge = Typtab.merge (eq_fst (eq_list eq_fp_sugar));
    2.15 +);
    2.16 +
    2.17 +fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) =
    2.18 +  (map (morph_fp_sugar phi) fp_sugars,
    2.19 +   (Option.map (morph_lfp_sugar_thms phi) lfp_sugar_thms_opt,
    2.20 +    Option.map (morph_gfp_sugar_thms phi) gfp_sugar_thms_opt));
    2.21 +
    2.22 +val transfer_n2m_sugar =
    2.23 +  morph_n2m_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
    2.24 +
    2.25 +fun n2m_sugar_of ctxt =
    2.26 +  Typtab.lookup (Data.get (Context.Proof ctxt))
    2.27 +  #> Option.map (transfer_n2m_sugar ctxt);
    2.28 +
    2.29 +fun register_n2m_sugar key n2m_sugar =
    2.30 +  Local_Theory.declaration {syntax = false, pervasive = false}
    2.31 +    (fn phi => Data.map (Typtab.default (key, morph_n2m_sugar phi n2m_sugar)));
    2.32 +
    2.33  fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1))
    2.34    | unfold_let (Const (@{const_name prod_case}, _) $ t) =
    2.35      (case unfold_let t of
    2.36 @@ -93,6 +119,9 @@
    2.37        case f x of SOME y => (y :: ys, (x :: good, bad)) | NONE => (ys, (good, x :: bad)))
    2.38      xs ([], ([], []));
    2.39  
    2.40 +fun key_of_fp_eqs fp fpTs fp_eqs =
    2.41 +  Type (fp_case fp "l" "g", fpTs @ maps (fn (z, T) => [TFree z, T]) fp_eqs);
    2.42 +
    2.43  (* TODO: test with sort constraints on As *)
    2.44  (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
    2.45     as deads? *)
    2.46 @@ -168,75 +197,82 @@
    2.47        val mss = map (map length) ctr_Tsss;
    2.48  
    2.49        val fp_eqs = map dest_TFree Xs ~~ ctrXs_sum_prod_Ts;
    2.50 -
    2.51 -      val base_fp_names = Name.variant_list [] fp_b_names;
    2.52 -      val fp_bs = map2 (fn b_name => fn base_fp_name =>
    2.53 -          Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
    2.54 -        b_names base_fp_names;
    2.55 +      val key = key_of_fp_eqs fp fpTs fp_eqs;
    2.56 +    in
    2.57 +      (case n2m_sugar_of no_defs_lthy key of
    2.58 +        SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
    2.59 +      | NONE =>
    2.60 +        let
    2.61 +          val base_fp_names = Name.variant_list [] fp_b_names;
    2.62 +          val fp_bs = map2 (fn b_name => fn base_fp_name =>
    2.63 +              Binding.qualify true b_name (Binding.name (n2mN ^ base_fp_name)))
    2.64 +            b_names base_fp_names;
    2.65  
    2.66 -      val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
    2.67 -             dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
    2.68 -        fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' fp_eqs no_defs_lthy;
    2.69 +          val (pre_bnfs, (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
    2.70 +                 dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
    2.71 +            fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' fp_eqs no_defs_lthy;
    2.72  
    2.73 -      val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
    2.74 -      val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
    2.75 -
    2.76 -      val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
    2.77 -        mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
    2.78 +          val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
    2.79 +          val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
    2.80  
    2.81 -      fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
    2.82 +          val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
    2.83 +            mk_co_iters_prelims fp ctr_Tsss fpTs Cs ns mss xtor_co_iterss0 lthy;
    2.84 +
    2.85 +          fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
    2.86  
    2.87 -      val ((co_iterss, co_iter_defss), lthy) =
    2.88 -        fold_map2 (fn b =>
    2.89 -          (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
    2.90 -           else define_coiters [unfoldN, corecN] (the coiters_args_types))
    2.91 -            (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
    2.92 -        |>> split_list;
    2.93 +          val ((co_iterss, co_iter_defss), lthy) =
    2.94 +            fold_map2 (fn b =>
    2.95 +              (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
    2.96 +               else define_coiters [unfoldN, corecN] (the coiters_args_types))
    2.97 +                (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
    2.98 +            |>> split_list;
    2.99  
   2.100 -      val rho = tvar_subst thy Ts fpTs;
   2.101 -      val ctr_sugar_phi =
   2.102 -        Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
   2.103 -          (Morphism.term_morphism (Term.subst_TVars rho));
   2.104 -      val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
   2.105 -
   2.106 -      val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
   2.107 +          val rho = tvar_subst thy Ts fpTs;
   2.108 +          val ctr_sugar_phi =
   2.109 +            Morphism.compose (Morphism.typ_morphism (Term.typ_subst_TVars rho))
   2.110 +              (Morphism.term_morphism (Term.subst_TVars rho));
   2.111 +          val inst_ctr_sugar = morph_ctr_sugar ctr_sugar_phi;
   2.112  
   2.113 -      val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
   2.114 -            sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
   2.115 -        if fp = Least_FP then
   2.116 -          derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
   2.117 -            xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
   2.118 -            co_iterss co_iter_defss lthy
   2.119 -          |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
   2.120 -            ([induct], fold_thmss, rec_thmss, [], [], [], []))
   2.121 -          ||> (fn info => (SOME info, NONE))
   2.122 -        else
   2.123 -          derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
   2.124 -            dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
   2.125 -            ctr_defss ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy)
   2.126 -            lthy
   2.127 -          |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
   2.128 -                  (disc_unfold_thmss, disc_corec_thmss, _), _,
   2.129 -                  (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
   2.130 -            (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
   2.131 -             disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
   2.132 -          ||> (fn info => (NONE, SOME info));
   2.133 +          val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
   2.134  
   2.135 -      val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
   2.136 +          val ((co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
   2.137 +                sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
   2.138 +            if fp = Least_FP then
   2.139 +              derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
   2.140 +                xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
   2.141 +                co_iterss co_iter_defss lthy
   2.142 +              |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
   2.143 +                ([induct], fold_thmss, rec_thmss, [], [], [], []))
   2.144 +              ||> (fn info => (SOME info, NONE))
   2.145 +            else
   2.146 +              derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types)
   2.147 +                xtor_co_induct dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs
   2.148 +                ctrXs_Tsss kss mss ns ctr_defss ctr_sugars co_iterss co_iter_defss
   2.149 +                (Proof_Context.export lthy no_defs_lthy) lthy
   2.150 +              |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
   2.151 +                      (disc_unfold_thmss, disc_corec_thmss, _), _,
   2.152 +                      (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
   2.153 +                (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
   2.154 +                 disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
   2.155 +              ||> (fn info => (NONE, SOME info));
   2.156  
   2.157 -      fun mk_target_fp_sugar (kk, T) =
   2.158 -        {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
   2.159 -         nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
   2.160 -         ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
   2.161 -         co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
   2.162 -         disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
   2.163 -         sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
   2.164 -        |> morph_fp_sugar phi;
   2.165 -    in
   2.166 -      ((map_index mk_target_fp_sugar fpTs, fp_sugar_thms), lthy)
   2.167 +          val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
   2.168 +
   2.169 +          fun mk_target_fp_sugar (kk, T) =
   2.170 +            {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
   2.171 +             nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
   2.172 +             ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
   2.173 +             co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
   2.174 +             disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
   2.175 +             sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
   2.176 +            |> morph_fp_sugar phi;
   2.177 +
   2.178 +          val n2m_sugar = (map_index mk_target_fp_sugar fpTs, fp_sugar_thms);
   2.179 +        in
   2.180 +          (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
   2.181 +        end)
   2.182      end
   2.183    else
   2.184 -    (* TODO: reorder hypotheses and predicates in (co)induction rules? *)
   2.185      ((fp_sugars0, (NONE, NONE)), no_defs_lthy0);
   2.186  
   2.187  fun indexify_callsss fp_sugar callsss =
   2.188 @@ -299,7 +335,7 @@
   2.189      val Ts = actual_Ts @ missing_Ts;
   2.190  
   2.191      fun generalize_simple_type T (seen, lthy) =
   2.192 -      mk_TFrees 1 lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)));
   2.193 +      variant_tfrees ["aa"] lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)));
   2.194  
   2.195      fun generalize_type T (seen_lthy as (seen, _)) =
   2.196        (case AList.lookup (op =) seen T of
     3.1 --- a/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     3.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     3.3 @@ -200,11 +200,11 @@
     3.4      fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss =
     3.5        let
     3.6          val ctrs = #ctrs (nth ctr_sugars index);
     3.7 -        val rec_thmss = co_rec_of (nth iter_thmsss index);
     3.8 +        val rec_thms = co_rec_of (nth iter_thmsss index);
     3.9          val k = offset_of_ctr index ctr_sugars;
    3.10          val n = length ctrs;
    3.11        in
    3.12 -        map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thmss
    3.13 +        map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thms
    3.14        end;
    3.15  
    3.16      fun mk_spec ({T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...}
     4.1 --- a/src/HOL/BNF/Tools/ctr_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     4.2 +++ b/src/HOL/BNF/Tools/ctr_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
     4.3 @@ -33,6 +33,7 @@
     4.4       case_conv_ifs: thm list};
     4.5  
     4.6    val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
     4.7 +  val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar
     4.8    val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
     4.9    val ctr_sugars_of: Proof.context -> ctr_sugar list
    4.10