-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Exhaustivity Checking Library
--   
@package coverage
@version 0.1.0.2


-- | Module for internal representation.
module Coverage.Internal

-- | A type synonym for names.
type Name = String

-- | A collection of binders, as used to match products, in product binders
--   or collections of binders in top-level declarations.
type Binders lit = [Binder lit]

-- | Binders
data Binder lit
Var :: (Maybe Name) -> Binder lit
Lit :: lit -> Binder lit
Tagged :: Name -> (Binder lit) -> Binder lit
Product :: (Binders lit) -> Binder lit
Record :: [(Name, Binder lit)] -> Binder lit

-- | Environment
--   
--   The language implementor should provide an environment to let the
--   checker lookup for constructors' names (just for one type for now).
newtype Environment
Environment :: (Name -> Maybe [Name]) -> Environment
envInfo :: Environment -> Name -> Maybe [Name]
makeEnv :: (Name -> Maybe [Name]) -> Environment
defaultEnv :: Environment

-- | 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.
data Guard
CatchAll :: Guard
Opaque :: Guard

-- | A case alternative consists of a collection of binders which match a
--   collection of values, and an optional guard.
type Alternative lit = (Binders lit, Maybe Guard)

-- | Data-type for redundant cases representation.
data Redundant a
DontKnow :: Redundant a
NotRedundant :: Redundant a
Redundant :: a -> Redundant a

-- | Functor instance for Redundant (TODO: proofs).

-- | Applicative instance for Redundant.

-- | Check wraps both uncovered and redundant cases.
data Check lit
Check :: [Binders lit] -> Redundant [Binders lit] -> Check lit
getUncovered :: Check lit -> [Binders lit]
getRedundant :: Check lit -> Redundant [Binders 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
wildcard :: Binder lit

-- | Applies a function over two lists of tuples that may lack elements.
genericMerge :: Ord a => (a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]

-- | Returns the uncovered set after one binder is applied to the set of
--   values represented by another.
missingSingle :: Eq lit => Environment -> Binder lit -> Binder lit -> ([Binder lit], Maybe Bool)

-- | Generates a list of initial binders.
initialize :: Int -> [Binder lit]

-- | <a>missingMultiple</a> returns the whole set of uncovered cases.
missingMultiple :: Eq lit => Environment -> Binders lit -> Binders lit -> ([Binders lit], Maybe Bool)

-- | <a>missingCases</a> applies <a>missingMultiple</a> to an alternative.
missingCases :: Eq lit => Environment -> Binders lit -> Alternative lit -> ([Binders lit], Maybe Bool)

-- | <a>missingAlternative</a> is <a>missingCases</a> with guard handling.
missingAlternative :: Eq lit => Environment -> Alternative lit -> Binders lit -> ([Binders lit], Maybe Bool)
instance Show lit => Show (Binder lit)
instance Eq lit => Eq (Binder lit)
instance Show Guard
instance Eq Guard
instance Show a => Show (Redundant a)
instance Eq a => Eq (Redundant a)
instance Show lit => Show (Check lit)
instance Eq lit => Eq (Check lit)
instance Applicative Redundant
instance Functor Redundant


-- | Exhaustivity checking main function.
module Coverage

-- | Given a list of alternatives, <a>check</a> generates the proper set of
--   uncovered cases.
check :: Eq lit => Environment -> [Alternative lit] -> Check lit

-- | Binders
data Binder lit
Var :: (Maybe Name) -> Binder lit
Lit :: lit -> Binder lit
Tagged :: Name -> (Binder lit) -> Binder lit
Product :: (Binders lit) -> Binder lit
Record :: [(Name, Binder lit)] -> Binder lit

-- | 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.
data Guard
CatchAll :: Guard
Opaque :: Guard
makeEnv :: (Name -> Maybe [Name]) -> Environment

-- | Check wraps both uncovered and redundant cases.
data Check lit
Check :: [Binders lit] -> Redundant [Binders lit] -> Check lit
getUncovered :: Check lit -> [Binders lit]
getRedundant :: Check lit -> Redundant [Binders lit]

-- | Data-type for redundant cases representation.
data Redundant a
DontKnow :: Redundant a
NotRedundant :: Redundant a
Redundant :: a -> Redundant a