| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Termination.RecCheck
Description
Checking for recursion:
- We detect truly (co)recursive definitions by computing the dependency graph and checking for cycles.
- This is inexpensive and let us skip the termination check when there's no (co)recursion
Original contribution by Andrea Vezzosi (sanzhiyan). This implementation by Andreas.
Documentation
type MutualNames = Set QName Source #
The mutual block we are checking.
The functions are numbered according to their order of appearance in this set.
recursive :: Set QName -> TCM [MutualNames] Source #
Given a list of formally mutually recursive functions, check for actual recursive calls in the bodies of these functions. Returns the actually recursive functions as strongly connected components.
As a side effect, update the clauseRecursive field in the
clauses belonging to the given functions.