95 |
95 |
96 (* TODO: test with sort constraints on As *) |
96 (* TODO: test with sort constraints on As *) |
97 (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables |
97 (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables |
98 as deads? *) |
98 as deads? *) |
99 fun mutualize_fp_sugars has_nested fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 = |
99 fun mutualize_fp_sugars has_nested fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 = |
100 if has_nested orelse has_duplicates (op =) fpTs then |
100 if has_nested then |
101 let |
101 let |
102 val thy = Proof_Context.theory_of no_defs_lthy0; |
102 val thy = Proof_Context.theory_of no_defs_lthy0; |
103 |
103 |
104 val qsotm = quote o Syntax.string_of_term no_defs_lthy0; |
104 val qsotm = quote o Syntax.string_of_term no_defs_lthy0; |
105 |
105 |
134 no_defs_lthy0 |
134 no_defs_lthy0 |
135 |> fold Variable.declare_typ As |
135 |> fold Variable.declare_typ As |
136 |> mk_TFrees nn |
136 |> mk_TFrees nn |
137 ||>> variant_tfrees fp_b_names; |
137 ||>> variant_tfrees fp_b_names; |
138 |
138 |
139 fun freeze_fp_default (T as Type (s, Ts)) = |
|
140 (case find_index (curry (op =) T) fpTs of |
|
141 ~1 => Type (s, map freeze_fp_default Ts) |
|
142 | kk => nth Xs kk) |
|
143 | freeze_fp_default T = T; |
|
144 |
|
145 fun check_call_dead live_call call = |
139 fun check_call_dead live_call call = |
146 if null (get_indices call) then () else incompatible_calls live_call call; |
140 if null (get_indices call) then () else incompatible_calls live_call call; |
|
141 |
|
142 fun freeze_fp_simple (T as Type (s, Ts)) = |
|
143 (case find_index (curry (op =) T) fpTs of |
|
144 ~1 => Type (s, map freeze_fp_simple Ts) |
|
145 | kk => nth Xs kk) |
|
146 | freeze_fp_simple T = T; |
147 |
147 |
148 fun freeze_fp_map (callss, (live_call :: _, dead_calls)) s Ts = |
148 fun freeze_fp_map (callss, (live_call :: _, dead_calls)) s Ts = |
149 (List.app (check_call_dead live_call) dead_calls; |
149 (List.app (check_call_dead live_call) dead_calls; |
150 Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] |
150 Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) [] |
151 (transpose callss)) Ts)) |
151 (transpose callss)) Ts)) |
152 and freeze_fp calls (T as Type (s, Ts)) = |
152 and freeze_fp calls (T as Type (s, Ts)) = |
153 (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of |
153 (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of |
154 ([], _) => |
154 ([], _) => |
155 (case map_partition (try (snd o dest_abs_or_applied_map_or_ctr no_defs_lthy s)) calls of |
155 (case map_partition (try (snd o dest_abs_or_applied_map_or_ctr no_defs_lthy s)) calls of |
156 ([], _) => freeze_fp_default T |
156 ([], _) => freeze_fp_simple T |
157 | callsp => freeze_fp_map callsp s Ts) |
157 | callsp => freeze_fp_map callsp s Ts) |
158 | callsp => freeze_fp_map callsp s Ts) |
158 | callsp => freeze_fp_map callsp s Ts) |
159 | freeze_fp _ T = T; |
159 | freeze_fp _ T = T; |
160 |
160 |
161 val ctr_Tsss = map (map binder_types) ctr_Tss; |
161 val ctr_Tsss = map (map binder_types) ctr_Tss; |
255 fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy = |
255 fun nested_to_mutual_fps fp actual_bs actual_Ts get_indices actual_callssss0 lthy = |
256 let |
256 let |
257 val qsoty = quote o Syntax.string_of_typ lthy; |
257 val qsoty = quote o Syntax.string_of_typ lthy; |
258 val qsotys = space_implode " or " o map qsoty; |
258 val qsotys = space_implode " or " o map qsoty; |
259 |
259 |
|
260 fun duplicate_datatype T = error (qsoty T ^ " is not mutually recursive with itself"); |
260 fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype"); |
261 fun not_co_datatype0 T = error (qsoty T ^ " is not a " ^ co_prefix fp ^ "datatype"); |
261 fun not_co_datatype (T as Type (s, _)) = |
262 fun not_co_datatype (T as Type (s, _)) = |
262 if fp = Least_FP andalso |
263 if fp = Least_FP andalso |
263 is_some (Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then |
264 is_some (Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then |
264 error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")") |
265 error (qsoty T ^ " is not a new-style datatype (cf. \"datatype_new\")") |
266 not_co_datatype0 T |
267 not_co_datatype0 T |
267 | not_co_datatype T = not_co_datatype0 T; |
268 | not_co_datatype T = not_co_datatype0 T; |
268 fun not_mutually_nested_rec Ts1 Ts2 = |
269 fun not_mutually_nested_rec Ts1 Ts2 = |
269 error (qsotys Ts1 ^ " is neither mutually recursive with nor nested recursive via " ^ |
270 error (qsotys Ts1 ^ " is neither mutually recursive with nor nested recursive via " ^ |
270 qsotys Ts2); |
271 qsotys Ts2); |
|
272 |
|
273 val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T); |
271 |
274 |
272 val perm_actual_Ts as Type (_, ty_args0) :: _ = |
275 val perm_actual_Ts as Type (_, ty_args0) :: _ = |
273 sort (int_ord o pairself Term.size_of_typ) actual_Ts; |
276 sort (int_ord o pairself Term.size_of_typ) actual_Ts; |
274 |
277 |
275 fun check_enrich_with_mutuals _ [] = [] |
278 fun check_enrich_with_mutuals _ [] = [] |