1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 00:20:37 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 00:55:11 2012 +0200
1.3 @@ -127,18 +127,20 @@
1.4 Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
1.5 unsorted_As);
1.6
1.7 - val bs = map type_binder_of specs;
1.8 - val fake_Ts = map mk_fake_T bs;
1.9 + val fp_bs = map type_binder_of specs;
1.10 + val fake_Ts = map mk_fake_T fp_bs;
1.11
1.12 val mixfixes = map mixfix_of specs;
1.13
1.14 - val _ = (case duplicates Binding.eq_name bs of [] => ()
1.15 + val _ = (case duplicates Binding.eq_name fp_bs of [] => ()
1.16 | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b)));
1.17
1.18 val ctr_specss = map ctr_specs_of specs;
1.19
1.20 val disc_binderss = map (map disc_of) ctr_specss;
1.21 - val ctr_binderss = map (map ctr_of) ctr_specss;
1.22 + val ctr_binderss =
1.23 + map2 (fn fp_b => map (Binding.qualify false (Binding.name_of fp_b) o ctr_of))
1.24 + fp_bs ctr_specss;
1.25 val ctr_argsss = map (map args_of) ctr_specss;
1.26 val ctr_mixfixess = map (map ctr_mixfix_of) ctr_specss;
1.27
1.28 @@ -176,7 +178,7 @@
1.29
1.30 val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects,
1.31 fp_iter_thms, fp_rec_thms), lthy)) =
1.32 - fp_bnf (if lfp then bnf_lfp else bnf_gfp) bs mixfixes (map dest_TFree unsorted_As) fp_eqs
1.33 + fp_bnf (if lfp then bnf_lfp else bnf_gfp) fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs
1.34 no_defs_lthy0;
1.35
1.36 val add_nested_bnf_names =
1.37 @@ -329,7 +331,7 @@
1.38 (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss))))
1.39 end;
1.40
1.41 - fun define_ctrs_case_for_type ((((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec),
1.42 + fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec),
1.43 fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_binders), ctr_mixfixes), ctr_Tss),
1.44 disc_binders), sel_binderss), raw_sel_defaultss) no_defs_lthy =
1.45 let
1.46 @@ -349,7 +351,7 @@
1.47 map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $
1.48 mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss;
1.49
1.50 - val case_binder = Binding.suffix_name ("_" ^ caseN) b;
1.51 + val case_binder = Binding.suffix_name ("_" ^ caseN) fp_b;
1.52
1.53 val case_rhs =
1.54 fold_rev Term.lambda (fs @ [v])
1.55 @@ -357,8 +359,8 @@
1.56
1.57 val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
1.58 |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
1.59 - Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
1.60 - (case_binder :: ctr_binders) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
1.61 + Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd)
1.62 + (case_binder :: ctr_binders) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss)
1.63 ||> `Local_Theory.restore;
1.64
1.65 (*transforms defined frees into consts (and more)*)
1.66 @@ -418,7 +420,7 @@
1.67 let
1.68 val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
1.69
1.70 - val binder = Binding.suffix_name ("_" ^ suf) b;
1.71 + val binder = Binding.suffix_name ("_" ^ suf) fp_b;
1.72
1.73 val spec =
1.74 mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binder, res_T)),
1.75 @@ -432,8 +434,6 @@
1.76
1.77 val (binders, specs) = map generate_iter_like iter_like_infos |> split_list;
1.78
1.79 - (* TODO: Allow same constructor (and selector/discriminator) names for different
1.80 - types (cf. old "datatype" package) *)
1.81 val ((csts, defs), (lthy', lthy)) = no_defs_lthy
1.82 |> apfst split_list o fold_map2 (fn b => fn spec =>
1.83 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
1.84 @@ -464,7 +464,7 @@
1.85 let
1.86 val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
1.87
1.88 - val binder = Binding.suffix_name ("_" ^ suf) b;
1.89 + val binder = Binding.suffix_name ("_" ^ suf) fp_b;
1.90
1.91 val spec =
1.92 mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
1.93 @@ -578,7 +578,7 @@
1.94 |> maps (fn (thmN, thmss, attrs) =>
1.95 map2 (fn b => fn thms =>
1.96 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
1.97 - [(thms, [])])) bs thmss);
1.98 + [(thms, [])])) fp_bs thmss);
1.99 in
1.100 lthy |> Local_Theory.notes notes |> snd
1.101 end;
1.102 @@ -676,7 +676,7 @@
1.103 |> maps (fn (thmN, thmss, attrs) =>
1.104 map_filter (fn (_, []) => NONE | (b, thms) =>
1.105 SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
1.106 - [(thms, [])])) (bs ~~ thmss));
1.107 + [(thms, [])])) (fp_bs ~~ thmss));
1.108 in
1.109 lthy |> Local_Theory.notes notes |> snd
1.110 end;
1.111 @@ -685,7 +685,7 @@
1.112 fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list11
1.113
1.114 val lthy' = lthy
1.115 - |> fold_map define_ctrs_case_for_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
1.116 + |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
1.117 fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~
1.118 ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss ~~ raw_sel_defaultsss)
1.119 |>> split_list |> wrap_types_and_define_iter_likes