Idris.Coverage

Documentation

mkPatTm :: PTerm -> Idris Term

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]

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

Does this error result rule out a case as valid when coverage checking?

recoverableCoverage :: Context -> Err -> Bool

Check whether an error is recoverable in the sense needed for coverage checking.

genAll :: IState -> (Bool, [PTerm]) -> [PTerm]

upd :: t -> PArg' t -> PArg' t

checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()

Check whether function and all descendants cover all cases (partial is okay, as long as it's due to recursion)

checkPositive

Arguments

:: [Name]

the group of type declarations

-> (Name, Type)

the constructor

-> Idris Totality

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

Calculate the totality of a function from its patterns. Either follow the size change graph (if inductive) or check for productivity (if coinductive)

checkTotality :: [Name] -> FC -> Name -> Idris Totality

checkDeclTotality :: (FC, Name) -> Idris Totality

verifyTotality :: (FC, Name) -> Idris ()

buildSCG :: (FC, Name) -> Idris ()

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

delazy :: TT Name -> TT Name

delazy' :: Bool -> TT Name -> TT Name

data Guardedness

Constructors

Toplevel

Unguarded

Guarded

Delayed

Instances

Show Guardedness

Methods

showsPrec :: Int -> Guardedness -> ShowS

show :: Guardedness -> String

showList :: [Guardedness] -> ShowS

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 ()