# HG changeset patch # User blanchet # Date 1367330690 -7200 # Node ID b304fb6c5ef5ccb6323208baf0773d6f6cc9926f # Parent 5c552de1d8d1c4ac674bb403ab4a6a5a60562313 renamed records diff -r 5c552de1d8d1 -r b304fb6c5ef5 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Apr 30 15:58:32 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Apr 30 16:04:50 2013 +0200 @@ -7,7 +7,7 @@ signature BNF_CTR_SUGAR = sig - type ctr_wrap_result = + type ctr_sugar = {ctrs: term list, discs: term list, selss: term list list, @@ -19,7 +19,7 @@ discIs: thm list, sel_thmss: thm list list}; - val morph_ctr_wrap_result: morphism -> ctr_wrap_result -> ctr_wrap_result + val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar val rep_compat_prefix: string @@ -35,7 +35,7 @@ val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list -> (((bool * bool) * term list) * term) * (binding list * (binding list list * (binding * term) list list)) -> local_theory -> - ctr_wrap_result * local_theory + ctr_sugar * local_theory val parse_wrap_options: (bool * bool) parser val parse_bound_term: (binding * string) parser end; @@ -46,7 +46,7 @@ open BNF_Util open BNF_Ctr_Sugar_Tactics -type ctr_wrap_result = +type ctr_sugar = {ctrs: term list, discs: term list, selss: term list list, @@ -58,8 +58,8 @@ discIs: thm list, sel_thmss: thm list list}; -fun morph_ctr_wrap_result phi {ctrs, discs, selss, exhaust, injects, distincts, case_thms, - disc_thmss, discIs, sel_thmss} = +fun morph_ctr_sugar phi {ctrs, discs, selss, exhaust, injects, distincts, case_thms, disc_thmss, + discIs, sel_thmss} = {ctrs = map (Morphism.term phi) ctrs, discs = map (Morphism.term phi) discs, selss = map (map (Morphism.term phi)) selss, diff -r 5c552de1d8d1 -r b304fb6c5ef5 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Apr 30 15:58:32 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Apr 30 16:04:50 2013 +0200 @@ -7,14 +7,14 @@ signature BNF_FP_DEF_SUGAR = sig - type fp = + type fp_sugar = {lfp: bool, index: int, pre_bnfs: BNF_Def.bnf list, fp_res: BNF_FP.fp_result, - ctr_wrap_res: BNF_Ctr_Sugar.ctr_wrap_result}; + ctr_sugar: BNF_Ctr_Sugar.ctr_sugar}; - val fp_of: Proof.context -> string -> fp option + val fp_sugar_of: Proof.context -> string -> fp_sugar option val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> @@ -25,7 +25,7 @@ val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> int list list -> int list list -> int list -> - thm list list -> BNF_Ctr_Sugar.ctr_wrap_result list -> term list -> term list -> thm list -> + thm list list -> BNF_Ctr_Sugar.ctr_sugar list -> term list -> term list -> thm list -> thm list -> Proof.context -> (thm * thm list * thm * thm list * Args.src list) * (thm list list * thm list list * Args.src list) @@ -59,40 +59,40 @@ val EqN = "Eq_"; -type fp = +type fp_sugar = {lfp: bool, index: int, pre_bnfs: bnf list, fp_res: fp_result, - ctr_wrap_res: ctr_wrap_result}; + ctr_sugar: ctr_sugar}; -fun eq_fp ({lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp, - {lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp) = +fun eq_fp_sugar ({lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, + {lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); -fun morph_fp phi {lfp, index, pre_bnfs, fp_res, ctr_wrap_res} = +fun morph_fp_sugar phi {lfp, index, pre_bnfs, fp_res, ctr_sugar} = {lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, - fp_res = morph_fp_result phi fp_res, ctr_wrap_res = morph_ctr_wrap_result phi ctr_wrap_res}; + fp_res = morph_fp_result phi fp_res, ctr_sugar = morph_ctr_sugar phi ctr_sugar}; structure Data = Generic_Data ( - type T = fp Symtab.table; + type T = fp_sugar Symtab.table; val empty = Symtab.empty; val extend = I; - val merge = Symtab.merge eq_fp; + val merge = Symtab.merge eq_fp_sugar; ); -val fp_of = Symtab.lookup o Data.get o Context.Proof; +val fp_sugar_of = Symtab.lookup o Data.get o Context.Proof; -fun register_fp key fp = +fun register_fp_sugar key fp_sugar = Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => Data.map (Symtab.update_new (key, morph_fp phi fp))); + (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); -fun register_fps lfp pre_bnfs (fp_res as {ctors, ...}) ctr_wrap_ress lthy = +fun register_fp_sugars lfp pre_bnfs (fp_res as {ctors, ...}) ctr_sugars lthy = ((1, ctors), lthy) - |> fold (fn ctr_wrap_res => fn ((kk, ctor :: ctors), lthy) => - ((kk + 1, ctors), register_fp (fp_name_of_ctor ctor) {lfp = lfp, index = kk, - pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_wrap_res = ctr_wrap_res} lthy)) ctr_wrap_ress + |> fold (fn ctr_sugar => fn ((kk, ctor :: ctors), lthy) => + ((kk + 1, ctors), register_fp_sugar (fp_name_of_ctor ctor) {lfp = lfp, index = kk, + pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugar = ctr_sugar} lthy)) ctr_sugars |> snd; (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) @@ -525,7 +525,7 @@ fun derive_coinduct_unfold_corec_thms_for_types pre_bnfs dtor_unfolds0 dtor_corecs0 dtor_coinduct dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs - As kss mss ns ctr_defss ctr_wrap_ress unfolds corecs unfold_defs corec_defs lthy = + As kss mss ns ctr_defss ctr_sugars unfolds corecs unfold_defs corec_defs lthy = let val nn = length pre_bnfs; @@ -542,13 +542,13 @@ val (_, dtor_unfold_fun_Ts) = mk_fp_rec_like false As Cs dtor_unfolds0; val (_, dtor_corec_fun_Ts) = mk_fp_rec_like false As Cs dtor_corecs0; - val ctrss = map (map (mk_ctr As) o #ctrs) ctr_wrap_ress; - val discss = map (map (mk_disc_or_sel As) o #discs) ctr_wrap_ress; - val selsss = map (map (map (mk_disc_or_sel As)) o #selss) ctr_wrap_ress; - val exhausts = map #exhaust ctr_wrap_ress; - val disc_thmsss = map #disc_thmss ctr_wrap_ress; - val discIss = map #discIs ctr_wrap_ress; - val sel_thmsss = map #sel_thmss ctr_wrap_ress; + val ctrss = map (map (mk_ctr As) o #ctrs) ctr_sugars; + val discss = map (map (mk_disc_or_sel As) o #discs) ctr_sugars; + val selsss = map (map (map (mk_disc_or_sel As)) o #selss) ctr_sugars; + val exhausts = map #exhaust ctr_sugars; + val disc_thmsss = map #disc_thmss ctr_sugars; + val discIss = map #discIs ctr_sugars; + val sel_thmsss = map #sel_thmss ctr_sugars; val ((cs, cpss, ((pgss, crssss, cgssss), _), ((phss, csssss, chssss), _)), names_lthy0) = mk_unfold_corec_terms_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy; @@ -1068,9 +1068,9 @@ (sel_bindingss, sel_defaultss))) lthy end; - fun derive_maps_sets_rels (ctr_wrap_res, lthy) = + fun derive_maps_sets_rels (ctr_sugar, lthy) = if live = 0 then - ((([], [], [], []), ctr_wrap_res), lthy) + ((([], [], [], []), ctr_sugar), lthy) else let val rel_flip = rel_flip_of_bnf fp_bnf; @@ -1148,7 +1148,7 @@ (setsN, flat set_thmss, code_simp_attrs)] |> massage_simple_notes fp_b_name; in - (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_wrap_res), + (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar), lthy |> Local_Theory.notes notes |> snd) end; @@ -1270,8 +1270,8 @@ ((unfold, corec, unfold_def, corec_def), lthy') end; - fun massage_res (((maps_sets_rels, ctr_wrap_res), rec_like_res), lthy) = - (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_wrap_res)), rec_like_res), lthy); + fun massage_res (((maps_sets_rels, ctr_sugar), rec_like_res), lthy) = + (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), rec_like_res), lthy); in (wrap #> derive_maps_sets_rels @@ -1291,7 +1291,7 @@ @ rel_distincts @ flat setss); fun derive_and_note_induct_fold_rec_thms_for_types - ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_wrap_ress)), + ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)), (folds, recs, fold_defs, rec_defs)), lthy) = let val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs), @@ -1303,7 +1303,7 @@ val induct_type_attr = Attrib.internal o K o Induct.induct_type; val simp_thmss = - mk_simp_thmss ctr_wrap_ress rec_thmss fold_thmss mapsx rel_injects rel_distincts setss; + mk_simp_thmss ctr_sugars rec_thmss fold_thmss mapsx rel_injects rel_distincts setss; val common_notes = (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) @@ -1318,11 +1318,11 @@ in lthy |> Local_Theory.notes (common_notes @ notes) |> snd - |> register_fps true pre_bnfs fp_res ctr_wrap_ress + |> register_fp_sugars true pre_bnfs fp_res ctr_sugars end; fun derive_and_note_coinduct_unfold_corec_thms_for_types - ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_wrap_ress)), + ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)), (unfolds, corecs, unfold_defs, corec_defs)), lthy) = let val ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms, @@ -1334,7 +1334,7 @@ (sel_unfold_thmss, sel_corec_thmss, sel_corec_like_attrs)) = derive_coinduct_unfold_corec_thms_for_types pre_bnfs fp_folds0 fp_recs0 fp_induct fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As - kss mss ns ctr_defss ctr_wrap_ress unfolds corecs unfold_defs corec_defs lthy; + kss mss ns ctr_defss ctr_sugars unfolds corecs unfold_defs corec_defs lthy; val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; @@ -1342,7 +1342,7 @@ corec_likes @ disc_corec_likes @ sel_corec_likes; val simp_thmss = - mk_simp_thmss ctr_wrap_ress + mk_simp_thmss ctr_sugars (map3 flat_corec_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss) (map3 flat_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss) mapsx rel_injects rel_distincts setss; @@ -1376,7 +1376,7 @@ in lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd - |> register_fps false pre_bnfs fp_res ctr_wrap_ress + |> register_fp_sugars false pre_bnfs fp_res ctr_sugars end; val lthy' = lthy