tuning
authorblanchet
Wed Sep 12 17:26:05 2012 +0200 (2012-09-12)
changeset 49336a2e6473145e4
parent 49335 096967bf3940
child 49337 538687a77075
tuning
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_wrap.ML
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 17:26:05 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 12 17:26:05 2012 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4    if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types ();
     1.5  
     1.6  fun type_args_constrained_of (((cAs, _), _), _) = cAs;
     1.7 -fun type_binder_of (((_, b), _), _) = b;
     1.8 +fun type_binding_of (((_, b), _), _) = b;
     1.9  fun mixfix_of ((_, mx), _) = mx;
    1.10  fun ctr_specs_of (_, ctr_specs) = ctr_specs;
    1.11  
    1.12 @@ -123,14 +123,14 @@
    1.13        locale and shadows an existing global type*)
    1.14      val fake_thy =
    1.15        Theory.copy #> fold (fn spec => perhaps (try (Sign.add_type no_defs_lthy
    1.16 -        (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
    1.17 +        (type_binding_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
    1.18      val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy;
    1.19  
    1.20      fun mk_fake_T b =
    1.21        Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
    1.22          unsorted_As);
    1.23  
    1.24 -    val fp_bs = map type_binder_of specs;
    1.25 +    val fp_bs = map type_binding_of specs;
    1.26      val fake_Ts = map mk_fake_T fp_bs;
    1.27  
    1.28      val mixfixes = map mixfix_of specs;
    1.29 @@ -140,14 +140,14 @@
    1.30  
    1.31      val ctr_specss = map ctr_specs_of specs;
    1.32  
    1.33 -    val disc_binderss = map (map disc_of) ctr_specss;
    1.34 -    val ctr_binderss =
    1.35 +    val disc_bindingss = map (map disc_of) ctr_specss;
    1.36 +    val ctr_bindingss =
    1.37        map2 (fn fp_b => map (Binding.qualify false (Binding.name_of fp_b) o ctr_of))
    1.38          fp_bs ctr_specss;
    1.39      val ctr_argsss = map (map args_of) ctr_specss;
    1.40      val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
    1.41  
    1.42 -    val sel_bindersss = map (map (map fst)) ctr_argsss;
    1.43 +    val sel_bindingsss = map (map (map fst)) ctr_argsss;
    1.44      val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
    1.45      val raw_sel_defaultsss = map (map defaults_of) ctr_specss;
    1.46  
    1.47 @@ -218,8 +218,8 @@
    1.48  
    1.49      fun mk_iter_like Ts Us t =
    1.50        let
    1.51 -        val (binders, body) = strip_type (fastype_of t);
    1.52 -        val (f_Us, prebody) = split_last binders;
    1.53 +        val (bindings, body) = strip_type (fastype_of t);
    1.54 +        val (f_Us, prebody) = split_last bindings;
    1.55          val Type (_, Ts0) = if lfp then prebody else body;
    1.56          val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us);
    1.57        in
    1.58 @@ -334,8 +334,8 @@
    1.59          end;
    1.60  
    1.61      fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec),
    1.62 -          fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_binders), ctr_mixfixes), ctr_Tss),
    1.63 -        disc_binders), sel_binderss), raw_sel_defaultss) no_defs_lthy =
    1.64 +          fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
    1.65 +        disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
    1.66        let
    1.67          val unfT = domain_type (fastype_of fld);
    1.68          val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
    1.69 @@ -353,7 +353,7 @@
    1.70            map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $
    1.71              mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss;
    1.72  
    1.73 -        val case_binder = Binding.suffix_name ("_" ^ caseN) fp_b;
    1.74 +        val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b;
    1.75  
    1.76          val case_rhs =
    1.77            fold_rev Term.lambda (fs @ [v])
    1.78 @@ -362,7 +362,7 @@
    1.79          val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
    1.80            |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
    1.81                Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
    1.82 -            (case_binder :: ctr_binders) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
    1.83 +            (case_binding :: ctr_bindings) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
    1.84            ||> `Local_Theory.restore;
    1.85  
    1.86          val phi = Proof_Context.export_morphism lthy lthy';
    1.87 @@ -420,25 +420,23 @@
    1.88              fun generate_iter_like (suf, fp_iter_like, (fss, f_Tss, xssss)) =
    1.89                let
    1.90                  val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
    1.91 -
    1.92 -                val binder = Binding.suffix_name ("_" ^ suf) fp_b;
    1.93 -
    1.94 +                val binding = Binding.suffix_name ("_" ^ suf) fp_b;
    1.95                  val spec =
    1.96 -                  mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binder, res_T)),
    1.97 +                  mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
    1.98                      Term.list_comb (fp_iter_like,
    1.99                        map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss));
   1.100 -              in (binder, spec) end;
   1.101 +              in (binding, spec) end;
   1.102  
   1.103              val iter_like_infos =
   1.104                [(iterN, fp_iter, iter_only),
   1.105                 (recN, fp_rec, rec_only)];
   1.106  
   1.107 -            val (binders, specs) = map generate_iter_like iter_like_infos |> split_list;
   1.108 +            val (bindings, specs) = map generate_iter_like iter_like_infos |> split_list;
   1.109  
   1.110              val ((csts, defs), (lthy', lthy)) = no_defs_lthy
   1.111                |> apfst split_list o fold_map2 (fn b => fn spec =>
   1.112                  Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
   1.113 -                #>> apsnd snd) binders specs
   1.114 +                #>> apsnd snd) bindings specs
   1.115                ||> `Local_Theory.restore;
   1.116  
   1.117              val phi = Proof_Context.export_morphism lthy lthy';
   1.118 @@ -463,25 +461,23 @@
   1.119                  pf_Tss))) =
   1.120                let
   1.121                  val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
   1.122 -
   1.123 -                val binder = Binding.suffix_name ("_" ^ suf) fp_b;
   1.124 -
   1.125 +                val binding = Binding.suffix_name ("_" ^ suf) fp_b;
   1.126                  val spec =
   1.127 -                  mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
   1.128 +                  mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),
   1.129                      Term.list_comb (fp_iter_like,
   1.130                        map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss));
   1.131 -              in (binder, spec) end;
   1.132 +              in (binding, spec) end;
   1.133  
   1.134              val coiter_like_infos =
   1.135                [(coiterN, fp_iter, coiter_only),
   1.136                 (corecN, fp_rec, corec_only)];
   1.137  
   1.138 -            val (binders, specs) = map generate_coiter_like coiter_like_infos |> split_list;
   1.139 +            val (bindings, specs) = map generate_coiter_like coiter_like_infos |> split_list;
   1.140  
   1.141              val ((csts, defs), (lthy', lthy)) = no_defs_lthy
   1.142                |> apfst split_list o fold_map2 (fn b => fn spec =>
   1.143                  Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
   1.144 -                #>> apsnd snd) binders specs
   1.145 +                #>> apsnd snd) bindings specs
   1.146                ||> `Local_Theory.restore;
   1.147  
   1.148              val phi = Proof_Context.export_morphism lthy lthy';
   1.149 @@ -496,7 +492,7 @@
   1.150  
   1.151          fun wrap lthy =
   1.152            let val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in
   1.153 -            wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss,
   1.154 +            wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,
   1.155                sel_defaultss))) lthy
   1.156            end;
   1.157  
   1.158 @@ -685,8 +681,8 @@
   1.159  
   1.160      val lthy' = lthy
   1.161        |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
   1.162 -        fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~
   1.163 -        ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss ~~ raw_sel_defaultsss)
   1.164 +        fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
   1.165 +        ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
   1.166        |>> split_list |> wrap_types_and_define_iter_likes
   1.167        |> (if lfp then derive_iter_rec_thms_for_types else derive_coiter_corec_thms_for_types);
   1.168  
   1.169 @@ -701,11 +697,11 @@
   1.170  val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
   1.171  
   1.172  val parse_binding_colon = Parse.binding --| @{keyword ":"};
   1.173 -val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binder;
   1.174 +val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binding;
   1.175  
   1.176  val parse_ctr_arg =
   1.177    @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
   1.178 -  (Parse.typ >> pair no_binder);
   1.179 +  (Parse.typ >> pair no_binding);
   1.180  
   1.181  val parse_defaults =
   1.182    @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 12 17:26:05 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 12 17:26:05 2012 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  signature BNF_WRAP =
     2.6  sig
     2.7 -  val no_binder: binding
     2.8 +  val no_binding: binding
     2.9    val mk_half_pairss: 'a list -> ('a * 'a) list list
    2.10    val mk_ctr: typ list -> term -> term
    2.11    val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
    2.12 @@ -45,8 +45,8 @@
    2.13  val split_asmN = "split_asm";
    2.14  val weak_case_cong_thmsN = "weak_case_cong";
    2.15  
    2.16 -val no_binder = @{binding ""};
    2.17 -val std_binder = @{binding _};
    2.18 +val no_binding = @{binding ""};
    2.19 +val std_binding = @{binding _};
    2.20  
    2.21  val induct_simp_attrs = @{attributes [induct_simp]};
    2.22  val cong_attrs = @{attributes [cong]};
    2.23 @@ -80,7 +80,7 @@
    2.24      | _ => error "Cannot extract name of constructor");
    2.25  
    2.26  fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
    2.27 -    (raw_disc_binders, (raw_sel_binderss, raw_sel_defaultss))) no_defs_lthy =
    2.28 +    (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
    2.29    let
    2.30      (* TODO: sanity checks on arguments *)
    2.31      (* TODO: attributes (simp, case_names, etc.) *)
    2.32 @@ -111,47 +111,47 @@
    2.33  
    2.34      val ms = map length ctr_Tss;
    2.35  
    2.36 -    val raw_disc_binders' = pad_list no_binder n raw_disc_binders;
    2.37 +    val raw_disc_bindings' = pad_list no_binding n raw_disc_bindings;
    2.38  
    2.39      fun can_really_rely_on_disc k =
    2.40 -      not (Binding.eq_name (nth raw_disc_binders' (k - 1), no_binder)) orelse nth ms (k - 1) = 0;
    2.41 +      not (Binding.eq_name (nth raw_disc_bindings' (k - 1), no_binding)) orelse nth ms (k - 1) = 0;
    2.42      fun can_rely_on_disc k =
    2.43        can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
    2.44 -    fun can_omit_disc_binder k m =
    2.45 +    fun can_omit_disc_binding k m =
    2.46        n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k));
    2.47  
    2.48 -    val std_disc_binder =
    2.49 +    val std_disc_binding =
    2.50        Binding.qualify false (Binding.name_of data_b) o Binding.name o prefix isN o base_name_of_ctr;
    2.51  
    2.52 -    val disc_binders =
    2.53 -      raw_disc_binders'
    2.54 +    val disc_bindings =
    2.55 +      raw_disc_bindings'
    2.56        |> map4 (fn k => fn m => fn ctr => fn disc =>
    2.57          Option.map (Binding.qualify false (Binding.name_of data_b))
    2.58 -          (if Binding.eq_name (disc, no_binder) then
    2.59 -             if can_omit_disc_binder k m then NONE else SOME (std_disc_binder ctr)
    2.60 -           else if Binding.eq_name (disc, std_binder) then
    2.61 -             SOME (std_disc_binder ctr)
    2.62 +          (if Binding.eq_name (disc, no_binding) then
    2.63 +             if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr)
    2.64 +           else if Binding.eq_name (disc, std_binding) then
    2.65 +             SOME (std_disc_binding ctr)
    2.66             else
    2.67               SOME disc)) ks ms ctrs0;
    2.68  
    2.69 -    val no_discs = map is_none disc_binders;
    2.70 +    val no_discs = map is_none disc_bindings;
    2.71      val no_discs_at_all = forall I no_discs;
    2.72  
    2.73 -    fun std_sel_binder m l = Binding.name o mk_unN m l o base_name_of_ctr;
    2.74 +    fun std_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
    2.75  
    2.76 -    val sel_binderss =
    2.77 -      pad_list [] n raw_sel_binderss
    2.78 +    val sel_bindingss =
    2.79 +      pad_list [] n raw_sel_bindingss
    2.80        |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
    2.81          Binding.qualify false (Binding.name_of data_b)
    2.82 -          (if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, std_binder) then
    2.83 -            std_sel_binder m l ctr
    2.84 +          (if Binding.eq_name (sel, no_binding) orelse Binding.eq_name (sel, std_binding) then
    2.85 +            std_sel_binding m l ctr
    2.86            else
    2.87 -            sel)) (1 upto m) o pad_list no_binder m) ctrs0 ms;
    2.88 +            sel)) (1 upto m) o pad_list no_binding m) ctrs0 ms;
    2.89  
    2.90      fun mk_case Ts T =
    2.91        let
    2.92 -        val (binders, body) = strip_type (fastype_of case0)
    2.93 -        val Type (_, Ts0) = List.last binders
    2.94 +        val (bindings, body) = strip_type (fastype_of case0)
    2.95 +        val Type (_, Ts0) = List.last bindings
    2.96        in Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) case0 end;
    2.97  
    2.98      val casex = mk_case As B;
    2.99 @@ -191,7 +191,7 @@
   2.100  
   2.101      fun alternate_disc_lhs get_disc k =
   2.102        HOLogic.mk_not
   2.103 -        (case nth disc_binders (k - 1) of
   2.104 +        (case nth disc_bindings (k - 1) of
   2.105            NONE => nth exist_xs_v_eq_ctrs (k - 1)
   2.106          | SOME b => get_disc b (k - 1) $ v);
   2.107  
   2.108 @@ -237,22 +237,22 @@
   2.109                  Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ v)
   2.110              end;
   2.111  
   2.112 -          val sel_binders = flat sel_binderss;
   2.113 -          val uniq_sel_binders = distinct Binding.eq_name sel_binders;
   2.114 -          val all_sels_distinct = (length uniq_sel_binders = length sel_binders);
   2.115 +          val sel_bindings = flat sel_bindingss;
   2.116 +          val uniq_sel_bindings = distinct Binding.eq_name sel_bindings;
   2.117 +          val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings);
   2.118  
   2.119 -          val sel_binder_index =
   2.120 -            if all_sels_distinct then 1 upto length sel_binders
   2.121 -            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_binders) sel_binders;
   2.122 +          val sel_binding_index =
   2.123 +            if all_sels_distinct then 1 upto length sel_bindings
   2.124 +            else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings;
   2.125  
   2.126            val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
   2.127            val sel_infos =
   2.128 -            AList.group (op =) (sel_binder_index ~~ proto_sels)
   2.129 +            AList.group (op =) (sel_binding_index ~~ proto_sels)
   2.130              |> sort (int_ord o pairself fst)
   2.131 -            |> map snd |> curry (op ~~) uniq_sel_binders;
   2.132 -          val sel_binders = map fst sel_infos;
   2.133 +            |> map snd |> curry (op ~~) uniq_sel_bindings;
   2.134 +          val sel_bindings = map fst sel_infos;
   2.135  
   2.136 -          fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss;
   2.137 +          fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss;
   2.138  
   2.139            val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
   2.140              no_defs_lthy
   2.141 @@ -263,7 +263,7 @@
   2.142                   else pair (alternate_disc k, alternate_disc_no_def)
   2.143                 | SOME b => Specification.definition (SOME (b, NONE, NoSyn),
   2.144                     ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd)
   2.145 -              ks ms exist_xs_v_eq_ctrs disc_binders
   2.146 +              ks ms exist_xs_v_eq_ctrs disc_bindings
   2.147              ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
   2.148                Specification.definition (SOME (b, NONE, NoSyn),
   2.149                  ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos