{-# LANGUAGE ApplicativeDo       #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns        #-}
{-# LANGUAGE MultiWayIf          #-}

-- | Domain types used in "GHC.HsToCore.Pmc.Solver".
-- The ultimate goal is to define 'Nabla', which models normalised refinement
-- types from the paper
-- [Lower Your Guards: A Compositional Pattern-Match Coverage Checker"](https://dl.acm.org/doi/abs/10.1145/3408989).
module GHC.HsToCore.Pmc.Solver.Types (

        -- * Normalised refinement types
        BotInfo(..), PmAltConApp(..), VarInfo(..), TmState(..), TyState(..),
        Nabla(..), Nablas(..), initNablas,
        lookupRefuts, lookupSolution,

        -- ** Looking up 'VarInfo'
        lookupVarInfo, lookupVarInfoNT, trvVarInfo,

        -- ** Caching residual COMPLETE sets
        CompleteMatch, ResidualCompleteMatches(..), getRcm, isRcmInitialised,

        -- ** Representations for Literals and AltCons
        PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,
        isPmAltConMatchStrict, pmAltConImplBangs,

        -- *** PmAltConSet
        PmAltConSet, emptyPmAltConSet, isEmptyPmAltConSet, elemPmAltConSet,
        extendPmAltConSet, pmAltConSetElems,

        -- *** Equality on 'PmAltCon's
        PmEquality(..), eqPmAltCon,

        -- *** Operations on 'PmLit'
        literalToPmLit, negatePmLit, overloadPmLit,
        pmLitAsStringLit, coreExprAsPmLit

    ) where

import GHC.Prelude

import GHC.Data.Bag
import GHC.Data.FastString
import GHC.Types.Id
import GHC.Types.Var.Set
import GHC.Types.Unique.DSet
import GHC.Types.Unique.SDFM
import GHC.Types.Name
import GHC.Core.DataCon
import GHC.Core.ConLike
import GHC.Utils.Outputable
import GHC.Utils.Panic.Plain
import GHC.Utils.Misc (lastMaybe)
import GHC.Data.List.SetOps (unionLists)
import GHC.Data.Maybe
import GHC.Core.Type
import GHC.Core.TyCon
import GHC.Types.Literal
import GHC.Core
import GHC.Core.Map.Expr
import GHC.Core.Utils (exprType)
import GHC.Builtin.Names
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim
import GHC.Tc.Solver.InertSet (InertSet, emptyInert)
import GHC.Tc.Utils.TcType (isStringTy)
import GHC.Types.CompleteMatch (CompleteMatch(..))
import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit
                            , fractionalLitFromRational
                            , FractionalExponentBase(..))
import Numeric (fromRat)
import Data.Foldable (find)
import Data.Ratio
import GHC.Real (Ratio(..))
import qualified Data.Semigroup as Semi

-- import GHC.Driver.Ppr

--
-- * Normalised refinement types
--

-- | A normalised refinement type ∇ (\"nabla\"), comprised of an inert set of
-- canonical (i.e. mutually compatible) term and type constraints that form the
-- refinement type's predicate.
data Nabla
  = MkNabla
  { Nabla -> TyState
nabla_ty_st :: !TyState
  -- ^ Type oracle; things like a~Int
  , Nabla -> TmState
nabla_tm_st :: !TmState
  -- ^ Term oracle; things like x~Nothing
  }

-- | An initial nabla that is always satisfiable
initNabla :: Nabla
initNabla :: Nabla
initNabla = TyState -> TmState -> Nabla
MkNabla TyState
initTyState TmState
initTmState

instance Outputable Nabla where
  ppr :: Nabla -> SDoc
ppr Nabla
nabla = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Nabla") Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat [
      -- intentionally formatted this way enable the dev to comment in only
      -- the info they need
      TmState -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Nabla -> TmState
nabla_tm_st Nabla
nabla),
      TyState -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Nabla -> TyState
nabla_ty_st Nabla
nabla)
    ]

-- | A disjunctive bag of 'Nabla's, representing a refinement type.
newtype Nablas = MkNablas (Bag Nabla)

initNablas :: Nablas
initNablas :: Nablas
initNablas = Bag Nabla -> Nablas
MkNablas (Nabla -> Bag Nabla
forall a. a -> Bag a
unitBag Nabla
initNabla)

instance Outputable Nablas where
  ppr :: Nablas -> SDoc
ppr (MkNablas Bag Nabla
nablas) = Bag Nabla -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag Nabla
nablas

instance Semigroup Nablas where
  MkNablas Bag Nabla
l <> :: Nablas -> Nablas -> Nablas
<> MkNablas Bag Nabla
r = Bag Nabla -> Nablas
MkNablas (Bag Nabla
l Bag Nabla -> Bag Nabla -> Bag Nabla
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Nabla
r)

instance Monoid Nablas where
  mempty :: Nablas
mempty = Bag Nabla -> Nablas
MkNablas Bag Nabla
forall a. Bag a
emptyBag

-- | The type oracle state. An 'GHC.Tc.Solver.Monad.InertSet' that we
-- incrementally add local type constraints to, together with a sequence
-- number that counts the number of times we extended it with new facts.
data TyState = TySt { TyState -> Int
ty_st_n :: !Int, TyState -> InertSet
ty_st_inert :: !InertSet }

-- | Not user-facing.
instance Outputable TyState where
  ppr :: TyState -> SDoc
ppr (TySt Int
n InertSet
inert) = Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n SDoc -> SDoc -> SDoc
<+> InertSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr InertSet
inert

initTyState :: TyState
initTyState :: TyState
initTyState = Int -> InertSet -> TyState
TySt Int
0 InertSet
emptyInert

-- | The term oracle state. Stores 'VarInfo' for encountered 'Id's. These
-- entries are possibly shared when we figure out that two variables must be
-- equal, thus represent the same set of values.
--
-- See Note [TmState invariants] in "GHC.HsToCore.Pmc.Solver".
data TmState
  = TmSt
  { TmState -> UniqSDFM Id VarInfo
ts_facts :: !(UniqSDFM Id VarInfo)
  -- ^ Facts about term variables. Deterministic env, so that we generate
  -- deterministic error messages.
  , TmState -> CoreMap Id
ts_reps  :: !(CoreMap Id)
  -- ^ An environment for looking up whether we already encountered semantically
  -- equivalent expressions that we want to represent by the same 'Id'
  -- representative.
  , TmState -> DIdSet
ts_dirty :: !DIdSet
  -- ^ Which 'VarInfo' needs to be checked for inhabitants because of new
  -- negative constraints (e.g. @x ≁ ⊥@ or @x ≁ K@).
  }

