Encode shape information in `PmOracle`
[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
10 module PmExpr (
11 PmLit(..), PmLitValue(..), PmAltCon(..),
12 pmAltConType, PmEquality(..), eqPmAltCon,
13 pmLitType, literalToPmLit, negatePmLit, overloadPmLit,
14 pmLitAsStringLit, coreExprAsPmLit
15 ) where
16
17 #include "HsVersions.h"
18
19 import GhcPrelude
20
21 import Util
22 import FastString
23 import Id
24 import Name
25 import DataCon
26 import ConLike
27 import Outputable
28 import Maybes
29 import Type
30 import TyCon
31 import Literal
32 import CoreSyn
33 import CoreUtils (exprType)
34 import PrelNames
35 import TysWiredIn
36 import TysPrim
37
38 import Numeric (fromRat)
39 import Data.Foldable (find)
40 import Data.Ratio
41
42 {-
43 %************************************************************************
44 %* *
45 Lifted Expressions
46 %* *
47 %************************************************************************
48 -}
49
50 -- ----------------------------------------------------------------------------
51 -- ** Types
52
53 -- | Literals (simple and overloaded ones) for pattern match checking.
54 --
55 -- See Note [Undecidable Equality for PmAltCons]
56 data PmLit = PmLit
57 { pm_lit_ty :: Type
58 , pm_lit_val :: PmLitValue }
59
60 data PmLitValue
61 = PmLitInt Integer
62 | PmLitRat Rational
63 | PmLitChar Char
64 -- We won't actually see PmLitString in the oracle since we desugar strings to
65 -- lists
66 | PmLitString FastString
67 | PmLitOverInt Int {- How often Negated? -} Integer
68 | PmLitOverRat Int {- How often Negated? -} Rational
69 | PmLitOverString FastString
70
71 -- | Undecidable semantic equality result.
72 -- See Note [Undecidable Equality for PmAltCons]
73 data PmEquality
74 = Equal
75 | Disjoint
76 | PossiblyOverlap
77 deriving (Eq, Show)
78
79 -- | When 'PmEquality' can be decided. @True <=> Equal@, @False <=> Disjoint@.
80 decEquality :: Bool -> PmEquality
81 decEquality True = Equal
82 decEquality False = Disjoint
83
84 -- | Undecidable equality for values represented by 'PmLit's.
85 -- See Note [Undecidable Equality for PmAltCons]
86 --
87 -- * @Just True@ ==> Surely equal
88 -- * @Just False@ ==> Surely different (non-overlapping, even!)
89 -- * @Nothing@ ==> Equality relation undecidable
90 eqPmLit :: PmLit -> PmLit -> PmEquality
91 eqPmLit (PmLit t1 v1) (PmLit t2 v2)
92 -- no haddock | pprTrace "eqPmLit" (ppr t1 <+> ppr v1 $$ ppr t2 <+> ppr v2) False = undefined
93 | not (t1 `eqType` t2) = Disjoint
94 | otherwise = go v1 v2
95 where
96 go (PmLitInt i1) (PmLitInt i2) = decEquality (i1 == i2)
97 go (PmLitRat r1) (PmLitRat r2) = decEquality (r1 == r2)
98 go (PmLitChar c1) (PmLitChar c2) = decEquality (c1 == c2)
99 go (PmLitString s1) (PmLitString s2) = decEquality (s1 == s2)
100 go (PmLitOverInt n1 i1) (PmLitOverInt n2 i2)
101 | n1 == n2 && i1 == i2 = Equal
102 go (PmLitOverRat n1 r1) (PmLitOverRat n2 r2)
103 | n1 == n2 && r1 == r2 = Equal
104 go (PmLitOverString s1) (PmLitOverString s2)
105 | s1 == s2 = Equal
106 go _ _ = PossiblyOverlap
107
108 -- | Syntactic equality.
109 instance Eq PmLit where
110 a == b = eqPmLit a b == Equal
111
112 -- | Type of a 'PmLit'
113 pmLitType :: PmLit -> Type
114 pmLitType (PmLit ty _) = ty
115
116 -- | Type of a 'PmAltCon'
117 pmAltConType :: PmAltCon -> [Type] -> Type
118 pmAltConType (PmAltLit lit) _arg_tys = ASSERT( null _arg_tys ) pmLitType lit
119 pmAltConType (PmAltConLike con) arg_tys = conLikeResTy con arg_tys
120
121 -- | Undecidable equality for values represented by 'ConLike's.
122 -- See Note [Undecidable Equality for PmAltCons].
123 -- 'PatSynCon's aren't enforced to be generative, so two syntactically different
124 -- 'PatSynCon's might match the exact same values. Without looking into and
125 -- reasoning about the pattern synonym's definition, we can't decide if their
126 -- sets of matched values is different.
127 --
128 -- * @Just True@ ==> Surely equal
129 -- * @Just False@ ==> Surely different (non-overlapping, even!)
130 -- * @Nothing@ ==> Equality relation undecidable
131 eqConLike :: ConLike -> ConLike -> PmEquality
132 eqConLike (RealDataCon dc1) (RealDataCon dc2) = decEquality (dc1 == dc2)
133 eqConLike (PatSynCon psc1) (PatSynCon psc2)
134 | psc1 == psc2
135 = Equal
136 eqConLike _ _ = PossiblyOverlap
137
138 -- | Represents the head of a match against a 'ConLike' or literal.
139 -- Really similar to 'CoreSyn.AltCon'.
140 data PmAltCon = PmAltConLike ConLike
141 | PmAltLit PmLit
142
143 -- | We can't in general decide whether two 'PmAltCon's match the same set of
144 -- values. In addition to the reasons in 'eqPmLit' and 'eqConLike', a
145 -- 'PmAltConLike' might or might not represent the same value as a 'PmAltLit'.
146 -- See Note [Undecidable Equality for PmAltCons].
147 --
148 -- * @Just True@ ==> Surely equal
149 -- * @Just False@ ==> Surely different (non-overlapping, even!)
150 -- * @Nothing@ ==> Equality relation undecidable
151 --
152 -- Examples (omitting some constructor wrapping):
153 --
154 -- * @eqPmAltCon (LitInt 42) (LitInt 1) == Just False@: Lit equality is
155 -- decidable
156 -- * @eqPmAltCon (DataCon A) (DataCon B) == Just False@: DataCon equality is
157 -- decidable
158 -- * @eqPmAltCon (LitOverInt 42) (LitOverInt 1) == Nothing@: OverLit equality
159 -- is undecidable
160 -- * @eqPmAltCon (PatSyn PA) (PatSyn PB) == Nothing@: PatSyn equality is
161 -- undecidable
162 -- * @eqPmAltCon (DataCon I#) (LitInt 1) == Nothing@: DataCon to Lit
163 -- comparisons are undecidable without reasoning about the wrapped @Int#@
164 -- * @eqPmAltCon (LitOverInt 1) (LitOverInt 1) == Just True@: We assume
165 -- reflexivity for overloaded literals
166 -- * @eqPmAltCon (PatSyn PA) (PatSyn PA) == Just True@: We assume reflexivity
167 -- for Pattern Synonyms
168 eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality
169 eqPmAltCon (PmAltConLike cl1) (PmAltConLike cl2) = eqConLike cl1 cl2
170 eqPmAltCon (PmAltLit l1) (PmAltLit l2) = eqPmLit l1 l2
171 eqPmAltCon _ _ = PossiblyOverlap
172
173 -- | Syntactic equality.
174 instance Eq PmAltCon where
175 a == b = eqPmAltCon a b == Equal
176
177 {- Note [Undecidable Equality for PmAltCons]
178 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
179 Equality on overloaded literals is undecidable in the general case. Consider
180 the following example:
181
182 instance Num Bool where
183 ...
184 fromInteger 0 = False -- C-like representation of booleans
185 fromInteger _ = True
186
187 f :: Bool -> ()
188 f 1 = () -- Clause A
189 f 2 = () -- Clause B
190
191 Clause B is redundant but to detect this, we must decide the constraint:
192 @fromInteger 2 ~ fromInteger 1@ which means that we
193 have to look through function @fromInteger@, whose implementation could
194 be anything. This poses difficulties for:
195
196 1. The expressive power of the check.
197 We cannot expect a reasonable implementation of pattern matching to detect
198 that @fromInteger 2 ~ fromInteger 1@ is True, unless we unfold function
199 fromInteger. This puts termination at risk and is undecidable in the
200 general case.
201
202 2. Error messages/Warnings.
203 What should our message for @f@ above be? A reasonable approach would be
204 to issue:
205
206 Pattern matches are (potentially) redundant:
207 f 2 = ... under the assumption that 1 == 2
208
209 but seems to complex and confusing for the user.
210
211 We choose to equate only obviously equal overloaded literals, in all other cases
212 we signal undecidability by returning Nothing from 'eqPmAltCons'. We do
213 better for non-overloaded literals, because we know their fromInteger/fromString
214 implementation is actually injective, allowing us to simplify the constraint
215 @fromInteger 1 ~ fromInteger 2@ to @1 ~ 2@, which is trivially unsatisfiable.
216
217 The impact of this treatment of overloaded literals is the following:
218
219 * Redundancy checking is rather conservative, since it cannot see that clause
220 B above is redundant.
221
222 * We have instant equality check for overloaded literals (we do not rely on
223 the term oracle which is rather expensive, both in terms of performance and
224 memory). This significantly improves the performance of functions `covered`
225 `uncovered` and `divergent` in deSugar/Check.hs and effectively addresses
226 #11161.
227
228 * The warnings issued are simpler.
229
230 Similar reasoning applies to pattern synonyms: In contrast to data constructors,
231 which are generative, constraints like F a ~ G b for two different pattern
232 synonyms F and G aren't immediately unsatisfiable. We assume F a ~ F a, though.
233 -}
234
235 literalToPmLit :: Type -> Literal -> Maybe PmLit
236 literalToPmLit ty l = PmLit ty <$> go l
237 where
238 go (LitChar c) = Just (PmLitChar c)
239 go (LitFloat r) = Just (PmLitRat r)
240 go (LitDouble r) = Just (PmLitRat r)
241 go (LitString s) = Just (PmLitString (mkFastStringByteString s))
242 go (LitNumber _ i _) = Just (PmLitInt i)
243 go _ = Nothing
244
245 negatePmLit :: PmLit -> Maybe PmLit
246 negatePmLit (PmLit ty v) = PmLit ty <$> go v
247 where
248 go (PmLitInt i) = Just (PmLitInt (-i))
249 go (PmLitRat r) = Just (PmLitRat (-r))
250 go (PmLitOverInt n i) = Just (PmLitOverInt (n+1) i)
251 go (PmLitOverRat n r) = Just (PmLitOverRat (n+1) r)
252 go _ = Nothing
253
254 overloadPmLit :: Type -> PmLit -> Maybe PmLit
255 overloadPmLit ty (PmLit _ v) = PmLit ty <$> go v
256 where
257 go (PmLitInt i) = Just (PmLitOverInt 0 i)
258 go (PmLitRat r) = Just (PmLitOverRat 0 r)
259 go (PmLitString s)
260 | ty `eqType` stringTy = Just v
261 | otherwise = Just (PmLitOverString s)
262 go _ = Nothing
263
264 pmLitAsStringLit :: PmLit -> Maybe FastString
265 pmLitAsStringLit (PmLit _ (PmLitString s)) = Just s
266 pmLitAsStringLit _ = Nothing
267
268 -- ----------------------------------------------------------------------------
269 -- ** Predicates on PmExpr
270
271 -- -----------------------------------------------------------------------
272 -- ** Lift source expressions (HsExpr Id) to PmExpr
273
274 coreExprAsPmLit :: CoreExpr -> Maybe PmLit
275 -- coreExprAsPmLit e | pprTrace "coreExprAsPmLit" (ppr e) False = undefined
276 coreExprAsPmLit (Tick _t e) = coreExprAsPmLit e
277 coreExprAsPmLit (Lit l) = literalToPmLit (literalType l) l
278 coreExprAsPmLit e = case collectArgs e of
279 (Var x, [Lit l])
280 | Just dc <- isDataConWorkId_maybe x
281 , dc `elem` [intDataCon, wordDataCon, charDataCon, floatDataCon, doubleDataCon]
282 -> literalToPmLit (exprType e) l
283 (Var x, [_ty, Lit n, Lit d])
284 | Just dc <- isDataConWorkId_maybe x
285 , dataConName dc == ratioDataConName
286 -- HACK: just assume we have a literal double. This case only occurs for
287 -- overloaded lits anyway, so we immediately override type information
288 -> literalToPmLit (exprType e) (mkLitDouble (litValue n % litValue d))
289 (Var x, args)
290 -- Take care of -XRebindableSyntax. The last argument should be the (only)
291 -- integer literal, otherwise we can't really do much about it.
292 | [Lit l] <- dropWhile (not . is_lit) args
293 -- getOccFS because of -XRebindableSyntax
294 , getOccFS (idName x) == getOccFS fromIntegerName
295 -> literalToPmLit (literalType l) l >>= overloadPmLit (exprType e)
296 (Var x, args)
297 -- Similar to fromInteger case
298 | [r] <- dropWhile (not . is_ratio) args
299 , getOccFS (idName x) == getOccFS fromRationalName
300 -> coreExprAsPmLit r >>= overloadPmLit (exprType e)
301 (Var x, [Type _ty, _dict, s])
302 | idName x == fromStringName
303 -- NB: Calls coreExprAsPmLit and then overloadPmLit, so that we return PmLitOverStrings
304 -> coreExprAsPmLit s >>= overloadPmLit (exprType e)
305 -- These last two cases handle String literals
306 (Var x, [Type ty])
307 | Just dc <- isDataConWorkId_maybe x
308 , dc == nilDataCon
309 , ty `eqType` charTy
310 -> literalToPmLit stringTy (mkLitString "")
311 (Var x, [Lit l])
312 | idName x `elem` [unpackCStringName, unpackCStringUtf8Name]
313 -> literalToPmLit stringTy l
314 _ -> Nothing
315 where
316 is_lit Lit{} = True
317 is_lit _ = False
318 is_ratio (Type _) = False
319 is_ratio r
320 | Just (tc, _) <- splitTyConApp_maybe (exprType r)
321 = tyConName tc == ratioTyConName
322 | otherwise
323 = False
324
325 {-
326 %************************************************************************
327 %* *
328 Pretty printing
329 %* *
330 %************************************************************************
331 -}
332
333 instance Outputable PmLitValue where
334 ppr (PmLitInt i) = ppr i
335 ppr (PmLitRat r) = ppr (double (fromRat r)) -- good enough
336 ppr (PmLitChar c) = pprHsChar c
337 ppr (PmLitString s) = pprHsString s
338 ppr (PmLitOverInt n i) = minuses n (ppr i)
339 ppr (PmLitOverRat n r) = minuses n (ppr (double (fromRat r)))
340 ppr (PmLitOverString s) = pprHsString s
341
342 -- Take care of negated literals
343 minuses :: Int -> SDoc -> SDoc
344 minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n
345
346 instance Outputable PmLit where
347 ppr (PmLit ty v) = ppr v <> suffix
348 where
349 -- Some ad-hoc hackery for displaying proper lit suffixes based on type
350 tbl = [ (intPrimTy, primIntSuffix)
351 , (int64PrimTy, primInt64Suffix)
352 , (wordPrimTy, primWordSuffix)
353 , (word64PrimTy, primWord64Suffix)
354 , (charPrimTy, primCharSuffix)
355 , (floatPrimTy, primFloatSuffix)
356 , (doublePrimTy, primDoubleSuffix) ]
357 suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl)
358
359 instance Outputable PmAltCon where
360 ppr (PmAltConLike cl) = ppr cl
361 ppr (PmAltLit l) = ppr l
362
363 instance Outputable PmEquality where
364 ppr = text . show