Detect termination for nested local definitions

[lukaszcz]

• Closes Termination checking doesn't work with local lets #3147

When we call a function that is currently being defined (there may be several such due to nested local definitions), we add a reflexive edge in the call map instead of adding an edge from the most nested definition. For example, for

go {A B} (f : A -> B) : List A -> List B
  | nil := nil
  | (elem :: next) :=
    let var1 := f elem;
        var2 := go f next;
    in var1 :: var2;

we add an edge from go to the recursive call go f next, instead of adding an edge from var2 to go f next as before.

This makes the above type-check.

The following still doesn't type-check, because next' is not a subpattern of the clause pattern of go. But this is a less pressing problem.

go {A B} (f : A -> B) : List A -> List B
  | nil := nil
  | (elem :: next) :=
    let var1 := f elem;
        var2 (next' : List A) : List B := go f next';
    in myCons var1 (var2 next);