-- | Information about an 'Id'. Stores positive ('vi_pos') facts, like @x ~ Just 42@,
-- and negative ('vi_neg') facts, like "x is not (:)".
-- Also caches the type ('vi_ty'), the 'ResidualCompleteMatches' of a COMPLETE set
-- ('vi_rcm').
--
-- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.Pmc.Solver".
data VarInfo
  = VI
  { VarInfo -> Id
vi_id  :: !Id
  -- ^ The 'Id' in question. Important for adding new constraints relative to
  -- this 'VarInfo' when we don't easily have the 'Id' available.

  , VarInfo -> [PmAltConApp]
vi_pos :: ![PmAltConApp]
  -- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
  -- at the same time (i.e. conjunctive).  We need a list because of nested
  -- pattern matches involving pattern synonym
  --    case x of { Just y -> case x of PatSyn z -> ... }
  -- However, no more than one RealDataCon in the list, otherwise contradiction
  -- because of generativity.

  , VarInfo -> PmAltConSet
vi_neg :: !PmAltConSet
  -- ^ Negative info: A list of 'PmAltCon's that it cannot match.
  -- Example, assuming
  --
  -- @
  --     data T = Leaf Int | Branch T T | Node Int T
  -- @
  --
  -- then @x ≁ [Leaf, Node]@ means that @x@ cannot match a @Leaf@ or @Node@,
  -- and hence can only match @Branch@. Is orthogonal to anything from 'vi_pos',
  -- in the sense that 'eqPmAltCon' returns @PossiblyOverlap@ for any pairing
  -- between 'vi_pos' and 'vi_neg'.

  -- See Note [Why record both positive and negative info?]
  -- It's worth having an actual set rather than a simple association list,
  -- because files like Cabal's `LicenseId` define relatively huge enums
  -- that lead to quadratic or worse behavior.

  , VarInfo -> BotInfo
vi_bot :: BotInfo
  -- ^ Can this variable be ⊥? Models (mutually contradicting) @x ~ ⊥@ and
  --   @x ≁ ⊥@ constraints. E.g.
  --    * 'MaybeBot': Don't know; Neither @x ~ ⊥@ nor @x ≁ ⊥@.
  --    * 'IsBot': @x ~ ⊥@
  --    * 'IsNotBot': @x ≁ ⊥@

  , VarInfo -> ResidualCompleteMatches
vi_rcm :: !ResidualCompleteMatches
  -- ^ A cache of the associated COMPLETE sets. At any time a superset of
  -- possible constructors of each COMPLETE set. So, if it's not in here, we
  -- can't possibly match on it. Complementary to 'vi_neg'. We still need it
  -- to recognise completion of a COMPLETE set efficiently for large enums.
  }

data PmAltConApp
  = PACA
  { PmAltConApp -> PmAltCon
paca_con :: !PmAltCon
  , PmAltConApp -> [Id]
paca_tvs :: ![TyVar]
  , PmAltConApp -> [Id]
paca_ids :: ![Id]
  }

-- | See 'vi_bot'.
data BotInfo
  = IsBot
  | IsNotBot
  | MaybeBot
  deriving BotInfo -> BotInfo -> Bool
(BotInfo -> BotInfo -> Bool)
-> (BotInfo -> BotInfo -> Bool) -> Eq BotInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BotInfo -> BotInfo -> Bool
== :: BotInfo -> BotInfo -> Bool
$c/= :: BotInfo -> BotInfo -> Bool
/= :: BotInfo -> BotInfo -> Bool
Eq

instance Outputable PmAltConApp where
  ppr :: PmAltConApp -> SDoc
ppr PACA{paca_con :: PmAltConApp -> PmAltCon
paca_con = PmAltCon
con, paca_tvs :: PmAltConApp -> [Id]
paca_tvs = [Id]
tvs, paca_ids :: PmAltConApp -> [Id]
paca_ids = [Id]
ids} =
    [SDoc] -> SDoc
hsep (PmAltCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmAltCon
con SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
: (Id -> SDoc) -> [Id] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> SDoc
char Char
'@' SDoc -> SDoc -> SDoc
<>) (SDoc -> SDoc) -> (Id -> SDoc) -> Id -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr) [Id]
tvs [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ (Id -> SDoc) -> [Id] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
ids)

instance Outputable BotInfo where
  ppr :: BotInfo -> SDoc
ppr BotInfo
MaybeBot = SDoc
underscore
  ppr BotInfo
IsBot    = String -> SDoc
text String
"~⊥"
  ppr BotInfo
IsNotBot = String -> SDoc
text String
"≁⊥"

-- | Not user-facing.
instance Outputable TmState where
  ppr :: TmState -> SDoc
ppr (TmSt UniqSDFM Id VarInfo
state CoreMap Id
reps DIdSet
dirty) = UniqSDFM Id VarInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr UniqSDFM Id VarInfo
state SDoc -> SDoc -> SDoc
$$ CoreMap Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreMap Id
reps SDoc -> SDoc -> SDoc
$$ DIdSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr DIdSet
dirty

-- | Not user-facing.
instance Outputable VarInfo where
  ppr :: VarInfo -> SDoc
ppr (VI Id
x [PmAltConApp]
pos PmAltConSet
neg BotInfo
bot ResidualCompleteMatches
cache)
    = SDoc -> SDoc
braces ([SDoc] -> SDoc
hcat (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma [SDoc
pp_x, SDoc
pp_pos, SDoc
pp_neg, BotInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr BotInfo
bot, SDoc
pp_cache]))
    where
      pp_x :: SDoc
pp_x = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<> SDoc
dcolon SDoc -> SDoc -> SDoc
<> Kind -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id -> Kind
idType Id
x)
      pp_pos :: SDoc
pp_pos
        | [] <- [PmAltConApp]
pos  = SDoc
underscore
        | [PmAltConApp
p] <- [PmAltConApp]
pos = Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<> PmAltConApp -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmAltConApp
p -- suppress outer [_] if singleton
        | Bool
otherwise  = Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<> [PmAltConApp] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [PmAltConApp]
pos
      pp_neg :: SDoc
pp_neg
        | PmAltConSet -> Bool
isEmptyPmAltConSet PmAltConSet
neg = SDoc
underscore
        | Bool
otherwise              = Char -> SDoc
char Char
'≁' SDoc -> SDoc -> SDoc
<> PmAltConSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmAltConSet
neg
      pp_cache :: SDoc
pp_cache
        | RCM Maybe CompleteMatch
Nothing Maybe [CompleteMatch]
Nothing <- ResidualCompleteMatches
cache = SDoc
underscore
        | Bool
otherwise                    = ResidualCompleteMatches -> SDoc
forall a. Outputable a => a -> SDoc
ppr ResidualCompleteMatches
cache

-- | Initial state of the term oracle.
initTmState :: TmState
initTmState :: TmState
initTmState = UniqSDFM Id VarInfo -> CoreMap Id -> DIdSet -> TmState
TmSt UniqSDFM Id VarInfo
forall key ele. UniqSDFM key ele
emptyUSDFM CoreMap Id
forall a. CoreMap a
emptyCoreMap DIdSet
emptyDVarSet

-- | A data type that caches for the 'VarInfo' of @x@ the results of querying
-- 'dsGetCompleteMatches' and then striking out all occurrences of @K@ for
-- which we already know @x ≁ K@ from these sets.
--
-- For motivation, see Section 5.3 in Lower Your Guards.
-- See also Note [Implementation of COMPLETE pragmas]
data ResidualCompleteMatches
  = RCM
  { ResidualCompleteMatches -> Maybe CompleteMatch
rcm_vanilla :: !(Maybe CompleteMatch)
  -- ^ The residual set for the vanilla COMPLETE set from the data defn.
  -- Tracked separately from 'rcm_pragmas', because it might only be
  -- known much later (when we have enough type information to see the 'TyCon'
  -- of the match), or not at all even. Until that happens, it is 'Nothing'.
  , ResidualCompleteMatches -> Maybe [CompleteMatch]
rcm_pragmas :: !(Maybe [CompleteMatch])
  -- ^ The residual sets for /all/ COMPLETE sets from pragmas that are
  -- visible when compiling this module. Querying that set with
  -- 'dsGetCompleteMatches' requires 'DsM', so we initialise it with 'Nothing'
  -- until first needed in a 'DsM' context.
  }

getRcm :: ResidualCompleteMatches -> [CompleteMatch]
getRcm :: ResidualCompleteMatches -> [CompleteMatch]
getRcm (RCM Maybe CompleteMatch
vanilla Maybe [CompleteMatch]
pragmas) = Maybe CompleteMatch -> [CompleteMatch]
forall a. Maybe a -> [a]
maybeToList Maybe CompleteMatch
vanilla [CompleteMatch] -> [CompleteMatch] -> [CompleteMatch]
forall a. [a] -> [a] -> [a]
++ [CompleteMatch] -> Maybe [CompleteMatch] -> [CompleteMatch]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [CompleteMatch]
pragmas

