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!

genAll :: IState -> [PTerm] -> [PTerm]

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

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

checkPositive :: [Name] -> (Name, Type) -> Idris Totality

calcProd :: IState -> FC -> Name -> [([Name], Term, Term)] -> 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

Constructors

Toplevel

Unguarded

Guarded

Instances

Show Guardedness

buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]

checkSizeChange :: Name -> Idris Totality

type MultiPath = [SCGEntry]

mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]

checkMP :: IState -> Int -> MultiPath -> Totality

allNothing :: [Maybe a] -> Bool

collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]

noPartial :: [Totality] -> Totality

collapse :: [Totality] -> Totality

collapse' :: Totality -> [Totality] -> Totality