{-
Author: George Karachalias <george.karachalias@cs.kuleuven.be>
        Sebastian Graf <sgraf1337@gmail.com>
-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ApplicativeDo #-}

-- | Types used through-out pattern match checking. This module is mostly there
-- to be imported from "GHC.Tc.Types". The exposed API is that of
-- "GHC.HsToCore.PmCheck.Oracle" and "GHC.HsToCore.PmCheck".
module GHC.HsToCore.PmCheck.Types (
        -- * Representations for Literals and AltCons
        PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,

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

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

        -- * Caching partially matched COMPLETE sets
        ConLikeSet, PossibleMatches(..),

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

        -- * A 'DIdEnv' where entries may be shared
        Shared(..), SharedDIdEnv(..), emptySDIE, lookupSDIE, sameRepresentativeSDIE,
        setIndirectSDIE, setEntrySDIE, traverseSDIE,

        -- * The pattern match oracle
        VarInfo(..), TmState(..), TyState(..), Delta(..),
        Deltas(..), initDeltas, liftDeltasM
    ) where

#include "HsVersions.h"

import GHC.Prelude

import GHC.Utils.Misc
import GHC.Data.Bag
import GHC.Data.FastString
import GHC.Types.Var (EvVar)
import GHC.Types.Id
import GHC.Types.Var.Env
import GHC.Types.Unique.DSet
import GHC.Types.Unique.DFM
import GHC.Types.Name
import GHC.Core.DataCon
import GHC.Core.ConLike
import GHC.Utils.Outputable
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
import GHC.Core.Utils (exprType)
import GHC.Builtin.Names
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim
import GHC.Tc.Utils.TcType (evVarPred)

import Numeric (fromRat)
import Data.Foldable (find)
import qualified Data.List.NonEmpty as NonEmpty
import Data.Ratio
import qualified Data.Semigroup as Semi

-- | Literals (simple and overloaded ones) for pattern match checking.
--
-- See Note [Undecidable Equality for PmAltCons]
data PmLit = PmLit
           { PmLit -> Type
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? -} Rational
  | 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
/= :: PmEquality -> PmEquality -> Bool
$c/= :: PmEquality -> PmEquality -> Bool
== :: PmEquality -> PmEquality -> Bool
$c== :: 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
showList :: [PmEquality] -> ShowS
$cshowList :: [PmEquality] -> ShowS
show :: PmEquality -> String
$cshow :: PmEquality -> String
showsPrec :: Int -> PmEquality -> ShowS
$cshowsPrec :: Int -> 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 Type
t1 PmLitValue
v1) (PmLit Type
t2 PmLitValue
v2)
  -- no haddock | pprTrace "eqPmLit" (ppr t1 <+> ppr v1 $$ ppr t2 <+> ppr v2) False = undefined
  | Bool -> Bool
not (Type
t1 Type -> Type -> Bool
`eqType` Type
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 Rational
r1) (PmLitOverRat Int
n2 Rational
r2)
      | Int
n1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n2 Bool -> Bool -> Bool
&& Rational
r1 Rational -> Rational -> Bool
forall a. Eq a => a -> a -> Bool
== Rational
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 -> Type
pmLitType (PmLit Type
ty PmLitValue
_) = Type
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 !ConLikeSet ![PmLit]

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

isEmptyPmAltConSet :: PmAltConSet -> Bool
isEmptyPmAltConSet :: PmAltConSet -> Bool
isEmptyPmAltConSet (PACS ConLikeSet
cls [PmLit]
lits) = ConLikeSet -> Bool
forall a. UniqDSet a -> Bool
isEmptyUniqDSet ConLikeSet
cls Bool -> Bool -> Bool
&& [PmLit] -> 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 ConLikeSet
cls [PmLit]
_   ) = ConLike -> ConLikeSet -> Bool
forall a. Uniquable a => a -> UniqDSet a -> Bool
elementOfUniqDSet ConLike
cl ConLikeSet
cls
elemPmAltConSet (PmAltLit PmLit
lit)    (PACS ConLikeSet
_   [PmLit]
lits) = PmLit -> [PmLit] -> 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 ConLikeSet
cls [PmLit]
lits) (PmAltConLike ConLike
cl)
  = ConLikeSet -> [PmLit] -> PmAltConSet
