Closed AntonPing closed 2 months ago
Was the fix invalid or?
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.
This pull request is moved to #3272, since github doesn't allow me to reopen it.
Description
fuel
field in Core/Value.idr toJust 1000
. This fixed only half of the problem. total025 now terminates with fuel, bug total026 still hangs.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:
The lambda function with pattern matching
\(x::xs) => ...
is actually encoded in such way(f
is a fresh variable):In CallGraph.idr, such
f
is called a case function, and they are treated specially: each timefindSCall
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:In such way,
findSCall
in CallGraph.idr will loop forever here, since it corresponds to a program of infinite length:The fix in CallGraph.idr introduce a new parameter
cbs
. Each timefindSCall
enters a case function, it appends the function name tocbs
. If it's already there,findSCall
then will treat it as a regular function call.