isRcmInitialised :: ResidualCompleteMatches -> Bool
isRcmInitialised :: ResidualCompleteMatches -> Bool
isRcmInitialised (RCM Maybe CompleteMatch
vanilla Maybe [CompleteMatch]
pragmas) = Maybe CompleteMatch -> Bool
forall a. Maybe a -> Bool
isJust Maybe CompleteMatch
vanilla Bool -> Bool -> Bool
&& Maybe [CompleteMatch] -> Bool
forall a. Maybe a -> Bool
isJust Maybe [CompleteMatch]
pragmas

instance Outputable ResidualCompleteMatches where
  -- formats as "[{Nothing,Just},{P,Q}]"
  ppr :: ResidualCompleteMatches -> SDoc
ppr ResidualCompleteMatches
rcm = [CompleteMatch] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (ResidualCompleteMatches -> [CompleteMatch]
getRcm ResidualCompleteMatches
rcm)

-----------------------
-- * Looking up VarInfo

emptyRCM :: ResidualCompleteMatches
emptyRCM :: ResidualCompleteMatches
emptyRCM = Maybe CompleteMatch
-> Maybe [CompleteMatch] -> ResidualCompleteMatches
RCM Maybe CompleteMatch
forall a. Maybe a
Nothing Maybe [CompleteMatch]
forall a. Maybe a
Nothing

emptyVarInfo :: Id -> VarInfo
emptyVarInfo :: Id -> VarInfo
emptyVarInfo Id
x
  = VI
  { vi_id :: Id
vi_id = Id
x
  , vi_pos :: [PmAltConApp]
vi_pos = []
  , vi_neg :: PmAltConSet
vi_neg = PmAltConSet
emptyPmAltConSet
  -- Why not set IsNotBot for unlifted type here?
  -- Because we'd have to trigger an inhabitation test, which we can't.
  -- See case (4) in Note [Strict fields and variables of unlifted type]
  -- in GHC.HsToCore.Pmc.Solver
  , vi_bot :: BotInfo
vi_bot = BotInfo
MaybeBot
  , vi_rcm :: ResidualCompleteMatches
vi_rcm = ResidualCompleteMatches
emptyRCM
  }

lookupVarInfo :: TmState -> Id -> VarInfo
-- (lookupVarInfo tms x) tells what we know about 'x'
lookupVarInfo :: TmState -> Id -> VarInfo
lookupVarInfo (TmSt UniqSDFM Id VarInfo
env CoreMap Id
_ DIdSet
_) Id
x = VarInfo -> Maybe VarInfo -> VarInfo
forall a. a -> Maybe a -> a
fromMaybe (Id -> VarInfo
emptyVarInfo Id
x) (UniqSDFM Id VarInfo -> Id -> Maybe VarInfo
forall key ele.
Uniquable key =>
UniqSDFM key ele -> key -> Maybe ele
lookupUSDFM UniqSDFM Id VarInfo
env Id
x)

-- | Like @lookupVarInfo ts x@, but @lookupVarInfo ts x = (y, vi)@ also looks
-- through newtype constructors. We have @x ~ N1 (... (Nk y))@ such that the
-- returned @y@ doesn't have a positive newtype constructor constraint
-- associated with it (yet). The 'VarInfo' returned is that of @y@'s
-- representative.
--
-- Careful, this means that @idType x@ might be different to @idType y@, even
-- modulo type normalisation!
--
-- See also Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
lookupVarInfoNT :: TmState -> Id -> (Id, VarInfo)
lookupVarInfoNT TmState
ts Id
x = case TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x of
  VI{ vi_pos :: VarInfo -> [PmAltConApp]
vi_pos = [PmAltConApp] -> Maybe Id
as_newtype -> Just Id
y } -> TmState -> Id -> (Id, VarInfo)
lookupVarInfoNT TmState
ts Id
y
  VarInfo
res                                 -> (Id
x, VarInfo
res)
  where
    as_newtype :: [PmAltConApp] -> Maybe Id
as_newtype = [Id] -> Maybe Id
forall a. [a] -> Maybe a
listToMaybe ([Id] -> Maybe Id)
-> ([PmAltConApp] -> [Id]) -> [PmAltConApp] -> Maybe Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PmAltConApp -> Maybe Id) -> [PmAltConApp] -> [Id]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PmAltConApp -> Maybe Id
go
    go :: PmAltConApp -> Maybe Id
go PACA{paca_con :: PmAltConApp -> PmAltCon
paca_con = PmAltConLike (RealDataCon DataCon
dc), paca_ids :: PmAltConApp -> [Id]
paca_ids = [Id
y]}
      | DataCon -> Bool
isNewDataCon DataCon
dc = Id -> Maybe Id
forall a. a -> Maybe a
Just Id
y
    go PmAltConApp
_                = Maybe Id
forall a. Maybe a
Nothing

trvVarInfo :: Functor f => (VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
trvVarInfo :: forall (f :: * -> *) a.
Functor f =>
(VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
trvVarInfo VarInfo -> f (a, VarInfo)
f nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env} } Id
x
  = (a, VarInfo) -> (a, Nabla)
set_vi ((a, VarInfo) -> (a, Nabla)) -> f (a, VarInfo) -> f (a, Nabla)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarInfo -> f (a, VarInfo)
f (TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x)
  where
    set_vi :: (a, VarInfo) -> (a, Nabla)
