git.iko.soy/elk
on 785bc76 help sign in
elk/src/Nitpick/PatternMatches.hs
641 lines 14 kB history raw
1{-# OPTIONS_GHC -Wall #-}
2{-# LANGUAGE OverloadedStrings #-}
3module Nitpick.PatternMatches
4 ( check
5 , Error(..)
6 , Context(..)
7 , Pattern(..)
8 , Literal(..)
9 )
10 where
13{- The algorithm used here comes from "Warnings for Pattern Matching"
14by Luc Maranget. Check it out for more information!
16http://moscova.inria.fr/~maranget/papers/warn/warn.pdf
18-}
20import qualified Data.List as List
21import qualified Data.Map as Map
22import qualified Data.Maybe as Maybe
23import qualified Data.Text as Text
25import qualified AST.Canonical as Can
26import qualified AST.Module.Name as ModuleName
27import qualified Data.Index as Index
28import qualified Elm.Name as N
29import qualified Reporting.Annotation as A
30import qualified Reporting.Region as R
34-- PATTERN
37data Pattern
38 = Anything
39 | Literal Literal
40 | Ctor Can.Union N.Name [Pattern]
43data Literal
44 = Chr Text.Text
45 | Str Text.Text
46 | Int Int
47 deriving (Eq)
51-- CREATE SIMPLIFIED PATTERNS
54simplify :: Can.Pattern -> Pattern
55simplify (A.At _ pattern) =
56 case pattern of
57 Can.PAnything ->
58 Anything
60 Can.PVar _ ->
61 Anything
63 Can.PRecord _ ->
64 Anything
66 Can.PUnit ->
67 Ctor unit unitName []
69 Can.PTuple a b Nothing ->
70 Ctor pair pairName [ simplify a, simplify b ]
72 Can.PTuple a b (Just c) ->
73 Ctor triple tripleName [ simplify a, simplify b, simplify c ]
75 Can.PCtor _ _ union name _ args ->
76 Ctor union name $
77 map (\(Can.PatternCtorArg _ _ arg) -> simplify arg) args
79 Can.PList entries ->
80 foldr cons nil entries
82 Can.PCons hd tl ->
83 cons hd (simplify tl)
85 Can.PAlias subPattern _ ->
86 simplify subPattern
88 Can.PInt int ->
89 Literal (Int int)
91 Can.PStr str ->
92 Literal (Str str)
94 Can.PChr chr ->
95 Literal (Chr chr)
98cons :: Can.Pattern -> Pattern -> Pattern
99cons hd tl =
100 Ctor list consName [ simplify hd, tl ]
103{-# NOINLINE nil #-}
104nil :: Pattern
105nil =
106 Ctor list nilName []
110-- BUILT-IN UNIONS
113{-# NOINLINE unit #-}
114unit :: Can.Union
115unit =
116 let
117 ctor =
118 Can.Ctor unitName Index.first 0 []
119 in
120 Can.Union [] [ ctor ] 1 Can.Normal
123{-# NOINLINE pair #-}
124pair :: Can.Union
125pair =
126 let
127 ctor =
128 Can.Ctor pairName Index.first 2 [Can.TVar "a", Can.TVar "b"]
129 in
130 Can.Union ["a","b"] [ ctor ] 1 Can.Normal
133{-# NOINLINE triple #-}
134triple :: Can.Union
135triple =
136 let
137 ctor =
138 Can.Ctor tripleName Index.first 3 [Can.TVar "a", Can.TVar "b", Can.TVar "c"]
139 in
140 Can.Union ["a","b","c"] [ ctor ] 1 Can.Normal
143{-# NOINLINE list #-}
144list :: Can.Union
145list =
146 let
147 nilCtor =
148 Can.Ctor nilName Index.first 0 []
150 consCtor =
151 Can.Ctor consName Index.second 2
152 [ Can.TVar "a"
153 , Can.TType ModuleName.list N.list [Can.TVar "a"]
154 ]
155 in
156 Can.Union ["a"] [ nilCtor, consCtor ] 2 Can.Normal
159{-# NOINLINE unitName #-}
160unitName :: N.Name
161unitName = "#0"
164{-# NOINLINE pairName #-}
165pairName :: N.Name
166pairName = "#2"
169{-# NOINLINE tripleName #-}
170tripleName :: N.Name
171tripleName = "#3"
174{-# NOINLINE consName #-}
175consName :: N.Name
176consName = "::"
179{-# NOINLINE nilName #-}
180nilName :: N.Name
181nilName = "[]"
185-- ERROR
188data Error
189 = Incomplete R.Region Context [Pattern]
190 | Redundant R.Region R.Region Int
193data Context
194 = BadArg
195 | BadDestruct
196 | BadCase
200-- CHECK
203check :: Can.Module -> Either [Error] ()
204check (Can.Module _ _ _ decls _ _ _ _) =
205 case checkDecls decls [] of
206 [] ->
207 Right ()
209 errors ->
210 Left errors
214-- CHECK DECLS
217checkDecls :: Can.Decls -> [Error] -> [Error]
218checkDecls decls errors =
219 case decls of
220 Can.Declare def subDecls ->
221 checkDef def $ checkDecls subDecls errors
223 Can.DeclareRec defs subDecls ->
224 foldr checkDef (checkDecls subDecls errors) defs
226 Can.SaveTheEnvironment ->
227 errors
231-- CHECK DEFS
234checkDef :: Can.Def -> [Error] -> [Error]
235checkDef def errors =
236 case def of
237 Can.Def _ args body ->
238 foldr checkArg (checkExpr body errors) args
240 Can.TypedDef _ _ args body _ ->
241 foldr checkTypedArg (checkExpr body errors) args
244checkArg :: Can.Pattern -> [Error] -> [Error]
245checkArg pattern@(A.At region _) errors =
246 checkPatterns region BadArg [pattern] errors
249checkTypedArg :: (Can.Pattern, tipe) -> [Error] -> [Error]
250checkTypedArg (pattern@(A.At region _), _) errors =
251 checkPatterns region BadArg [pattern] errors
255-- CHECK EXPRESSIONS
258checkExpr :: Can.Expr -> [Error] -> [Error]
259checkExpr (A.At region expression) errors =
260 case expression of
261 Can.VarLocal _ ->
262 errors
264 Can.VarTopLevel _ _ ->
265 errors
267 Can.VarKernel _ _ ->
268 errors
270 Can.VarForeign _ _ _ ->
271 errors
273 Can.VarCtor _ _ _ _ _ ->
274 errors
276 Can.VarDebug _ _ _ ->
277 errors
279 Can.VarOperator _ _ _ _ ->
280 errors
282 Can.Chr _ ->
283 errors
285 Can.Str _ ->
286 errors
288 Can.Int _ ->
289 errors
291 Can.Float _ ->
292 errors
294 Can.List entries ->
295 foldr checkExpr errors entries
297 Can.Negate expr ->
298 checkExpr expr errors
300 Can.Binop _ _ _ _ left right ->
301 checkExpr left $
302 checkExpr right errors
304 Can.Lambda args body ->
305 foldr checkArg (checkExpr body errors) args
307 Can.Call func args ->
308 checkExpr func $ foldr checkExpr errors args
310 Can.If branches finally ->
311 foldr checkIfBranch (checkExpr finally errors) branches
313 Can.Let def body ->
314 checkDef def $ checkExpr body errors
316 Can.LetRec defs body ->
317 foldr checkDef (checkExpr body errors) defs
319 Can.LetDestruct pattern@(A.At reg _) expr body ->
320 checkPatterns reg BadDestruct [pattern] $
321 checkExpr expr $ checkExpr body errors
323 Can.Case expr branches ->
324 checkExpr expr $ checkCases region branches errors
326 Can.Accessor _ ->
327 errors
329 Can.Access record _ ->
330 checkExpr record errors
332 Can.Update record fields ->
333 checkExpr record $ Map.foldr checkExpr errors fields
335 Can.Record fields ->
336 Map.foldr checkExpr errors fields
338 Can.Unit ->
339 errors
341 Can.Tuple a b maybeC ->
342 checkExpr a $
343 checkExpr b $
344 case maybeC of
345 Nothing ->
346 errors
348 Just c ->
349 checkExpr c errors
351 Can.Shader _ _ _ ->
352 errors
356-- CHECK IF BRANCH
359checkIfBranch :: (Can.Expr, Can.Expr) -> [Error] -> [Error]
360checkIfBranch (condition, branch) errs =
361 checkExpr condition $ checkExpr branch errs
365-- CHECK CASE EXPRESSION
368checkCases :: R.Region -> [Can.CaseBranch] -> [Error] -> [Error]
369checkCases region branches errors =
370 let
371 (patterns, newErrors) =
372 foldr checkCaseBranch ([], errors) branches
373 in
374 checkPatterns region BadCase patterns newErrors
377checkCaseBranch :: Can.CaseBranch -> ([Can.Pattern], [Error]) -> ([Can.Pattern], [Error])
378checkCaseBranch (Can.CaseBranch pattern expr) (patterns, errors) =
379 ( pattern:patterns
380 , checkExpr expr errors
381 )
385-- CHECK PATTERNS
388checkPatterns :: R.Region -> Context -> [Can.Pattern] -> [Error] -> [Error]
389checkPatterns region context patterns errors =
390 case toNonRedundantRows region patterns of
391 Left err ->
392 err:errors
394 Right matrix ->
395 case isExhaustive matrix 1 of
396 [] ->
397 errors
399 badPatterns ->
400 Incomplete region context (map head badPatterns) : errors
404-- EXHAUSTIVE PATTERNS
407-- INVARIANTS:
408--
409-- The initial rows "matrix" are all of length 1
410-- The initial count of items per row "n" is also 1
411-- The resulting rows are examples of missing patterns
412--
413isExhaustive :: [[Pattern]] -> Int -> [[Pattern]]
414isExhaustive matrix n =
415 case matrix of
416 [] ->
417 [replicate n Anything]
419 _ ->
420 if n == 0 then
421 []
422 else
423 let
424 ctors = collectCtors matrix
425 numSeen = Map.size ctors
426 in
427 if numSeen == 0 then
428 (:) Anything
429 <$> isExhaustive (Maybe.mapMaybe specializeRowByAnything matrix) (n - 1)
431 else
432 let alts@(Can.Union _ altList numAlts _) = snd (Map.findMin ctors) in
433 if numSeen < numAlts then
434 (:)
435 <$> Maybe.mapMaybe (isMissing alts ctors) altList
436 <*> isExhaustive (Maybe.mapMaybe specializeRowByAnything matrix) (n - 1)
438 else
439 let
440 isAltExhaustive (Can.Ctor name _ arity _) =
441 recoverCtor alts name arity <$>
442 isExhaustive
443 (Maybe.mapMaybe (specializeRowByCtor name arity) matrix)
444 (arity + n - 1)
445 in
446 concatMap isAltExhaustive altList
449isMissing :: Can.Union -> Map.Map N.Name a -> Can.Ctor -> Maybe Pattern
450isMissing union ctors (Can.Ctor name _ arity _) =
451 if Map.member name ctors then
452 Nothing
453 else
454 Just (Ctor union name (replicate arity Anything))
457recoverCtor :: Can.Union -> N.Name -> Int -> [Pattern] -> [Pattern]
458recoverCtor union name arity patterns =
459 let
460 (args, rest) =
461 splitAt arity patterns
462 in
463 Ctor union name args : rest
467-- REDUNDANT PATTERNS
470-- INVARIANT: Produces a list of rows where (forall row. length row == 1)
471toNonRedundantRows :: R.Region -> [Can.Pattern] -> Either Error [[Pattern]]
472toNonRedundantRows region patterns =
473 toSimplifiedUsefulRows region [] patterns
476-- INVARIANT: Produces a list of rows where (forall row. length row == 1)
477toSimplifiedUsefulRows :: R.Region -> [[Pattern]] -> [Can.Pattern] -> Either Error [[Pattern]]
478toSimplifiedUsefulRows overallRegion checkedRows uncheckedPatterns =
479 case uncheckedPatterns of
480 [] ->
481 Right checkedRows
483 pattern@(A.At region _) : rest ->
484 let nextRow = [simplify pattern] in
485 if isUseful checkedRows nextRow then
486 toSimplifiedUsefulRows overallRegion (nextRow : checkedRows) rest
487 else
488 Left (Redundant overallRegion region (length checkedRows + 1))
491-- Check if a new row "vector" is useful given previous rows "matrix"
492isUseful :: [[Pattern]] -> [Pattern] -> Bool
493isUseful matrix vector =
494 case matrix of
495 [] ->
496 -- No rows are the same as the new vector! The vector is useful!
497 True
499 _ ->
500 case vector of
501 [] ->
502 -- There is nothing left in the new vector, but we still have
503 -- rows that match the same things. This is not a useful vector!
504 False
506 firstPattern : patterns ->
507 case firstPattern of
508 Ctor _ name args ->
509 -- keep checking rows that start with this Ctor or Anything
510 isUseful
511 (Maybe.mapMaybe (specializeRowByCtor name (length args)) matrix)
512 (args ++ patterns)
514 Anything ->
515 -- check if all alts appear in matrix
516 case isComplete matrix of
517 No ->
518 -- This Anything is useful because some Ctors are missing.
519 -- But what if a previous row has an Anything?
520 -- If so, this one is not useful.
521 isUseful (Maybe.mapMaybe specializeRowByAnything matrix) patterns
523 Yes alts ->
524 -- All Ctors are covered, so this Anything is not needed for any
525 -- of those. But what if some of those Ctors have subpatterns
526 -- that make them less general? If so, this actually is useful!
527 let
528 isUsefulAlt (Can.Ctor name _ arity _) =
529 isUseful
530 (Maybe.mapMaybe (specializeRowByCtor name arity) matrix)
531 (replicate arity Anything ++ patterns)
532 in
533 any isUsefulAlt alts
535 Literal literal ->
536 -- keep checking rows that start with this Literal or Anything
537 isUseful
538 (Maybe.mapMaybe (specializeRowByLiteral literal) matrix)
539 patterns
542-- INVARIANT: (length row == N) ==> (length result == arity + N - 1)
543specializeRowByCtor :: N.Name -> Int -> [Pattern] -> Maybe [Pattern]
544specializeRowByCtor ctorName arity row =
545 case row of
546 Ctor _ name args : patterns ->
547 if name == ctorName then
548 Just (args ++ patterns)
549 else
550 Nothing
552 Anything : patterns ->
553 Just (replicate arity Anything ++ patterns)
555 Literal _ : _ ->
556 error $
557 "Compiler bug! After type checking, constructors and literals\
558 \ should never align in pattern match exhaustiveness checks."
560 [] ->
561 error "Compiler error! Empty matrices should not get specialized."
564-- INVARIANT: (length row == N) ==> (length result == N-1)
565specializeRowByLiteral :: Literal -> [Pattern] -> Maybe [Pattern]
566specializeRowByLiteral literal row =
567 case row of
568 Literal lit : patterns ->
569 if lit == literal then
570 Just patterns
571 else
572 Nothing
574 Anything : patterns ->
575 Just patterns
577 Ctor _ _ _ : _ ->
578 error $
579 "Compiler bug! After type checking, constructors and literals\
580 \ should never align in pattern match exhaustiveness checks."
582 [] ->
583 error "Compiler error! Empty matrices should not get specialized."
586-- INVARIANT: (length row == N) ==> (length result == N-1)
587specializeRowByAnything :: [Pattern] -> Maybe [Pattern]
588specializeRowByAnything row =
589 case row of
590 [] ->
591 Nothing
593 Ctor _ _ _ : _ ->
594 Nothing
596 Anything : patterns ->
597 Just patterns
599 Literal _ : _ ->
600 Nothing
604-- ALL CONSTRUCTORS ARE PRESENT?
607data Complete
608 = Yes [Can.Ctor]
609 | No
612isComplete :: [[Pattern]] -> Complete
613isComplete matrix =
614 let
615 ctors = collectCtors matrix
616 numSeen = Map.size ctors
617 in
618 if numSeen == 0 then
619 No
620 else
621 let (Can.Union _ alts numAlts _) = snd (Map.findMin ctors) in
622 if numSeen == numAlts then Yes alts else No
626-- COLLECT CTORS
629collectCtors :: [[Pattern]] -> Map.Map N.Name Can.Union
630collectCtors matrix =
631 List.foldl' collectCtorsHelp Map.empty matrix
634collectCtorsHelp :: Map.Map N.Name Can.Union -> [Pattern] -> Map.Map N.Name Can.Union
635collectCtorsHelp ctors row =
636 case row of
637 Ctor union name _ : _ ->
638 Map.insert name union ctors
640 _ ->
641 ctors