302 error (qsotys Ts1 ^ " is neither mutually recursive with nor nested recursive via " ^ |
302 error (qsotys Ts1 ^ " is neither mutually recursive with nor nested recursive via " ^ |
303 qsotys Ts2); |
303 qsotys Ts2); |
304 |
304 |
305 val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T); |
305 val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T); |
306 |
306 |
307 val perm_actual_Ts as Type (_, ty_args0) :: _ = |
307 val perm_actual_Ts as Type (_, tyargs0) :: _ = |
308 sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts; |
308 sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts; |
309 |
309 |
310 fun check_enrich_with_mutuals _ [] = [] |
310 fun check_enrich_with_mutuals _ [] = [] |
311 | check_enrich_with_mutuals seen ((T as Type (T_name, ty_args)) :: Ts) = |
311 | check_enrich_with_mutuals seen ((T as Type (T_name, tyargs)) :: Ts) = |
312 (case fp_sugar_of lthy T_name of |
312 (case fp_sugar_of lthy T_name of |
313 SOME ({fp = fp', fp_res = {Ts = Ts', ...}, ...}) => |
313 SOME ({fp = fp', fp_res = {Ts = Ts', ...}, ...}) => |
314 if fp = fp' then |
314 if fp = fp' then |
315 let |
315 let |
316 val mutual_Ts = map (fn Type (s, _) => Type (s, ty_args)) Ts'; |
316 val mutual_Ts = map (fn Type (s, _) => Type (s, tyargs)) Ts'; |
317 val _ = |
317 val _ = |
318 seen = [] orelse exists (exists_subtype_in seen) mutual_Ts orelse |
318 seen = [] orelse exists (exists_subtype_in seen) mutual_Ts orelse |
319 not_mutually_nested_rec mutual_Ts seen; |
319 not_mutually_nested_rec mutual_Ts seen; |
320 val (seen', Ts') = List.partition (member (op =) mutual_Ts) Ts; |
320 val (seen', Ts') = List.partition (member (op =) mutual_Ts) Ts; |
321 in |
321 in |
328 |
328 |
329 val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts; |
329 val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts; |
330 val missing_Ts = perm_Ts |> subtract (op =) actual_Ts; |
330 val missing_Ts = perm_Ts |> subtract (op =) actual_Ts; |
331 val Ts = actual_Ts @ missing_Ts; |
331 val Ts = actual_Ts @ missing_Ts; |
332 |
332 |
333 (* The name "'z" is likely not to clash with the context, resulting in more cache hits. *) |
333 fun generalize_subtype T (tyarps_lthy as (tyarps, lthy)) = |
334 fun generalize_simple_type T (seen, lthy) = |
334 (* The name "'z" is unlikely to clash with the context, resulting in more cache hits. *) |
335 variant_tfrees ["z"] lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy))); |
335 if exists_subtype_in Ts T then generalize_Type T tyarps_lthy |
336 |
336 else variant_tfrees ["z"] lthy |> (fn ([U], lthy) => (U, (tyarps, lthy))) |
337 fun generalize_type T (seen_lthy as (seen, _)) = |
337 and generalize_Type (Type (s, tyargs)) (tyarps_lthy as (tyarps, _)) = |
338 (case AList.lookup (op =) seen T of |
338 (case AList.lookup (op =) tyarps tyargs of |
339 SOME U => (U, seen_lthy) |
339 SOME tyargs' => (Type (s, tyargs'), tyarps_lthy) |
340 | NONE => |
340 | NONE => fold_map generalize_subtype tyargs tyarps_lthy |
341 (case T of |
341 |> (fn (tyargs', (tyarps, lthy)) => |
342 Type (s, Ts') => |
342 (Type (s, tyargs'), ((tyargs, tyargs') :: tyarps, lthy)))); |
343 if exists_subtype_in Ts T then fold_map generalize_type Ts' seen_lthy |>> curry Type s |
343 |
344 else generalize_simple_type T seen_lthy |
344 val (perm_Us, _) = fold_map generalize_Type perm_Ts ([], lthy); |
345 | _ => generalize_simple_type T seen_lthy)); |
|
346 |
|
347 val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy); |
|
348 |
345 |
349 val nn = length Ts; |
346 val nn = length Ts; |
350 val kks = 0 upto nn - 1; |
347 val kks = 0 upto nn - 1; |
351 |
348 |
352 val callssss0 = pad_list [] nn actual_callssss0; |
349 val callssss0 = pad_list [] nn actual_callssss0; |
360 val perm_bs = permute bs; |
357 val perm_bs = permute bs; |
361 val perm_kks = permute kks; |
358 val perm_kks = permute kks; |
362 val perm_callssss0 = permute callssss0; |
359 val perm_callssss0 = permute callssss0; |
363 val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts; |
360 val perm_fp_sugars0 = map (the o fp_sugar_of lthy o fst o dest_Type) perm_Ts; |
364 |
361 |
365 val has_nested = exists (fn Type (_, ty_args) => ty_args <> ty_args0) Ts; |
362 val has_nested = exists (fn Type (_, tyargs) => tyargs <> tyargs0) Ts; |
366 val perm_callssss = map2 indexify_callsss perm_fp_sugars0 perm_callssss0; |
363 val perm_callssss = map2 indexify_callsss perm_fp_sugars0 perm_callssss0; |
367 |
364 |
368 val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices; |
365 val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices; |
369 |
366 |
370 val ((perm_fp_sugars, fp_sugar_thms), lthy) = |
367 val ((perm_fp_sugars, fp_sugar_thms), lthy) = |