-- |
-- Module for exhaustivity checking over pattern matching definitions
-- The algorithm analyses the clauses of a definition one by one from top
-- to bottom, where in each step it has the cases already missing (uncovered),
-- and it generates the new set of missing cases.
--
module Language.PureScript.Linter.Exhaustive
  ( checkExhaustiveExpr
  ) where

import Prelude
import Protolude (ordNub)

import Control.Applicative (Applicative(..))
import Control.Arrow (first, second)
import Control.Monad (unless)
import Control.Monad.Writer.Class (MonadWriter(..))

import Data.List (foldl', sortOn)
import Data.Maybe (fromMaybe)
import Data.Map qualified as M
import Data.Text qualified as T

import Language.PureScript.AST.Binders (Binder(..))
import Language.PureScript.AST.Declarations (CaseAlternative(..), Expr(..), Guard(..), GuardedExpr(..), pattern MkUnguarded, isTrueExpr)
import Language.PureScript.AST.Literals (Literal(..))
import Language.PureScript.AST.Traversals (everywhereOnValuesM)
import Language.PureScript.Crash (internalError)
import Language.PureScript.Environment (DataDeclType, Environment(..), TypeKind(..))
import Language.PureScript.Errors (MultipleErrors, pattern NullSourceAnn, SimpleErrorMessage(..), SourceSpan, errorMessage')
import Language.PureScript.Names as P
import Language.PureScript.Pretty.Values (prettyPrintBinderAtom)
import Language.PureScript.Types as P
import Language.PureScript.Constants.Prim qualified as C

-- | There are two modes of failure for the redundancy check:
--
-- 1. Exhaustivity was incomplete due to too many cases, so we couldn't determine redundancy.
-- 2. We didn't attempt to determine redundancy for a binder, e.g. an integer binder.
--
-- We want to warn the user in the first case.
data RedundancyError = Incomplete | Unknown

-- |
-- Qualifies a propername from a given qualified propername and a default module name
--
qualifyName
  :: ProperName a
  -> ModuleName
  -> Qualified (ProperName b)
  -> Qualified (ProperName a)
qualifyName :: forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a
-> ModuleName
-> Qualified (ProperName b)
-> Qualified (ProperName a)
qualifyName ProperName a
n ModuleName
defmn Qualified (ProperName b)
qn = forall a. QualifiedBy -> a -> Qualified a
Qualified (ModuleName -> QualifiedBy
ByModuleName ModuleName
mn) ProperName a
n
  where
  (ModuleName
mn, ProperName b
_) = forall a. ModuleName -> Qualified a -> (ModuleName, a)
qualify ModuleName
defmn Qualified (ProperName b)
qn

-- |
-- Given an environment and a datatype or newtype name,
-- this function returns the associated data constructors if it is the case of a datatype
-- where: - ProperName is the name of the constructor (for example, "Nothing" in Maybe)
--        - [Type] is the list of arguments, if it has (for example, "Just" has [TypeVar "a"])
--
getConstructors :: Environment -> ModuleName -> Qualified (ProperName 'ConstructorName) -> [(ProperName 'ConstructorName, [SourceType])]
getConstructors :: Environment
-> ModuleName
-> Qualified (ProperName 'ConstructorName)
-> [(ProperName 'ConstructorName, [SourceType])]
getConstructors Environment
env ModuleName
defmn Qualified (ProperName 'ConstructorName)
n = Maybe (SourceType, TypeKind)
-> [(ProperName 'ConstructorName, [SourceType])]
extractConstructors Maybe (SourceType, TypeKind)
lnte
  where

  extractConstructors :: Maybe (SourceType, TypeKind) -> [(ProperName 'ConstructorName, [SourceType])]
  extractConstructors :: Maybe (SourceType, TypeKind)
-> [(ProperName 'ConstructorName, [SourceType])]
extractConstructors (Just (SourceType
_, DataType DataDeclType
_ [(Text, Maybe SourceType, Role)]
_ [(ProperName 'ConstructorName, [SourceType])]
pt)) = [(ProperName 'ConstructorName, [SourceType])]
pt
  extractConstructors Maybe (SourceType, TypeKind)
_ = forall a. HasCallStack => [Char] -> a
internalError [Char]
"Data name not in the scope of the current environment in extractConstructors"

  lnte :: Maybe (SourceType, TypeKind)
  lnte :: Maybe (SourceType, TypeKind)
lnte = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'TypeName)
qpn (Environment
-> Map (Qualified (ProperName 'TypeName)) (SourceType, TypeKind)
types Environment
env)

  qpn :: Qualified (ProperName 'TypeName)
  qpn :: Qualified (ProperName 'TypeName)
qpn = Qualified (ProperName 'ConstructorName)
-> Qualified (ProperName 'TypeName)
getConsDataName Qualified (ProperName 'ConstructorName)
n

  getConsDataName :: Qualified (ProperName 'ConstructorName) -> Qualified (ProperName 'TypeName)
  getConsDataName :: Qualified (ProperName 'ConstructorName)
-> Qualified (ProperName 'TypeName)
getConsDataName Qualified (ProperName 'ConstructorName)
con =
    case Qualified (ProperName 'ConstructorName)
-> Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
getConsInfo Qualified (ProperName 'ConstructorName)
con of
      Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
Nothing -> forall a. HasCallStack => [Char] -> a
internalError forall a b. (a -> b) -> a -> b
$ [Char]
"Constructor " forall a. [a] -> [a] -> [a]
++ Text -> [Char]
T.unpack (forall a. (a -> Text) -> Qualified a -> Text
showQualified forall (a :: ProperNameType). ProperName a -> Text
runProperName Qualified (ProperName 'ConstructorName)
con) forall a. [a] -> [a] -> [a]
++ [Char]
" not in the scope of the current environment in getConsDataName."
      Just (DataDeclType
_, ProperName 'TypeName
pm, SourceType
_, [Ident]
_) -> forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a
-> ModuleName
-> Qualified (ProperName b)
-> Qualified (ProperName a)
qualifyName ProperName 'TypeName
pm ModuleName
defmn Qualified (ProperName 'ConstructorName)
con

  getConsInfo :: Qualified (ProperName 'ConstructorName) -> Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
  getConsInfo :: Qualified (ProperName 'ConstructorName)
-> Maybe (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
getConsInfo Qualified (ProperName 'ConstructorName)
con = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Qualified (ProperName 'ConstructorName)
con (Environment
-> Map
     (Qualified (ProperName 'ConstructorName))
     (DataDeclType, ProperName 'TypeName, SourceType, [Ident])
dataConstructors Environment
env)

-- |
-- Replicates a wildcard binder
--
initialize :: Int -> [Binder]
initialize :: Int -> [Binder]
initialize Int
l = forall a. Int -> a -> [a]
replicate Int
l Binder
NullBinder

-- |
-- 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]
genericMerge :: forall a b c d.
Ord a =>
(a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]
genericMerge a -> Maybe b -> Maybe c -> d
_ [] [] = []
genericMerge a -> Maybe b -> Maybe c -> d
f [(a, b)]
bs [] = forall a b. (a -> b) -> [a] -> [b]
map (\(a
s, b
b) -> a -> Maybe b -> Maybe c -> d
f a
s (forall a. a -> Maybe a
Just b
b) forall a. Maybe a
Nothing) [(a, b)]
bs
genericMerge a -> Maybe b -> Maybe c -> d
f [] [(a, c)]
bs = forall a b. (a -> b) -> [a] -> [b]
map (\(a
s, c
b) -> a -> Maybe b -> Maybe c -> d
f a
s forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just c
b)) [(a, c)]
bs
genericMerge a -> Maybe b -> Maybe c -> d
f bsl :: [(a, b)]
bsl@((a
s, b
b):[(a, b)]
bs) bsr :: [(a, c)]
bsr@((a
s', c
b'):[(a, c)]
bs')
  | a
s forall a. Ord a => a -> a -> Bool
< a
s' = a -> Maybe b -> Maybe c -> d
f a
s (forall a. a -> Maybe a
Just b
b) forall a. Maybe a
Nothing forall a. a -> [a] -> [a]
: forall a b c d.
Ord a =>
(a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]
genericMerge a -> Maybe b -> Maybe c -> d
f [(a, b)]
bs [(a, c)]
bsr
  | a
s forall a. Ord a => a -> a -> Bool
> a
s' = a -> Maybe b -> Maybe c -> d
f a
s' forall a. Maybe a
Nothing (forall a. a -> Maybe a
Just c
b') forall a. a -> [a] -> [a]
: forall a b c d.
Ord a =>
(a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]
genericMerge a -> Maybe b -> Maybe c -> d
f [(a, b)]
bsl [(a, c)]
bs'
  | Bool
otherwise = a -> Maybe b -> Maybe c -> d
f a
s (forall a. a -> Maybe a
Just b
b) (forall a. a -> Maybe a
Just c
b') forall a. a -> [a] -> [a]
: forall a b c d.
Ord a =>
(a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]
genericMerge a -> Maybe b -> Maybe c -> d
f [(a, b)]
bs [(a, c)]
bs'

-- |
-- Find the uncovered set between two binders:
-- the first binder is the case we are trying to cover, the second one is the matching binder
--
missingCasesSingle :: Environment -> ModuleName -> Binder -> Binder -> ([Binder], Either RedundancyError Bool)
missingCasesSingle :: Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
_ ModuleName
_ Binder
_ Binder
NullBinder = ([], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
missingCasesSingle Environment
_ ModuleName
_ Binder
_ (VarBinder SourceSpan
_ Ident
_) = ([], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
missingCasesSingle Environment
env ModuleName
mn (VarBinder SourceSpan
_ Ident
_) Binder
b = Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
NullBinder Binder
b
missingCasesSingle Environment
env ModuleName
mn Binder
br (NamedBinder SourceSpan
_ Ident
_ Binder
bl) = Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
br Binder
bl
missingCasesSingle Environment
env ModuleName
mn Binder
NullBinder cb :: Binder
cb@(ConstructorBinder SourceSpan
ss Qualified (ProperName 'ConstructorName)
con [Binder]
_) =
  (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\Binder
cp -> forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
cp Binder
cb) [Binder]
allPatterns, forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
  where
  allPatterns :: [Binder]
allPatterns = forall a b. (a -> b) -> [a] -> [b]
map (\(ProperName 'ConstructorName
p, [SourceType]
t) -> SourceSpan
-> Qualified (ProperName 'ConstructorName) -> [Binder] -> Binder
ConstructorBinder SourceSpan
ss (forall (a :: ProperNameType) (b :: ProperNameType).
ProperName a
-> ModuleName
-> Qualified (ProperName b)
-> Qualified (ProperName a)
qualifyName ProperName 'ConstructorName
p ModuleName
mn Qualified (ProperName 'ConstructorName)
con) (Int -> [Binder]
initialize forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length [SourceType]
t))
                  forall a b. (a -> b) -> a -> b
$ Environment
-> ModuleName
-> Qualified (ProperName 'ConstructorName)
-> [(ProperName 'ConstructorName, [SourceType])]
getConstructors Environment
env ModuleName
mn Qualified (ProperName 'ConstructorName)
con
missingCasesSingle Environment
env ModuleName
mn cb :: Binder
cb@(ConstructorBinder SourceSpan
ss Qualified (ProperName 'ConstructorName)
con [Binder]
bs) (ConstructorBinder SourceSpan
_ Qualified (ProperName 'ConstructorName)
con' [Binder]
bs')
  | Qualified (ProperName 'ConstructorName)
con forall a. Eq a => a -> a -> Bool
== Qualified (ProperName 'ConstructorName)
con' = let ([[Binder]]
bs'', Either RedundancyError Bool
pr) = Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
mn [Binder]
bs [Binder]
bs' in (forall a b. (a -> b) -> [a] -> [b]
map (SourceSpan
-> Qualified (ProperName 'ConstructorName) -> [Binder] -> Binder
ConstructorBinder SourceSpan
ss Qualified (ProperName 'ConstructorName)
con) [[Binder]]
bs'', Either RedundancyError Bool
pr)
  | Bool
otherwise = ([Binder
cb], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
missingCasesSingle Environment
env ModuleName
mn Binder
NullBinder (LiteralBinder SourceSpan
ss (ObjectLiteral [(PSString, Binder)]
bs)) =
  (forall a b. (a -> b) -> [a] -> [b]
map (SourceSpan -> Literal Binder -> Binder
LiteralBinder SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(PSString, a)] -> Literal a
ObjectLiteral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(PSString, Binder)]
bs)) [[Binder]]
allMisses, Either RedundancyError Bool
pr)
  where
  ([[Binder]]
allMisses, Either RedundancyError Bool
pr) = Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
mn (Int -> [Binder]
initialize forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length [(PSString, Binder)]
bs) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(PSString, Binder)]
bs)
missingCasesSingle Environment
env ModuleName
mn (LiteralBinder SourceSpan
_ (ObjectLiteral [(PSString, Binder)]
bs)) (LiteralBinder SourceSpan
ss (ObjectLiteral [(PSString, Binder)]
bs')) =
  (forall a b. (a -> b) -> [a] -> [b]
map (SourceSpan -> Literal Binder -> Binder
LiteralBinder SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [(PSString, a)] -> Literal a
ObjectLiteral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip [PSString]
sortedNames) [[Binder]]
allMisses, Either RedundancyError Bool
pr)
  where
  ([[Binder]]
allMisses, Either RedundancyError Bool
pr) = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
mn) (forall a b. [(a, b)] -> ([a], [b])
unzip [(Binder, Binder)]
binders)

  sortNames :: [(PSString, b)] -> [(PSString, b)]
sortNames = forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst

  ([(PSString, Binder)]
sbs, [(PSString, Binder)]
sbs') = (forall {b}. [(PSString, b)] -> [(PSString, b)]
sortNames [(PSString, Binder)]
bs, forall {b}. [(PSString, b)] -> [(PSString, b)]
sortNames [(PSString, Binder)]
bs')

  compB :: a -> Maybe a -> Maybe a -> (a, a)
  compB :: forall a. a -> Maybe a -> Maybe a -> (a, a)
compB a
e Maybe a
b Maybe a
b' = (Maybe a -> a
fm Maybe a
b, Maybe a -> a
fm Maybe a
b')
    where
    fm :: Maybe a -> a
fm = forall a. a -> Maybe a -> a
fromMaybe a
e

  compBS :: b -> a -> Maybe b -> Maybe b -> (a, (b, b))
  compBS :: forall b a. b -> a -> Maybe b -> Maybe b -> (a, (b, b))
compBS b
e a
s Maybe b
b Maybe b
b' = (a
s, forall a. a -> Maybe a -> Maybe a -> (a, a)
compB b
e Maybe b
b Maybe b
b')

  ([PSString]
sortedNames, [(Binder, Binder)]
binders) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall a b c d.
Ord a =>
(a -> Maybe b -> Maybe c -> d) -> [(a, b)] -> [(a, c)] -> [d]
genericMerge (forall b a. b -> a -> Maybe b -> Maybe b -> (a, (b, b))
compBS Binder
NullBinder) [(PSString, Binder)]
sbs [(PSString, Binder)]
sbs'
missingCasesSingle Environment
_ ModuleName
_ Binder
NullBinder (LiteralBinder SourceSpan
ss (BooleanLiteral Bool
b)) = ([SourceSpan -> Literal Binder -> Binder
LiteralBinder SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bool -> Literal a
BooleanLiteral forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
missingCasesSingle Environment
_ ModuleName
_ (LiteralBinder SourceSpan
ss (BooleanLiteral Bool
bl)) (LiteralBinder SourceSpan
_ (BooleanLiteral Bool
br))
  | Bool
bl forall a. Eq a => a -> a -> Bool
== Bool
br = ([], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
  | Bool
otherwise = ([SourceSpan -> Literal Binder -> Binder
LiteralBinder SourceSpan
ss forall a b. (a -> b) -> a -> b
$ forall a. Bool -> Literal a
BooleanLiteral Bool
bl], forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
missingCasesSingle Environment
env ModuleName
mn Binder
b (PositionedBinder SourceSpan
_ [Comment]
_ Binder
cb) = Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
b Binder
cb
missingCasesSingle Environment
env ModuleName
mn Binder
b (TypedBinder SourceType
_ Binder
cb) = Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
b Binder
cb
missingCasesSingle Environment
_ ModuleName
_ Binder
b Binder
_ = ([Binder
b], forall a b. a -> Either a b
Left RedundancyError
Unknown)

-- |
-- Returns the uncovered set of binders
-- the first argument is the list of uncovered binders at step i
-- the second argument is the (i+1)th clause of a pattern matching definition
--
-- The idea of the algorithm is as follows:
-- it processes each binder of the two lists (say, `x` and `y`) one by one
-- at each step two cases arises:
--   - there are no missing cases between `x` and `y`: this is very straightforward, it continues with the remaining cases
--       but keeps the uncovered binder in its position.
--   - there are missing cases, let us call it the set `U`: on the one hand, we mix each new uncovered case in `U`
--       with the current tail of uncovered set. On the other hand, it continues with the remaining cases: here we
--       can use `x` (but it will generate overlapping cases), or `y`, which will generate non-overlapping cases.
--
--     As an example, consider:
--
--       data N = Z | S N
--       f Z Z = Z   --> {[S _, _], [Z, S _]} which are the right non-overlapping cases (GHC uses this).
--
--       if we use `x` instead of `y` (in this case, `y` stands for `Z` and `x` for `_`) we obtain:
--       f Z Z = Z   --> {[S _, _], [_, S _]} you can see that both cases overlaps each other.
--
--       Up to now, we've decided to use `x` just because we expect to generate uncovered cases which might be
--       redundant or not, but uncovered at least. If we use `y` instead, we'll need to have a redundancy checker
--       (which ought to be available soon), or increase the complexity of the algorithm.
--
missingCasesMultiple :: Environment -> ModuleName -> [Binder] -> [Binder] -> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple :: Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
mn = [Binder] -> [Binder] -> ([[Binder]], Either RedundancyError Bool)
go
  where
  go :: [Binder] -> [Binder] -> ([[Binder]], Either RedundancyError Bool)
go (Binder
x:[Binder]
xs) (Binder
y:[Binder]
ys) = (forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> [a] -> [a]
: [Binder]
xs) [Binder]
miss1 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Binder
x forall a. a -> [a] -> [a]
:) [[Binder]]
miss2, forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&) Either RedundancyError Bool
pr1 Either RedundancyError Bool
pr2)
    where
    ([Binder]
miss1, Either RedundancyError Bool
pr1) = Environment
-> ModuleName
-> Binder
-> Binder
-> ([Binder], Either RedundancyError Bool)
missingCasesSingle Environment
env ModuleName
mn Binder
x Binder
y
    ([[Binder]]
miss2, Either RedundancyError Bool
pr2) = [Binder] -> [Binder] -> ([[Binder]], Either RedundancyError Bool)
go [Binder]
xs [Binder]
ys
  go [Binder]
_ [Binder]
_ = ([], forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)

-- |
-- Guard handling
--
-- We say a guard is exhaustive iff it has an `otherwise` (or `true`) expression.
-- Example:
--   f x | x < 0 = 0
--       | otherwise = 1
--   is exhaustive, whereas `f x | x < 0` is not
--
-- or in case of a pattern guard if the pattern is exhaustive.
--
-- The function below say whether or not a guard has an `otherwise` expression
-- It is considered that `otherwise` is defined in Prelude
--
isExhaustiveGuard :: Environment -> ModuleName -> [GuardedExpr] -> Bool
isExhaustiveGuard :: Environment -> ModuleName -> [GuardedExpr] -> Bool
isExhaustiveGuard Environment
_ ModuleName
_ [MkUnguarded Expr
_] = Bool
True
isExhaustiveGuard Environment
env ModuleName
moduleName [GuardedExpr]
gs   =
  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(GuardedExpr [Guard]
grd Expr
_) -> [Guard] -> Bool
isExhaustive [Guard]
grd) [GuardedExpr]
gs
  where
    isExhaustive :: [Guard] -> Bool
    isExhaustive :: [Guard] -> Bool
isExhaustive = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Guard -> Bool
checkGuard

    checkGuard :: Guard -> Bool
    checkGuard :: Guard -> Bool
checkGuard (ConditionGuard Expr
cond)   = Expr -> Bool
isTrueExpr Expr
cond
    checkGuard (PatternGuard Binder
binder Expr
_) =
      case Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
moduleName [Binder
NullBinder] [Binder
binder] of
        ([], Either RedundancyError Bool
_) -> Bool
True -- there are no missing pattern for this guard
        ([[Binder]], Either RedundancyError Bool)
_       -> Bool
False

-- |
-- Returns the uncovered set of case alternatives
--
missingCases :: Environment -> ModuleName -> [Binder] -> CaseAlternative -> ([[Binder]], Either RedundancyError Bool)
missingCases :: Environment
-> ModuleName
-> [Binder]
-> CaseAlternative
-> ([[Binder]], Either RedundancyError Bool)
missingCases Environment
env ModuleName
mn [Binder]
uncovered CaseAlternative
ca = Environment
-> ModuleName
-> [Binder]
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingCasesMultiple Environment
env ModuleName
mn [Binder]
uncovered (CaseAlternative -> [Binder]
caseAlternativeBinders CaseAlternative
ca)

missingAlternative :: Environment -> ModuleName -> CaseAlternative -> [Binder] -> ([[Binder]], Either RedundancyError Bool)
missingAlternative :: Environment
-> ModuleName
-> CaseAlternative
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingAlternative Environment
env ModuleName
mn CaseAlternative
ca [Binder]
uncovered
  | Environment -> ModuleName -> [GuardedExpr] -> Bool
isExhaustiveGuard Environment
env ModuleName
mn (CaseAlternative -> [GuardedExpr]
caseAlternativeResult CaseAlternative
ca) = ([[Binder]], Either RedundancyError Bool)
mcases
  | Bool
otherwise = ([[Binder]
uncovered], forall a b. (a, b) -> b
snd ([[Binder]], Either RedundancyError Bool)
mcases)
  where
  mcases :: ([[Binder]], Either RedundancyError Bool)
mcases = Environment
-> ModuleName
-> [Binder]
-> CaseAlternative
-> ([[Binder]], Either RedundancyError Bool)
missingCases Environment
env ModuleName
mn [Binder]
uncovered CaseAlternative
ca

-- |
-- Main exhaustivity checking function
-- Starting with the set `uncovered = { _ }` (nothing covered, one `_` for each function argument),
-- it partitions that set with the new uncovered cases, until it consumes the whole set of clauses.
-- Then, returns the uncovered set of case alternatives.
--
checkExhaustive
  :: forall m
   . MonadWriter MultipleErrors m
   => SourceSpan
   -> Environment
   -> ModuleName
   -> Int
   -> [CaseAlternative]
   -> Expr
   -> m Expr
checkExhaustive :: forall (m :: * -> *).
MonadWriter MultipleErrors m =>
SourceSpan
-> Environment
-> ModuleName
-> Int
-> [CaseAlternative]
-> Expr
-> m Expr
checkExhaustive SourceSpan
ss Environment
env ModuleName
mn Int
numArgs [CaseAlternative]
cas Expr
expr = ([[Binder]], (Either RedundancyError Bool, [[Binder]])) -> m Expr
makeResult forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first forall a. Ord a => [a] -> [a]
ordNub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ([[Binder]], (Either RedundancyError Bool, [[Binder]]))
-> CaseAlternative
-> ([[Binder]], (Either RedundancyError Bool, [[Binder]]))
step ([Int -> [Binder]
initialize Int
numArgs], (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True, [])) [CaseAlternative]
cas
  where
  step :: ([[Binder]], (Either RedundancyError Bool, [[Binder]])) -> CaseAlternative -> ([[Binder]], (Either RedundancyError Bool, [[Binder]]))
  step :: ([[Binder]], (Either RedundancyError Bool, [[Binder]]))
-> CaseAlternative
-> ([[Binder]], (Either RedundancyError Bool, [[Binder]]))
step ([[Binder]]
uncovered, (Either RedundancyError Bool
nec, [[Binder]]
redundant)) CaseAlternative
ca =
    let ([[[Binder]]]
missed, [Either RedundancyError Bool]
pr) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall a b. (a -> b) -> [a] -> [b]
map (Environment
-> ModuleName
-> CaseAlternative
-> [Binder]
-> ([[Binder]], Either RedundancyError Bool)
missingAlternative Environment
env ModuleName
mn CaseAlternative
ca) [[Binder]]
uncovered)
        ([[Binder]]
missed', [[Binder]]
approx) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
10000 (forall a. Ord a => [a] -> [a]
ordNub (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[Binder]]]
missed))
        cond :: Either RedundancyError Bool
cond = forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA [Either RedundancyError Bool]
pr
    in ([[Binder]]
missed', ( if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Binder]]
approx
                     then forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> Bool
(&&) Either RedundancyError Bool
cond Either RedundancyError Bool
nec
                     else forall a b. a -> Either a b
Left RedundancyError
Incomplete
                 , if forall (t :: * -> *). Foldable t => t Bool -> Bool
and Either RedundancyError Bool
cond
                     then [[Binder]]
redundant
                     else CaseAlternative -> [Binder]
caseAlternativeBinders CaseAlternative
ca forall a. a -> [a] -> [a]
: [[Binder]]
redundant
                 )
       )

  makeResult :: ([[Binder]], (Either RedundancyError Bool, [[Binder]])) -> m Expr
  makeResult :: ([[Binder]], (Either RedundancyError Bool, [[Binder]])) -> m Expr
makeResult ([[Binder]]
bss, (Either RedundancyError Bool
rr, [[Binder]]
bss')) =
    do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Binder]]
bss') m ()
tellRedundant
       case Either RedundancyError Bool
rr of
         Left RedundancyError
Incomplete -> m ()
tellIncomplete
         Either RedundancyError Bool
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Binder]]
bss
         then Expr
expr
         else ([[Binder]], Bool) -> Expr -> Expr
addPartialConstraint (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. Int -> [a] -> ([a], [a])
splitAt Int
5 [[Binder]]
bss)) Expr
expr
    where
      tellRedundant :: m ()
tellRedundant = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [[Binder]] -> Bool -> SimpleErrorMessage
OverlappingPattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> ([a], [a])
splitAt Int
5 forall a b. (a -> b) -> a -> b
$ [[Binder]]
bss'
      tellIncomplete :: m ()
tellIncomplete = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> SimpleErrorMessage -> MultipleErrors
errorMessage' SourceSpan
ss forall a b. (a -> b) -> a -> b
$ SimpleErrorMessage
IncompleteExhaustivityCheck

  -- We add a Partial constraint by annotating the expression to have type `Partial => _`.
  --
  -- The binder information is provided so that it can be embedded in the constraint,
  -- and then included in the error message.
  addPartialConstraint :: ([[Binder]], Bool) -> Expr -> Expr
  addPartialConstraint :: ([[Binder]], Bool) -> Expr -> Expr
addPartialConstraint ([[Binder]]
bss, Bool
complete) Expr
e =
    Bool -> Expr -> SourceType -> Expr
TypedValue Bool
True Expr
e forall a b. (a -> b) -> a -> b
$
      SourceConstraint -> SourceType -> SourceType
srcConstrainedType (Qualified (ProperName 'ClassName)
-> [SourceType]
-> [SourceType]
-> Maybe ConstraintData
-> SourceConstraint
srcConstraint Qualified (ProperName 'ClassName)
C.Partial [] [] (forall a. a -> Maybe a
Just ConstraintData
constraintData)) forall a b. (a -> b) -> a -> b
$ forall a. a -> WildcardData -> Type a
TypeWildcard SourceAnn
NullSourceAnn WildcardData
IgnoredWildcard
    where
      constraintData :: ConstraintData
      constraintData :: ConstraintData
constraintData =
        [[Text]] -> Bool -> ConstraintData
PartialConstraintData (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map Binder -> Text
prettyPrintBinderAtom) [[Binder]]
bss) Bool
complete

-- |
-- Exhaustivity checking
--
checkExhaustiveExpr
  :: forall m
   . MonadWriter MultipleErrors m
   => SourceSpan
   -> Environment
   -> ModuleName
   -> Expr
   -> m Expr
checkExhaustiveExpr :: forall (m :: * -> *).
MonadWriter MultipleErrors m =>
SourceSpan -> Environment -> ModuleName -> Expr -> m Expr
checkExhaustiveExpr SourceSpan
ss Environment
env ModuleName
mn = Expr -> m Expr
onExpr'
  where
  (Declaration -> m Declaration
_, Expr -> m Expr
onExpr', Binder -> m Binder
_) = forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration)
-> (Expr -> m Expr)
-> (Binder -> m Binder)
-> (Declaration -> m Declaration, Expr -> m Expr,
    Binder -> m Binder)
everywhereOnValuesM forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr -> m Expr
onExpr forall (f :: * -> *) a. Applicative f => a -> f a
pure

  onExpr :: Expr -> m Expr
  onExpr :: Expr -> m Expr
onExpr Expr
e = case Expr
e of
    Case [Expr]
es [CaseAlternative]
cas ->
      forall (m :: * -> *).
MonadWriter MultipleErrors m =>
SourceSpan
-> Environment
-> ModuleName
-> Int
-> [CaseAlternative]
-> Expr
-> m Expr
checkExhaustive SourceSpan
ss Environment
env ModuleName
mn (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es) [CaseAlternative]
cas Expr
e
    Expr
_ ->
      forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e