set_vi (a
a, VarInfo
vi') =
      (a
a, Nabla
nabla{ nabla_tm_st :: TmState
nabla_tm_st = TmState
ts{ ts_facts :: UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo -> Id -> VarInfo -> UniqSDFM Id VarInfo
forall key ele.
Uniquable key =>
UniqSDFM key ele -> key -> ele -> UniqSDFM key ele
addToUSDFM UniqSDFM Id VarInfo
env (VarInfo -> Id
vi_id VarInfo
vi') VarInfo
vi' } })

------------------------------------------------
-- * Exported utility functions querying 'Nabla'

lookupRefuts :: Nabla -> Id -> [PmAltCon]
-- Unfortunately we need the extra bit of polymorphism and the unfortunate
-- duplication of lookupVarInfo here.
lookupRefuts :: Nabla -> Id -> [PmAltCon]
lookupRefuts MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = TmState
ts } Id
x =
  PmAltConSet -> [PmAltCon]
pmAltConSetElems (PmAltConSet -> [PmAltCon]) -> PmAltConSet -> [PmAltCon]
forall a b. (a -> b) -> a -> b
$ VarInfo -> PmAltConSet
vi_neg (VarInfo -> PmAltConSet) -> VarInfo -> PmAltConSet
forall a b. (a -> b) -> a -> b
$ TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x

isDataConSolution :: PmAltConApp -> Bool
isDataConSolution :: PmAltConApp -> Bool
isDataConSolution PACA{paca_con :: PmAltConApp -> PmAltCon
paca_con = PmAltConLike (RealDataCon DataCon
_)} = Bool
True
isDataConSolution PmAltConApp
_                                             = Bool
False

-- @lookupSolution nabla x@ picks a single solution ('vi_pos') of @x@ from
-- possibly many, preferring 'RealDataCon' solutions whenever possible.
lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
lookupSolution :: Nabla -> Id -> Maybe PmAltConApp
lookupSolution Nabla
nabla Id
x = case VarInfo -> [PmAltConApp]
vi_pos (TmState -> Id -> VarInfo
lookupVarInfo (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x) of
  []                                         -> Maybe PmAltConApp
forall a. Maybe a
Nothing
  [PmAltConApp]
pos
    | Just PmAltConApp
sol <- (PmAltConApp -> Bool) -> [PmAltConApp] -> Maybe PmAltConApp
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find PmAltConApp -> Bool
isDataConSolution [PmAltConApp]
pos -> PmAltConApp -> Maybe PmAltConApp
forall a. a -> Maybe a
Just PmAltConApp
sol
    | Bool
otherwise                              -> PmAltConApp -> Maybe PmAltConApp
forall a. a -> Maybe a
Just ([PmAltConApp] -> PmAltConApp
forall a. HasCallStack => [a] -> a
head [PmAltConApp]
pos)

--------------------------------------------------------------------------------
-- The rest is just providing an IR for (overloaded!) literals and AltCons that
-- sits between Hs and Core. We need a reliable way to detect and determine
-- equality between them, which is impossible with Hs (too expressive) and with
-- Core (no notion of overloaded literals, and even plain 'Int' literals are
-- actually constructor apps). Also String literals are troublesome.

-- | Literals (simple and overloaded ones) for pattern match checking.
--
-- See Note [Undecidable Equality for PmAltCons]
data PmLit = PmLit
           { PmLit -> Kind
pm_lit_ty  :: Type
           , PmLit -> PmLitValue
pm_lit_val :: PmLitValue }

data PmLitValue
  = PmLitInt Integer
  | PmLitRat Rational
  | PmLitChar Char
  -- We won't actually see PmLitString in the oracle since we desugar strings to
  -- lists
  | PmLitString FastString
  | PmLitOverInt Int {- How often Negated? -} Integer
  | PmLitOverRat Int {- How often Negated? -} FractionalLit
  | PmLitOverString FastString

-- | Undecidable semantic equality result.
-- See Note [Undecidable Equality for PmAltCons]
data PmEquality
  = Equal
  | Disjoint
  | PossiblyOverlap
  deriving (PmEquality -> PmEquality -> Bool
(PmEquality -> PmEquality -> Bool)
-> (PmEquality -> PmEquality -> Bool) -> Eq PmEquality
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PmEquality -> PmEquality -> Bool
== :: PmEquality -> PmEquality -> Bool
$c/= :: PmEquality -> PmEquality -> Bool
/= :: PmEquality -> PmEquality -> Bool
Eq, Int -> PmEquality -> ShowS
[PmEquality] -> ShowS
PmEquality -> String
(Int -> PmEquality -> ShowS)
-> (PmEquality -> String)
-> ([PmEquality] -> ShowS)
-> Show PmEquality
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PmEquality -> ShowS
showsPrec :: Int -> PmEquality -> ShowS
$cshow :: PmEquality -> String
show :: PmEquality -> String
$cshowList :: [PmEquality] -> ShowS
showList :: [PmEquality] -> ShowS
Show)

-- | When 'PmEquality' can be decided. @True <=> Equal@, @False <=> Disjoint@.
decEquality :: Bool -> PmEquality
decEquality :: Bool -> PmEquality
decEquality Bool
True  = PmEquality
Equal
decEquality Bool
False = PmEquality
Disjoint

-- | Undecidable equality for values represented by 'PmLit's.
-- See Note [Undecidable Equality for PmAltCons]
--
-- * @Just True@ ==> Surely equal
-- * @Just False@ ==> Surely different (non-overlapping, even!)
-- * @Nothing@ ==> Equality relation undecidable
eqPmLit :: PmLit -> PmLit -> PmEquality
eqPmLit :: PmLit -> PmLit -> PmEquality
eqPmLit (PmLit Kind
t1 PmLitValue
v1) (PmLit Kind
t2 PmLitValue
v2)
  -- no haddock | pprTrace "eqPmLit" (ppr t1 <+> ppr v1 $$ ppr t2 <+> ppr v2) False = undefined
  | Bool -> Bool
not (Kind
t1 Kind -> Kind -> Bool
`eqType` Kind
t2) = PmEquality
Disjoint
  | Bool
otherwise            = PmLitValue -> PmLitValue -> PmEquality
go PmLitValue
v1 PmLitValue
v2
  where
    go :: PmLitValue -> PmLitValue -> PmEquality
go (PmLitInt Integer
i1)        (PmLitInt Integer
i2)        = Bool -> PmEquality
decEquality (Integer
i1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
i2)
    go (PmLitRat Rational
r1)        (PmLitRat Rational
r2)        = Bool -> PmEquality
decEquality (Rational
r1 Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
r2)
    go (PmLitChar Char
c1)       (PmLitChar Char
c2)       = Bool -> PmEquality
decEquality (Char
c1 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c2)
    go (PmLitString FastString
s1)     (PmLitString FastString
s2)     = Bool -> PmEquality
decEquality (FastString
s1 FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
s2)
    go (PmLitOverInt Int
n1 Integer
i1) (PmLitOverInt Int
n2 Integer
i2)
      | Int
n1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n2 Bool -> Bool -> Bool
&& Integer
i1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
i2                     = PmEquality
Equal
    go (PmLitOverRat Int
n1 FractionalLit
r1) (PmLitOverRat Int
n2 FractionalLit
r2)
      | Int
n1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n2 Bool -> Bool -> Bool
&& FractionalLit
r1 FractionalLit -> FractionalLit -> Bool
forall a. Eq a => a -> a -> Bool
== FractionalLit
r2                     = PmEquality
Equal
    go (PmLitOverString FastString
s1) (PmLitOverString FastString
s2)
      | FastString
s1 FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== FastString
s2                                 = PmEquality
Equal
    go PmLitValue
_                    PmLitValue
_                    = PmEquality
PossiblyOverlap

-- | Syntactic equality.
instance Eq PmLit where
  PmLit
a == :: PmLit -> PmLit -> Bool
== PmLit
b = PmLit -> PmLit -> PmEquality
eqPmLit PmLit
a PmLit
b PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
Equal

-- | Type of a 'PmLit'
pmLitType :: PmLit -> Type
pmLitType :: PmLit -> Kind
pmLitType (PmLit Kind
ty PmLitValue
_) = Kind
ty

-- | Undecidable equality for values represented by 'ConLike's.
-- See Note [Undecidable Equality for PmAltCons].
-- 'PatSynCon's aren't enforced to be generative, so two syntactically different
-- 'PatSynCon's might match the exact same values. Without looking into and
-- reasoning about the pattern synonym's definition, we can't decide if their
-- sets of matched values is different.
--
-- * @Just True@ ==> Surely equal
-- * @Just False@ ==> Surely different (non-overlapping, even!)
-- * @Nothing@ ==> Equality relation undecidable
eqConLike :: ConLike -> ConLike -> PmEquality
eqConLike :: ConLike -> ConLike -> PmEquality
eqConLike (RealDataCon DataCon
dc1) (RealDataCon DataCon
dc2) = Bool -> PmEquality
decEquality (DataCon
dc1 DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
dc2)
eqConLike (PatSynCon PatSyn
psc1)  (PatSynCon PatSyn
psc2)
  | PatSyn
psc1 PatSyn -> PatSyn -> Bool
forall a. Eq a => a -> a -> Bool
== PatSyn
psc2
  = PmEquality
Equal
eqConLike ConLike
_                 ConLike
_                 = PmEquality
PossiblyOverlap

-- | Represents the head of a match against a 'ConLike' or literal.
-- Really similar to 'GHC.Core.AltCon'.
data PmAltCon = PmAltConLike ConLike
              | PmAltLit     PmLit

data PmAltConSet = PACS !(UniqDSet ConLike) ![PmLit]

emptyPmAltConSet :: PmAltConSet
emptyPmAltConSet :: PmAltConSet
emptyPmAltConSet = UniqDSet ConLike -> [PmLit] -> PmAltConSet
PACS UniqDSet ConLike
forall a. UniqDSet a
emptyUniqDSet []

isEmptyPmAltConSet :: PmAltConSet -> Bool
isEmptyPmAltConSet :: PmAltConSet -> Bool
isEmptyPmAltConSet (PACS UniqDSet ConLike
cls [PmLit]
lits) = UniqDSet ConLike -> Bool
forall a. UniqDSet a -> Bool
isEmptyUniqDSet UniqDSet ConLike
cls Bool -> Bool -> Bool
&& [PmLit] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PmLit]
lits

-- | Whether there is a 'PmAltCon' in the 'PmAltConSet' that compares 'Equal' to
-- the given 'PmAltCon' according to 'eqPmAltCon'.
elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool
elemPmAltConSet :: PmAltCon -> PmAltConSet -> Bool
elemPmAltConSet (PmAltConLike ConLike
cl) (PACS UniqDSet ConLike
cls [PmLit]
_   ) = ConLike -> UniqDSet ConLike -> Bool
forall a. Uniquable a => a -> UniqDSet a -> Bool
elementOfUniqDSet ConLike
cl UniqDSet ConLike
cls
elemPmAltConSet (PmAltLit PmLit
lit)    (PACS UniqDSet ConLike
_   [PmLit]
lits) = PmLit -> [PmLit] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem PmLit
lit [PmLit]
lits

extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet
extendPmAltConSet :: PmAltConSet -> PmAltCon -> PmAltConSet
extendPmAltConSet (PACS UniqDSet ConLike
cls [PmLit]
lits) (PmAltConLike ConLike
cl)
  = UniqDSet ConLike -> [PmLit] -> PmAltConSet
PACS (UniqDSet ConLike -> ConLike -> UniqDSet ConLike
forall a. Uniquable a => UniqDSet a -> a -> UniqDSet a
addOneToUniqDSet UniqDSet ConLike
cls ConLike
cl) [PmLit]
lits
extendPmAltConSet (PACS UniqDSet ConLike
cls [PmLit]
lits) (PmAltLit PmLit
lit)
  = UniqDSet ConLike -> [PmLit] -> PmAltConSet
PACS UniqDSet ConLike
cls ([PmLit] -> [PmLit] -> [PmLit]
forall a.
(() :: Constraint, Outputable a, Eq a) =>
[a] -> [a] -> [a]
unionLists [PmLit]
lits [PmLit
lit])

pmAltConSetElems :: PmAltConSet -> [PmAltCon]
pmAltConSetElems :: PmAltConSet -> [PmAltCon]
pmAltConSetElems (PACS UniqDSet ConLike
cls [PmLit]
lits)
  = (ConLike -> PmAltCon) -> [ConLike] -> [PmAltCon]
forall a b. (a -> b) -> [a] -> [b]
map ConLike -> PmAltCon
PmAltConLike (UniqDSet ConLike -> [ConLike]
forall a. UniqDSet a -> [a]
uniqDSetToList UniqDSet ConLike
cls) [PmAltCon] -> [PmAltCon] -> [PmAltCon]
forall a. [a] -> [a] -> [a]
++ (PmLit -> PmAltCon) -> [PmLit] -> [PmAltCon]
forall a b. (a -> b) -> [a] -> [b]
map PmLit -> PmAltCon
PmAltLit [PmLit]
lits

instance Outputable PmAltConSet where
  ppr :: PmAltConSet -> SDoc
ppr = [PmAltCon] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([PmAltCon] -> SDoc)
-> (PmAltConSet -> [PmAltCon]) -> PmAltConSet -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltConSet -> [PmAltCon]
pmAltConSetElems

-- | We can't in general decide whether two 'PmAltCon's match the same set of
-- values. In addition to the reasons in 'eqPmLit' and 'eqConLike', a
-- 'PmAltConLike' might or might not represent the same value as a 'PmAltLit'.
-- See Note [Undecidable Equality for PmAltCons].
--
-- * @Just True@ ==> Surely equal
-- * @Just False@ ==> Surely different (non-overlapping, even!)
-- * @Nothing@ ==> Equality relation undecidable
--
-- Examples (omitting some constructor wrapping):
--
-- * @eqPmAltCon (LitInt 42) (LitInt 1) == Just False@: Lit equality is
--   decidable
-- * @eqPmAltCon (DataCon A) (DataCon B) == Just False@: DataCon equality is
--   decidable
-- * @eqPmAltCon (LitOverInt 42) (LitOverInt 1) == Nothing@: OverLit equality
--   is undecidable
-- * @eqPmAltCon (PatSyn PA) (PatSyn PB) == Nothing@: PatSyn equality is
--   undecidable
-- * @eqPmAltCon (DataCon I#) (LitInt 1) == Nothing@: DataCon to Lit
--   comparisons are undecidable without reasoning about the wrapped @Int#@
-- * @eqPmAltCon (LitOverInt 1) (LitOverInt 1) == Just True@: We assume
--   reflexivity for overloaded literals
-- * @eqPmAltCon (PatSyn PA) (PatSyn PA) == Just True@: We assume reflexivity
--   for Pattern Synonyms
eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon :: PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon (PmAltConLike ConLike
cl1) (PmAltConLike ConLike
cl2) = ConLike -> ConLike -> PmEquality
eqConLike ConLike
cl1 ConLike
cl2
eqPmAltCon (PmAltLit     PmLit
l1)  (PmAltLit     PmLit
l2)  = PmLit -> PmLit -> PmEquality
eqPmLit PmLit
l1 PmLit
l2
eqPmAltCon PmAltCon
_                  PmAltCon
_                  = PmEquality
PossiblyOverlap

-- | Syntactic equality.
instance Eq PmAltCon where
  PmAltCon
a == :: PmAltCon -> PmAltCon -> Bool
== PmAltCon
b = PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
a PmAltCon
b PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
Equal

-- | Type of a 'PmAltCon'
pmAltConType :: PmAltCon -> [Type] -> Type
pmAltConType :: PmAltCon -> [Kind] -> Kind
pmAltConType (PmAltLit PmLit
lit)     [Kind]
_arg_tys = Bool -> Kind -> Kind
forall a. HasCallStack => Bool -> a -> a
assert ([Kind] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Kind]
_arg_tys ) (Kind -> Kind) -> Kind -> Kind
forall a b. (a -> b) -> a -> b
$ PmLit -> Kind
pmLitType PmLit
lit
pmAltConType (PmAltConLike ConLike
con) [Kind]
arg_tys  = ConLike -> [Kind] -> Kind
conLikeResTy ConLike
con [Kind]
arg_tys

-- | Is a match on this constructor forcing the match variable?
-- True of data constructors, literals and pattern synonyms (#17357), but not of
-- newtypes.
-- See Note [Coverage checking Newtype matches] in GHC.HsToCore.Pmc.Solver.
isPmAltConMatchStrict :: PmAltCon -> Bool
isPmAltConMatchStrict :: PmAltCon -> Bool
isPmAltConMatchStrict PmAltLit{}                      = Bool
True
isPmAltConMatchStrict (PmAltConLike PatSynCon{})      = Bool
True -- #17357
isPmAltConMatchStrict (PmAltConLike (RealDataCon DataCon
dc)) = Bool -> Bool
not (DataCon -> Bool
isNewDataCon DataCon
dc)

pmAltConImplBangs :: PmAltCon -> [HsImplBang]
pmAltConImplBangs :: PmAltCon -> [HsImplBang]
pmAltConImplBangs PmAltLit{}         = []
pmAltConImplBangs (PmAltConLike ConLike
con) = ConLike -> [HsImplBang]
conLikeImplBangs ConLike
con

{- Note [Undecidable Equality for PmAltCons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Equality on overloaded literals is undecidable in the general case. Consider
the following example:

  instance Num Bool where
    ...
    fromInteger 0 = False -- C-like representation of booleans
    fromInteger _ = True

    f :: Bool -> ()
    f 1 = ()        -- Clause A
    f 2 = ()        -- Clause B

Clause B is redundant but to detect this, we must decide the constraint:
@fromInteger 2 ~ fromInteger 1@ which means that we
have to look through function @fromInteger@, whose implementation could
be anything. This poses difficulties for:

1. The expressive power of the check.
   We cannot expect a reasonable implementation of pattern matching to detect
   that @fromInteger 2 ~ fromInteger 1@ is True, unless we unfold function
   fromInteger. This puts termination at risk and is undecidable in the
   general case.

2. Error messages/Warnings.
   What should our message for @f@ above be? A reasonable approach would be
   to issue:

     Pattern matches are (potentially) redundant:
       f 2 = ...    under the assumption that 1 == 2

   but seems to complex and confusing for the user.

We choose to equate only obviously equal overloaded literals, in all other cases
we signal undecidability by returning Nothing from 'eqPmAltCons'. We do
better for non-overloaded literals, because we know their fromInteger/fromString
implementation is actually injective, allowing us to simplify the constraint
@fromInteger 1 ~ fromInteger 2@ to @1 ~ 2@, which is trivially unsatisfiable.

The impact of this treatment of overloaded literals is the following:

  * Redundancy checking is rather conservative, since it cannot see that clause
    B above is redundant.

  * We have instant equality check for overloaded literals (we do not rely on
    the term oracle which is rather expensive, both in terms of performance and
    memory). This significantly improves the performance of functions `covered`
    `uncovered` and `divergent` in "GHC.HsToCore.Pmc" and effectively addresses
    #11161.

  * The warnings issued are simpler.

Similar reasoning applies to pattern synonyms: In contrast to data constructors,
which are generative, constraints like F a ~ G b for two different pattern
synonyms F and G aren't immediately unsatisfiable. We assume F a ~ F a, though.
-}

literalToPmLit :: Type -> Literal -> Maybe PmLit
literalToPmLit :: Kind -> Literal -> Maybe PmLit
literalToPmLit Kind
ty Literal
l = Kind -> PmLitValue -> PmLit
PmLit Kind
ty (PmLitValue -> PmLit) -> Maybe PmLitValue -> Maybe PmLit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Literal -> Maybe PmLitValue
go Literal
l
  where
    go :: Literal -> Maybe PmLitValue
go (LitChar Char
c)       = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (Char -> PmLitValue
PmLitChar Char
c)
    go (LitFloat Rational
r)      = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (Rational -> PmLitValue
PmLitRat Rational
r)
    go (LitDouble Rational
r)     = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (Rational -> PmLitValue
PmLitRat Rational
r)
    go (LitString ByteString
s)     = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (FastString -> PmLitValue
PmLitString (ByteString -> FastString
mkFastStringByteString ByteString
s))
    go (LitNumber LitNumType
_ Integer
i)   = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (Integer -> PmLitValue
PmLitInt Integer
i)
    go Literal
_                 = Maybe PmLitValue
forall a. Maybe a
Nothing

negatePmLit :: PmLit -> Maybe PmLit
negatePmLit :: PmLit -> Maybe PmLit
negatePmLit (PmLit Kind
ty PmLitValue
v) = Kind -> PmLitValue -> PmLit
PmLit Kind
ty (PmLitValue -> PmLit) -> Maybe PmLitValue -> Maybe PmLit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PmLitValue -> Maybe PmLitValue
go PmLitValue
v
  where
    go :: PmLitValue -> Maybe PmLitValue
go (PmLitInt Integer
i)       = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (Integer -> PmLitValue
PmLitInt (-Integer
i))
    go (PmLitRat Rational
r)       = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (Rational -> PmLitValue
PmLitRat (-Rational
r))
    go (PmLitOverInt Int
n Integer
i) = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (Int -> Integer -> PmLitValue
PmLitOverInt (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Integer
i)
    go (PmLitOverRat Int
n FractionalLit
r) = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (Int -> FractionalLit -> PmLitValue
PmLitOverRat (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) FractionalLit
r)
    go PmLitValue
_                  = Maybe PmLitValue
forall a. Maybe a
Nothing

overloadPmLit :: Type -> PmLit -> Maybe PmLit
overloadPmLit :: Kind -> PmLit -> Maybe PmLit
overloadPmLit Kind
ty (PmLit Kind
_ PmLitValue
v) = Kind -> PmLitValue -> PmLit
PmLit Kind
ty (PmLitValue -> PmLit) -> Maybe PmLitValue -> Maybe PmLit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PmLitValue -> Maybe PmLitValue
go PmLitValue
v
  where
    go :: PmLitValue -> Maybe PmLitValue
go (PmLitInt Integer
i)          = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (Int -> Integer -> PmLitValue
PmLitOverInt Int
0 Integer
i)
    go (PmLitRat Rational
r)          = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (PmLitValue -> Maybe PmLitValue) -> PmLitValue -> Maybe PmLitValue
forall a b. (a -> b) -> a -> b
$! Int -> FractionalLit -> PmLitValue
PmLitOverRat Int
0 (FractionalLit -> PmLitValue) -> FractionalLit -> PmLitValue
forall a b. (a -> b) -> a -> b
$! Rational -> FractionalLit
fractionalLitFromRational Rational
r
    go (PmLitString FastString
s)
      | Kind
ty Kind -> Kind -> Bool
`eqType` Kind
stringTy = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just PmLitValue
v
      | Bool
otherwise            = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (FastString -> PmLitValue
PmLitOverString FastString
s)
    go ovRat :: PmLitValue
ovRat@PmLitOverRat{}  = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just PmLitValue
ovRat
    go PmLitValue
_               = Maybe PmLitValue
forall a. Maybe a
Nothing

pmLitAsStringLit :: PmLit -> Maybe FastString
pmLitAsStringLit :: PmLit -> Maybe FastString
pmLitAsStringLit (PmLit Kind
_ (PmLitString FastString
s)) = FastString -> Maybe FastString
forall a. a -> Maybe a
Just FastString
s
pmLitAsStringLit PmLit
_                         = Maybe FastString
forall a. Maybe a
Nothing

coreExprAsPmLit :: CoreExpr -> Maybe PmLit
-- coreExprAsPmLit e | pprTrace "coreExprAsPmLit" (ppr e) False = undefined
coreExprAsPmLit :: CoreExpr -> Maybe PmLit
coreExprAsPmLit (Tick CoreTickish
_t CoreExpr
e) = CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
e
coreExprAsPmLit (Lit Literal
l) = Kind -> Literal -> Maybe PmLit
literalToPmLit (Literal -> Kind
literalType Literal
l) Literal
l
coreExprAsPmLit CoreExpr
e = case CoreExpr -> (CoreExpr, [CoreExpr])
forall b. Expr b -> (Expr b, [Expr b])
collectArgs CoreExpr
e of
  (Var Id
x, [Lit Literal
l])
    | Just DataCon
dc <- Id -> Maybe DataCon
isDataConWorkId_maybe Id
x
    , DataCon
dc DataCon -> [DataCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DataCon
intDataCon, DataCon
wordDataCon, DataCon
charDataCon, DataCon
floatDataCon, DataCon
doubleDataCon]
    -> Kind -> Literal -> Maybe PmLit
literalToPmLit ((() :: Constraint) => CoreExpr -> Kind
CoreExpr -> Kind
exprType CoreExpr
e) Literal
l
  (Var Id
x, [Lit (LitNumber LitNumType
_ Integer
l)])
    | Just (Kind
ty,Integer
l) <- Id -> Integer -> Maybe (Kind, Integer)
forall {b}. Num b => Id -> b -> Maybe (Kind, b)
bignum_lit_maybe Id
x Integer
l
    -> PmLit -> Maybe PmLit
forall a. a -> Maybe a
Just (Kind -> PmLitValue -> PmLit
PmLit Kind
ty (Integer -> PmLitValue
PmLitInt Integer
l))
  (Var Id
x, [CoreExpr
_ty, CoreExpr
n_arg, CoreExpr
d_arg])
    | Just DataCon
dc <- Id -> Maybe DataCon
isDataConWorkId_maybe Id
x
    , DataCon -> Name
dataConName DataCon
dc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
ratioDataConName
    , Just (PmLit Kind
_ (PmLitInt Integer
n)) <- CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
n_arg
    , Just (PmLit Kind
_ (PmLitInt Integer
d)) <- CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
d_arg
    -- HACK: just assume we have a literal double. This case only occurs for
    --       overloaded lits anyway, so we immediately override type information
    -> Kind -> Literal -> Maybe PmLit
literalToPmLit ((() :: Constraint) => CoreExpr -> Kind
CoreExpr -> Kind
exprType CoreExpr
e) (Rational -> Literal
mkLitDouble (Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
d))

  (Var Id
x, [CoreExpr]
args)
    -- See Note [Detecting overloaded literals with -XRebindableSyntax]
    | Id -> Name -> Bool
is_rebound_name Id
x Name
fromIntegerName
    , Just CoreExpr
arg <- [CoreExpr] -> Maybe CoreExpr
forall a. [a] -> Maybe a
lastMaybe [CoreExpr]
args
    , Just (Kind
_ty,Integer
l) <- CoreExpr -> Maybe (Kind, Integer)
forall {b}. Expr b -> Maybe (Kind, Integer)
bignum_conapp_maybe CoreExpr
arg
    -> PmLit -> Maybe PmLit
forall a. a -> Maybe a
Just (Kind -> PmLitValue -> PmLit
PmLit Kind
integerTy (Integer -> PmLitValue
PmLitInt Integer
l)) Maybe PmLit -> (PmLit -> Maybe PmLit) -> Maybe PmLit
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Kind -> PmLit -> Maybe PmLit
overloadPmLit ((() :: Constraint) => CoreExpr -> Kind
CoreExpr -> Kind
exprType CoreExpr
e)
  (Var Id
x, [CoreExpr]
args)
    -- See Note [Detecting overloaded literals with -XRebindableSyntax]
    -- fromRational <expr>
    | Id -> Name -> Bool
is_rebound_name Id
x Name
fromRationalName
    , [CoreExpr
r] <- (CoreExpr -> Bool) -> [CoreExpr] -> [CoreExpr]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool) -> (CoreExpr -> Bool) -> CoreExpr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> Bool
is_ratio) [CoreExpr]
args
    -> CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
r Maybe PmLit -> (PmLit -> Maybe PmLit) -> Maybe PmLit
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Kind -> PmLit -> Maybe PmLit
overloadPmLit ((() :: Constraint) => CoreExpr -> Kind
CoreExpr -> Kind
exprType CoreExpr
e)

  --Rationals with large exponents
  (Var Id
x, [CoreExpr]
args)
    -- See Note [Detecting overloaded literals with -XRebindableSyntax]
    -- See Note [Dealing with rationals with large exponents]
    -- mkRationalBase* <rational> <exponent>
    | Just FractionalExponentBase
exp_base <- Id -> Maybe FractionalExponentBase
is_larg_exp_ratio Id
x
    , [CoreExpr
r, CoreExpr
exp] <- (CoreExpr -> Bool) -> [CoreExpr] -> [CoreExpr]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool) -> (CoreExpr -> Bool) -> CoreExpr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoreExpr -> Bool
is_ratio) [CoreExpr]
args
    , (Var Id
x, [CoreExpr
_ty, CoreExpr
n_arg, CoreExpr
d_arg]) <- CoreExpr -> (CoreExpr, [CoreExpr])
forall b. Expr b -> (Expr b, [Expr b])
collectArgs CoreExpr
r
    , Just DataCon
dc <- Id -> Maybe DataCon
isDataConWorkId_maybe Id
x
    , DataCon -> Name
dataConName DataCon
dc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
ratioDataConName
    , Just (PmLit Kind
_ (PmLitInt Integer
n)) <- CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
n_arg
    , Just (PmLit Kind
_ (PmLitInt Integer
d)) <- CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
d_arg
    , Just (Kind
_exp_ty,Integer
exp') <- CoreExpr -> Maybe (Kind, Integer)
forall {b}. Expr b -> Maybe (Kind, Integer)
bignum_conapp_maybe CoreExpr
exp
    -> do
      let rational :: Rational
rational = (Integer -> Integer
forall a. Num a => a -> a
abs Integer
n) Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
d
      let neg :: Int
neg = if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 then Int
1 else Int
0
      let frac :: FractionalLit
frac = SourceText
-> Bool
-> Rational
-> Integer
-> FractionalExponentBase
-> FractionalLit
mkFractionalLit SourceText
NoSourceText Bool
False Rational
rational Integer
exp' FractionalExponentBase
exp_base
      PmLit -> Maybe PmLit
forall a. a -> Maybe a
Just (PmLit -> Maybe PmLit) -> PmLit -> Maybe PmLit
forall a b. (a -> b) -> a -> b
$ Kind -> PmLitValue -> PmLit
PmLit ((() :: Constraint) => CoreExpr -> Kind
CoreExpr -> Kind
exprType CoreExpr
e) (Int -> FractionalLit -> PmLitValue
PmLitOverRat Int
neg FractionalLit
frac)

  (Var Id
x, [CoreExpr]
args)
    | Id -> Name -> Bool
is_rebound_name Id
x Name
fromStringName
    -- See Note [Detecting overloaded literals with -XRebindableSyntax]
    , CoreExpr
s:[CoreExpr]
_ <- (CoreExpr -> Bool) -> [CoreExpr] -> [CoreExpr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Kind -> Bool
isStringTy (Kind -> Bool) -> (CoreExpr -> Kind) -> CoreExpr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() :: Constraint) => CoreExpr -> Kind
CoreExpr -> Kind
exprType) ([CoreExpr] -> [CoreExpr]) -> [CoreExpr] -> [CoreExpr]
forall a b. (a -> b) -> a -> b
$ (CoreExpr -> Bool) -> [CoreExpr] -> [CoreExpr]
forall a. (a -> Bool) -> [a] -> [a]
filter CoreExpr -> Bool
forall b. Expr b -> Bool
isValArg [CoreExpr]
args
    -- NB: Calls coreExprAsPmLit and then overloadPmLit, so that we return PmLitOverStrings
    -> CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
s Maybe PmLit -> (PmLit -> Maybe PmLit) -> Maybe PmLit
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Kind -> PmLit -> Maybe PmLit
overloadPmLit ((() :: Constraint) => CoreExpr -> Kind
CoreExpr -> Kind
exprType CoreExpr
e)
  -- These last two cases handle proper String literals
  (Var Id
x, [Type Kind
ty])
    | Just DataCon
dc <- Id -> Maybe DataCon
isDataConWorkId_maybe Id
x
    , DataCon
dc DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
nilDataCon
    , Kind
ty Kind -> Kind -> Bool
`eqType` Kind
charTy
    -> Kind -> Literal -> Maybe PmLit
literalToPmLit Kind
stringTy (String -> Literal
mkLitString String
"")
  (Var Id
x, [Lit Literal
l])
    | Id -> Name
idName Id
x Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name
unpackCStringName, Name
unpackCStringUtf8Name]
    -> Kind -> Literal -> Maybe PmLit
literalToPmLit Kind
stringTy Literal
l

  (CoreExpr, [CoreExpr])
_ -> Maybe PmLit
forall a. Maybe a
Nothing
  where
    bignum_conapp_maybe :: Expr b -> Maybe (Kind, Integer)
bignum_conapp_maybe (App (Var Id
x) (Lit (LitNumber LitNumType
_ Integer
l)))
      = Id -> Integer -> Maybe (Kind, Integer)
forall {b}. Num b => Id -> b -> Maybe (Kind, b)
bignum_lit_maybe Id
x Integer
l
    bignum_conapp_maybe Expr b
_ = Maybe (Kind, Integer)
forall a. Maybe a
Nothing

    bignum_lit_maybe :: Id -> b -> Maybe (Kind, b)
bignum_lit_maybe Id
x b
l
      | Just DataCon
dc <- Id -> Maybe DataCon
isDataConWorkId_maybe Id
x
      = if | DataCon
dc DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
integerISDataCon -> (Kind, b) -> Maybe (Kind, b)
forall a. a -> Maybe a
Just (Kind
integerTy,b
l)
           | DataCon
dc DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
integerIPDataCon -> (Kind, b) -> Maybe (Kind, b)
forall a. a -> Maybe a
Just (Kind
integerTy,b
l)
           | DataCon
dc DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
integerINDataCon -> (Kind, b) -> Maybe (Kind, b)
forall a. a -> Maybe a
Just (Kind
integerTy,b -> b
forall a. Num a => a -> a
negate b
l)
           | DataCon
dc DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
naturalNSDataCon -> (Kind, b) -> Maybe (Kind, b)
forall a. a -> Maybe a
Just (Kind
naturalTy,b
l)
           | DataCon
dc DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
naturalNBDataCon -> (Kind, b) -> Maybe (Kind, b)
forall a. a -> Maybe a
Just (Kind
naturalTy,b
l)
           | Bool
otherwise              -> Maybe (Kind, b)
forall a. Maybe a
Nothing
    bignum_lit_maybe Id
_ b
_ = Maybe (Kind, b)
forall a. Maybe a
Nothing

    is_ratio :: CoreExpr -> Bool
is_ratio (Type Kind
_) = Bool
False
    is_ratio CoreExpr
r
      | Just (TyCon
tc, [Kind]
_) <- (() :: Constraint) => Kind -> Maybe (TyCon, [Kind])
Kind -> Maybe (TyCon, [Kind])
splitTyConApp_maybe ((() :: Constraint) => CoreExpr -> Kind
CoreExpr -> Kind
exprType CoreExpr
r)
      = TyCon -> Name
tyConName TyCon
tc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
ratioTyConName
      | Bool
otherwise
      = Bool
False
    is_larg_exp_ratio :: Id -> Maybe FractionalExponentBase
is_larg_exp_ratio Id
x
      | Id -> Name -> Bool
is_rebound_name Id
x Name
mkRationalBase10Name
      = FractionalExponentBase -> Maybe FractionalExponentBase
forall a. a -> Maybe a
Just FractionalExponentBase
Base10
      | Id -> Name -> Bool
is_rebound_name Id
x Name
mkRationalBase2Name
      = FractionalExponentBase -> Maybe FractionalExponentBase
forall a. a -> Maybe a
Just FractionalExponentBase
Base2
      | Bool
otherwise
      = Maybe FractionalExponentBase
forall a. Maybe a
Nothing


    -- See Note [Detecting overloaded literals with -XRebindableSyntax]
    is_rebound_name :: Id -> Name -> Bool
    is_rebound_name :: Id -> Name -> Bool
is_rebound_name Id
x Name
n = Name -> FastString
forall a. NamedThing a => a -> FastString
getOccFS (Id -> Name
idName Id
x) FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> FastString
forall a. NamedThing a => a -> FastString
getOccFS Name
n

{- Note [Detecting overloaded literals with -XRebindableSyntax]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Normally, we'd find e.g. overloaded string literals by comparing the
application head of an expression to `fromStringName`. But that doesn't work
with -XRebindableSyntax: The `Name` of a user-provided `fromString` function is
different to `fromStringName`, which lives in a certain module, etc.

There really is no other way than to compare `OccName`s and guess which
argument is the actual literal string (we assume it's the first argument of
type `String`).

The same applies to other overloaded literals, such as overloaded rationals
(`fromRational`)and overloaded integer literals (`fromInteger`).

Note [Dealing with rationals with large exponents]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Rationals with large exponents are *not* desugared to
a simple rational. As that would require us to compute
their value which can be expensive. Rather they desugar
to an expression. For example 1e1000 will desugar to an
expression of the form: `mkRationalWithExponentBase10 (1 :% 1) 1000`

Only overloaded literals desugar to this form however, so we
we can just return a overloaded rational literal.

The most complex case is if we have RebindableSyntax enabled.
By example if we have a pattern like this: `f 3.3 = True`

It will desugar to:
  fromRational
    [TYPE: Rational, mkRationalBase10 (:% @Integer 10 1) (-1)]

The fromRational is properly detected as an overloaded Rational by
coreExprAsPmLit and it's general code for detecting overloaded rationals.
See Note [Detecting overloaded literals with -XRebindableSyntax].

This case then recurses into coreExprAsPmLit passing only the expression
`mkRationalBase10 (:% @Integer 10 1) (-1)`. Which is caught by rationals
with large exponents case. This will return a `PmLitOverRat` literal.

Which is then passed to overloadPmLit which simply returns it as-is since
it's already overloaded.

-}

instance Outputable PmLitValue where
  ppr :: PmLitValue -> SDoc
ppr (PmLitInt Integer
i)        = Integer -> SDoc
forall a. Outputable a => a -> SDoc
ppr Integer
i
  ppr (PmLitRat Rational
r)        = SDoc -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Double -> SDoc
double (Rational -> Double
forall a. RealFloat a => Rational -> a
fromRat Rational
r)) -- good enough
  ppr (PmLitChar Char
c)       = Char -> SDoc
pprHsChar Char
c
  ppr (PmLitString FastString
s)     = FastString -> SDoc
pprHsString FastString
s
  ppr (PmLitOverInt Int
n Integer
i)  = Int -> SDoc -> SDoc
minuses Int
n (Integer -> SDoc
forall a. Outputable a => a -> SDoc
ppr Integer
i)
  ppr (PmLitOverRat Int
n FractionalLit
r)  = Int -> SDoc -> SDoc
minuses Int
n (FractionalLit -> SDoc
forall a. Outputable a => a -> SDoc
ppr FractionalLit
r)
  ppr (PmLitOverString FastString
s) = FastString -> SDoc
pprHsString FastString
s

-- Take care of negated literals
minuses :: Int -> SDoc -> SDoc
minuses :: Int -> SDoc -> SDoc
minuses Int
n SDoc
sdoc = (SDoc -> SDoc) -> SDoc -> [SDoc]
forall a. (a -> a) -> a -> [a]
iterate (\SDoc
sdoc -> SDoc -> SDoc
parens (Char -> SDoc
char Char
'-' SDoc -> SDoc -> SDoc
<> SDoc
sdoc)) SDoc
sdoc [SDoc] -> Int -> SDoc
forall a. HasCallStack => [a] -> Int -> a
!! Int
n

instance Outputable PmLit where
  ppr :: PmLit -> SDoc
ppr (PmLit Kind
ty PmLitValue
v) = PmLitValue -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmLitValue
v SDoc -> SDoc -> SDoc
<> SDoc
suffix
    where
      -- Some ad-hoc hackery for displaying proper lit suffixes based on type
      tbl :: [(Kind, SDoc)]
tbl = [ (Kind
intPrimTy, SDoc
primIntSuffix)
            , (Kind
int64PrimTy, SDoc
primInt64Suffix)
            , (Kind
wordPrimTy, SDoc
primWordSuffix)
            , (Kind
word64PrimTy, SDoc
primWord64Suffix)
            , (Kind
charPrimTy, SDoc
primCharSuffix)
            , (Kind
floatPrimTy, SDoc
primFloatSuffix)
            , (Kind
doublePrimTy, SDoc
primDoubleSuffix) ]
      suffix :: SDoc
suffix = SDoc -> Maybe SDoc -> SDoc
forall a. a -> Maybe a -> a
fromMaybe SDoc
empty ((Kind, SDoc) -> SDoc
forall a b. (a, b) -> b
snd ((Kind, SDoc) -> SDoc) -> Maybe (Kind, SDoc) -> Maybe SDoc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Kind, SDoc) -> Bool) -> [(Kind, SDoc)] -> Maybe (Kind, SDoc)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Kind -> Kind -> Bool
eqType Kind
ty (Kind -> Bool) -> ((Kind, SDoc) -> Kind) -> (Kind, SDoc) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind, SDoc) -> Kind
forall a b. (a, b) -> a
fst) [(Kind, SDoc)]
tbl)

instance Outputable PmAltCon where
  ppr :: PmAltCon -> SDoc
ppr (PmAltConLike ConLike
cl) = ConLike -> SDoc
forall a. Outputable a => a -> SDoc
ppr ConLike
cl
  ppr (PmAltLit PmLit
l)      = PmLit -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmLit
l

instance Outputable PmEquality where
  ppr :: PmEquality -> SDoc
ppr = String -> SDoc
text (String -> SDoc) -> (PmEquality -> String) -> PmEquality -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmEquality -> String
forall a. Show a => a -> String
show