# HG changeset patch # User blanchet # Date 1347463565 -7200 # Node ID a2e6473145e43bfd8632ae4442f91d0fb15cf6e9 # Parent 096967bf394055c38b2b3f51f35524b692dd87c7 tuning diff -r 096967bf3940 -r a2e6473145e4 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 17:26:05 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 17:26:05 2012 +0200 @@ -83,7 +83,7 @@ if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types (); fun type_args_constrained_of (((cAs, _), _), _) = cAs; -fun type_binder_of (((_, b), _), _) = b; +fun type_binding_of (((_, b), _), _) = b; fun mixfix_of ((_, mx), _) = mx; fun ctr_specs_of (_, ctr_specs) = ctr_specs; @@ -123,14 +123,14 @@ locale and shadows an existing global type*) val fake_thy = Theory.copy #> fold (fn spec => perhaps (try (Sign.add_type no_defs_lthy - (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs; + (type_binding_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs; val fake_lthy = Proof_Context.background_theory fake_thy no_defs_lthy; fun mk_fake_T b = Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))), unsorted_As); - val fp_bs = map type_binder_of specs; + val fp_bs = map type_binding_of specs; val fake_Ts = map mk_fake_T fp_bs; val mixfixes = map mixfix_of specs; @@ -140,14 +140,14 @@ val ctr_specss = map ctr_specs_of specs; - val disc_binderss = map (map disc_of) ctr_specss; - val ctr_binderss = + val disc_bindingss = map (map disc_of) ctr_specss; + val ctr_bindingss = map2 (fn fp_b => map (Binding.qualify false (Binding.name_of fp_b) o ctr_of)) fp_bs ctr_specss; val ctr_argsss = map (map args_of) ctr_specss; val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss; - val sel_bindersss = map (map (map fst)) ctr_argsss; + val sel_bindingsss = map (map (map fst)) ctr_argsss; val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss; val raw_sel_defaultsss = map (map defaults_of) ctr_specss; @@ -218,8 +218,8 @@ fun mk_iter_like Ts Us t = let - val (binders, body) = strip_type (fastype_of t); - val (f_Us, prebody) = split_last binders; + val (bindings, body) = strip_type (fastype_of t); + val (f_Us, prebody) = split_last bindings; val Type (_, Ts0) = if lfp then prebody else body; val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us); in @@ -334,8 +334,8 @@ end; fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec), - fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_binders), ctr_mixfixes), ctr_Tss), - disc_binders), sel_binderss), raw_sel_defaultss) no_defs_lthy = + fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss), + disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = let val unfT = domain_type (fastype_of fld); val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss; @@ -353,7 +353,7 @@ map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $ mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss; - val case_binder = Binding.suffix_name ("_" ^ caseN) fp_b; + val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b; val case_rhs = fold_rev Term.lambda (fs @ [v]) @@ -362,7 +362,7 @@ val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs => Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd) - (case_binder :: ctr_binders) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss) + (case_binding :: ctr_bindings) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss) ||> `Local_Theory.restore; val phi = Proof_Context.export_morphism lthy lthy'; @@ -420,25 +420,23 @@ fun generate_iter_like (suf, fp_iter_like, (fss, f_Tss, xssss)) = let val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C; - - val binder = Binding.suffix_name ("_" ^ suf) fp_b; - + val binding = Binding.suffix_name ("_" ^ suf) fp_b; val spec = - mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binder, res_T)), + mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)), Term.list_comb (fp_iter_like, map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss)); - in (binder, spec) end; + in (binding, spec) end; val iter_like_infos = [(iterN, fp_iter, iter_only), (recN, fp_rec, rec_only)]; - val (binders, specs) = map generate_iter_like iter_like_infos |> split_list; + val (bindings, specs) = map generate_iter_like iter_like_infos |> split_list; val ((csts, defs), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map2 (fn b => fn spec => Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) - #>> apsnd snd) binders specs + #>> apsnd snd) bindings specs ||> `Local_Theory.restore; val phi = Proof_Context.export_morphism lthy lthy'; @@ -463,25 +461,23 @@ pf_Tss))) = let val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT; - - val binder = Binding.suffix_name ("_" ^ suf) fp_b; - + val binding = Binding.suffix_name ("_" ^ suf) fp_b; val spec = - mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)), + mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)), Term.list_comb (fp_iter_like, map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss)); - in (binder, spec) end; + in (binding, spec) end; val coiter_like_infos = [(coiterN, fp_iter, coiter_only), (corecN, fp_rec, corec_only)]; - val (binders, specs) = map generate_coiter_like coiter_like_infos |> split_list; + val (bindings, specs) = map generate_coiter_like coiter_like_infos |> split_list; val ((csts, defs), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map2 (fn b => fn spec => Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) - #>> apsnd snd) binders specs + #>> apsnd snd) bindings specs ||> `Local_Theory.restore; val phi = Proof_Context.export_morphism lthy lthy'; @@ -496,7 +492,7 @@ fun wrap lthy = let val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in - wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss, + wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss, sel_defaultss))) lthy end; @@ -685,8 +681,8 @@ val lthy' = lthy |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ - fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~ - ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss ~~ raw_sel_defaultsss) + fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~ + ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss) |>> split_list |> wrap_types_and_define_iter_likes |> (if lfp then derive_iter_rec_thms_for_types else derive_coiter_corec_thms_for_types); @@ -701,11 +697,11 @@ val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term; val parse_binding_colon = Parse.binding --| @{keyword ":"}; -val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binder; +val parse_opt_binding_colon = Scan.optional parse_binding_colon no_binding; val parse_ctr_arg = @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} || - (Parse.typ >> pair no_binder); + (Parse.typ >> pair no_binding); val parse_defaults = @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"}; diff -r 096967bf3940 -r a2e6473145e4 src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 12 17:26:05 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 12 17:26:05 2012 +0200 @@ -7,7 +7,7 @@ signature BNF_WRAP = sig - val no_binder: binding + val no_binding: binding val mk_half_pairss: 'a list -> ('a * 'a) list list val mk_ctr: typ list -> term -> term val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list -> @@ -45,8 +45,8 @@ val split_asmN = "split_asm"; val weak_case_cong_thmsN = "weak_case_cong"; -val no_binder = @{binding ""}; -val std_binder = @{binding _}; +val no_binding = @{binding ""}; +val std_binding = @{binding _}; val induct_simp_attrs = @{attributes [induct_simp]}; val cong_attrs = @{attributes [cong]}; @@ -80,7 +80,7 @@ | _ => error "Cannot extract name of constructor"); fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case), - (raw_disc_binders, (raw_sel_binderss, raw_sel_defaultss))) no_defs_lthy = + (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy = let (* TODO: sanity checks on arguments *) (* TODO: attributes (simp, case_names, etc.) *) @@ -111,47 +111,47 @@ val ms = map length ctr_Tss; - val raw_disc_binders' = pad_list no_binder n raw_disc_binders; + val raw_disc_bindings' = pad_list no_binding n raw_disc_bindings; fun can_really_rely_on_disc k = - not (Binding.eq_name (nth raw_disc_binders' (k - 1), no_binder)) orelse nth ms (k - 1) = 0; + not (Binding.eq_name (nth raw_disc_bindings' (k - 1), no_binding)) orelse nth ms (k - 1) = 0; fun can_rely_on_disc k = can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2)); - fun can_omit_disc_binder k m = + fun can_omit_disc_binding k m = n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k)); - val std_disc_binder = + val std_disc_binding = Binding.qualify false (Binding.name_of data_b) o Binding.name o prefix isN o base_name_of_ctr; - val disc_binders = - raw_disc_binders' + val disc_bindings = + raw_disc_bindings' |> map4 (fn k => fn m => fn ctr => fn disc => Option.map (Binding.qualify false (Binding.name_of data_b)) - (if Binding.eq_name (disc, no_binder) then - if can_omit_disc_binder k m then NONE else SOME (std_disc_binder ctr) - else if Binding.eq_name (disc, std_binder) then - SOME (std_disc_binder ctr) + (if Binding.eq_name (disc, no_binding) then + if can_omit_disc_binding k m then NONE else SOME (std_disc_binding ctr) + else if Binding.eq_name (disc, std_binding) then + SOME (std_disc_binding ctr) else SOME disc)) ks ms ctrs0; - val no_discs = map is_none disc_binders; + val no_discs = map is_none disc_bindings; val no_discs_at_all = forall I no_discs; - fun std_sel_binder m l = Binding.name o mk_unN m l o base_name_of_ctr; + fun std_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr; - val sel_binderss = - pad_list [] n raw_sel_binderss + val sel_bindingss = + pad_list [] n raw_sel_bindingss |> map3 (fn ctr => fn m => map2 (fn l => fn sel => Binding.qualify false (Binding.name_of data_b) - (if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, std_binder) then - std_sel_binder m l ctr + (if Binding.eq_name (sel, no_binding) orelse Binding.eq_name (sel, std_binding) then + std_sel_binding m l ctr else - sel)) (1 upto m) o pad_list no_binder m) ctrs0 ms; + sel)) (1 upto m) o pad_list no_binding m) ctrs0 ms; fun mk_case Ts T = let - val (binders, body) = strip_type (fastype_of case0) - val Type (_, Ts0) = List.last binders + val (bindings, body) = strip_type (fastype_of case0) + val Type (_, Ts0) = List.last bindings in Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) case0 end; val casex = mk_case As B; @@ -191,7 +191,7 @@ fun alternate_disc_lhs get_disc k = HOLogic.mk_not - (case nth disc_binders (k - 1) of + (case nth disc_bindings (k - 1) of NONE => nth exist_xs_v_eq_ctrs (k - 1) | SOME b => get_disc b (k - 1) $ v); @@ -237,22 +237,22 @@ Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ v) end; - val sel_binders = flat sel_binderss; - val uniq_sel_binders = distinct Binding.eq_name sel_binders; - val all_sels_distinct = (length uniq_sel_binders = length sel_binders); + val sel_bindings = flat sel_bindingss; + val uniq_sel_bindings = distinct Binding.eq_name sel_bindings; + val all_sels_distinct = (length uniq_sel_bindings = length sel_bindings); - val sel_binder_index = - if all_sels_distinct then 1 upto length sel_binders - else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_binders) sel_binders; + val sel_binding_index = + if all_sels_distinct then 1 upto length sel_bindings + else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) sel_bindings; val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss); val sel_infos = - AList.group (op =) (sel_binder_index ~~ proto_sels) + AList.group (op =) (sel_binding_index ~~ proto_sels) |> sort (int_ord o pairself fst) - |> map snd |> curry (op ~~) uniq_sel_binders; - val sel_binders = map fst sel_infos; + |> map snd |> curry (op ~~) uniq_sel_bindings; + val sel_bindings = map fst sel_infos; - fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss; + fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss; val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = no_defs_lthy @@ -263,7 +263,7 @@ else pair (alternate_disc k, alternate_disc_no_def) | SOME b => Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd) - ks ms exist_xs_v_eq_ctrs disc_binders + ks ms exist_xs_v_eq_ctrs disc_bindings ||>> apfst split_list o fold_map (fn (b, proto_sels) => Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos