fixed bugs that caused compiler to hang forever when there is %tcinline pragma

[AntonPing]

Description

• Two new tests are added: total025 and total026. they all caused compiler to hang without this fix.
• Modify fuel field in Core/Value.idr to Just 1000. This fixed only half of the problem. total025 now terminates with fuel, bug total026 still hangs.
• Add parameters cbs in file Core/Termination/CallGraph.idr. This fixed the second test total026.

The cause of looping in total026 is pretty complicated. Consider such an example:

%tcinline
incAll' : Stream Nat -> Stream Nat
incAll' = \(x::xs) => S x :: incAll' xs

The lambda function with pattern matching \(x::xs) => ... is actually encoded in such way(f is a fresh variable):

incAll' = f
f (x::xs) => S x :: incAll' xs

In CallGraph.idr, such f is called a case function, and they are treated specially: each time findSCall meets a case function, it will jump to the definition of the case function, and it won't be treated as regular function call.
After tcinlining, f becomes a recursive definition:

incAll' = f
f (x::xs) => S x :: f xs

In such way, findSCall in CallGraph.idr will loop forever here, since it corresponds to a program of infinite length:

incAll' =  \(x::xs) => S x :: (\(x::xs) => S x :: (\(x::xs) => S x :: (\(x::xs) =>  ... ))) ...)

The fix in CallGraph.idr introduce a new parameter cbs. Each time findSCall enters a case function, it appends the function name to cbs. If it's already there, findSCall then will treat it as a regular function call.

[gallais]

Was the fix invalid or?

[buzden]

Was the fix invalid or?

As a superviser of this work, I can say that this fix is okay, but still leaves some cases where some total functions that can be checked as total, are not checked as total. That's why another PR that this one relies on is being prepared. This PR should have been converted to a draft rather than being closed.

[AntonPing]

This pull request is moved to #3272, since github doesn't allow me to reopen it.