10 type fp_sugar = |
10 type fp_sugar = |
11 {lfp: bool, |
11 {lfp: bool, |
12 index: int, |
12 index: int, |
13 pre_bnfs: BNF_Def.bnf list, |
13 pre_bnfs: BNF_Def.bnf list, |
14 fp_res: BNF_FP.fp_result, |
14 fp_res: BNF_FP.fp_result, |
15 ctr_sugar: BNF_Ctr_Sugar.ctr_sugar}; |
15 ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list}; |
16 |
16 |
17 val fp_sugar_of: Proof.context -> string -> fp_sugar option |
17 val fp_sugar_of: Proof.context -> string -> fp_sugar option |
18 |
18 |
19 val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> |
19 val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> |
20 thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> |
20 thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> |
62 type fp_sugar = |
62 type fp_sugar = |
63 {lfp: bool, |
63 {lfp: bool, |
64 index: int, |
64 index: int, |
65 pre_bnfs: bnf list, |
65 pre_bnfs: bnf list, |
66 fp_res: fp_result, |
66 fp_res: fp_result, |
67 ctr_sugar: ctr_sugar}; |
67 ctr_sugars: ctr_sugar list}; |
68 |
68 |
69 fun eq_fp_sugar ({lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, |
69 fun eq_fp_sugar ({lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, |
70 {lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = |
70 {lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = |
71 lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); |
71 lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); |
72 |
72 |
73 fun morph_fp_sugar phi {lfp, index, pre_bnfs, fp_res, ctr_sugar} = |
73 fun morph_fp_sugar phi {lfp, index, pre_bnfs, fp_res, ctr_sugars} = |
74 {lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, |
74 {lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, |
75 fp_res = morph_fp_result phi fp_res, ctr_sugar = morph_ctr_sugar phi ctr_sugar}; |
75 fp_res = morph_fp_result phi fp_res, ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars}; |
76 |
76 |
77 structure Data = Generic_Data |
77 structure Data = Generic_Data |
78 ( |
78 ( |
79 type T = fp_sugar Symtab.table; |
79 type T = fp_sugar Symtab.table; |
80 val empty = Symtab.empty; |
80 val empty = Symtab.empty; |
87 fun register_fp_sugar key fp_sugar = |
87 fun register_fp_sugar key fp_sugar = |
88 Local_Theory.declaration {syntax = false, pervasive = true} |
88 Local_Theory.declaration {syntax = false, pervasive = true} |
89 (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); |
89 (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); |
90 |
90 |
91 fun register_fp_sugars lfp pre_bnfs (fp_res as {ctors, ...}) ctr_sugars lthy = |
91 fun register_fp_sugars lfp pre_bnfs (fp_res as {ctors, ...}) ctr_sugars lthy = |
92 ((1, ctors), lthy) |
92 (1, lthy) |
93 |> fold (fn ctr_sugar => fn ((kk, ctor :: ctors), lthy) => |
93 |> fold (fn ctor => fn (kk, lthy) => (kk + 1, |
94 ((kk + 1, ctors), register_fp_sugar (fp_name_of_ctor ctor) {lfp = lfp, index = kk, |
94 register_fp_sugar (fp_name_of_ctor ctor) {lfp = lfp, index = kk, |
95 pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugar = ctr_sugar} lthy)) ctr_sugars |
95 pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_sugars = ctr_sugars} lthy)) ctors |
96 |> snd; |
96 |> snd; |
97 |
97 |
98 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |
98 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |
99 fun quasi_unambiguous_case_names names = |
99 fun quasi_unambiguous_case_names names = |
100 let |
100 let |