3697dd8cc16e12e49f4421a88049206d22a21016
[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 {-# LANGUAGE ViewPatterns #-}
9 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
10
11 module PmExpr (
12 PmExpr(..), PmLit(..), PmAltCon(..), TmVarCt(..),
13 eqPmLit, isNotPmExprOther, lhsExprToPmExpr, hsExprToPmExpr
14 ) where
15
16 #include "HsVersions.h"
17
18 import GhcPrelude
19
20 import BasicTypes (SourceText)
21 import FastString (FastString, unpackFS)
22 import HsSyn
23 import Id
24 import Name
25 import DataCon
26 import ConLike
27 import TcEvidence (isErasableHsWrapper)
28 import TcType (isStringTy)
29 import TysWiredIn
30 import Outputable
31 import SrcLoc
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 | PmExprOther (HsExpr GhcTc) -- Note [PmExprOther in PmExpr]
59
60
61 mkPmExprData :: DataCon -> [PmExpr] -> PmExpr
62 mkPmExprData dc args = PmExprCon (RealDataCon dc) args
63
64 -- | Literals (simple and overloaded ones) for pattern match checking.
65 data PmLit = PmSLit (HsLit GhcTc) -- simple
66 | PmOLit Bool {- is it negated? -} (HsOverLit GhcTc) -- overloaded
67
68 -- | Equality between literals for pattern match checking.
69 eqPmLit :: PmLit -> PmLit -> Bool
70 eqPmLit (PmSLit l1) (PmSLit l2) = l1 == l2
71 eqPmLit (PmOLit b1 l1) (PmOLit b2 l2) = b1 == b2 && l1 == l2
72 -- See Note [Undecidable Equality for Overloaded Literals]
73 eqPmLit _ _ = False
74
75 -- | Represents a match against a literal. We mostly use it to to encode shapes
76 -- for a variable that immediately lead to a refutation.
77 --
78 -- See Note [Refutable shapes] in TmOracle. Really similar to 'CoreSyn.AltCon'.
79 newtype PmAltCon = PmAltLit PmLit
80 deriving Outputable
81
82 instance Eq PmAltCon where
83 PmAltLit l1 == PmAltLit l2 = eqPmLit l1 l2
84
85 {- Note [Undecidable Equality for Overloaded Literals]
86 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
87 Equality on overloaded literals is undecidable in the general case. Consider
88 the following example:
89
90 instance Num Bool where
91 ...
92 fromInteger 0 = False -- C-like representation of booleans
93 fromInteger _ = True
94
95 f :: Bool -> ()
96 f 1 = () -- Clause A
97 f 2 = () -- Clause B
98
99 Clause B is redundant but to detect this, we should be able to solve the
100 constraint: False ~ (fromInteger 2 ~ fromInteger 1) which means that we
101 have to look through function `fromInteger`, whose implementation could
102 be anything. This poses difficulties for:
103
104 1. The expressive power of the check.
105 We cannot expect a reasonable implementation of pattern matching to detect
106 that fromInteger 2 ~ fromInteger 1 is True, unless we unfold function
107 fromInteger. This puts termination at risk and is undecidable in the
108 general case.
109
110 2. Performance.
111 Having an unresolved constraint False ~ (fromInteger 2 ~ fromInteger 1)
112 lying around could become expensive really fast. Ticket #11161 illustrates
113 how heavy use of overloaded literals can generate plenty of those
114 constraints, effectively undermining the term oracle's performance.
115
116 3. Error nessages/Warnings.
117 What should our message for `f` above be? A reasonable approach would be
118 to issue:
119
120 Pattern matches are (potentially) redundant:
121 f 2 = ... under the assumption that 1 == 2
122
123 but seems to complex and confusing for the user.
124
125 We choose to treat overloaded literals that look different as different. The
126 impact of this is the following:
127
128 * Redundancy checking is rather conservative, since it cannot see that clause
129 B above is redundant.
130
131 * We have instant equality check for overloaded literals (we do not rely on
132 the term oracle which is rather expensive, both in terms of performance and
133 memory). This significantly improves the performance of functions `covered`
134 `uncovered` and `divergent` in deSugar/Check.hs and effectively addresses
135 #11161.
136
137 * The warnings issued are simpler.
138
139 * We do not play on the safe side, strictly speaking. The assumption that
140 1 /= 2 makes the redundancy check more conservative but at the same time
141 makes its dual (exhaustiveness check) unsafe. This we can live with, mainly
142 for two reasons:
143 1. At the moment we do not use the results of the check during compilation
144 where this would be a disaster (could result in runtime errors even if
145 our function was deemed exhaustive).
146 2. Pattern matcing on literals can never be considered exhaustive unless we
147 have a catch-all clause. Hence, this assumption affects mainly the
148 appearance of the warnings and is, in practice safe.
149 -}
150
151 -- | A term constraint. @TVC x e@ encodes that @x@ is equal to @e@.
152 data TmVarCt = TVC !Id !PmExpr
153
154 instance Outputable TmVarCt where
155 ppr (TVC x e) = ppr x <+> char '~' <+> ppr e
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 -- -----------------------------------------------------------------------
166 -- ** Lift source expressions (HsExpr Id) to PmExpr
167
168 lhsExprToPmExpr :: LHsExpr GhcTc -> PmExpr
169 lhsExprToPmExpr (dL->L _ e) = hsExprToPmExpr e
170
171 hsExprToPmExpr :: HsExpr GhcTc -> PmExpr
172
173 -- Translating HsVar to flexible meta variables in the unification problem is
174 -- morally wrong, but it does the right thing for now.
175 -- In contrast to the situation in pattern matches, HsVars in expression syntax
176 -- are object language variables, most similar to rigid variables with an
177 -- unknown solution. The correct way would be to handle them through PmExprOther
178 -- and identify syntactically equal occurrences by the same rigid meta variable,
179 -- but we can't compare the wrapped HsExpr for equality. Hence we are stuck with
180 -- this hack.
181 hsExprToPmExpr (HsVar _ x) = PmExprVar (idName (unLoc x))
182
183 -- Translating HsConLikeOut to a flexible meta variable is misleading.
184 -- For an example why, consider `consAreRigid` in
185 -- `testsuite/tests/pmcheck/should_compile/PmExprVars.hs`.
186 -- hsExprToPmExpr (HsConLikeOut _ c) = PmExprVar (conLikeName c)
187
188 -- Desugar literal strings as a list of characters. For other literal values,
189 -- keep it as it is.
190 -- See `translatePat` in Check.hs (the `NPat` and `LitPat` case), and
191 -- Note [Translate Overloaded Literal for Exhaustiveness Checking].
192 hsExprToPmExpr (HsOverLit _ olit)
193 | OverLit (OverLitTc False ty) (HsIsString src s) _ <- olit, isStringTy ty
194 = stringExprToList src s
195 | otherwise = PmExprLit (PmOLit False olit)
196 hsExprToPmExpr (HsLit _ lit)
197 | HsString src s <- lit
198 = stringExprToList src s
199 | otherwise = PmExprLit (PmSLit lit)
200
201 hsExprToPmExpr e@(NegApp _ (dL->L _ neg_expr) _)
202 | PmExprLit (PmOLit False olit) <- hsExprToPmExpr neg_expr
203 -- NB: DON'T simply @(NegApp (NegApp olit))@ as @x@. when extension
204 -- @RebindableSyntax@ enabled, (-(-x)) may not equals to x.
205 = PmExprLit (PmOLit True olit)
206 | otherwise = PmExprOther e
207
208 hsExprToPmExpr (HsPar _ (dL->L _ e)) = hsExprToPmExpr e
209
210 hsExprToPmExpr e@(ExplicitTuple _ ps boxity)
211 | all tupArgPresent ps = mkPmExprData tuple_con tuple_args
212 | otherwise = PmExprOther e
213 where
214 tuple_con = tupleDataCon boxity (length ps)
215 tuple_args = [ lhsExprToPmExpr e | (dL->L _ (Present _ e)) <- ps ]
216
217 hsExprToPmExpr e@(ExplicitList _ mb_ol elems)
218 | Nothing <- mb_ol = foldr cons nil (map lhsExprToPmExpr elems)
219 | otherwise = PmExprOther e {- overloaded list: No PmExprApp -}
220 where
221 cons x xs = mkPmExprData consDataCon [x,xs]
222 nil = mkPmExprData nilDataCon []
223
224 -- we want this but we would have to make everything monadic :/
225 -- ./compiler/deSugar/DsMonad.hs:397:dsLookupDataCon :: Name -> DsM DataCon
226 --
227 -- hsExprToPmExpr (RecordCon c _ binds) = do
228 -- con <- dsLookupDataCon (unLoc c)
229 -- args <- mapM lhsExprToPmExpr (hsRecFieldsArgs binds)
230 -- return (PmExprCon con args)
231 hsExprToPmExpr e@(RecordCon {}) = PmExprOther e
232
233 hsExprToPmExpr (HsTick _ _ e) = lhsExprToPmExpr e
234 hsExprToPmExpr (HsBinTick _ _ _ e) = lhsExprToPmExpr e
235 hsExprToPmExpr (HsTickPragma _ _ _ _ e) = lhsExprToPmExpr e
236 hsExprToPmExpr (HsSCC _ _ _ e) = lhsExprToPmExpr e
237 hsExprToPmExpr (HsCoreAnn _ _ _ e) = lhsExprToPmExpr e
238 hsExprToPmExpr (ExprWithTySig _ e _) = lhsExprToPmExpr e
239 hsExprToPmExpr (HsWrap _ w e)
240 -- A dictionary application spoils e and we have no choice but to return an
241 -- PmExprOther. Same thing for other stuff that can't erased in the
242 -- compilation process. Otherwise this bites in
243 -- teststuite/tests/pmcheck/should_compile/PmExprVars.hs.
244 | isErasableHsWrapper w = hsExprToPmExpr e
245 hsExprToPmExpr e = PmExprOther e -- the rest are not handled by the oracle
246
247 stringExprToList :: SourceText -> FastString -> PmExpr
248 stringExprToList src s = foldr cons nil (map charToPmExpr (unpackFS s))
249 where
250 cons x xs = mkPmExprData consDataCon [x,xs]
251 nil = mkPmExprData nilDataCon []
252 charToPmExpr c = PmExprLit (PmSLit (HsChar src c))
253
254 {-
255 %************************************************************************
256 %* *
257 Pretty printing
258 %* *
259 %************************************************************************
260 -}
261
262 instance Outputable PmLit where
263 ppr (PmSLit l) = pmPprHsLit l
264 ppr (PmOLit neg l) = (if neg then char '-' else empty) <> ppr l
265
266 instance Outputable PmExpr where
267 ppr = go (0 :: Int)
268 where
269 go _ (PmExprLit l) = ppr l
270 go _ (PmExprVar v) = ppr v
271 go _ (PmExprOther e) = angleBrackets (ppr e)
272 go _ (PmExprCon (RealDataCon dc) args)
273 | isTupleDataCon dc = parens $ comma_sep $ map ppr args
274 | dc == consDataCon = brackets $ comma_sep $ map ppr (list_cells args)
275 where
276 comma_sep = fsep . punctuate comma
277 list_cells (hd:tl) = hd : list_cells tl
278 list_cells _ = []
279 go prec (PmExprCon cl args)
280 = cparen (null args || prec > 0) (hcat (ppr cl:map (go 1) args))