Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
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.

Synopsis

- type MutualNames = Set QName
- recursive :: Set QName -> TCM [MutualNames]
- anyDefs :: GetDefs a => (QName -> Bool) -> a -> TCM (Set QName)

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

anyDefs :: GetDefs a => (QName -> Bool) -> a -> TCM (Set QName) Source #

`anysDef names a` returns all definitions from `names` that are used in `a`.