COMPLETE pragmas for enhanced pattern exhaustiveness checking
[ghc.git] / compiler / deSugar / PmExpr.hs
1 {-
2 Author: George Karachalias <george.karachalias@cs.kuleuven.be>
3
4 Haskell expressions (as used by the pattern matching checker) and utilities.
5 -}
6
7 {-# LANGUAGE CPP #-}
8
9 module PmExpr (
10 PmExpr(..), PmLit(..), SimpleEq, ComplexEq, toComplex, eqPmLit,
11 truePmExpr, falsePmExpr, isTruePmExpr, isFalsePmExpr, isNotPmExprOther,
12 lhsExprToPmExpr, hsExprToPmExpr, substComplexEq, filterComplex,
13 pprPmExprWithParens, runPmPprM
14 ) where
15
16 #include "HsVersions.h"
17
18 import HsSyn
19 import Id
20 import Name
21 import NameSet
22 import DataCon
23 import ConLike
24 import TysWiredIn
25 import Outputable
26 import Util
27 import SrcLoc
28
29 import Data.Maybe (mapMaybe)
30 import Data.List (groupBy, sortBy, nubBy)
31 import Control.Monad.Trans.State.Lazy
32
33 {-
34 %************************************************************************
35 %* *
36 Lifted Expressions
37 %* *
38 %************************************************************************
39 -}
40
41 {- Note [PmExprOther in PmExpr]
42 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
43 Since there is no plan to extend the (currently pretty naive) term oracle in
44 the near future, instead of playing with the verbose (HsExpr Id), we lift it to
45 PmExpr. All expressions the term oracle does not handle are wrapped by the
46 constructor PmExprOther. Note that we do not perform substitution in
47 PmExprOther. Because of this, we do not even print PmExprOther, since they may
48 refer to variables that are otherwise substituted away.
49 -}
50
51 -- ----------------------------------------------------------------------------
52 -- ** Types
53
54 -- | Lifted expressions for pattern match checking.
55 data PmExpr = PmExprVar Name
56 | PmExprCon ConLike [PmExpr]
57 | PmExprLit PmLit
58 | PmExprEq PmExpr PmExpr -- Syntactic equality
59 | PmExprOther (HsExpr Id) -- Note [PmExprOther in PmExpr]
60
61
62 mkPmExprData :: DataCon -> [PmExpr] -> PmExpr
63 mkPmExprData dc args = PmExprCon (RealDataCon dc) args
64
65 -- | Literals (simple and overloaded ones) for pattern match checking.
66 data PmLit = PmSLit HsLit -- simple
67 | PmOLit Bool {- is it negated? -} (HsOverLit Id) -- overloaded
68
69 -- | Equality between literals for pattern match checking.
70 eqPmLit :: PmLit -> PmLit -> Bool
71 eqPmLit (PmSLit l1) (PmSLit l2) = l1 == l2
72 eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2
73 -- See Note [Undecidable Equality for Overloaded Literals]
74 eqPmLit _ _ = False
75
76 {- Note [Undecidable Equality for Overloaded Literals]
77 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
78 Equality on overloaded literals is undecidable in the general case. Consider
79 the following example:
80
81 instance Num Bool where
82 ...
83 fromInteger 0 = False -- C-like representation of booleans
84 fromInteger _ = True
85
86 f :: Bool -> ()
87 f 1 = () -- Clause A
88 f 2 = () -- Clause B
89
90 Clause B is redundant but to detect this, we should be able to solve the
91 constraint: False ~ (fromInteger 2 ~ fromInteger 1) which means that we
92 have to look through function `fromInteger`, whose implementation could
93 be anything. This poses difficulties for:
94
95 1. The expressive power of the check.
96 We cannot expect a reasonable implementation of pattern matching to detect
97 that fromInteger 2 ~ fromInteger 1 is True, unless we unfold function
98 fromInteger. This puts termination at risk and is undecidable in the
99 general case.
100
101 2. Performance.
102 Having an unresolved constraint False ~ (fromInteger 2 ~ fromInteger 1)
103 lying around could become expensive really fast. Ticket #11161 illustrates
104 how heavy use of overloaded literals can generate plenty of those
105 constraints, effectively undermining the term oracle's performance.
106
107 3. Error nessages/Warnings.
108 What should our message for `f` above be? A reasonable approach would be
109 to issue:
110
111 Pattern matches are (potentially) redundant:
112 f 2 = ... under the assumption that 1 == 2
113
114 but seems to complex and confusing for the user.
115
116 We choose to treat overloaded literals that look different as different. The
117 impact of this is the following:
118
119 * Redundancy checking is rather conservative, since it cannot see that clause
120 B above is redundant.
121
122 * We have instant equality check for overloaded literals (we do not rely on
123 the term oracle which is rather expensive, both in terms of performance and
124 memory). This significantly improves the performance of functions `covered`
125 `uncovered` and `divergent` in deSugar/Check.hs and effectively addresses
126 #11161.
127
128 * The warnings issued are simpler.
129
130 * We do not play on the safe side, strictly speaking. The assumption that
131 1 /= 2 makes the redundancy check more conservative but at the same time
132 makes its dual (exhaustiveness check) unsafe. This we can live with, mainly
133 for two reasons:
134 1. At the moment we do not use the results of the check during compilation
135 where this would be a disaster (could result in runtime errors even if
136 our function was deemed exhaustive).
137 2. Pattern matcing on literals can never be considered exhaustive unless we
138 have a catch-all clause. Hence, this assumption affects mainly the
139 appearance of the warnings and is, in practice safe.
140 -}
141
142 nubPmLit :: [PmLit] -> [PmLit]
143 nubPmLit = nubBy eqPmLit
144
145 -- | Term equalities
146 type SimpleEq = (Id, PmExpr) -- We always use this orientation
147 type ComplexEq = (PmExpr, PmExpr)
148
149 -- | Lift a `SimpleEq` to a `ComplexEq`
150 toComplex :: SimpleEq -> ComplexEq
151 toComplex (x,e) = (PmExprVar (idName x), e)
152
153 -- | Expression `True'
154 truePmExpr :: PmExpr
155 truePmExpr = mkPmExprData trueDataCon []
156
157 -- | Expression `False'
158 falsePmExpr :: PmExpr
159 falsePmExpr = mkPmExprData falseDataCon []
160
161 -- ----------------------------------------------------------------------------
162 -- ** Predicates on PmExpr
163
164 -- | Check if an expression is lifted or not
165 isNotPmExprOther :: PmExpr -> Bool
166 isNotPmExprOther (PmExprOther _) = False
167 isNotPmExprOther _expr = True
168
169 -- | Check whether a literal is negated
170 isNegatedPmLit :: PmLit -> Bool
171 isNegatedPmLit (PmOLit b _) = b
172 isNegatedPmLit _other_lit = False
173
174 -- | Check whether a PmExpr is syntactically equal to term `True'.
175 isTruePmExpr :: PmExpr -> Bool
176 isTruePmExpr (PmExprCon c []) = c == RealDataCon trueDataCon
177 isTruePmExpr _other_expr = False
178
179 -- | Check whether a PmExpr is syntactically equal to term `False'.
180 isFalsePmExpr :: PmExpr -> Bool
181 isFalsePmExpr (PmExprCon c []) = c == RealDataCon falseDataCon
182 isFalsePmExpr _other_expr = False
183
184 -- | Check whether a PmExpr is syntactically e
185 isNilPmExpr :: PmExpr -> Bool
186 isNilPmExpr (PmExprCon c _) = c == RealDataCon nilDataCon
187 isNilPmExpr _other_expr = False
188
189 -- | Check whether a PmExpr is syntactically equal to (x == y).
190 -- Since (==) is overloaded and can have an arbitrary implementation, we use
191 -- the PmExprEq constructor to represent only equalities with non-overloaded
192 -- literals where it coincides with a syntactic equality check.
193 isPmExprEq :: PmExpr -> Maybe (PmExpr, PmExpr)
194 isPmExprEq (PmExprEq e1 e2) = Just (e1,e2)
195 isPmExprEq _other_expr = Nothing
196
197 -- | Check if a DataCon is (:).
198 isConsDataCon :: DataCon -> Bool
199 isConsDataCon con = consDataCon == con
200
201 -- ----------------------------------------------------------------------------
202 -- ** Substitution in PmExpr
203
204 -- | We return a boolean along with the expression. Hence, if substitution was
205 -- a no-op, we know that the expression still cannot progress.
206 substPmExpr :: Name -> PmExpr -> PmExpr -> (PmExpr, Bool)
207 substPmExpr x e1 e =
208 case e of
209 PmExprVar z | x == z -> (e1, True)
210 | otherwise -> (e, False)
211 PmExprCon c ps -> let (ps', bs) = mapAndUnzip (substPmExpr x e1) ps
212 in (PmExprCon c ps', or bs)
213 PmExprEq ex ey -> let (ex', bx) = substPmExpr x e1 ex
214 (ey', by) = substPmExpr x e1 ey
215 in (PmExprEq ex' ey', bx || by)
216 _other_expr -> (e, False) -- The rest are terminals (We silently ignore
217 -- Other). See Note [PmExprOther in PmExpr]
218
219 -- | Substitute in a complex equality. We return (Left eq) if the substitution
220 -- affected the equality or (Right eq) if nothing happened.
221 substComplexEq :: Name -> PmExpr -> ComplexEq -> Either ComplexEq ComplexEq
222 substComplexEq x e (ex, ey)
223 | bx || by = Left (ex', ey')
224 | otherwise = Right (ex', ey')
225 where
226 (ex', bx) = substPmExpr x e ex
227 (ey', by) = substPmExpr x e ey
228
229 -- -----------------------------------------------------------------------
230 -- ** Lift source expressions (HsExpr Id) to PmExpr
231
232 lhsExprToPmExpr :: LHsExpr Id -> PmExpr
233 lhsExprToPmExpr (L _ e) = hsExprToPmExpr e
234
235 hsExprToPmExpr :: HsExpr Id -> PmExpr
236
237 hsExprToPmExpr (HsVar x) = PmExprVar (idName (unLoc x))
238 hsExprToPmExpr (HsConLikeOut c) = PmExprVar (conLikeName c)
239 hsExprToPmExpr (HsOverLit olit) = PmExprLit (PmOLit False olit)
240 hsExprToPmExpr (HsLit lit) = PmExprLit (PmSLit lit)
241
242 hsExprToPmExpr e@(NegApp _ neg_e)
243 | PmExprLit (PmOLit False ol) <- synExprToPmExpr neg_e
244 = PmExprLit (PmOLit True ol)
245 | otherwise = PmExprOther e
246 hsExprToPmExpr (HsPar (L _ e)) = hsExprToPmExpr e
247
248 hsExprToPmExpr e@(ExplicitTuple ps boxity)
249 | all tupArgPresent ps = mkPmExprData tuple_con tuple_args
250 | otherwise = PmExprOther e
251 where
252 tuple_con = tupleDataCon boxity (length ps)
253 tuple_args = [ lhsExprToPmExpr e | L _ (Present e) <- ps ]
254
255 hsExprToPmExpr e@(ExplicitList _elem_ty mb_ol elems)
256 | Nothing <- mb_ol = foldr cons nil (map lhsExprToPmExpr elems)
257 | otherwise = PmExprOther e {- overloaded list: No PmExprApp -}
258 where
259 cons x xs = mkPmExprData consDataCon [x,xs]
260 nil = mkPmExprData nilDataCon []
261
262 hsExprToPmExpr (ExplicitPArr _elem_ty elems)
263 = mkPmExprData (parrFakeCon (length elems)) (map lhsExprToPmExpr elems)
264
265
266 -- we want this but we would have to make everything monadic :/
267 -- ./compiler/deSugar/DsMonad.hs:397:dsLookupDataCon :: Name -> DsM DataCon
268 --
269 -- hsExprToPmExpr (RecordCon c _ binds) = do
270 -- con <- dsLookupDataCon (unLoc c)
271 -- args <- mapM lhsExprToPmExpr (hsRecFieldsArgs binds)
272 -- return (PmExprCon con args)
273 hsExprToPmExpr e@(RecordCon _ _ _ _) = PmExprOther e
274
275 hsExprToPmExpr (HsTick _ e) = lhsExprToPmExpr e
276 hsExprToPmExpr (HsBinTick _ _ e) = lhsExprToPmExpr e
277 hsExprToPmExpr (HsTickPragma _ _ _ e) = lhsExprToPmExpr e
278 hsExprToPmExpr (HsSCC _ _ e) = lhsExprToPmExpr e
279 hsExprToPmExpr (HsCoreAnn _ _ e) = lhsExprToPmExpr e
280 hsExprToPmExpr (ExprWithTySig e _) = lhsExprToPmExpr e
281 hsExprToPmExpr (ExprWithTySigOut e _) = lhsExprToPmExpr e
282 hsExprToPmExpr (HsWrap _ e) = hsExprToPmExpr e
283 hsExprToPmExpr e = PmExprOther e -- the rest are not handled by the oracle
284
285 synExprToPmExpr :: SyntaxExpr Id -> PmExpr
286 synExprToPmExpr = hsExprToPmExpr . syn_expr -- ignore the wrappers
287
288 {-
289 %************************************************************************
290 %* *
291 Pretty printing
292 %* *
293 %************************************************************************
294 -}
295
296 {- 1. Literals
297 ~~~~~~~~~~~~~~
298 Starting with a function definition like:
299
300 f :: Int -> Bool
301 f 5 = True
302 f 6 = True
303
304 The uncovered set looks like:
305 { var |> False == (var == 5), False == (var == 6) }
306
307 Yet, we would like to print this nicely as follows:
308 x , where x not one of {5,6}
309
310 Function `filterComplex' takes the set of residual constraints and packs
311 together the negative constraints that refer to the same variable so we can do
312 just this. Since these variables will be shown to the programmer, we also give
313 them better names (t1, t2, ..), hence the SDoc in PmNegLitCt.
314
315 2. Residual Constraints
316 ~~~~~~~~~~~~~~~~~~~~~~~
317 Unhandled constraints that refer to HsExpr are typically ignored by the solver
318 (it does not even substitute in HsExpr so they are even printed as wildcards).
319 Additionally, the oracle returns a substitution if it succeeds so we apply this
320 substitution to the vectors before printing them out (see function `pprOne' in
321 Check.hs) to be more precice.
322 -}
323
324 -- -----------------------------------------------------------------------------
325 -- ** Transform residual constraints in appropriate form for pretty printing
326
327 type PmNegLitCt = (Name, (SDoc, [PmLit]))
328
329 filterComplex :: [ComplexEq] -> [PmNegLitCt]
330 filterComplex = zipWith rename nameList . map mkGroup
331 . groupBy name . sortBy order . mapMaybe isNegLitCs
332 where
333 order x y = compare (fst x) (fst y)
334 name x y = fst x == fst y
335 mkGroup l = (fst (head l), nubPmLit $ map snd l)
336 rename new (old, lits) = (old, (new, lits))
337
338 isNegLitCs (e1,e2)
339 | isFalsePmExpr e1, Just (x,y) <- isPmExprEq e2 = isNegLitCs' x y
340 | isFalsePmExpr e2, Just (x,y) <- isPmExprEq e1 = isNegLitCs' x y
341 | otherwise = Nothing
342
343 isNegLitCs' (PmExprVar x) (PmExprLit l) = Just (x, l)
344 isNegLitCs' (PmExprLit l) (PmExprVar x) = Just (x, l)
345 isNegLitCs' _ _ = Nothing
346
347 -- Try nice names p,q,r,s,t before using the (ugly) t_i
348 nameList :: [SDoc]
349 nameList = map text ["p","q","r","s","t"] ++
350 [ text ('t':show u) | u <- [(0 :: Int)..] ]
351
352 -- ----------------------------------------------------------------------------
353
354 runPmPprM :: PmPprM a -> [PmNegLitCt] -> (a, [(SDoc,[PmLit])])
355 runPmPprM m lit_env = (result, mapMaybe is_used lit_env)
356 where
357 (result, (_lit_env, used)) = runState m (lit_env, emptyNameSet)
358
359 is_used (x,(name, lits))
360 | elemNameSet x used = Just (name, lits)
361 | otherwise = Nothing
362
363 type PmPprM a = State ([PmNegLitCt], NameSet) a
364 -- (the first part of the state is read only. make it a reader?)
365
366 addUsed :: Name -> PmPprM ()
367 addUsed x = modify (\(negated, used) -> (negated, extendNameSet used x))
368
369 checkNegation :: Name -> PmPprM (Maybe SDoc) -- the clean name if it is negated
370 checkNegation x = do
371 negated <- gets fst
372 return $ case lookup x negated of
373 Just (new, _) -> Just new
374 Nothing -> Nothing
375
376 -- | Pretty print a pmexpr, but remember to prettify the names of the variables
377 -- that refer to neg-literals. The ones that cannot be shown are printed as
378 -- underscores.
379 pprPmExpr :: PmExpr -> PmPprM SDoc
380 pprPmExpr (PmExprVar x) = do
381 mb_name <- checkNegation x
382 case mb_name of
383 Just name -> addUsed x >> return name
384 Nothing -> return underscore
385
386 pprPmExpr (PmExprCon con args) = pprPmExprCon con args
387 pprPmExpr (PmExprLit l) = return (ppr l)
388 pprPmExpr (PmExprEq _ _) = return underscore -- don't show
389 pprPmExpr (PmExprOther _) = return underscore -- don't show
390
391 needsParens :: PmExpr -> Bool
392 needsParens (PmExprVar {}) = False
393 needsParens (PmExprLit l) = isNegatedPmLit l
394 needsParens (PmExprEq {}) = False -- will become a wildcard
395 needsParens (PmExprOther {}) = False -- will become a wildcard
396 needsParens (PmExprCon (RealDataCon c) es)
397 | isTupleDataCon c || isPArrFakeCon c
398 || isConsDataCon c || null es = False
399 | otherwise = True
400 needsParens (PmExprCon (PatSynCon _) es) = not (null es)
401
402 pprPmExprWithParens :: PmExpr -> PmPprM SDoc
403 pprPmExprWithParens expr
404 | needsParens expr = parens <$> pprPmExpr expr
405 | otherwise = pprPmExpr expr
406
407 pprPmExprCon :: ConLike -> [PmExpr] -> PmPprM SDoc
408 pprPmExprCon (RealDataCon con) args
409 | isTupleDataCon con = mkTuple <$> mapM pprPmExpr args
410 | isPArrFakeCon con = mkPArr <$> mapM pprPmExpr args
411 | isConsDataCon con = pretty_list
412 where
413 mkTuple, mkPArr :: [SDoc] -> SDoc
414 mkTuple = parens . fsep . punctuate comma
415 mkPArr = paBrackets . fsep . punctuate comma
416
417 -- lazily, to be used in the list case only
418 pretty_list :: PmPprM SDoc
419 pretty_list = case isNilPmExpr (last list) of
420 True -> brackets . fsep . punctuate comma <$> mapM pprPmExpr (init list)
421 False -> parens . hcat . punctuate colon <$> mapM pprPmExpr list
422
423 list = list_elements args
424
425 list_elements [x,y]
426 | PmExprCon c es <- y, RealDataCon nilDataCon == c
427 = ASSERT(null es) [x,y]
428 | PmExprCon c es <- y, RealDataCon consDataCon == c
429 = x : list_elements es
430 | otherwise = [x,y]
431 list_elements list = pprPanic "list_elements:" (ppr list)
432 pprPmExprCon cl args
433 | conLikeIsInfix cl = case args of
434 [x, y] -> do x' <- pprPmExprWithParens x
435 y' <- pprPmExprWithParens y
436 return (x' <+> ppr cl <+> y')
437 -- can it be infix but have more than two arguments?
438 list -> pprPanic "pprPmExprCon:" (ppr list)
439 | null args = return (ppr cl)
440 | otherwise = do args' <- mapM pprPmExprWithParens args
441 return (fsep (ppr cl : args'))
442
443 instance Outputable PmLit where
444 ppr (PmSLit l) = pmPprHsLit l
445 ppr (PmOLit neg l) = (if neg then char '-' else empty) <> ppr l
446
447 -- not really useful for pmexprs per se
448 instance Outputable PmExpr where
449 ppr e = fst $ runPmPprM (pprPmExpr e) []