| Copyright | License : BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell98 |
Idris.Termination
Description
- checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()
- checkIfGuarded :: Name -> Idris ()
- checkPositive :: [Name] -> (Name, Type) -> Idris Totality
- calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality
- checkTotality :: [Name] -> FC -> Name -> Idris Totality
- checkDeclTotality :: (FC, Name) -> Idris Totality
- verifyTotality :: (FC, Name) -> Idris ()
- buildSCG :: (FC, Name) -> Idris ()
- delazy :: TT Name -> TT Name
- delazy' :: Bool -> TT Name -> TT Name
- data Guardedness
- buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
- checkSizeChange :: Name -> Idris Totality
- type MultiPath = [SCGEntry]
- mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]
- checkMP :: IState -> Name -> Int -> MultiPath -> Totality
- allNothing :: [Maybe a] -> Bool
- collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]
- noPartial :: [Totality] -> Totality
- collapse :: [Totality] -> Totality
- collapse' :: Totality -> [Totality] -> Totality
Documentation
checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris () Source #
Check whether function and all descendants cover all cases (partial is okay, as long as it's due to recursion)
checkIfGuarded :: Name -> Idris () Source #
Check whether all Inf arguments to the name end up guaranteed to be
guarded by constructors (conservatively... maybe this can do better later).
Essentially, all it does is check that every branch is a constructor application
with no other function applications.
If so, set the AllGuarded flag which can be used by the productivity check
Check if, in a given group of type declarations mut_ns, the constructor cn : ty is strictly positive, and update the context accordingly
calcTotality :: FC -> Name -> [([Name], Term, Term)] -> Idris Totality Source #
Calculate the totality of a function from its patterns. Either follow the size change graph (if inductive) or check for productivity (if coinductive)
buildSCG :: (FC, Name) -> Idris () Source #
Calculate the size change graph for this definition
SCG for a function f consists of a list of: (g, [(a1, sizechange1), (a2, sizechange2), ..., (an, sizechangen)])
where g is a function called a1 ... an are the arguments of f in positions 1..n of g sizechange1 ... sizechange2 is how their size has changed wrt the input to f Nothing, if the argument is unrelated to the input
data Guardedness Source #
Instances
allNothing :: [Maybe a] -> Bool Source #
collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)] Source #