@@ -0,0 +1,275 @@
1+-----------------------------------------------------------------------------
3+-- Module : Language.PureScript.Exhaustive
4+-- Copyright : (c) 2013-14 Phil Freeman, (c) 2014 Gary Burgess, and other contributors
7+-- Maintainer : Phil Freeman <paf31@cantab.net>
8+-- Stability : experimental
12+-- | Module for exhaustivity checking over pattern matching definitions
13+-- | The algorithm analyses the clauses of a definition one by one from top
14+-- | to bottom, where in each step it has the cases already missing (uncovered),
15+-- | and it generates the new set of missing cases.
17+-----------------------------------------------------------------------------
19+{-# LANGUAGE FlexibleContexts #-}
20+{-# LANGUAGE ScopedTypeVariables #-}
22+module Language.PureScript.Linter.Exhaustive
24+ , checkExhaustiveModule
27+import qualified Data.Map as M
28+import Data.Maybe (fromMaybe)
29+import Data.List (foldl', sortBy, nub)
30+import Data.Function (on)
32+import Control.Monad (unless)
33+import Control.Applicative
34+import Control.Monad.Writer.Class
36+import Language.PureScript.AST.Binders
37+import Language.PureScript.AST.Declarations
38+import Language.PureScript.Environment
39+import Language.PureScript.Names as P
40+import Language.PureScript.Kinds
41+import Language.PureScript.Types as P
42+import Language.PureScript.Errors
44+import Language.PureScript.AST.Traversals (everywhereOnValuesTopDownM)
47+-- Qualifies a propername from a given qualified propername and a default module name
49+qualifyName :: a -> ModuleName -> Qualified a -> Qualified a
50+qualifyName n defmn qn = Qualified (Just mn) n
52+ (mn, _) = qualify defmn qn
55+-- Given an environment and a datatype or newtype name,
56+-- this function returns the associated data constructors if it is the case of a datatype
57+-- where: - ProperName is the name of the constructor (for example, "Nothing" in Maybe)
58+-- - [Type] is the list of arguments, if it has (for example, "Just" has [TypeVar "a"])
60+getConstructors :: Environment -> ModuleName -> (Qualified ProperName) -> [(ProperName, [Type])]
61+getConstructors env defmn n = extractConstructors lnte
63+ qpn :: Qualified ProperName
64+ qpn = getConsDataName n
66+ getConsDataName :: (Qualified ProperName) -> (Qualified ProperName)
67+ getConsDataName con = qualifyName nm defmn con
69+ nm = case getConsInfo con of
70+ Nothing -> error $ "ProperName " ++ show con ++ " not in the scope of the current environment in getConsDataName."
71+ Just (_, pm, _, _) -> pm
73+ getConsInfo :: (Qualified ProperName) -> Maybe (DataDeclType, ProperName, Type, [Ident])
74+ getConsInfo con = M.lookup con dce
76+ dce :: M.Map (Qualified ProperName) (DataDeclType, ProperName, Type, [Ident])
77+ dce = dataConstructors env
79+ lnte :: Maybe (Kind, TypeKind)
80+ lnte = M.lookup qpn (types env)
82+ extractConstructors :: Maybe (Kind, TypeKind) -> [(ProperName, [Type])]
83+ extractConstructors (Just (_, DataType _ pt)) = pt
84+ extractConstructors _ = error "Data name not in the scope of the current environment in extractConstructors"
87+-- Replicates a wildcard binder
89+initialize :: Int -> [Binder]
90+initialize l = replicate l NullBinder
93+-- Applies a function over two lists of tuples that may lack elements
95+genericMerge :: Ord a =>
96+ (a -> Maybe b -> Maybe c -> d) ->
100+genericMerge _ [] [] = []
101+genericMerge f bs [] = map (\(s, b) -> f s (Just b) Nothing) bs
102+genericMerge f [] bs = map (\(s, b) -> f s Nothing (Just b)) bs
103+genericMerge f bsl@((s, b):bs) bsr@((s', b'):bs')
104+ | s < s' = (f s (Just b) Nothing) : genericMerge f bs bsr
105+ | s > s' = (f s' Nothing (Just b')) : genericMerge f bsl bs'
106+ | otherwise = (f s (Just b) (Just b')) : genericMerge f bs bs'
109+-- Find the uncovered set between two binders:
110+-- the first binder is the case we are trying to cover the second one is the matching binder
112+missingCasesSingle :: Environment -> ModuleName -> Binder -> Binder -> [Binder]
113+missingCasesSingle _ _ _ NullBinder = []
114+missingCasesSingle _ _ _ (VarBinder _) = []
115+missingCasesSingle env mn (VarBinder _) b = missingCasesSingle env mn NullBinder b
116+missingCasesSingle env mn br (NamedBinder _ bl) = missingCasesSingle env mn br bl
117+missingCasesSingle env mn NullBinder cb@(ConstructorBinder con _) =
118+ concatMap (\cp -> missingCasesSingle env mn cp cb) allPatterns
120+ allPatterns = map (\(p, t) -> ConstructorBinder (qualifyName p mn con) (initialize $ length t))
121+ $ getConstructors env mn con
122+missingCasesSingle env mn cb@(ConstructorBinder con bs) (ConstructorBinder con' bs')
123+ | con == con' = map (ConstructorBinder con) (missingCasesMultiple env mn bs bs')
125+missingCasesSingle _ _ NullBinder (ArrayBinder bs)
128+missingCasesSingle env mn NullBinder (ObjectBinder bs) =
129+ map (ObjectBinder . zip (map fst bs)) allMisses
131+ allMisses = missingCasesMultiple env mn (initialize $ length bs) (map snd bs)
132+missingCasesSingle env mn (ObjectBinder bs) (ObjectBinder bs') =
133+ map (ObjectBinder . zip sortedNames) $ uncurry (missingCasesMultiple env mn) (unzip binders)
135+ sortNames = sortBy (compare `on` fst)
137+ (sbs, sbs') = (sortNames bs, sortNames bs')
139+ compB :: a -> Maybe a -> Maybe a -> (a, a)
140+ compB e b b' = (fm b, fm b')
144+ compBS :: Eq a => b -> a -> Maybe b -> Maybe b -> (a, (b, b))
145+ compBS e s b b' = (s, compB e b b')
147+ (sortedNames, binders) = unzip $ genericMerge (compBS NullBinder) sbs sbs'
148+missingCasesSingle _ _ NullBinder (BooleanBinder b) = [BooleanBinder $ not b]
149+missingCasesSingle _ _ (BooleanBinder bl) (BooleanBinder br)
151+ | otherwise = [BooleanBinder bl]
152+missingCasesSingle env mn b (PositionedBinder _ _ cb) = missingCasesSingle env mn b cb
153+missingCasesSingle _ _ b _ = [b]
156+-- Returns the uncovered set of binders
157+-- the first argument is the list of uncovered binders at step i
158+-- the second argument is the (i+1)th clause of a pattern matching definition
160+-- The idea of the algorithm is as follows:
161+-- it processes each binder of the two lists (say, `x` and `y`) one by one
162+-- at each step two cases arises:
163+-- - there are no missing cases between `x` and `y`: this is very straightforward, it continues with the remaining cases
164+-- but keeps the uncovered binder in its position.
165+-- - there are missing cases, let us call it the set `U`: on the one hand, we mix each new uncovered case in `U`
166+-- with the current tail of uncovered set. On the other hand, it continues with the remaining cases: here we
167+-- can use `x` (but it will generate overlapping cases), or `y`, which will generate non-overlapping cases.
169+-- As an example, consider:
172+-- f Z Z = Z --> {[S _, _], [Z, S _]} which are the right non-overlapping cases (GHC uses this).
174+-- if we use `x` instead of `y` (in this case, `y` stands for `Z` and `x` for `_`) we obtain:
175+-- f Z Z = Z --> {[S _, _], [_, S _]} you can see that both cases overlaps each other.
177+-- Up to now, we've decided to use `x` just because we expect to generate uncovered cases which might be
178+-- redundant or not, but uncovered at least. If we use `y` instead, we'll need to have a redundancy checker
179+-- (which ought to be available soon), or increase the complexity of the algorithm.
181+missingCasesMultiple :: Environment -> ModuleName -> [Binder] -> [Binder] -> [[Binder]]
182+missingCasesMultiple env mn = go
186+ | null miss = map (x :) (go xs ys)
187+ | otherwise = map (: xs) miss ++ map (x :) (go xs ys)
189+ miss = missingCasesSingle env mn x y
190+ go _ _ = error "Argument lengths did not match in missingCasesMultiple."
195+-- We say a guard is exhaustive iff it has an `otherwise` (or `true`) expression.
199+-- is exhaustive, whereas `f x | x < 0` is not
201+-- The function below say whether or not a guard has an `otherwise` expression
202+-- It is considered that `otherwise` is defined in Prelude
204+isExhaustiveGuard :: Either [(Guard, Expr)] Expr -> Bool
205+isExhaustiveGuard (Left gs) = not . null $ filter (\(g, _) -> isOtherwise g) gs
207+ isOtherwise :: Expr -> Bool
208+ isOtherwise (TypedValue _ (BooleanLiteral True) _) = True
209+ isOtherwise (TypedValue _ (Var (Qualified (Just (ModuleName [ProperName "Prelude"])) (Ident "otherwise"))) _) = True
210+ isOtherwise _ = False
211+isExhaustiveGuard (Right _) = True
214+-- Returns the uncovered set of case alternatives
216+missingCases :: Environment -> ModuleName -> [Binder] -> CaseAlternative -> [[Binder]]
217+missingCases env mn uncovered ca = missingCasesMultiple env mn uncovered (caseAlternativeBinders ca)
219+missingAlternative :: Environment -> ModuleName -> CaseAlternative -> [Binder] -> [[Binder]]
220+missingAlternative env mn ca uncovered
221+ | isExhaustiveGuard (caseAlternativeResult ca) = missingCases env mn uncovered ca
222+ | otherwise = [uncovered]
225+-- Main exhaustivity checking function
226+-- Starting with the set `uncovered = { _ }` (nothing covered, one `_` for each function argument),
227+-- it partitions that set with the new uncovered cases, until it consumes the whole set of clauses.
228+-- Then, returns the uncovered set of case alternatives.
230+checkExhaustive :: forall m. (MonadWriter MultipleErrors m) => Environment -> ModuleName -> [CaseAlternative] -> m ()
231+checkExhaustive env mn cas = makeResult . nub $ foldl' step [initial] cas
233+ step :: [[Binder]] -> CaseAlternative -> [[Binder]]
234+ step uncovered ca = concatMap (missingAlternative env mn ca) uncovered
237+ initial = initialize numArgs
239+ numArgs = length . caseAlternativeBinders . head $ cas
241+ makeResult :: [[Binder]] -> m ()
242+ makeResult bss = unless (null bss) tellWarning
244+ tellWarning = tell . errorMessage $ NotExhaustivePattern bss
247+-- Exhaustivity checking over a list of declarations
249+checkExhaustiveDecls :: forall m. (Applicative m, MonadWriter MultipleErrors m) => Environment -> ModuleName -> [Declaration] -> m ()
250+checkExhaustiveDecls env mn ds =
251+ let (f, _, _) = everywhereOnValuesTopDownM return checkExpr return
253+ f' :: Declaration -> m Declaration
254+ f' d@(BindingGroupDeclaration bs) = mapM_ (f' . convert) bs >> return d
256+ convert :: (Ident, NameKind, Expr) -> Declaration
257+ convert (name, nk, e) = ValueDeclaration name nk [] (Right e)
258+ f' d@(ValueDeclaration name _ _ _) = censor (onErrorMessages (ErrorInValueDeclaration name)) $ f d
259+ f' (PositionedDeclaration pos com dec) = PositionedDeclaration pos com <$> censor (onErrorMessages (PositionedError pos)) (f' dec)
260+ -- Don't generate two warnings for desugared dictionaries.
261+ f' d@TypeInstanceDeclaration{} = return d
266+ checkExpr :: Expr -> m Expr
267+ checkExpr c@(Case _ cas) = checkExhaustive env mn cas >> return c
268+ checkExpr other = return other
271+-- Exhaustivity checking over a single module
273+checkExhaustiveModule :: forall m. (Applicative m, MonadWriter MultipleErrors m) => Environment -> Module -> m ()
274+checkExhaustiveModule env (Module _ mn ds _) = censor (onErrorMessages (ErrorInModule mn)) $ checkExhaustiveDecls env mn ds