never executed always true always false
1 {-# LANGUAGE ApplicativeDo #-}
2 {-# LANGUAGE ScopedTypeVariables #-}
3 {-# LANGUAGE ViewPatterns #-}
4 {-# LANGUAGE MultiWayIf #-}
5
6 -- | Domain types used in "GHC.HsToCore.Pmc.Solver".
7 -- The ultimate goal is to define 'Nabla', which models normalised refinement
8 -- types from the paper
9 -- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989).
10 module GHC.HsToCore.Pmc.Solver.Types (
11
12 -- * Normalised refinement types
13 BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
14 Nabla(..), Nablas(..), initNablas,
15 lookupRefuts, lookupSolution,
16
17 -- ** Looking up 'VarInfo'
18 lookupVarInfo, lookupVarInfoNT, trvVarInfo,
19
20 -- ** Caching residual COMPLETE sets
21 CompleteMatch, ResidualCompleteMatches(..), getRcm, isRcmInitialised,
22
23 -- ** Representations for Literals and AltCons
24 PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,
25 isPmAltConMatchStrict, pmAltConImplBangs,
26
27 -- *** PmAltConSet
28 PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet,
29 extendPmAltConSet, pmAltConSetElems,
30
31 -- *** Equality on 'PmAltCon's
32 PmEquality(..), eqPmAltCon,
33
34 -- *** Operations on 'PmLit'
35 literalToPmLit, negatePmLit, overloadPmLit,
36 pmLitAsStringLit, coreExprAsPmLit
37
38 ) where
39
40 import GHC.Prelude
41
42 import GHC.Data.Bag
43 import GHC.Data.FastString
44 import GHC.Types.Id
45 import GHC.Types.Var.Set
46 import GHC.Types.Unique.DSet
47 import GHC.Types.Unique.SDFM
48 import GHC.Types.Name
49 import GHC.Core.DataCon
50 import GHC.Core.ConLike
51 import GHC.Utils.Outputable
52 import GHC.Utils.Panic.Plain
53 import GHC.Utils.Misc (lastMaybe)
54 import GHC.Data.List.SetOps (unionLists)
55 import GHC.Data.Maybe
56 import GHC.Core.Type
57 import GHC.Core.TyCon
58 import GHC.Types.Literal
59 import GHC.Core
60 import GHC.Core.Map.Expr
61 import GHC.Core.Utils (exprType)
62 import GHC.Builtin.Names
63 import GHC.Builtin.Types
64 import GHC.Builtin.Types.Prim
65 import GHC.Tc.Solver.InertSet (InertSet, emptyInert)
66 import GHC.Tc.Utils.TcType (isStringTy)
67 import GHC.Types.CompleteMatch (CompleteMatch(..))
68 import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit
69 , fractionalLitFromRational
70 , FractionalExponentBase(..))
71 import Numeric (fromRat)
72 import Data.Foldable (find)
73 import Data.Ratio
74 import GHC.Real (Ratio(..))
75 import qualified Data.Semigroup as Semi
76
77 -- import GHC.Driver.Ppr
78
79 --
80 -- * Normalised refinement types
81 --
82
83 -- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of
84 -- canonical (i.e. mutually compatible) term and type constraints that form the
85 -- refinement type's predicate.
86 data Nabla
87 = MkNabla
88 { nabla_ty_st :: !TyState
89 -- ^ Type oracle; things like a~Int
90 , nabla_tm_st :: !TmState
91 -- ^ Term oracle; things like x~Nothing
92 }
93
94 -- | An initial nabla that is always satisfiable
95 initNabla :: Nabla
96 initNabla = MkNabla initTyState initTmState
97
98 instance Outputable Nabla where
99 ppr nabla = hang (text "Nabla") 2 $ vcat [
100 -- intentionally formatted this way enable the dev to comment in only
101 -- the info they need
102 ppr (nabla_tm_st nabla),
103 ppr (nabla_ty_st nabla)
104 ]
105
106 -- | A disjunctive bag of 'Nabla's, representing a refinement type.
107 newtype Nablas = MkNablas (Bag Nabla)
108
109 initNablas :: Nablas
110 initNablas = MkNablas (unitBag initNabla)
111
112 instance Outputable Nablas where
113 ppr (MkNablas nablas) = ppr nablas
114
115 instance Semigroup Nablas where
116 MkNablas l <> MkNablas r = MkNablas (l `unionBags` r)
117
118 instance Monoid Nablas where
119 mempty = MkNablas emptyBag
120
121 -- | The type oracle state. An 'GHC.Tc.Solver.Monad.InertSet' that we
122 -- incrementally add local type constraints to, together with a sequence
123 -- number that counts the number of times we extended it with new facts.
124 data TyState = TySt { ty_st_n :: !Int, ty_st_inert :: !InertSet }
125
126 -- | Not user-facing.
127 instance Outputable TyState where
128 ppr (TySt n inert) = ppr n <+> ppr inert
129
130 initTyState :: TyState
131 initTyState = TySt 0 emptyInert
132
133 -- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
134 -- entries are possibly shared when we figure out that two variables must be
135 -- equal, thus represent the same set of values.
136 --
137 -- See Note [TmState invariants] in "GHC.HsToCore.Pmc.Solver".
138 data TmState
139 = TmSt
140 { ts_facts :: !(UniqSDFM Id VarInfo)
141 -- ^ Facts about term variables. Deterministic env, so that we generate
142 -- deterministic error messages.
143 , ts_reps :: !(CoreMap Id)
144 -- ^ An environment for looking up whether we already encountered semantically
145 -- equivalent expressions that we want to represent by the same 'Id'
146 -- representative.
147 , ts_dirty :: !DIdSet
148 -- ^ Which 'VarInfo' needs to be checked for inhabitants because of new
149 -- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@).
150 }
151
152 -- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
153 -- and negative ('vi_neg') facts, like "x is not (:)".
154 -- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
155 -- ('vi_rcm').
156 --
157 -- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.Pmc.Solver".
158 data VarInfo
159 = VI
160 { vi_id :: !Id
161 -- ^ The 'Id' in question. Important for adding new constraints relative to
162 -- this 'VarInfo' when we don't easily have the 'Id' available.
163
164 , vi_pos :: ![PmAltConApp]
165 -- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
166 -- at the same time (i.e. conjunctive). We need a list because of nested
167 -- pattern matches involving pattern synonym
168 -- case x of { Just y -> case x of PatSyn z -> ... }
169 -- However, no more than one RealDataCon in the list, otherwise contradiction
170 -- because of generativity.
171
172 , vi_neg :: !PmAltConSet
173 -- ^ Negative info: A list of 'PmAltCon's that it cannot match.
174 -- Example, assuming
175 --
176 -- @
177 -- data T = Leaf Int | Branch T T | Node Int T
178 -- @
179 --
180 -- then @x ≁ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
181 -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos',
182 -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing
183 -- between 'vi_pos' and 'vi_neg'.
184
185 -- See Note [Why record both positive and negative info?]
186 -- It's worth having an actual set rather than a simple association list,
187 -- because files like Cabal's `LicenseId` define relatively huge enums
188 -- that lead to quadratic or worse behavior.
189
190 , vi_bot :: BotInfo
191 -- ^ Can this variable be ⊥? Models (mutually contradicting) @x ~ ⊥@ and
192 -- @x ≁ ⊥@ constraints. E.g.
193 -- * 'MaybeBot': Don't know; Neither @x ~ ⊥@ nor @x ≁ ⊥@.
194 -- * 'IsBot': @x ~ ⊥@
195 -- * 'IsNotBot': @x ≁ ⊥@
196
197 , vi_rcm :: !ResidualCompleteMatches
198 -- ^ A cache of the associated COMPLETE sets. At any time a superset of
199 -- possible constructors of each COMPLETE set. So, if it's not in here, we
200 -- can't possibly match on it. Complementary to 'vi_neg'. We still need it
201 -- to recognise completion of a COMPLETE set efficiently for large enums.
202 }
203
204 data PmAltConApp
205 = PACA
206 { paca_con :: !PmAltCon
207 , paca_tvs :: ![TyVar]
208 , paca_ids :: ![Id]
209 }
210
211 -- | See 'vi_bot'.
212 data BotInfo
213 = IsBot
214 | IsNotBot
215 | MaybeBot
216 deriving Eq
217
218 instance Outputable PmAltConApp where
219 ppr PACA{paca_con = con, paca_tvs = tvs, paca_ids = ids} =
220 hsep (ppr con : map ((char '@' <>) . ppr) tvs ++ map ppr ids)
221
222 instance Outputable BotInfo where
223 ppr MaybeBot = underscore
224 ppr IsBot = text "~⊥"
225 ppr IsNotBot = text "≁⊥"
226
227 -- | Not user-facing.
228 instance Outputable TmState where
229 ppr (TmSt state reps dirty) = ppr state $$ ppr reps $$ ppr dirty
230
231 -- | Not user-facing.
232 instance Outputable VarInfo where
233 ppr (VI x pos neg bot cache)
234 = braces (hcat (punctuate comma [pp_x, pp_pos, pp_neg, ppr bot, pp_cache]))
235 where
236 pp_x = ppr x <> dcolon <> ppr (idType x)
237 pp_pos
238 | [] <- pos = underscore
239 | [p] <- pos = char '~' <> ppr p -- suppress outer [_] if singleton
240 | otherwise = char '~' <> ppr pos
241 pp_neg
242 | isEmptyPmAltConSet neg = underscore
243 | otherwise = char '≁' <> ppr neg
244 pp_cache
245 | RCM Nothing Nothing <- cache = underscore
246 | otherwise = ppr cache
247
248 -- | Initial state of the term oracle.
249 initTmState :: TmState
250 initTmState = TmSt emptyUSDFM emptyCoreMap emptyDVarSet
251
252 -- | A data type that caches for the 'VarInfo' of @x@ the results of querying
253 -- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
254 -- which we already know @x ≁ K@ from these sets.
255 --
256 -- For motivation, see Section 5.3 in Lower Your Guards.
257 -- See also Note [Implementation of COMPLETE pragmas]
258 data ResidualCompleteMatches
259 = RCM
260 { rcm_vanilla :: !(Maybe CompleteMatch)
261 -- ^ The residual set for the vanilla COMPLETE set from the data defn.
262 -- Tracked separately from 'rcm_pragmas', because it might only be
263 -- known much later (when we have enough type information to see the 'TyCon'
264 -- of the match), or not at all even. Until that happens, it is 'Nothing'.
265 , rcm_pragmas :: !(Maybe [CompleteMatch])
266 -- ^ The residual sets for /all/ COMPLETE sets from pragmas that are
267 -- visible when compiling this module. Querying that set with
268 -- 'dsGetCompleteMatches' requires 'DsM', so we initialise it with 'Nothing'
269 -- until first needed in a 'DsM' context.
270 }
271
272 getRcm :: ResidualCompleteMatches -> [CompleteMatch]
273 getRcm (RCM vanilla pragmas) = maybeToList vanilla ++ fromMaybe [] pragmas
274
275 isRcmInitialised :: ResidualCompleteMatches -> Bool
276 isRcmInitialised (RCM vanilla pragmas) = isJust vanilla && isJust pragmas
277
278 instance Outputable ResidualCompleteMatches where
279 -- formats as "[{Nothing,Just},{P,Q}]"
280 ppr rcm = ppr (getRcm rcm)
281
282 -----------------------
283 -- * Looking up VarInfo
284
285 emptyRCM :: ResidualCompleteMatches
286 emptyRCM = RCM Nothing Nothing
287
288 emptyVarInfo :: Id -> VarInfo
289 emptyVarInfo x
290 = VI
291 { vi_id = x
292 , vi_pos = []
293 , vi_neg = emptyPmAltConSet
294 -- Case (3) in Note [Strict fields and fields of unlifted type]
295 -- in GHC.HsToCore.Pmc.Solver
296 , vi_bot = if isUnliftedType (idType x) then IsNotBot else MaybeBot
297 , vi_rcm = emptyRCM
298 }
299
300 lookupVarInfo :: TmState -> Id -> VarInfo
301 -- (lookupVarInfo tms x) tells what we know about 'x'
302 lookupVarInfo (TmSt env _ _) x = fromMaybe (emptyVarInfo x) (lookupUSDFM env x)
303
304 -- | Like @lookupVarInfo ts x@, but @lookupVarInfo ts x = (y, vi)@ also looks
305 -- through newtype constructors. We have @x ~ N1 (... (Nk y))@ such that the
306 -- returned @y@ doesn't have a positive newtype constructor constraint
307 -- associated with it (yet). The 'VarInfo' returned is that of @y@'s
308 -- representative.
309 --
310 -- Careful, this means that @idType x@ might be different to @idType y@, even
311 -- modulo type normalisation!
312 --
313 -- See also Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
314 lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
315 lookupVarInfoNT ts x = case lookupVarInfo ts x of
316 VI{ vi_pos = as_newtype -> Just y } -> lookupVarInfoNT ts y
317 res -> (x, res)
318 where
319 as_newtype = listToMaybe . mapMaybe go
320 go PACA{paca_con = PmAltConLike (RealDataCon dc), paca_ids = [y]}
321 | isNewDataCon dc = Just y
322 go _ = Nothing
323
324 trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
325 trvVarInfo f nabla@MkNabla{ nabla_tm_st = ts@TmSt{ts_facts = env} } x
326 = set_vi <$> f (lookupVarInfo ts x)
327 where
328 set_vi (a, vi') =
329 (a, nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env (vi_id vi') vi' } })
330
331 ------------------------------------------------
332 -- * Exported utility functions querying 'Nabla'
333
334 lookupRefuts :: Nabla -> Id -> [PmAltCon]
335 -- Unfortunately we need the extra bit of polymorphism and the unfortunate
336 -- duplication of lookupVarInfo here.
337 lookupRefuts MkNabla{ nabla_tm_st = ts } x =
338 pmAltConSetElems $ vi_neg $ lookupVarInfo ts x
339
340 isDataConSolution :: PmAltConApp -> Bool
341 isDataConSolution PACA{paca_con = PmAltConLike (RealDataCon _)} = True
342 isDataConSolution _ = False
343
344 -- @lookupSolution nabla x@ picks a single solution ('vi_pos') of @x@ from
345 -- possibly many, preferring 'RealDataCon' solutions whenever possible.
346 lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
347 lookupSolution nabla x = case vi_pos (lookupVarInfo (nabla_tm_st nabla) x) of
348 [] -> Nothing
349 pos
350 | Just sol <- find isDataConSolution pos -> Just sol
351 | otherwise -> Just (head pos)
352
353 --------------------------------------------------------------------------------
354 -- The rest is just providing an IR for (overloaded!) literals and AltCons that
355 -- sits between Hs and Core. We need a reliable way to detect and determine
356 -- equality between them, which is impossible with Hs (too expressive) and with
357 -- Core (no notion of overloaded literals, and even plain 'Int' literals are
358 -- actually constructor apps). Also String literals are troublesome.
359
360 -- | Literals (simple and overloaded ones) for pattern match checking.
361 --
362 -- See Note [Undecidable Equality for PmAltCons]
363 data PmLit = PmLit
364 { pm_lit_ty :: Type
365 , pm_lit_val :: PmLitValue }
366
367 data PmLitValue
368 = PmLitInt Integer
369 | PmLitRat Rational
370 | PmLitChar Char
371 -- We won't actually see PmLitString in the oracle since we desugar strings to
372 -- lists
373 | PmLitString FastString
374 | PmLitOverInt Int {- How often Negated? -} Integer
375 | PmLitOverRat Int {- How often Negated? -} FractionalLit
376 | PmLitOverString FastString
377
378 -- | Undecidable semantic equality result.
379 -- See Note [Undecidable Equality for PmAltCons]
380 data PmEquality
381 = Equal
382 | Disjoint
383 | PossiblyOverlap
384 deriving (Eq, Show)
385
386 -- | When 'PmEquality' can be decided. @True <=> Equal@, @False <=> Disjoint@.
387 decEquality :: Bool -> PmEquality
388 decEquality True = Equal
389 decEquality False = Disjoint
390
391 -- | Undecidable equality for values represented by 'PmLit's.
392 -- See Note [Undecidable Equality for PmAltCons]
393 --
394 -- * @Just True@ ==> Surely equal
395 -- * @Just False@ ==> Surely different (non-overlapping, even!)
396 -- * @Nothing@ ==> Equality relation undecidable
397 eqPmLit :: PmLit -> PmLit -> PmEquality
398 eqPmLit (PmLit t1 v1) (PmLit t2 v2)
399 -- no haddock | pprTrace "eqPmLit" (ppr t1 <+> ppr v1 $$ ppr t2 <+> ppr v2) False = undefined
400 | not (t1 `eqType` t2) = Disjoint
401 | otherwise = go v1 v2
402 where
403 go (PmLitInt i1) (PmLitInt i2) = decEquality (i1 == i2)
404 go (PmLitRat r1) (PmLitRat r2) = decEquality (r1 == r2)
405 go (PmLitChar c1) (PmLitChar c2) = decEquality (c1 == c2)
406 go (PmLitString s1) (PmLitString s2) = decEquality (s1 == s2)
407 go (PmLitOverInt n1 i1) (PmLitOverInt n2 i2)
408 | n1 == n2 && i1 == i2 = Equal
409 go (PmLitOverRat n1 r1) (PmLitOverRat n2 r2)
410 | n1 == n2 && r1 == r2 = Equal
411 go (PmLitOverString s1) (PmLitOverString s2)
412 | s1 == s2 = Equal
413 go _ _ = PossiblyOverlap
414
415 -- | Syntactic equality.
416 instance Eq PmLit where
417 a == b = eqPmLit a b == Equal
418
419 -- | Type of a 'PmLit'
420 pmLitType :: PmLit -> Type
421 pmLitType (PmLit ty _) = ty
422
423 -- | Undecidable equality for values represented by 'ConLike's.
424 -- See Note [Undecidable Equality for PmAltCons].
425 -- 'PatSynCon's aren't enforced to be generative, so two syntactically different
426 -- 'PatSynCon's might match the exact same values. Without looking into and
427 -- reasoning about the pattern synonym's definition, we can't decide if their
428 -- sets of matched values is different.
429 --
430 -- * @Just True@ ==> Surely equal
431 -- * @Just False@ ==> Surely different (non-overlapping, even!)
432 -- * @Nothing@ ==> Equality relation undecidable
433 eqConLike :: ConLike -> ConLike -> PmEquality
434 eqConLike (RealDataCon dc1) (RealDataCon dc2) = decEquality (dc1 == dc2)
435 eqConLike (PatSynCon psc1) (PatSynCon psc2)
436 | psc1 == psc2
437 = Equal
438 eqConLike _ _ = PossiblyOverlap
439
440 -- | Represents the head of a match against a 'ConLike' or literal.
441 -- Really similar to 'GHC.Core.AltCon'.
442 data PmAltCon = PmAltConLike ConLike
443 | PmAltLit PmLit
444
445 data PmAltConSet = PACS !(UniqDSet ConLike) ![PmLit]
446
447 emptyPmAltConSet :: PmAltConSet
448 emptyPmAltConSet = PACS emptyUniqDSet []
449
450 isEmptyPmAltConSet :: PmAltConSet -> Bool
451 isEmptyPmAltConSet (PACS cls lits) = isEmptyUniqDSet cls && null lits
452
453 -- | Whether there is a 'PmAltCon' in the 'PmAltConSet' that compares 'Equal' to
454 -- the given 'PmAltCon' according to 'eqPmAltCon'.
455 elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool
456 elemPmAltConSet (PmAltConLike cl) (PACS cls _ ) = elementOfUniqDSet cl cls
457 elemPmAltConSet (PmAltLit lit) (PACS _ lits) = elem lit lits
458
459 extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet
460 extendPmAltConSet (PACS cls lits) (PmAltConLike cl)
461 = PACS (addOneToUniqDSet cls cl) lits
462 extendPmAltConSet (PACS cls lits) (PmAltLit lit)
463 = PACS cls (unionLists lits [lit])
464
465 pmAltConSetElems :: PmAltConSet -> [PmAltCon]
466 pmAltConSetElems (PACS cls lits)
467 = map PmAltConLike (uniqDSetToList cls) ++ map PmAltLit lits
468
469 instance Outputable PmAltConSet where
470 ppr = ppr . pmAltConSetElems
471
472 -- | We can't in general decide whether two 'PmAltCon's match the same set of
473 -- values. In addition to the reasons in 'eqPmLit' and 'eqConLike', a
474 -- 'PmAltConLike' might or might not represent the same value as a 'PmAltLit'.
475 -- See Note [Undecidable Equality for PmAltCons].
476 --
477 -- * @Just True@ ==> Surely equal
478 -- * @Just False@ ==> Surely different (non-overlapping, even!)
479 -- * @Nothing@ ==> Equality relation undecidable
480 --
481 -- Examples (omitting some constructor wrapping):
482 --
483 -- * @eqPmAltCon (LitInt 42) (LitInt 1) == Just False@: Lit equality is
484 -- decidable
485 -- * @eqPmAltCon (DataCon A) (DataCon B) == Just False@: DataCon equality is
486 -- decidable
487 -- * @eqPmAltCon (LitOverInt 42) (LitOverInt 1) == Nothing@: OverLit equality
488 -- is undecidable
489 -- * @eqPmAltCon (PatSyn PA) (PatSyn PB) == Nothing@: PatSyn equality is
490 -- undecidable
491 -- * @eqPmAltCon (DataCon I#) (LitInt 1) == Nothing@: DataCon to Lit
492 -- comparisons are undecidable without reasoning about the wrapped @Int#@
493 -- * @eqPmAltCon (LitOverInt 1) (LitOverInt 1) == Just True@: We assume
494 -- reflexivity for overloaded literals
495 -- * @eqPmAltCon (PatSyn PA) (PatSyn PA) == Just True@: We assume reflexivity
496 -- for Pattern Synonyms
497 eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality
498 eqPmAltCon (PmAltConLike cl1) (PmAltConLike cl2) = eqConLike cl1 cl2
499 eqPmAltCon (PmAltLit l1) (PmAltLit l2) = eqPmLit l1 l2
500 eqPmAltCon _ _ = PossiblyOverlap
501
502 -- | Syntactic equality.
503 instance Eq PmAltCon where
504 a == b = eqPmAltCon a b == Equal
505
506 -- | Type of a 'PmAltCon'
507 pmAltConType :: PmAltCon -> [Type] -> Type
508 pmAltConType (PmAltLit lit) _arg_tys = assert (null _arg_tys ) $ pmLitType lit
509 pmAltConType (PmAltConLike con) arg_tys = conLikeResTy con arg_tys
510
511 -- | Is a match on this constructor forcing the match variable?
512 -- True of data constructors, literals and pattern synonyms (#17357), but not of
513 -- newtypes.
514 -- See Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
515 isPmAltConMatchStrict :: PmAltCon -> Bool
516 isPmAltConMatchStrict PmAltLit{} = True
517 isPmAltConMatchStrict (PmAltConLike PatSynCon{}) = True -- #17357
518 isPmAltConMatchStrict (PmAltConLike (RealDataCon dc)) = not (isNewDataCon dc)
519
520 pmAltConImplBangs :: PmAltCon -> [HsImplBang]
521 pmAltConImplBangs PmAltLit{} = []
522 pmAltConImplBangs (PmAltConLike con) = conLikeImplBangs con
523
524 {- Note [Undecidable Equality for PmAltCons]
525 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
526 Equality on overloaded literals is undecidable in the general case. Consider
527 the following example:
528
529 instance Num Bool where
530 ...
531 fromInteger 0 = False -- C-like representation of booleans
532 fromInteger _ = True
533
534 f :: Bool -> ()
535 f 1 = () -- Clause A
536 f 2 = () -- Clause B
537
538 Clause B is redundant but to detect this, we must decide the constraint:
539 @fromInteger 2 ~ fromInteger 1@ which means that we
540 have to look through function @fromInteger@, whose implementation could
541 be anything. This poses difficulties for:
542
543 1. The expressive power of the check.
544 We cannot expect a reasonable implementation of pattern matching to detect
545 that @fromInteger 2 ~ fromInteger 1@ is True, unless we unfold function
546 fromInteger. This puts termination at risk and is undecidable in the
547 general case.
548
549 2. Error messages/Warnings.
550 What should our message for @f@ above be? A reasonable approach would be
551 to issue:
552
553 Pattern matches are (potentially) redundant:
554 f 2 = ... under the assumption that 1 == 2
555
556 but seems to complex and confusing for the user.
557
558 We choose to equate only obviously equal overloaded literals, in all other cases
559 we signal undecidability by returning Nothing from 'eqPmAltCons'. We do
560 better for non-overloaded literals, because we know their fromInteger/fromString
561 implementation is actually injective, allowing us to simplify the constraint
562 @fromInteger 1 ~ fromInteger 2@ to @1 ~ 2@, which is trivially unsatisfiable.
563
564 The impact of this treatment of overloaded literals is the following:
565
566 * Redundancy checking is rather conservative, since it cannot see that clause
567 B above is redundant.
568
569 * We have instant equality check for overloaded literals (we do not rely on
570 the term oracle which is rather expensive, both in terms of performance and
571 memory). This significantly improves the performance of functions `covered`
572 `uncovered` and `divergent` in "GHC.HsToCore.Pmc" and effectively addresses
573 #11161.
574
575 * The warnings issued are simpler.
576
577 Similar reasoning applies to pattern synonyms: In contrast to data constructors,
578 which are generative, constraints like F a ~ G b for two different pattern
579 synonyms F and G aren't immediately unsatisfiable. We assume F a ~ F a, though.
580 -}
581
582 literalToPmLit :: Type -> Literal -> Maybe PmLit
583 literalToPmLit ty l = PmLit ty <$> go l
584 where
585 go (LitChar c) = Just (PmLitChar c)
586 go (LitFloat r) = Just (PmLitRat r)
587 go (LitDouble r) = Just (PmLitRat r)
588 go (LitString s) = Just (PmLitString (mkFastStringByteString s))
589 go (LitNumber _ i) = Just (PmLitInt i)
590 go _ = Nothing
591
592 negatePmLit :: PmLit -> Maybe PmLit
593 negatePmLit (PmLit ty v) = PmLit ty <$> go v
594 where
595 go (PmLitInt i) = Just (PmLitInt (-i))
596 go (PmLitRat r) = Just (PmLitRat (-r))
597 go (PmLitOverInt n i) = Just (PmLitOverInt (n+1) i)
598 go (PmLitOverRat n r) = Just (PmLitOverRat (n+1) r)
599 go _ = Nothing
600
601 overloadPmLit :: Type -> PmLit -> Maybe PmLit
602 overloadPmLit ty (PmLit _ v) = PmLit ty <$> go v
603 where
604 go (PmLitInt i) = Just (PmLitOverInt 0 i)
605 go (PmLitRat r) = Just $! PmLitOverRat 0 $! fractionalLitFromRational r
606 go (PmLitString s)
607 | ty `eqType` stringTy = Just v
608 | otherwise = Just (PmLitOverString s)
609 go ovRat@PmLitOverRat{} = Just ovRat
610 go _ = Nothing
611
612 pmLitAsStringLit :: PmLit -> Maybe FastString
613 pmLitAsStringLit (PmLit _ (PmLitString s)) = Just s
614 pmLitAsStringLit _ = Nothing
615
616 coreExprAsPmLit :: CoreExpr -> Maybe PmLit
617 -- coreExprAsPmLit e | pprTrace "coreExprAsPmLit" (ppr e) False = undefined
618 coreExprAsPmLit (Tick _t e) = coreExprAsPmLit e
619 coreExprAsPmLit (Lit l) = literalToPmLit (literalType l) l
620 coreExprAsPmLit e = case collectArgs e of
621 (Var x, [Lit l])
622 | Just dc <- isDataConWorkId_maybe x
623 , dc `elem` [intDataCon, wordDataCon, charDataCon, floatDataCon, doubleDataCon]
624 -> literalToPmLit (exprType e) l
625 (Var x, [Lit (LitNumber _ l)])
626 | Just (ty,l) <- bignum_lit_maybe x l
627 -> Just (PmLit ty (PmLitInt l))
628 (Var x, [_ty, n_arg, d_arg])
629 | Just dc <- isDataConWorkId_maybe x
630 , dataConName dc == ratioDataConName
631 , Just (PmLit _ (PmLitInt n)) <- coreExprAsPmLit n_arg
632 , Just (PmLit _ (PmLitInt d)) <- coreExprAsPmLit d_arg
633 -- HACK: just assume we have a literal double. This case only occurs for
634 -- overloaded lits anyway, so we immediately override type information
635 -> literalToPmLit (exprType e) (mkLitDouble (n % d))
636
637 (Var x, args)
638 -- See Note [Detecting overloaded literals with -XRebindableSyntax]
639 | is_rebound_name x fromIntegerName
640 , Just arg <- lastMaybe args
641 , Just (_ty,l) <- bignum_conapp_maybe arg
642 -> Just (PmLit integerTy (PmLitInt l)) >>= overloadPmLit (exprType e)
643 (Var x, args)
644 -- See Note [Detecting overloaded literals with -XRebindableSyntax]
645 -- fromRational <expr>
646 | is_rebound_name x fromRationalName
647 , [r] <- dropWhile (not . is_ratio) args
648 -> coreExprAsPmLit r >>= overloadPmLit (exprType e)
649
650 --Rationals with large exponents
651 (Var x, args)
652 -- See Note [Detecting overloaded literals with -XRebindableSyntax]
653 -- See Note [Dealing with rationals with large exponents]
654 -- mkRationalBase* <rational> <exponent>
655 | Just exp_base <- is_larg_exp_ratio x
656 , [r, exp] <- dropWhile (not . is_ratio) args
657 , (Var x, [_ty, n_arg, d_arg]) <- collectArgs r
658 , Just dc <- isDataConWorkId_maybe x
659 , dataConName dc == ratioDataConName
660 , Just (PmLit _ (PmLitInt n)) <- coreExprAsPmLit n_arg
661 , Just (PmLit _ (PmLitInt d)) <- coreExprAsPmLit d_arg
662 , Just (_exp_ty,exp') <- bignum_conapp_maybe exp
663 -> do
664 let rational = (abs n) :% d
665 let neg = if n < 0 then 1 else 0
666 let frac = mkFractionalLit NoSourceText False rational exp' exp_base
667 Just $ PmLit (exprType e) (PmLitOverRat neg frac)
668
669 (Var x, args)
670 | is_rebound_name x fromStringName
671 -- See Note [Detecting overloaded literals with -XRebindableSyntax]
672 , s:_ <- filter (isStringTy . exprType) $ filter isValArg args
673 -- NB: Calls coreExprAsPmLit and then overloadPmLit, so that we return PmLitOverStrings
674 -> coreExprAsPmLit s >>= overloadPmLit (exprType e)
675 -- These last two cases handle proper String literals
676 (Var x, [Type ty])
677 | Just dc <- isDataConWorkId_maybe x
678 , dc == nilDataCon
679 , ty `eqType` charTy
680 -> literalToPmLit stringTy (mkLitString "")
681 (Var x, [Lit l])
682 | idName x `elem` [unpackCStringName, unpackCStringUtf8Name]
683 -> literalToPmLit stringTy l
684
685 _ -> Nothing
686 where
687 bignum_conapp_maybe (App (Var x) (Lit (LitNumber _ l)))
688 = bignum_lit_maybe x l
689 bignum_conapp_maybe _ = Nothing
690
691 bignum_lit_maybe x l
692 | Just dc <- isDataConWorkId_maybe x
693 = if | dc == integerISDataCon -> Just (integerTy,l)
694 | dc == integerIPDataCon -> Just (integerTy,l)
695 | dc == integerINDataCon -> Just (integerTy,negate l)
696 | dc == naturalNSDataCon -> Just (naturalTy,l)
697 | dc == naturalNBDataCon -> Just (naturalTy,l)
698 | otherwise -> Nothing
699 bignum_lit_maybe _ _ = Nothing
700
701 is_ratio (Type _) = False
702 is_ratio r
703 | Just (tc, _) <- splitTyConApp_maybe (exprType r)
704 = tyConName tc == ratioTyConName
705 | otherwise
706 = False
707 is_larg_exp_ratio x
708 | is_rebound_name x mkRationalBase10Name
709 = Just Base10
710 | is_rebound_name x mkRationalBase2Name
711 = Just Base2
712 | otherwise
713 = Nothing
714
715
716 -- See Note [Detecting overloaded literals with -XRebindableSyntax]
717 is_rebound_name :: Id -> Name -> Bool
718 is_rebound_name x n = getOccFS (idName x) == getOccFS n
719
720 {- Note [Detecting overloaded literals with -XRebindableSyntax]
721 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
722 Normally, we'd find e.g. overloaded string literals by comparing the
723 application head of an expression to `fromStringName`. But that doesn't work
724 with -XRebindableSyntax: The `Name` of a user-provided `fromString` function is
725 different to `fromStringName`, which lives in a certain module, etc.
726
727 There really is no other way than to compare `OccName`s and guess which
728 argument is the actual literal string (we assume it's the first argument of
729 type `String`).
730
731 The same applies to other overloaded literals, such as overloaded rationals
732 (`fromRational`)and overloaded integer literals (`fromInteger`).
733
734 Note [Dealing with rationals with large exponents]
735 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
736 Rationals with large exponents are *not* desugared to
737 a simple rational. As that would require us to compute
738 their value which can be expensive. Rather they desugar
739 to an expression. For example 1e1000 will desugar to an
740 expression of the form: `mkRationalWithExponentBase10 (1 :% 1) 1000`
741
742 Only overloaded literals desugar to this form however, so we
743 we can just return a overloaded rational literal.
744
745 The most complex case is if we have RebindableSyntax enabled.
746 By example if we have a pattern like this: `f 3.3 = True`
747
748 It will desugar to:
749 fromRational
750 [TYPE: Rational, mkRationalBase10 (:% @Integer 10 1) (-1)]
751
752 The fromRational is properly detected as an overloaded Rational by
753 coreExprAsPmLit and it's general code for detecting overloaded rationals.
754 See Note [Detecting overloaded literals with -XRebindableSyntax].
755
756 This case then recurses into coreExprAsPmLit passing only the expression
757 `mkRationalBase10 (:% @Integer 10 1) (-1)`. Which is caught by rationals
758 with large exponents case. This will return a `PmLitOverRat` literal.
759
760 Which is then passed to overloadPmLit which simply returns it as-is since
761 it's already overloaded.
762
763 -}
764
765 instance Outputable PmLitValue where
766 ppr (PmLitInt i) = ppr i
767 ppr (PmLitRat r) = ppr (double (fromRat r)) -- good enough
768 ppr (PmLitChar c) = pprHsChar c
769 ppr (PmLitString s) = pprHsString s
770 ppr (PmLitOverInt n i) = minuses n (ppr i)
771 ppr (PmLitOverRat n r) = minuses n (ppr r)
772 ppr (PmLitOverString s) = pprHsString s
773
774 -- Take care of negated literals
775 minuses :: Int -> SDoc -> SDoc
776 minuses n sdoc = iterate (\sdoc -> parens (char '-' <> sdoc)) sdoc !! n
777
778 instance Outputable PmLit where
779 ppr (PmLit ty v) = ppr v <> suffix
780 where
781 -- Some ad-hoc hackery for displaying proper lit suffixes based on type
782 tbl = [ (intPrimTy, primIntSuffix)
783 , (int64PrimTy, primInt64Suffix)
784 , (wordPrimTy, primWordSuffix)
785 , (word64PrimTy, primWord64Suffix)
786 , (charPrimTy, primCharSuffix)
787 , (floatPrimTy, primFloatSuffix)
788 , (doublePrimTy, primDoubleSuffix) ]
789 suffix = fromMaybe empty (snd <$> find (eqType ty . fst) tbl)
790
791 instance Outputable PmAltCon where
792 ppr (PmAltConLike cl) = ppr cl
793 ppr (PmAltLit l) = ppr l
794
795 instance Outputable PmEquality where
796 ppr = text . show