| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Termination.Inlining
Description
This module defines an inlining transformation on clauses that's run before termination checking. The purpose is to improve termination checking of with clauses (issue 59). The transformation inlines generated with-functions expanding the clauses of the parent function in such a way that termination checking the expanded clauses guarantees termination of the original function, while allowing more terminating functions to be accepted. It does in no way pretend to preserve the semantics of the original function.
Roughly, the source program
f ps with as
{f ps₁i qsi = bi}is represented internally as
f ps = f-aux xs as where xs = vars(ps)
{f-aux ps₂i qsi = bi} where ps₁i = ps[ps₂i/xs]The inlining transformation turns this into
{f ps = aj} for aj ∈ as
{f ps₁i qsi = bi}The first set of clauses, called withExprClauses, ensure that we
don't forget any recursive calls in as.
The second set of clauses, henceforth called inlinedClauses,
are the surface-level clauses the user sees (and probably reasons about).
The reason this works is that there is a single call site for each with-function.
Note that the lhss of the inlined clauses are not type-correct,
neither with the type of f (since there are additional patterns qsi)
nor with the type of f-aux (since there are the surface-level patterns
ps₁i instead of the actual patterns ps₂i).