equal
deleted
inserted
replaced
293 not_co_datatype T |
293 not_co_datatype T |
294 | NONE => not_co_datatype T) |
294 | NONE => not_co_datatype T) |
295 | check_enrich_with_mutuals _ (T :: _) = not_co_datatype T; |
295 | check_enrich_with_mutuals _ (T :: _) = not_co_datatype T; |
296 |
296 |
297 val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts; |
297 val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts; |
298 |
|
299 val missing_Ts = perm_Ts |> subtract (op =) actual_Ts; |
298 val missing_Ts = perm_Ts |> subtract (op =) actual_Ts; |
300 val Ts = actual_Ts @ missing_Ts; |
299 val Ts = actual_Ts @ missing_Ts; |
|
300 |
|
301 fun generalize_type (T as Type (s, Ts)) (seen_lthy as (seen, lthy)) = |
|
302 (case AList.lookup (op =) seen T of |
|
303 SOME U => (U, seen_lthy) |
|
304 | NONE => |
|
305 if exists_subtype_in Ts T then fold_map generalize_type Ts seen_lthy |>> curry Type s |
|
306 else mk_TFrees 1 lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)))) |
|
307 | generalize_type T seen_lthy = (T, seen_lthy); |
|
308 |
|
309 val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy); |
301 |
310 |
302 val nn = length Ts; |
311 val nn = length Ts; |
303 val kks = 0 upto nn - 1; |
312 val kks = 0 upto nn - 1; |
304 |
313 |
305 val common_name = mk_common_name (map Binding.name_of actual_bs); |
314 val common_name = mk_common_name (map Binding.name_of actual_bs); |
316 val perm_callssss = pad_and_indexify_calls perm_fp_sugars0 nn actual_callssss0; |
325 val perm_callssss = pad_and_indexify_calls perm_fp_sugars0 nn actual_callssss0; |
317 |
326 |
318 val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices; |
327 val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices; |
319 |
328 |
320 val ((perm_fp_sugars, fp_sugar_thms), lthy) = |
329 val ((perm_fp_sugars, fp_sugar_thms), lthy) = |
321 mutualize_fp_sugars has_nested fp perm_bs perm_Ts get_perm_indices perm_callssss |
330 mutualize_fp_sugars has_nested fp perm_bs perm_Us get_perm_indices perm_callssss |
322 perm_fp_sugars0 lthy; |
331 perm_fp_sugars0 lthy; |
323 |
332 |
324 val fp_sugars = unpermute perm_fp_sugars; |
333 val fp_sugars = unpermute perm_fp_sugars; |
325 in |
334 in |
326 ((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy) |
335 ((missing_Ts, perm_kks, fp_sugars, fp_sugar_thms), lthy) |