11 type fp_result = |
11 type fp_result = |
12 {Ts: typ list, |
12 {Ts: typ list, |
13 bnfs: BNF_Def.bnf list, |
13 bnfs: BNF_Def.bnf list, |
14 ctors: term list, |
14 ctors: term list, |
15 dtors: term list, |
15 dtors: term list, |
16 xtor_co_folds: term list, |
|
17 xtor_co_recs: term list, |
16 xtor_co_recs: term list, |
18 xtor_co_induct: thm, |
17 xtor_co_induct: thm, |
19 dtor_ctors: thm list, |
18 dtor_ctors: thm list, |
20 ctor_dtors: thm list, |
19 ctor_dtors: thm list, |
21 ctor_injects: thm list, |
20 ctor_injects: thm list, |
22 dtor_injects: thm list, |
21 dtor_injects: thm list, |
23 xtor_map_thms: thm list, |
22 xtor_map_thms: thm list, |
24 xtor_set_thmss: thm list list, |
23 xtor_set_thmss: thm list list, |
25 xtor_rel_thms: thm list, |
24 xtor_rel_thms: thm list, |
26 xtor_co_fold_thms: thm list, |
|
27 xtor_co_rec_thms: thm list, |
25 xtor_co_rec_thms: thm list, |
28 xtor_co_fold_o_map_thms: thm list, |
|
29 xtor_co_rec_o_map_thms: thm list, |
26 xtor_co_rec_o_map_thms: thm list, |
30 rel_xtor_co_induct_thm: thm} |
27 rel_xtor_co_induct_thm: thm} |
31 |
28 |
32 val morph_fp_result: morphism -> fp_result -> fp_result |
29 val morph_fp_result: morphism -> fp_result -> fp_result |
33 |
30 |
192 type fp_result = |
189 type fp_result = |
193 {Ts: typ list, |
190 {Ts: typ list, |
194 bnfs: BNF_Def.bnf list, |
191 bnfs: BNF_Def.bnf list, |
195 ctors: term list, |
192 ctors: term list, |
196 dtors: term list, |
193 dtors: term list, |
197 xtor_co_folds: term list, |
|
198 xtor_co_recs: term list, |
194 xtor_co_recs: term list, |
199 xtor_co_induct: thm, |
195 xtor_co_induct: thm, |
200 dtor_ctors: thm list, |
196 dtor_ctors: thm list, |
201 ctor_dtors: thm list, |
197 ctor_dtors: thm list, |
202 ctor_injects: thm list, |
198 ctor_injects: thm list, |
203 dtor_injects: thm list, |
199 dtor_injects: thm list, |
204 xtor_map_thms: thm list, |
200 xtor_map_thms: thm list, |
205 xtor_set_thmss: thm list list, |
201 xtor_set_thmss: thm list list, |
206 xtor_rel_thms: thm list, |
202 xtor_rel_thms: thm list, |
207 xtor_co_fold_thms: thm list, |
|
208 xtor_co_rec_thms: thm list, |
203 xtor_co_rec_thms: thm list, |
209 xtor_co_fold_o_map_thms: thm list, |
|
210 xtor_co_rec_o_map_thms: thm list, |
204 xtor_co_rec_o_map_thms: thm list, |
211 rel_xtor_co_induct_thm: thm}; |
205 rel_xtor_co_induct_thm: thm}; |
212 |
206 |
213 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_folds, xtor_co_recs, xtor_co_induct, |
207 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct, |
214 dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, |
208 dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, |
215 xtor_rel_thms, xtor_co_fold_thms, xtor_co_rec_thms, xtor_co_fold_o_map_thms, |
209 xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} = |
216 xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} = |
|
217 {Ts = map (Morphism.typ phi) Ts, |
210 {Ts = map (Morphism.typ phi) Ts, |
218 bnfs = map (morph_bnf phi) bnfs, |
211 bnfs = map (morph_bnf phi) bnfs, |
219 ctors = map (Morphism.term phi) ctors, |
212 ctors = map (Morphism.term phi) ctors, |
220 dtors = map (Morphism.term phi) dtors, |
213 dtors = map (Morphism.term phi) dtors, |
221 xtor_co_folds = map (Morphism.term phi) xtor_co_folds, |
|
222 xtor_co_recs = map (Morphism.term phi) xtor_co_recs, |
214 xtor_co_recs = map (Morphism.term phi) xtor_co_recs, |
223 xtor_co_induct = Morphism.thm phi xtor_co_induct, |
215 xtor_co_induct = Morphism.thm phi xtor_co_induct, |
224 dtor_ctors = map (Morphism.thm phi) dtor_ctors, |
216 dtor_ctors = map (Morphism.thm phi) dtor_ctors, |
225 ctor_dtors = map (Morphism.thm phi) ctor_dtors, |
217 ctor_dtors = map (Morphism.thm phi) ctor_dtors, |
226 ctor_injects = map (Morphism.thm phi) ctor_injects, |
218 ctor_injects = map (Morphism.thm phi) ctor_injects, |
227 dtor_injects = map (Morphism.thm phi) dtor_injects, |
219 dtor_injects = map (Morphism.thm phi) dtor_injects, |
228 xtor_map_thms = map (Morphism.thm phi) xtor_map_thms, |
220 xtor_map_thms = map (Morphism.thm phi) xtor_map_thms, |
229 xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss, |
221 xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss, |
230 xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, |
222 xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, |
231 xtor_co_fold_thms = map (Morphism.thm phi) xtor_co_fold_thms, |
|
232 xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, |
223 xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, |
233 xtor_co_fold_o_map_thms = map (Morphism.thm phi) xtor_co_fold_o_map_thms, |
|
234 xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms, |
224 xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms, |
235 rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm}; |
225 rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm}; |
236 |
226 |
237 fun time ctxt timer msg = (if Config.get ctxt bnf_timing |
227 fun time ctxt timer msg = (if Config.get ctxt bnf_timing |
238 then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ |
228 then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ |