git.iko.soy/elk
on master help sign in
Introduce faster exhaustiveness checker
c5b225dEvan Czaplicki
src/Nitpick/Pattern.hs+27−46
compare with master
unifiedsplit
@@ -1,7 +1,12 @@
1+{-# OPTIONS_GHC -Wall #-}
1−module Nitpick.Pattern where
2+module Nitpick.Pattern
3+ ( Pattern(..)
4+ , fromCanonicalPattern
5+ , toString
6+ )
7+ where
2
8
3import qualified Data.List as List
9import qualified Data.List as List
4−import qualified Data.Set as Set
5
10
6import qualified AST.Literal as L
11import qualified AST.Literal as L
7import qualified AST.Pattern as P
12import qualified AST.Pattern as P
@@ -9,56 +14,58 @@ import qualified AST.Variable as Var
9import qualified Reporting.Annotation as A
14import qualified Reporting.Annotation as A
10
15
11
16
17+
18+-- PATTERN
19+
20+
12data Pattern
21data Pattern
13− = Data Var.Canonical [Pattern]
22+ = Ctor Var.Canonical [Pattern]
14− | Record [String]
15− | Alias String Pattern
16− | Var String
17 | Anything
23 | Anything
18 | Literal L.Literal
24 | Literal L.Literal
19− | AnythingBut (Set.Set L.Literal)
20 deriving (Eq)
25 deriving (Eq)
21
26
22
27
23fromCanonicalPattern :: P.Canonical -> Pattern
28fromCanonicalPattern :: P.Canonical -> Pattern
24fromCanonicalPattern (A.A _ pattern) =
29fromCanonicalPattern (A.A _ pattern) =
25 case pattern of
30 case pattern of
26− P.Data tag patterns ->
31+ P.Data name patterns ->
27− Data tag (map fromCanonicalPattern patterns)
32+ Ctor name (map fromCanonicalPattern patterns)
28
33
29− P.Record fields ->
34+ P.Record _ ->
30− Record fields
35+ Anything
31
36
32− P.Alias name pattern ->
37+ P.Alias _ subPattern ->
33− Alias name (fromCanonicalPattern pattern)
38+ fromCanonicalPattern subPattern
34
39
35− P.Var name ->
40+ P.Var _ ->
36− Var name
41+ Anything
37
42
38 P.Anything ->
43 P.Anything ->
39 Anything
44 Anything
40
45
41 P.Literal (L.Boolean True) ->
46 P.Literal (L.Boolean True) ->
42− Data (Var.builtin "True") []
47+ Ctor (Var.builtin "True") []
43
48
44 P.Literal (L.Boolean False) ->
49 P.Literal (L.Boolean False) ->
45− Data (Var.builtin "False") []
50+ Ctor (Var.builtin "False") []
46
51
47 P.Literal literal ->
52 P.Literal literal ->
48 Literal literal
53 Literal literal
49
54
50
55
56+
51-- TO STRING
57-- TO STRING
52
58
59+
53toString :: Bool -> Pattern -> String
60toString :: Bool -> Pattern -> String
54toString needsParens pattern =
61toString needsParens pattern =
55 case pattern of
62 case pattern of
56− Data tag [first,rest] | Var.toString tag == "::" ->
63+ Ctor tag [first,rest] | Var.toString tag == "::" ->
57 toString (isCons first) first
64 toString (isCons first) first
58 ++ " :: "
65 ++ " :: "
59 ++ toString False rest
66 ++ toString False rest
60
67
61− Data tag args ->
68+ Ctor tag args ->
62 if Var.isTuple tag then
69 if Var.isTuple tag then
63 "(" ++ List.intercalate ", " (map (toString False) args) ++ ")"
70 "(" ++ List.intercalate ", " (map (toString False) args) ++ ")"
64
71
@@ -66,38 +73,12 @@ toString needsParens pattern =
66 addParensIf (needsParens && not (null args)) $
73 addParensIf (needsParens && not (null args)) $
67 List.intercalate " " (Var.toString tag : map (toString True) args)
74 List.intercalate " " (Var.toString tag : map (toString True) args)
68
75
69− Record fields ->
70− "{ " ++ List.intercalate ", " fields ++ " }"
71−
72− Alias alias realPattern ->
73− addParensIf needsParens $
74− toString False realPattern ++ " as " ++ alias
75−
76− Var name ->
77− name
78−
79 Anything ->
76 Anything ->
80 "_"
77 "_"
81
78
82 Literal literal ->
79 Literal literal ->
83 L.toString literal
80 L.toString literal
84
81
85− AnythingBut literalSet ->
86− case map L.toString (Set.toList literalSet) of
87− [] ->
88− error "should not have an AnythingBut with no literals"
89−
90− [x] ->
91− "<values besides " ++ x ++ ">"
92−
93− [x,y] ->
94− "<values besides " ++ x ++ " and " ++ y ++ ">"
95−
96− literals ->
97− "<values besides "
98− ++ List.intercalate ", " (init literals)
99− ++ ", and " ++ last literals ++ ">"
100−
101
82
102addParensIf :: Bool -> String -> String
83addParensIf :: Bool -> String -> String
103addParensIf needsParens str =
84addParensIf needsParens str =
@@ -111,7 +92,7 @@ addParensIf needsParens str =
111isCons :: Pattern -> Bool
92isCons :: Pattern -> Bool
112isCons pattern =
93isCons pattern =
113 case pattern of
94 case pattern of
114− Data tag [_,_] ->
95+ Ctor tag [_,_] ->
115 Var.toString tag == "::"
96 Var.toString tag == "::"
116
97
117 _ ->
98 _ ->
src/Nitpick/PatternMatches.hs+215−215
@@ -1,13 +1,23 @@
1+{-# OPTIONS_GHC -Wall #-}
1module Nitpick.PatternMatches (patternMatches) where
2module Nitpick.PatternMatches (patternMatches) where
2
3
4+{- The algorithm used here comes from "Warnings for Pattern Matching"
5+by Luc Maranget. Check it out for more information!
6+
7+http://moscova.inria.fr/~maranget/papers/warn/warn.pdf
8+
9+-}
10+
3−import Control.Arrow (second)
11+import Control.Arrow ((***), second)
4import qualified Data.Foldable as F
12import qualified Data.Foldable as F
13+import qualified Data.List as List
5import qualified Data.Map as Map
14import qualified Data.Map as Map
6import qualified Data.Maybe as Maybe
15import qualified Data.Maybe as Maybe
7import qualified Data.Set as Set
16import qualified Data.Set as Set
8
17
9import qualified AST.Expression.Canonical as C
18import qualified AST.Expression.Canonical as C
10import qualified AST.Helpers as Help
19import qualified AST.Helpers as Help
20+import qualified AST.Literal as L
11import qualified AST.Module as Module
21import qualified AST.Module as Module
12import qualified AST.Module.Name as ModuleName
22import qualified AST.Module.Name as ModuleName
13import qualified AST.Pattern as Pattern
23import qualified AST.Pattern as Pattern
@@ -29,100 +39,25 @@ type Result warning a =
29patternMatches :: Module.Interfaces -> Module.Canonical -> Result wrn DT.VariantDict
39patternMatches :: Module.Interfaces -> Module.Canonical -> Result wrn DT.VariantDict
30patternMatches interfaces (Module.Module name _ info) =
40patternMatches interfaces (Module.Module name _ info) =
31 let
41 let
32− tagDict =
42+ arityDict =
33− toTagDict interfaces name (Module.unions info)
43+ toArityDict interfaces name (Module.unions info)
34− in
35− const (Map.map (Map.map length) tagDict)
36− <$> checkExpression tagDict (Module.program info)
37−
38−
39−
40−-- TAG DICT
41−
42−
43−type TagDict =
44− Map.Map Var.Home (Map.Map Tag [TagInfo])
45
44
46−
45+ variantDict =
47−type Tag = String
46+ Map.map (Map.map _size) arityDict
48−
49−
50−data TagInfo = TagInfo
51− { _tag :: Tag
52− , _arity :: Int
53− }
54−
55−
56−toTagDict :: Module.Interfaces -> ModuleName.Canonical -> Module.Unions -> TagDict
57−toTagDict interfaces localName localUnions =
58− let
59− listTags =
60− [ TagInfo "::" 2
61− , TagInfo "[]" 0
62− ]
63−
64− boolTags =
65− [ TagInfo "True" 0
66− , TagInfo "False" 0
67− ]
68−
69− builtinDict =
70− Map.singleton Var.BuiltIn $
71− Map.fromList
72− [ ("::", listTags)
73− , ("[]", listTags)
74− , ("True", boolTags)
75− , ("False", boolTags)
76− ]
77−
78− interfaceDict =
79− interfaces
80− |> Map.map (toTagMapping . Module.iUnions)
81− |> Map.mapKeysMonotonic Var.Module
82− |> Map.insert (Var.Module localName) (toTagMapping localUnions)
83 in
47 in
84− Map.union builtinDict interfaceDict
48+ pure variantDict
85−
49+ <* checkExpression arityDict (Module.program info)
86−
87−toTagMapping :: Module.Unions -> Map.Map Tag [TagInfo]
88−toTagMapping adts =
89− let
90− toTagAndArity (_tvars, tagInfoList) =
91− let
92− info = map (\(tag, args) -> TagInfo tag (length args)) tagInfoList
93− in
94− map (second (const info)) tagInfoList
95− in
96− Map.elems adts
97− |> concatMap toTagAndArity
98− |> Map.fromList
99−
100−
101−lookupOtherTags :: Var.Canonical -> TagDict -> [TagInfo]
102−lookupOtherTags (Var.Canonical home name) tagDict =
103− case Map.lookup name =<< Map.lookup home tagDict of
104− Just otherTags ->
105− otherTags
106−
107− Nothing ->
108− if Help.isTuple name then
109− [ TagInfo name (read (drop 6 name)) ]
110− else
111− error
112− "Since the Nitpick phase happens after canonicalization and type \
113− \inference, it is impossible that a pattern in a case cannot be \
114− \found."
115
50
116
51
117
52
118-- CHECK EXPRESSIONS
53-- CHECK EXPRESSIONS
119
54
120
55
121−checkExpression :: TagDict -> C.Expr -> Result wrn ()
56+checkExpression :: ArityDict -> C.Expr -> Result wrn ()
122−checkExpression tagDict (A.A region expression) =
57+checkExpression arityDict (A.A region expression) =
123 let
58 let
124 go =
59 go =
125− checkExpression tagDict
60+ checkExpression arityDict
126
61
127 go2 a b =
62 go2 a b =
128 go a <* go b
63 go a <* go b
@@ -141,7 +76,7 @@ checkExpression tagDict (A.A region expression) =
141 go2 leftExpr rightExpr
76 go2 leftExpr rightExpr
142
77
143 C.Lambda pattern@(A.A patRegion _) body ->
78 C.Lambda pattern@(A.A patRegion _) body ->
144− checkPatterns tagDict patRegion Error.Arg [pattern]
79+ checkPatterns arityDict patRegion Error.Arg [pattern]
145 <* go body
80 <* go body
146
81
147 C.App func arg ->
82 C.App func arg ->
@@ -156,12 +91,12 @@ checkExpression tagDict (A.A region expression) =
156 <* F.traverse_ goDef defs
91 <* F.traverse_ goDef defs
157 where
92 where
158 goDef (C.Def _ pattern@(A.A patRegion _) expr _) =
93 goDef (C.Def _ pattern@(A.A patRegion _) expr _) =
159− checkPatterns tagDict patRegion Error.LetBound [pattern]
94+ checkPatterns arityDict patRegion Error.LetBound [pattern]
160 <* go expr
95 <* go expr
161
96
162 C.Case expr branches ->
97 C.Case expr branches ->
163 go expr
98 go expr
164− <* checkPatterns tagDict region Error.Case (map fst branches)
99+ <* checkPatterns arityDict region Error.Case (map fst branches)
165 <* F.traverse_ (go . snd) branches
100 <* F.traverse_ (go . snd) branches
166
101
167 C.Ctor _ctor exprs ->
102 C.Ctor _ctor exprs ->
@@ -203,180 +138,245 @@ checkExpression tagDict (A.A region expression) =
203-- CHECK PATTERNS
138-- CHECK PATTERNS
204
139
205
140
206−checkPatterns :: TagDict -> Region.Region -> Error.Origin -> [Pattern.Canonical] -> Result wrn ()
141+checkPatterns :: ArityDict -> Region.Region -> Error.Origin -> [Pattern.Canonical] -> Result wrn ()
207−checkPatterns tagDict region origin patterns =
142+checkPatterns arityDict region origin patterns =
208− checkPatternsHelp tagDict region origin [Anything] patterns
143+ let
144+ matrix =
145+ map (\p -> [fromCanonicalPattern p]) patterns
146+ in
147+ if isUseful arityDict matrix [Anything] then
148+ Result.throw region (Error.Incomplete origin (error "TODO"))
209
149
150+ else
151+ return ()
210
152
211−checkPatternsHelp
212− :: TagDict
213− -> Region.Region
214− -> Error.Origin
215− -> [Pattern]
216− -> [Pattern.Canonical]
217− -> Result wrn ()
218−checkPatternsHelp tagDict region origin unhandled patterns =
219− case (unhandled, patterns) of
220− ([], []) ->
221− return ()
222
153
223− (_:_, []) ->
224− Result.throw region (Error.Incomplete origin unhandled)
225
154
226− (_, pattern@(A.A localRegion _) : remainingPatterns) ->
155+-- MISSING PATTERNS
227− do newUnhandled <- filterPatterns tagDict localRegion pattern unhandled
228− checkPatternsHelp tagDict region origin newUnhandled remainingPatterns
229
156
230
157
231−filterPatterns
158+--missingPatterns :: [[Pattern]] -> Int -> [Pattern]
232− :: TagDict
159+--missingPatterns matrix n =
233− -> Region.Region
160+-- case matrix of
234− -> Pattern.Canonical
161+-- [] ->
235− -> [Pattern]
236− -> Result wrn [Pattern]
237−filterPatterns tagDict region pattern unhandled =
238− let
239− nitPattern =
240− fromCanonicalPattern pattern
241
162
242− noIntersection pat =
243− intersection pat nitPattern == Nothing
244− in
245− if all noIntersection unhandled then
246− Result.throw region Error.Redundant
247
163
248− else
249− do let complementPatterns = complement tagDict nitPattern
250− return $
251− concatMap
252− (\p -> Maybe.mapMaybe (intersection p) complementPatterns)
253− unhandled
254
164
255
165
166+-- REDUNDANT PATTERNS
256
167
257−-- PATTERN INTERSECTION
258
168
169+isUseful :: ArityDict -> [[Pattern]] -> [Pattern] -> Bool
170+isUseful arityDict matrix vector =
171+ case (matrix, vector) of
172+ ([], _) ->
173+ True
259
174
260−intersection :: Pattern -> Pattern -> Maybe Pattern
175+ (_, []) ->
261−intersection pattern1 pattern2 =
176+ False
262− case (pattern1, pattern2) of
263− (Alias _ pattern1', _) ->
264− intersection pattern1' pattern2
265
177
266− (_, Alias _ pattern2') ->
178+ (_, firstPattern : patterns) ->
267− intersection pattern1 pattern2'
179+ case firstPattern of
180+ Ctor name args ->
181+ let
182+ newMatrix =
183+ Maybe.mapMaybe (specialize name (length args)) matrix
184+ in
185+ isUseful arityDict newMatrix (args ++ patterns)
268
186
269− (Anything, _) ->
187+ Anything ->
270− Just pattern2
188+ case isComplete arityDict matrix of
189+ Nothing ->
190+ isUseful arityDict (Maybe.mapMaybe toDefault matrix) patterns
271
191
272− (Var _, _) ->
192+ Just arityInfo ->
273− Just pattern2
193+ let
194+ isUsefulHelp (ctor, arity) =
195+ isUseful
196+ arityDict
197+ (Maybe.mapMaybe (specialize ctor arity) matrix)
198+ (replicate arity Anything ++ patterns)
199+ in
200+ any isUsefulHelp arityInfo
274
201
275− (_, Anything) ->
202+ Literal literal ->
276− Just pattern1
203+ let
204+ newMatrix =
205+ Maybe.mapMaybe (specializeLiteral literal) matrix
206+ in
207+ isUseful arityDict newMatrix patterns
277
208
278− (_, Var _) ->
279− Just pattern1
280
209
281− (Data ctor1 args1, Data ctor2 args2) ->
282− if ctor1 /= ctor2 then
283− Nothing
284− else
285− Data ctor1 <$> sequence (zipWith intersection args1 args2)
286
210
287− (Record _, Record _) ->
211+-- SPECIALIZE MATRICES
288− Just pattern1
289
212
290− (Literal lit1, Literal lit2) ->
291− if lit1 == lit2 then
292− Just pattern1
293− else
294− Nothing
295
213
296− (AnythingBut literals, Literal lit) ->
214+specialize :: Var.Canonical -> Int -> [Pattern] -> Maybe [Pattern]
297− if Set.member lit literals then
215+specialize ctorName arity row =
298− Nothing
216+ case row of
299− else
217+ [] ->
300− Just pattern2
218+ error "Compiler error! Empty matrices should not get specialized."
301
219
302− (Literal lit, AnythingBut literals) ->
220+ firstPattern : patterns ->
303− if Set.member lit literals then
221+ case firstPattern of
304− Nothing
222+ Ctor name args ->
305− else
223+ if name == ctorName then Just (args ++ patterns) else Nothing
306− Just pattern1
307
224
308− (AnythingBut literals1, AnythingBut literals2) ->
225+ Anything ->
309− Just (AnythingBut (Set.union literals1 literals2))
226+ Just (replicate arity Anything ++ patterns)
310
227
311− _ ->
228+ Literal _ ->
312− Nothing
229+ error $
230+ "Compiler bug! After type checking, constructors and literals\
231+ \ should never align in pattern match exhaustiveness checks."
313
232
314
233
234+specializeLiteral :: L.Literal -> [Pattern] -> Maybe [Pattern]
235+specializeLiteral literal row =
236+ case row of
237+ [] ->
238+ error "Compiler error! Empty matrices should not get specialized."
315
239
316−-- PATTERN COMPLEMENT
240+ firstPattern : patterns ->
241+ case firstPattern of
242+ Literal lit ->
243+ if lit == literal then Just patterns else Nothing
317
244
245+ Anything ->
246+ Just patterns
318
247
319−complement :: TagDict -> Pattern -> [Pattern]
248+ Ctor _ _ ->
320−complement tagDict nitPattern =
249+ error $
321− case nitPattern of
250+ "Compiler bug! After type checking, constructors and literals\
322− Record _fields ->
251+ \ should never align in pattern match exhaustiveness checks."
323− []
324
252
325− Alias _name pattern ->
326− complement tagDict pattern
327
253
328− Var _name ->
254+toDefault :: [Pattern] -> Maybe [Pattern]
329− []
255+toDefault row =
256+ case row of
257+ [] ->
258+ Nothing
330
259
331− Anything ->
260+ Ctor _ _ : _ ->
332− []
261+ Nothing
333
262
334− Literal lit ->
263+ Anything : patterns ->
335− [AnythingBut (Set.singleton lit)]
264+ Just patterns
336
265
337− AnythingBut literals ->
266+ Literal _ : _ ->
338− map Literal (Set.toList literals)
267+ Nothing
339
268
340− Data ctor patterns ->
341− complementData tagDict ctor patterns
342
269
343
270
344−complementData :: TagDict -> Var.Canonical -> [Pattern] -> [Pattern]
271+-- ALL CONSTRUCTORS ARE PRESENT?
345−complementData tagDict tag patterns =
346− let
347− otherTags =
348− lookupOtherTags tag tagDict
349
272
350− tagComplements =
351− Maybe.mapMaybe (tagToPattern tag) otherTags
352
273
353− arity =
274+isComplete :: ArityDict -> [[Pattern]] -> Maybe [(Var.Canonical, Int)]
354− length patterns
275+isComplete arityDict matrix =
276+ let
277+ ctorSet =
278+ List.foldl' isCompleteHelp Set.empty matrix
355
279
356− argComplements =
280+ actual =
357− concat (zipWith (makeArgComplements tagDict tag arity) [0..] patterns)
281+ Set.size ctorSet
358 in
282 in
359− tagComplements ++ argComplements
283+ if actual == 0 then
284+ Nothing
285+
286+ else
287+ let
288+ (ArityInfo expected info) =
289+ getArityInfo (Set.findMin ctorSet) arityDict
290+ in
291+ if expected == actual then Just info else Nothing
292+
293+
294+isCompleteHelp :: Set.Set Var.Canonical -> [Pattern] -> Set.Set Var.Canonical
295+isCompleteHelp ctors row =
296+ case row of
297+ Ctor name _ : _ ->
298+ Set.insert name ctors
299+
300+ _ ->
301+ ctors
302+
303+
304+
305+-- ARITY DICT
306+
307+
308+type ArityDict =
309+ Map.Map Var.Home (Map.Map String ArityInfo)
310+
311+
312+data ArityInfo =
313+ ArityInfo
314+ { _size :: !Int
315+ , _info :: [(Var.Canonical, Int)]
316+ }
360
317
361
318
362−tagToPattern :: Var.Canonical -> TagInfo -> Maybe Pattern
319+toArityDict :: Module.Interfaces -> ModuleName.Canonical -> Module.Unions -> ArityDict
363−tagToPattern (Var.Canonical home rootTag) (TagInfo tag arity) =
320+toArityDict interfaces localName localUnions =
364− if rootTag == tag then
321+ interfaces
365− Nothing
322+ |> Map.mapWithKey (\name iface -> toArityEntry name (Module.iUnions iface))
366− else
323+ |> Map.mapKeysMonotonic Var.Module
367− Just (Data (Var.Canonical home tag) (replicate arity Anything))
324+ |> Map.insert (Var.Module localName) (toArityEntry localName localUnions)
325+ |> Map.union builtinDict
368
326
369
327
370−makeArgComplements :: TagDict -> Var.Canonical -> Int -> Int -> Pattern -> [Pattern]
328+builtinDict :: ArityDict
371−makeArgComplements tagDict tag arity index argPattern =
329+builtinDict =
372 let
330 let
373− complementList =
331+ listInfo =
374− complement tagDict argPattern
332+ ArityInfo 2 [ (Var.builtin "::", 2), (Var.builtin "[]", 0) ]
375
333
376− padArgs pattern =
334+ boolInfo =
377− replicate index Anything
335+ ArityInfo 2 [ (Var.builtin "True", 0), (Var.builtin "False", 0) ]
378− ++ pattern
379− : replicate (arity - index - 1) Anything
380 in
336 in
381− map (Data tag . padArgs) complementList
337+ Map.singleton Var.BuiltIn $ Map.fromList $
338+ [ ("::", listInfo)
339+ , ("[]", listInfo)
340+ , ("True", boolInfo)
341+ , ("False", boolInfo)
342+ ]
343+ ++ map makeTupleInfo [0..8]
382
344
345+
346+makeTupleInfo :: Int -> ( String, ArityInfo )
347+makeTupleInfo n =
348+ let
349+ name =
350+ "_Tuple" ++ show n
351+ in
352+ ( name, ArityInfo 1 [ (Var.builtin name, n) ] )
353+
354+
355+toArityEntry :: ModuleName.Canonical -> Module.Unions -> Map.Map String ArityInfo
356+toArityEntry name unions =
357+ Map.fromList (concatMap (toArityEntryHelp name) (Map.elems unions))
358+
359+
360+toArityEntryHelp :: ModuleName.Canonical -> Module.UnionInfo String -> [(String, ArityInfo)]
361+toArityEntryHelp name (_tvars, ctors) =
362+ let
363+ arityInfo =
364+ ArityInfo (length ctors) (map (Var.fromModule name *** length) ctors)
365+ in
366+ map (second (\_ -> arityInfo)) ctors
367+
368+
369+getArityInfo :: Var.Canonical -> ArityDict -> ArityInfo
370+getArityInfo var@(Var.Canonical home name) arityDict =
371+ case Map.lookup name =<< Map.lookup home arityDict of
372+ Just arityInfo ->
373+ arityInfo
374+
375+ Nothing ->
376+ if Help.isTuple name then
377+ ArityInfo 1 [ (var, read (drop 6 name)) ]
378+ else
379+ error
380+ "Since the Nitpick phase happens after canonicalization and type\
381+ \ inference, it is impossible that a pattern in a case cannot be\
382+ \ found."