Coverage.Internal

Module for internal representation.

Documentation

type Name = String

A type synonym for names.

type Binders lit = [Binder lit]

A collection of binders, as used to match products, in product binders or collections of binders in top-level declarations.

data Binder lit

Binders

Constructors

Var (Maybe Name)

Lit lit

Tagged Name (Binder lit)

Product (Binders lit)

Record [(Name, Binder lit)]

Instances

Eq lit => Eq (Binder lit)

Show lit => Show (Binder lit)

newtype Environment

Environment

The language implementor should provide an environment to let the checker lookup for constructors' names (just for one type for now).

Constructors

Environment

Fields

envInfo :: Name -> Maybe [Name]

makeEnv :: (Name -> Maybe [Name]) -> Environment

defaultEnv :: Environment

data Guard

Guards and alternatives

Guard are abstract, and it is up to the language implementor to interpret guards abstractly. Guards can catch all cases, or represent some opaque expression which cannot be analysed.

Constructors

CatchAll

Opaque

Instances

Eq Guard

Show Guard

type Alternative lit = (Binders lit, Maybe Guard)

A case alternative consists of a collection of binders which match a collection of values, and an optional guard.

data Redundant a

Data-type for redundant cases representation.

Constructors

DontKnow

Redundant

NotRedundant a

Instances

Functor Redundant

Functor instance for Redundant (TODO: proofs).

Applicative Redundant

Applicative instance for Redundant.

Eq a => Eq (Redundant a)

Show a => Show (Redundant a)

data Check lit

Check wraps both uncovered and redundant cases.

Constructors

Check

Fields

getUncovered :: [Binders lit]

getRedundant :: Redundant [Binders lit]

Instances

Eq lit => Eq (Check lit)

Show lit => Show (Check lit)

makeCheck :: [Binders lit] -> Redundant [Binders lit] -> Check lit

applyUncovered :: ([Binders lit] -> [Binders lit]) -> Check lit -> Check lit

applyRedundant :: (Redundant [Binders lit] -> Redundant [Binders lit]) -> Check lit -> Check lit

wildcard :: Binder lit

Wildcard

genericMerge :: Ord a => (a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]

Applies a function over two lists of tuples that may lack elements.

missingSingle :: Eq lit => Environment -> Binder lit -> Binder lit -> ([Binder lit], Maybe Bool)

Returns the uncovered set after one binder is applied to the set of values represented by another.

initialize :: Int -> [Binder lit]

Generates a list of initial binders.

missingMultiple :: Eq lit => Environment -> Binders lit -> Binders lit -> ([Binders lit], Maybe Bool)

missingMultiple returns the whole set of uncovered cases.

missingCases :: Eq lit => Environment -> Binders lit -> Alternative lit -> ([Binders lit], Maybe Bool)

missingCases applies missingMultiple to an alternative.

missingAlternative :: Eq lit => Environment -> Alternative lit -> Binders lit -> ([Binders lit], Maybe Bool)

missingAlternative is missingCases with guard handling.