| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Idris.Coverage
Description
The coverage and totality checkers for Idris are in this module.
- mkPatTm :: PTerm -> Idris Term
- genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]
- validCoverageCase :: Context -> Err -> Bool
- recoverableCoverage :: Context -> Err -> Bool
- genAll :: IState -> (Bool, [PTerm]) -> [PTerm]
- upd :: t -> PArg' t -> PArg' t
- checkAllCovering :: FC -> [Name] -> Name -> 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
- 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
- totalityCheckBlock :: Idris ()
Documentation
mkPatTm :: PTerm -> Idris Term Source
Generate a pattern from an impossible LHS.
We need this to eliminate the pattern clauses which have been provided explicitly from new clause generation.
genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm] Source
Given a list of LHSs, generate a extra clauses which cover the remaining
cases. The ones which haven't been provided are marked absurd so
that the checker will make sure they can't happen.
This will only work after the given clauses have been typechecked and the names are fully explicit!
validCoverageCase :: Context -> Err -> Bool Source
Does this error result rule out a case as valid when coverage checking?
recoverableCoverage :: Context -> Err -> Bool Source
Check whether an error is recoverable in the sense needed for coverage checking.
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
checkSizeChange :: Name -> Idris Totality Source
allNothing :: [Maybe a] -> Bool Source
collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)] Source
totalityCheckBlock :: Idris () Source