(This pull request is a continuation of pull request #3257, since github doesn't allow me to re-open it)
close #2995
This pull request consists of two part:
Add new pragma %tcinline_fuel to avoid totality checker from infinitely inlining recursive function with %tcinline and hang forever. The default value of %tcinline_fuel is 1000.
Fix a bug in CallGraph.idr that caused compiler to hang forever even when %tcinline_fuel is set.
The second part is somehow rely on the first part, so it can't be divided into two pull requests .
Description of the first part
As issue #2995 mentioned, this code will cause totality checker to hang.
-- See test `total025`
%tcinline
zs : Stream Nat
zs = Z :: zs
By adding new pragma %tcinline_fuel, this problem is solved. A new test total027 is added to test this new pragma.
Description of the second part
And also as issue #2995 mentioned, this code also hangs compilation.
-- See test `total026`
%tcinline
incAll : Stream Nat -> Stream Nat
incAll = \(x::xs) => S x :: incAll xs
But surprisingly, after adding new pragma %tcinline_fuel, it still hangs compilation. It was caused by a bug in CallGraph.idr.
The lambda function with pattern matching \(x::xs) => ... is actually encoded in such way(f is a fresh variable):
incAll : Stream Nat -> Stream Nat
f : Stream Nat -> Stream Nat
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.
Description
(This pull request is a continuation of pull request #3257, since github doesn't allow me to re-open it) close #2995
This pull request consists of two part:
%tcinline_fuelto avoid totality checker from infinitely inlining recursive function with%tcinlineand hang forever. The default value of%tcinline_fuelis1000.CallGraph.idrthat caused compiler to hang forever even when%tcinline_fuelis set.The second part is somehow rely on the first part, so it can't be divided into two pull requests .
Description of the first part
As issue #2995 mentioned, this code will cause totality checker to hang.
By adding new pragma
%tcinline_fuel, this problem is solved. A new testtotal027is added to test this new pragma.Description of the second part
And also as issue #2995 mentioned, this code also hangs compilation.
But surprisingly, after adding new pragma
%tcinline_fuel, it still hangs compilation. It was caused by a bug inCallGraph.idr. The lambda function with pattern matching\(x::xs) => ...is actually encoded in such way(fis a fresh variable):In CallGraph.idr, such
fis called a case function, and they are treated specially: each timefindSCallmeets 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,fbecomes a recursive definition:In such way,
findSCallinCallGraph.idrwill loop forever here, since it corresponds to a program of infinite length:The fix in CallGraph.idr introduce a new parameter
cbs. Each timefindSCallenters a case function, it appends the function name tocbs. If it's already there,findSCallthen will treat it as a regular function call.