# HG changeset patch # User blanchet # Date 1347404111 -7200 # Node ID f5bd87aac2241c2ed27a617cf14fc715aeeeadab # Parent 3577c7a2b30695b6093c002f1e309033ec982684 added optional qualifiers for constructors and destructors, similarly to the old package diff -r 3577c7a2b306 -r f5bd87aac224 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 00:20:37 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 00:55:11 2012 +0200 @@ -127,18 +127,20 @@ Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))), unsorted_As); - val bs = map type_binder_of specs; - val fake_Ts = map mk_fake_T bs; + val fp_bs = map type_binder_of specs; + val fake_Ts = map mk_fake_T fp_bs; val mixfixes = map mixfix_of specs; - val _ = (case duplicates Binding.eq_name bs of [] => () + val _ = (case duplicates Binding.eq_name fp_bs of [] => () | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b))); val ctr_specss = map ctr_specs_of specs; val disc_binderss = map (map disc_of) ctr_specss; - val ctr_binderss = map (map ctr_of) ctr_specss; + val ctr_binderss = + 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; @@ -176,7 +178,7 @@ val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects, fp_iter_thms, fp_rec_thms), lthy)) = - fp_bnf (if lfp then bnf_lfp else bnf_gfp) bs mixfixes (map dest_TFree unsorted_As) fp_eqs + fp_bnf (if lfp then bnf_lfp else bnf_gfp) fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0; val add_nested_bnf_names = @@ -329,7 +331,7 @@ (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))) end; - fun define_ctrs_case_for_type ((((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec), + 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 = let @@ -349,7 +351,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) b; + val case_binder = Binding.suffix_name ("_" ^ caseN) fp_b; val case_rhs = fold_rev Term.lambda (fs @ [v]) @@ -357,8 +359,8 @@ 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) + Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd) + (case_binder :: ctr_binders) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss) ||> `Local_Theory.restore; (*transforms defined frees into consts (and more)*) @@ -418,7 +420,7 @@ let val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C; - val binder = Binding.suffix_name ("_" ^ suf) b; + val binder = Binding.suffix_name ("_" ^ suf) fp_b; val spec = mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binder, res_T)), @@ -432,8 +434,6 @@ val (binders, specs) = map generate_iter_like iter_like_infos |> split_list; - (* TODO: Allow same constructor (and selector/discriminator) names for different - types (cf. old "datatype" package) *) 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)) @@ -464,7 +464,7 @@ let val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT; - val binder = Binding.suffix_name ("_" ^ suf) b; + val binder = Binding.suffix_name ("_" ^ suf) fp_b; val spec = mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)), @@ -578,7 +578,7 @@ |> maps (fn (thmN, thmss, attrs) => map2 (fn b => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), - [(thms, [])])) bs thmss); + [(thms, [])])) fp_bs thmss); in lthy |> Local_Theory.notes notes |> snd end; @@ -676,7 +676,7 @@ |> maps (fn (thmN, thmss, attrs) => map_filter (fn (_, []) => NONE | (b, thms) => SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), - [(thms, [])])) (bs ~~ thmss)); + [(thms, [])])) (fp_bs ~~ thmss)); in lthy |> Local_Theory.notes notes |> snd end; @@ -685,7 +685,7 @@ fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list11 val lthy' = lthy - |> fold_map define_ctrs_case_for_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ + |> 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) |>> split_list |> wrap_types_and_define_iter_likes diff -r 3577c7a2b306 -r f5bd87aac224 src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 12 00:20:37 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 12 00:55:11 2012 +0200 @@ -98,7 +98,7 @@ pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss); val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0)); - val b = Binding.qualified_name dataT_name; + val data_b = Binding.qualified_name dataT_name; val (As, B) = no_defs_lthy @@ -120,17 +120,19 @@ fun can_omit_disc_binder k m = n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k)); - val std_disc_binder = Binding.name o prefix isN o base_name_of_ctr; + val std_disc_binder = + 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' |> map4 (fn k => fn m => fn ctr => fn disc => - 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) - else - SOME disc) ks ms ctrs0; + 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) + else + SOME disc)) ks ms ctrs0; val no_discs = map is_none disc_binders; val no_discs_at_all = forall I no_discs; @@ -140,10 +142,11 @@ val sel_binderss = pad_list [] n raw_sel_binderss |> map3 (fn ctr => fn m => map2 (fn l => fn sel => - if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, std_binder) then - std_sel_binder m l ctr - else - sel) (1 upto m) o pad_list no_binder m) ctrs0 ms; + 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 + else + sel)) (1 upto m) o pad_list no_binder m) ctrs0 ms; fun mk_case Ts T = let @@ -571,7 +574,8 @@ (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] |> filter_out (null o #2) |> map (fn (thmN, thms, attrs) => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), [(thms, [])])); + ((Binding.qualify true (Binding.name_of data_b) (Binding.name thmN), attrs), + [(thms, [])])); val notes' = [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]