equal
deleted
inserted
replaced
331 |> map Free |
331 |> map Free |
332 |> fold (fn (ctr_arg_idx, (arg_idx, _)) => |
332 |> fold (fn (ctr_arg_idx, (arg_idx, _)) => |
333 nth_map arg_idx (K (nth ctr_args ctr_arg_idx))) |
333 nth_map arg_idx (K (nth ctr_args ctr_arg_idx))) |
334 no_calls' |
334 no_calls' |
335 |> fold (fn (ctr_arg_idx, (arg_idx, T)) => fn xs => |
335 |> fold (fn (ctr_arg_idx, (arg_idx, T)) => fn xs => |
336 nth_map arg_idx (K (ensure_unique xs (retype_free T (nth ctr_args ctr_arg_idx)))) xs) |
336 nth_map arg_idx (K (ensure_unique xs |
|
337 (retype_const_or_free T (nth ctr_args ctr_arg_idx)))) xs) |
337 mutual_calls' |
338 mutual_calls' |
338 |> fold (fn (ctr_arg_idx, (arg_idx, T)) => |
339 |> fold (fn (ctr_arg_idx, (arg_idx, T)) => |
339 nth_map arg_idx (K (retype_free T (nth ctr_args ctr_arg_idx)))) |
340 nth_map arg_idx (K (retype_const_or_free T (nth ctr_args ctr_arg_idx)))) |
340 nested_calls'; |
341 nested_calls'; |
341 |
342 |
342 val fun_name_ctr_pos_list = |
343 val fun_name_ctr_pos_list = |
343 map (fn (x :: _) => (#fun_name x, length (#left_args x))) funs_data; |
344 map (fn (x :: _) => (#fun_name x, length (#left_args x))) funs_data; |
344 val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1; |
345 val get_ctr_pos = try (the o AList.lookup (op =) fun_name_ctr_pos_list) #> the_default ~1; |