Skip to content

Conversation

@AntonPing
Copy link

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:

  • 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.

@mjustus
Copy link
Collaborator

mjustus commented Oct 9, 2024

I believe the examples involving Stream are instances of #964, where I just posted an outline of how to fix evaluation under delays.

Outside of those, do you have a test case that requires inlining a recursive function to show termination? I am not in principle opposed to introducing fuel for that purpose but it would be nice to have a real-world derived example.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Addition of %tcinline may hang compilation

2 participants