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