PACS (ConLikeSet -> ConLike -> ConLikeSet
forall a. Uniquable a => UniqDSet a -> a -> UniqDSet a
addOneToUniqDSet ConLikeSet
cls ConLike
cl) [PmLit]
lits
extendPmAltConSet (PACS ConLikeSet
cls [PmLit]
lits) (PmAltLit PmLit
lit)
  = ConLikeSet -> [PmLit] -> PmAltConSet
PACS ConLikeSet
cls ([PmLit] -> [PmLit] -> [PmLit]
forall a.
(HasDebugCallStack, Outputable a, Eq a) =>
[a] -> [a] -> [a]
unionLists [PmLit]
lits [PmLit
lit])

pmAltConSetElems :: PmAltConSet -> [PmAltCon]
pmAltConSetElems :: PmAltConSet -> [PmAltCon]
pmAltConSetElems (PACS ConLikeSet
cls [PmLit]
lits)
  = (ConLike -> PmAltCon) -> [ConLike] -> [PmAltCon]
forall a b. (a -> b) -> [a] -> [b]
map ConLike -> PmAltCon
PmAltConLike (ConLikeSet -> [ConLike]
forall a. UniqDSet a -> [a]
uniqDSetToList ConLikeSet
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 -> [Type] -> Type
pmAltConType (PmAltLit PmLit
lit)     [Type]
_arg_tys = ASSERT( null _arg_tys ) pmLitType lit
pmAltConType (PmAltConLike ConLike
con) [Type]
arg_tys  = ConLike -> [Type] -> Type
conLikeResTy ConLike
con [Type]
arg_tys

{- 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.PmCheck" 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 :: Type -> Literal -> Maybe PmLit
literalToPmLit Type
ty Literal
l = Type -> PmLitValue -> PmLit
PmLit Type
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 Type
ty PmLitValue
v) = Type -> PmLitValue -> PmLit
PmLit Type
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 Rational
r) = PmLitValue -> Maybe PmLitValue
forall a. a -> Maybe a
Just (Int -> Rational -> PmLitValue
PmLitOverRat (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Rational
r)
    go PmLitValue
_                  = Maybe PmLitValue
forall a. Maybe a
Nothing

overloadPmLit :: Type -> PmLit -> Maybe PmLit
overloadPmLit :: Type -> PmLit -> Maybe PmLit
overloadPmLit Type
ty (PmLit Type
_ PmLitValue
v) = Type -> PmLitValue -> PmLit
PmLit Type
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 (Int -> Rational -> PmLitValue
PmLitOverRat Int
0 Rational
r)
    go (PmLitString FastString
s)
      | Type
ty Type -> Type -> Bool
`eqType` Type
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 PmLitValue
_               = Maybe PmLitValue
forall a. Maybe a
Nothing

pmLitAsStringLit :: PmLit -> Maybe FastString
pmLitAsStringLit :: PmLit -> Maybe FastString
pmLitAsStringLit (PmLit Type
_ (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 Tickish Id
_t CoreExpr
e) = CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
e
coreExprAsPmLit (Lit Literal
l) = Type -> Literal -> Maybe PmLit
literalToPmLit (Literal -> Type
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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [DataCon
intDataCon, DataCon
wordDataCon, DataCon
charDataCon, DataCon
floatDataCon, DataCon
doubleDataCon]
    -> Type -> Literal -> Maybe PmLit
literalToPmLit (CoreExpr -> Type
exprType CoreExpr
e) Literal
l
  (Var Id
x, [CoreExpr
_ty, Lit Literal
n, Lit Literal
d])
    | 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
    -- HACK: just assume we have a literal double. This case only occurs for
    --       overloaded lits anyway, so we immediately override type information
    -> Type -> Literal -> Maybe PmLit
literalToPmLit (CoreExpr -> Type
exprType CoreExpr
e) (Rational -> Literal
mkLitDouble (Literal -> Integer
litValue Literal
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Literal -> Integer
litValue Literal
d))
  (Var Id
x, [CoreExpr]
args)
    -- Take care of -XRebindableSyntax. The last argument should be the (only)
    -- integer literal, otherwise we can't really do much about it.
    | [Lit Literal
l] <- (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
forall {b}. Expr b -> Bool
is_lit) [CoreExpr]
args
    -- getOccFS because of -XRebindableSyntax
    , 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
fromIntegerName
    -> Type -> Literal -> Maybe PmLit
literalToPmLit (Literal -> Type
literalType Literal
l) Literal
l Maybe PmLit -> (PmLit -> Maybe PmLit) -> Maybe PmLit
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> PmLit -> Maybe PmLit
overloadPmLit (CoreExpr -> Type
exprType CoreExpr
e)
  (Var Id
x, [CoreExpr]
args)
    -- Similar to fromInteger case
    | [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
    , 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
fromRationalName
    -> CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
r Maybe PmLit -> (PmLit -> Maybe PmLit) -> Maybe PmLit
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> PmLit -> Maybe PmLit
overloadPmLit (CoreExpr -> Type
exprType CoreExpr
e)
  (Var Id
x, [Type Type
_ty, CoreExpr
_dict, CoreExpr
s])
    | Id -> Name
idName Id
x Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
fromStringName
    -- 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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type -> PmLit -> Maybe PmLit
overloadPmLit (CoreExpr -> Type
exprType CoreExpr
e)
  -- These last two cases handle String literals
  (Var Id
x, [Type Type
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
    , Type
ty Type -> Type -> Bool
`eqType` Type
charTy
    -> Type -> Literal -> Maybe PmLit
literalToPmLit Type
stringTy (String -> Literal
mkLitString String
"")
  (Var Id
x, [Lit Literal
l])
    | Id -> Name
idName Id
x Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name
unpackCStringName, Name
unpackCStringUtf8Name]
    -> Type -> Literal -> Maybe PmLit
literalToPmLit Type
stringTy Literal
l
  (CoreExpr, [CoreExpr])
_ -> Maybe PmLit
forall a. Maybe a
Nothing
  where
    is_lit :: Expr b -> Bool
is_lit Lit{} = Bool
True
    is_lit Expr b
_     = Bool
False
    is_ratio :: CoreExpr -> Bool
is_ratio (Type Type
_) = Bool
False
    is_ratio CoreExpr
r
      | Just (TyCon
tc, [Type]
_) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (CoreExpr -> Type
exprType CoreExpr
r)
      = TyCon -> Name
tyConName TyCon
tc Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
ratioTyConName
      | Bool
otherwise
      = Bool
False

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 Rational
r)  = Int -> SDoc -> SDoc
minuses Int
n (SDoc -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Double -> SDoc
double (Rational -> Double
forall a. RealFloat a => Rational -> a
fromRat Rational
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. [a] -> Int -> a
!! Int
n

instance Outputable PmLit where
  ppr :: PmLit -> SDoc
ppr (PmLit Type
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 :: [(Type, SDoc)]
tbl = [ (Type
intPrimTy, SDoc
primIntSuffix)
            , (Type
int64PrimTy, SDoc
primInt64Suffix)
            , (Type
wordPrimTy, SDoc
primWordSuffix)
            , (Type
word64PrimTy, SDoc
primWord64Suffix)
            , (Type
charPrimTy, SDoc
primCharSuffix)
            , (Type
floatPrimTy, SDoc
primFloatSuffix)
            , (Type
doublePrimTy, SDoc
primDoubleSuffix) ]
      suffix :: SDoc
suffix = SDoc -> Maybe SDoc -> SDoc
forall a. a -> Maybe a -> a
fromMaybe SDoc
empty ((Type, SDoc) -> SDoc
forall a b. (a, b) -> b
snd ((Type, SDoc) -> SDoc) -> Maybe (Type, SDoc) -> Maybe SDoc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Type, SDoc) -> Bool) -> [(Type, SDoc)] -> Maybe (Type, SDoc)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Type -> Type -> Bool
eqType Type
ty (Type -> Bool) -> ((Type, SDoc) -> Type) -> (Type, SDoc) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, SDoc) -> Type
forall a b. (a, b) -> a
fst) [(Type, 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

type ConLikeSet = UniqDSet ConLike

-- | A data type caching the results of 'completeMatchConLikes' with support for
-- deletion of constructors that were already matched on.
data PossibleMatches
  = PM (NonEmpty.NonEmpty ConLikeSet)
  -- ^ Each ConLikeSet is a (subset of) the constructors in a COMPLETE set
  -- 'NonEmpty' because the empty case would mean that the type has no COMPLETE
  -- set at all, for which we have 'NoPM'.
  | NoPM
  -- ^ No COMPLETE set for this type (yet). Think of overloaded literals.

instance Outputable PossibleMatches where
  ppr :: PossibleMatches -> SDoc
ppr (PM NonEmpty ConLikeSet
cs) = [ConLikeSet] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (NonEmpty ConLikeSet -> [ConLikeSet]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty ConLikeSet
cs)
  ppr PossibleMatches
NoPM = String -> SDoc
text String
"<NoPM>"

-- | Either @Indirect x@, meaning the value is represented by that of @x@, or
-- an @Entry@ containing containing the actual value it represents.
data Shared a
  = Indirect Id
  | Entry a

-- | A 'DIdEnv' in which entries can be shared by multiple 'Id's.
-- Merge equivalence classes of two Ids by 'setIndirectSDIE' and set the entry
-- of an Id with 'setEntrySDIE'.
newtype SharedDIdEnv a
  = SDIE { forall a. SharedDIdEnv a -> DIdEnv (Shared a)
unSDIE :: DIdEnv (Shared a) }

emptySDIE :: SharedDIdEnv a
emptySDIE :: forall a. SharedDIdEnv a
emptySDIE = DIdEnv (Shared a) -> SharedDIdEnv a
forall a. DIdEnv (Shared a) -> SharedDIdEnv a
SDIE DIdEnv (Shared a)
forall a. DVarEnv a
emptyDVarEnv

lookupReprAndEntrySDIE :: SharedDIdEnv a -> Id -> (Id, Maybe a)
lookupReprAndEntrySDIE :: forall a. SharedDIdEnv a -> Id -> (Id, Maybe a)
lookupReprAndEntrySDIE sdie :: SharedDIdEnv a
sdie@(SDIE DIdEnv (Shared a)
env) Id
x = case DIdEnv (Shared a) -> Id -> Maybe (Shared a)
forall a. DVarEnv a -> Id -> Maybe a
lookupDVarEnv DIdEnv (Shared a)
env Id
x of
  Maybe (Shared a)
Nothing           -> (Id
x, Maybe a
forall a. Maybe a
Nothing)
  Just (Indirect Id
y) -> SharedDIdEnv a -> Id -> (Id, Maybe a)
forall a. SharedDIdEnv a -> Id -> (Id, Maybe a)
lookupReprAndEntrySDIE SharedDIdEnv a
sdie Id
y
  Just (Entry a
a)    -> (Id
x, a -> Maybe a
forall a. a -> Maybe a
Just a
a)

-- | @lookupSDIE env x@ looks up an entry for @x@, looking through all
-- 'Indirect's until it finds a shared 'Entry'.
lookupSDIE :: SharedDIdEnv a -> Id -> Maybe a
lookupSDIE :: forall a. SharedDIdEnv a -> Id -> Maybe a
lookupSDIE SharedDIdEnv a
sdie Id
x = (Id, Maybe a) -> Maybe a
forall a b. (a, b) -> b
snd (SharedDIdEnv a -> Id -> (Id, Maybe a)
forall a. SharedDIdEnv a -> Id -> (Id, Maybe a)
lookupReprAndEntrySDIE SharedDIdEnv a
sdie Id
x)

-- | Check if two variables are part of the same equivalence class.
sameRepresentativeSDIE :: SharedDIdEnv a -> Id -> Id -> Bool
sameRepresentativeSDIE :: forall a. SharedDIdEnv a -> Id -> Id -> Bool
sameRepresentativeSDIE SharedDIdEnv a
sdie Id
x Id
y =
  (Id, Maybe a) -> Id
forall a b. (a, b) -> a
fst (SharedDIdEnv a -> Id -> (Id, Maybe a)
forall a. SharedDIdEnv a -> Id -> (Id, Maybe a)
lookupReprAndEntrySDIE SharedDIdEnv a
sdie Id
x) Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== (Id, Maybe a) -> Id
forall a b. (a, b) -> a
fst (SharedDIdEnv a -> Id -> (Id, Maybe a)
forall a. SharedDIdEnv a -> Id -> (Id, Maybe a)
lookupReprAndEntrySDIE SharedDIdEnv a
sdie Id
y)

-- | @setIndirectSDIE env x y@ sets @x@'s 'Entry' to @Indirect y@, thereby
-- merging @x@'s equivalence class into @y@'s. This will discard all info on
-- @x@!
setIndirectSDIE :: SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
setIndirectSDIE :: forall a. SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
setIndirectSDIE sdie :: SharedDIdEnv a
sdie@(SDIE DIdEnv (Shared a)
env) Id
x Id
y =
  DIdEnv (Shared a) -> SharedDIdEnv a
forall a. DIdEnv (Shared a) -> SharedDIdEnv a
SDIE (DIdEnv (Shared a) -> SharedDIdEnv a)
-> DIdEnv (Shared a) -> SharedDIdEnv a
forall a b. (a -> b) -> a -> b
$ DIdEnv (Shared a) -> Id -> Shared a -> DIdEnv (Shared a)
forall a. DVarEnv a -> Id -> a -> DVarEnv a
extendDVarEnv DIdEnv (Shared a)
env ((Id, Maybe a) -> Id
forall a b. (a, b) -> a
fst (SharedDIdEnv a -> Id -> (Id, Maybe a)
forall a. SharedDIdEnv a -> Id -> (Id, Maybe a)
lookupReprAndEntrySDIE SharedDIdEnv a
sdie Id
x)) (Id -> Shared a
forall a. Id -> Shared a
Indirect Id
y)

-- | @setEntrySDIE env x a@ sets the 'Entry' @x@ is associated with to @a@,
-- thereby modifying its whole equivalence class.
setEntrySDIE :: SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE :: forall a. SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE sdie :: SharedDIdEnv a
sdie@(SDIE DIdEnv (Shared a)
env) Id
x a
a =
  DIdEnv (Shared a) -> SharedDIdEnv a
forall a. DIdEnv (Shared a) -> SharedDIdEnv a
SDIE (DIdEnv (Shared a) -> SharedDIdEnv a)
-> DIdEnv (Shared a) -> SharedDIdEnv a
forall a b. (a -> b) -> a -> b
$ DIdEnv (Shared a) -> Id -> Shared a -> DIdEnv (Shared a)
forall a. DVarEnv a -> Id -> a -> DVarEnv a
extendDVarEnv DIdEnv (Shared a)
env ((Id, Maybe a) -> Id
forall a b. (a, b) -> a
fst (SharedDIdEnv a -> Id -> (Id, Maybe a)
forall a. SharedDIdEnv a -> Id -> (Id, Maybe a)
lookupReprAndEntrySDIE SharedDIdEnv a
sdie Id
x)) (a -> Shared a
forall a. a -> Shared a
Entry a
a)

traverseSDIE :: forall a b f. Applicative f => (a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)
traverseSDIE :: forall a b (f :: * -> *).
Applicative f =>
(a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)
traverseSDIE a -> f b
f = ([(Unique, Shared b)] -> SharedDIdEnv b)
-> f [(Unique, Shared b)] -> f (SharedDIdEnv b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DIdEnv (Shared b) -> SharedDIdEnv b
forall a. DIdEnv (Shared a) -> SharedDIdEnv a
SDIE (DIdEnv (Shared b) -> SharedDIdEnv b)
-> ([(Unique, Shared b)] -> DIdEnv (Shared b))
-> [(Unique, Shared b)]
-> SharedDIdEnv b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Unique, Shared b)] -> DIdEnv (Shared b)
forall elt key. [(Unique, elt)] -> UniqDFM key elt
listToUDFM_Directly) (f [(Unique, Shared b)] -> f (SharedDIdEnv b))
-> (SharedDIdEnv a -> f [(Unique, Shared b)])
-> SharedDIdEnv a
-> f (SharedDIdEnv b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Unique, Shared a) -> f (Unique, Shared b))
-> [(Unique, Shared a)] -> f [(Unique, Shared b)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Unique, Shared a) -> f (Unique, Shared b)
g ([(Unique, Shared a)] -> f [(Unique, Shared b)])
-> (SharedDIdEnv a -> [(Unique, Shared a)])
-> SharedDIdEnv a
-> f [(Unique, Shared b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UniqDFM Id (Shared a) -> [(Unique, Shared a)]
forall key elt. UniqDFM key elt -> [(Unique, elt)]
udfmToList (UniqDFM Id (Shared a) -> [(Unique, Shared a)])
-> (SharedDIdEnv a -> UniqDFM Id (Shared a))
-> SharedDIdEnv a
-> [(Unique, Shared a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SharedDIdEnv a -> UniqDFM Id (Shared a)
forall a. SharedDIdEnv a -> DIdEnv (Shared a)
unSDIE
  where
    g :: (Unique, Shared a) -> f (Unique, Shared b)
    g :: (Unique, Shared a) -> f (Unique, Shared b)
g (Unique
u, Indirect Id
y) = (Unique, Shared b) -> f (Unique, Shared b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Unique
u,Id -> Shared b
forall a. Id -> Shared a
Indirect Id
y)
    g (Unique
u, Entry a
a)    = do
        b
a' <- a -> f b
f a
a
        pure (Unique
u,b -> Shared b
forall a. a -> Shared a
Entry b
a')

instance Outputable a => Outputable (Shared a) where
  ppr :: Shared a -> SDoc
ppr (Indirect Id
x) = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x
  ppr (Entry a
a)    = a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
a

instance Outputable a => Outputable (SharedDIdEnv a) where
  ppr :: SharedDIdEnv a -> SDoc
ppr (SDIE DIdEnv (Shared a)
env) = DIdEnv (Shared a) -> SDoc
forall a. Outputable a => a -> SDoc
ppr DIdEnv (Shared a)
env

-- | 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.PmCheck.Oracle".
data TmState
  = TmSt
  { TmState -> SharedDIdEnv VarInfo
ts_facts :: !(SharedDIdEnv 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.
  }

-- | 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 'PossibleMatches' of a COMPLETE set
-- ('vi_cache').
--
-- Subject to Note [The Pos/Neg invariant] in "GHC.HsToCore.PmCheck.Oracle".
data VarInfo
  = VI
  { VarInfo -> Type
vi_ty  :: !Type
  -- ^ The type of the variable. Important for rejecting possible GADT
  -- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@).

  , VarInfo -> [(PmAltCon, [Id], [Id])]
vi_pos :: ![(PmAltCon, [TyVar], [Id])]
  -- ^ 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 -> PossibleMatches
vi_cache :: !PossibleMatches
  -- ^ 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.
  }

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

-- | Not user-facing.
instance Outputable VarInfo where
  ppr :: VarInfo -> SDoc
ppr (VI Type
ty [(PmAltCon, [Id], [Id])]
pos PmAltConSet
neg PossibleMatches
cache)
    = SDoc -> SDoc
braces ([SDoc] -> SDoc
hcat (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma [Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty, [(PmAltCon, [Id], [Id])] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(PmAltCon, [Id], [Id])]
pos, PmAltConSet -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmAltConSet
neg, PossibleMatches -> SDoc
forall a. Outputable a => a -> SDoc
ppr PossibleMatches
cache]))

-- | Initial state of the term oracle.
initTmState :: TmState
initTmState :: TmState
initTmState = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt SharedDIdEnv VarInfo
forall a. SharedDIdEnv a
emptySDIE CoreMap Id
forall a. CoreMap a
emptyCoreMap

-- | The type oracle state. A poor man's 'GHC.Tc.Solver.Monad.InsertSet': The invariant is
-- that all constraints in there are mutually compatible.
newtype TyState = TySt (Bag EvVar)

-- | Not user-facing.
instance Outputable TyState where
  ppr :: TyState -> SDoc
ppr (TySt Bag Id
evs)
    = SDoc -> SDoc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
hcat ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma ([SDoc] -> [SDoc]) -> [SDoc] -> [SDoc]
forall a b. (a -> b) -> a -> b
$ (Id -> SDoc) -> [Id] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type -> SDoc) -> (Id -> Type) -> Id -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
evVarPred) ([Id] -> [SDoc]) -> [Id] -> [SDoc]
forall a b. (a -> b) -> a -> b
$ Bag Id -> [Id]
forall a. Bag a -> [a]
bagToList Bag Id
evs

initTyState :: TyState
initTyState :: TyState
initTyState = Bag Id -> TyState
TySt Bag Id
forall a. Bag a
emptyBag

-- | An inert set of canonical (i.e. mutually compatible) term and type
-- constraints.
data Delta = MkDelta { Delta -> TyState
delta_ty_st :: TyState    -- Type oracle; things like a~Int
                     , Delta -> TmState
delta_tm_st :: TmState }  -- Term oracle; things like x~Nothing

-- | An initial delta that is always satisfiable
initDelta :: Delta
initDelta :: Delta
initDelta = TyState -> TmState -> Delta
MkDelta TyState
initTyState TmState
initTmState

instance Outputable Delta where
  ppr :: Delta -> SDoc
ppr Delta
delta = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Delta") 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 she needs
      TmState -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Delta -> TmState
delta_tm_st Delta
delta),
      TyState -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Delta -> TyState
delta_ty_st Delta
delta)
    ]

-- | A disjunctive bag of 'Delta's, representing a refinement type.
newtype Deltas = MkDeltas (Bag Delta)

initDeltas :: Deltas
initDeltas :: Deltas
initDeltas = Bag Delta -> Deltas
MkDeltas (Delta -> Bag Delta
forall a. a -> Bag a
unitBag Delta
initDelta)

instance Outputable Deltas where
  ppr :: Deltas -> SDoc
ppr (MkDeltas Bag Delta
deltas) = Bag Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag Delta
deltas

instance Semigroup Deltas where
  MkDeltas Bag Delta
l <> :: Deltas -> Deltas -> Deltas
<> MkDeltas Bag Delta
r = Bag Delta -> Deltas
MkDeltas (Bag Delta
l Bag Delta -> Bag Delta -> Bag Delta
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Delta
r)

liftDeltasM :: Monad m => (Delta -> m (Maybe Delta)) -> Deltas -> m Deltas
liftDeltasM :: forall (m :: * -> *).
Monad m =>
(Delta -> m (Maybe Delta)) -> Deltas -> m Deltas
liftDeltasM Delta -> m (Maybe Delta)
f (MkDeltas Bag Delta
ds) = Bag Delta -> Deltas
MkDeltas (Bag Delta -> Deltas)
-> (Bag (Maybe Delta) -> Bag Delta) -> Bag (Maybe Delta) -> Deltas
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag (Maybe Delta) -> Bag Delta
forall a. Bag (Maybe a) -> Bag a
catBagMaybes (Bag (Maybe Delta) -> Deltas) -> m (Bag (Maybe Delta)) -> m Deltas
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Delta -> m (Maybe Delta)) -> Bag Delta -> m (Bag (Maybe Delta))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Delta -> m (Maybe Delta)
f Bag Delta
ds)