@@ -0,0 +1,275 @@
1+-----------------------------------------------------------------------------
2+--
3+-- Module : Language.PureScript.Exhaustive
4+-- Copyright : (c) 2013-14 Phil Freeman, (c) 2014 Gary Burgess, and other contributors
5+-- License : MIT
6+--
7+-- Maintainer : Phil Freeman <paf31@cantab.net>
8+-- Stability : experimental
9+-- Portability :
10+--
11+-- |
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.
16+--
17+-----------------------------------------------------------------------------
18+
19+{-# LANGUAGE FlexibleContexts #-}
20+{-# LANGUAGE ScopedTypeVariables #-}
21+
22+module Language.PureScript.Linter.Exhaustive
23+ ( checkExhaustive
24+ , checkExhaustiveModule
25+ ) where
26+
27+import qualified Data.Map as M
28+import Data.Maybe (fromMaybe)
29+import Data.List (foldl', sortBy, nub)
30+import Data.Function (on)
31+
32+import Control.Monad (unless)
33+import Control.Applicative
34+import Control.Monad.Writer.Class
35+
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
43+
44+import Language.PureScript.AST.Traversals (everywhereOnValuesTopDownM)
45+
46+-- |
47+-- Qualifies a propername from a given qualified propername and a default module name
48+--
49+qualifyName :: a -> ModuleName -> Qualified a -> Qualified a
50+qualifyName n defmn qn = Qualified (Just mn) n
51+ where
52+ (mn, _) = qualify defmn qn
53+
54+-- |
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"])
59+--
60+getConstructors :: Environment -> ModuleName -> (Qualified ProperName) -> [(ProperName, [Type])]
61+getConstructors env defmn n = extractConstructors lnte
62+ where
63+ qpn :: Qualified ProperName
64+ qpn = getConsDataName n
65+
66+ getConsDataName :: (Qualified ProperName) -> (Qualified ProperName)
67+ getConsDataName con = qualifyName nm defmn con
68+ where
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
72+
73+ getConsInfo :: (Qualified ProperName) -> Maybe (DataDeclType, ProperName, Type, [Ident])
74+ getConsInfo con = M.lookup con dce
75+ where
76+ dce :: M.Map (Qualified ProperName) (DataDeclType, ProperName, Type, [Ident])
77+ dce = dataConstructors env
78+
79+ lnte :: Maybe (Kind, TypeKind)
80+ lnte = M.lookup qpn (types env)
81+
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"
85+
86+-- |
87+-- Replicates a wildcard binder
88+--
89+initialize :: Int -> [Binder]
90+initialize l = replicate l NullBinder
91+
92+-- |
93+-- Applies a function over two lists of tuples that may lack elements
94+--
95+genericMerge :: Ord a =>
96+ (a -> Maybe b -> Maybe c -> d) ->
97+ [(a, b)] ->
98+ [(a, c)] ->
99+ [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'
107+
108+-- |
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
111+--
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
119+ where
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')
124+ | otherwise = [cb]
125+missingCasesSingle _ _ NullBinder (ArrayBinder bs)
126+ | null bs = []
127+ | otherwise = []
128+missingCasesSingle env mn NullBinder (ObjectBinder bs) =
129+ map (ObjectBinder . zip (map fst bs)) allMisses
130+ where
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)
134+ where
135+ sortNames = sortBy (compare `on` fst)
136+
137+ (sbs, sbs') = (sortNames bs, sortNames bs')
138+
139+ compB :: a -> Maybe a -> Maybe a -> (a, a)
140+ compB e b b' = (fm b, fm b')
141+ where
142+ fm = fromMaybe e
143+
144+ compBS :: Eq a => b -> a -> Maybe b -> Maybe b -> (a, (b, b))
145+ compBS e s b b' = (s, compB e b b')
146+
147+ (sortedNames, binders) = unzip $ genericMerge (compBS NullBinder) sbs sbs'
148+missingCasesSingle _ _ NullBinder (BooleanBinder b) = [BooleanBinder $ not b]
149+missingCasesSingle _ _ (BooleanBinder bl) (BooleanBinder br)
150+ | bl == br = []
151+ | otherwise = [BooleanBinder bl]
152+missingCasesSingle env mn b (PositionedBinder _ _ cb) = missingCasesSingle env mn b cb
153+missingCasesSingle _ _ b _ = [b]
154+
155+-- |
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
159+--
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.
168+--
169+-- As an example, consider:
170+--
171+-- data N = Z | S N
172+-- f Z Z = Z --> {[S _, _], [Z, S _]} which are the right non-overlapping cases (GHC uses this).
173+--
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.
176+--
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.
180+--
181+missingCasesMultiple :: Environment -> ModuleName -> [Binder] -> [Binder] -> [[Binder]]
182+missingCasesMultiple env mn = go
183+ where
184+ go [] _ = []
185+ go (x:xs) (y:ys)
186+ | null miss = map (x :) (go xs ys)
187+ | otherwise = map (: xs) miss ++ map (x :) (go xs ys)
188+ where
189+ miss = missingCasesSingle env mn x y
190+ go _ _ = error "Argument lengths did not match in missingCasesMultiple."
191+
192+-- |
193+-- Guard handling
194+--
195+-- We say a guard is exhaustive iff it has an `otherwise` (or `true`) expression.
196+-- Example:
197+-- f x | x < 0 = 0
198+-- | otherwise = 1
199+-- is exhaustive, whereas `f x | x < 0` is not
200+--
201+-- The function below say whether or not a guard has an `otherwise` expression
202+-- It is considered that `otherwise` is defined in Prelude
203+--
204+isExhaustiveGuard :: Either [(Guard, Expr)] Expr -> Bool
205+isExhaustiveGuard (Left gs) = not . null $ filter (\(g, _) -> isOtherwise g) gs
206+ where
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
212+
213+-- |
214+-- Returns the uncovered set of case alternatives
215+--
216+missingCases :: Environment -> ModuleName -> [Binder] -> CaseAlternative -> [[Binder]]
217+missingCases env mn uncovered ca = missingCasesMultiple env mn uncovered (caseAlternativeBinders ca)
218+
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]
223+
224+-- |
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.
229+--
230+checkExhaustive :: forall m. (MonadWriter MultipleErrors m) => Environment -> ModuleName -> [CaseAlternative] -> m ()
231+checkExhaustive env mn cas = makeResult . nub $ foldl' step [initial] cas
232+ where
233+ step :: [[Binder]] -> CaseAlternative -> [[Binder]]
234+ step uncovered ca = concatMap (missingAlternative env mn ca) uncovered
235+
236+ initial :: [Binder]
237+ initial = initialize numArgs
238+ where
239+ numArgs = length . caseAlternativeBinders . head $ cas
240+
241+ makeResult :: [[Binder]] -> m ()
242+ makeResult bss = unless (null bss) tellWarning
243+ where
244+ tellWarning = tell . errorMessage $ NotExhaustivePattern bss
245+
246+-- |
247+-- Exhaustivity checking over a list of declarations
248+--
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
252+
253+ f' :: Declaration -> m Declaration
254+ f' d@(BindingGroupDeclaration bs) = mapM_ (f' . convert) bs >> return d
255+ where
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
262+ f' d = f d
263+
264+ in mapM_ f' ds
265+ where
266+ checkExpr :: Expr -> m Expr
267+ checkExpr c@(Case _ cas) = checkExhaustive env mn cas >> return c
268+ checkExpr other = return other
269+
270+-- |
271+-- Exhaustivity checking over a single module
272+--
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
275+