{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, MultiWayIf #-}
module GHC.HsToCore.PmCheck.Oracle (
DsM, tracePm, mkPmId,
Delta, initDelta, lookupRefuts, lookupSolution,
TmCt(..),
addTypeEvidence,
addRefutableAltCon,
addTmCt,
addVarCoreCt,
canDiverge,
provideEvidence,
) where
#include "HsVersions.h"
import GhcPrelude
import GHC.HsToCore.PmCheck.Types
import DynFlags
import Outputable
import ErrUtils
import Util
import Bag
import UniqSet
import UniqDSet
import Unique
import Id
import VarEnv
import UniqDFM
import Var (EvVar)
import Name
import CoreSyn
import CoreFVs ( exprFreeVars )
import CoreMap
import CoreOpt (simpleOptExpr, exprIsConApp_maybe)
import CoreUtils (exprType)
import MkCore (mkListExpr, mkCharExpr)
import UniqSupply
import FastString
import SrcLoc
import ListSetOps (unionLists)
import Maybes
import ConLike
import DataCon
import PatSyn
import TyCon
import TysWiredIn
import TysPrim (tYPETyCon)
import TyCoRep
import Type
import TcSimplify (tcNormalise, tcCheckSatisfiability)
import TcType (evVarPred)
import Unify (tcMatchTy)
import TcRnTypes (completeMatchConLikes)
import Coercion
import MonadUtils hiding (foldlM)
import DsMonad hiding (foldlM)
import FamInst
import FamInstEnv
import Control.Monad (guard, mzero)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State.Strict
import Data.Bifunctor (second)
import Data.Foldable (foldlM, minimumBy)
import Data.List (find)
import qualified Data.List.NonEmpty as NonEmpty
import Data.Ord (comparing)
import qualified Data.Semigroup as Semigroup
import Data.Tuple (swap)
tracePm :: String -> SDoc -> DsM ()
tracePm :: String -> SDoc -> DsM ()
tracePm String
herald SDoc
doc = do
DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
PrintUnqualified
printer <- DsM PrintUnqualified
mkPrintUnqualifiedDs
IO () -> DsM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> DsM ()) -> IO () -> DsM ()
forall a b. (a -> b) -> a -> b
$ PrintUnqualified -> DynFlags -> DumpFlag -> SDoc -> IO ()
dumpIfSet_dyn_printer PrintUnqualified
printer DynFlags
dflags
DumpFlag
Opt_D_dump_ec_trace (String -> SDoc
text String
herald SDoc -> SDoc -> SDoc
$$ (Int -> SDoc -> SDoc
nest Int
2 SDoc
doc))
mkPmId :: Type -> DsM Id
mkPmId :: Type -> DsM Id
mkPmId Type
ty = IOEnv (Env DsGblEnv DsLclEnv) Unique
forall (m :: * -> *). MonadUnique m => m Unique
getUniqueM IOEnv (Env DsGblEnv DsLclEnv) Unique
-> (Unique -> DsM Id) -> DsM Id
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Unique
unique ->
let occname :: OccName
occname = FastString -> OccName
mkVarOccFS (FastString -> OccName) -> FastString -> OccName
forall a b. (a -> b) -> a -> b
$ String -> FastString
fsLit String
"pm"
name :: Name
name = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
unique OccName
occname SrcSpan
noSrcSpan
in Id -> DsM Id
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> Id
mkLocalId Name
name Type
ty)
markMatched :: ConLike -> PossibleMatches -> PossibleMatches
markMatched :: ConLike -> PossibleMatches -> PossibleMatches
markMatched ConLike
_ PossibleMatches
NoPM = PossibleMatches
NoPM
markMatched ConLike
con (PM NonEmpty ConLikeSet
ms) = NonEmpty ConLikeSet -> PossibleMatches
PM (ConLike -> ConLikeSet -> ConLikeSet
del_one_con ConLike
con (ConLikeSet -> ConLikeSet)
-> NonEmpty ConLikeSet -> NonEmpty ConLikeSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty ConLikeSet
ms)
where
del_one_con :: ConLike -> ConLikeSet -> ConLikeSet
del_one_con = (ConLikeSet -> ConLike -> ConLikeSet)
-> ConLike -> ConLikeSet -> ConLikeSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip ConLikeSet -> ConLike -> ConLikeSet
forall a. Uniquable a => UniqDSet a -> a -> UniqDSet a
delOneFromUniqDSet
mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type])
mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type])
mkOneConFull [Type]
arg_tys ConLike
con = do
let ([Id]
univ_tvs, [Id]
ex_tvs, [EqSpec]
eq_spec, [Type]
thetas, [Type]
_req_theta , [Type]
field_tys, Type
_con_res_ty)
= ConLike -> ([Id], [Id], [EqSpec], [Type], [Type], [Type], Type)
conLikeFullSig ConLike
con
let subst_univ :: TCvSubst
subst_univ = [Id] -> [Type] -> TCvSubst
HasDebugCallStack => [Id] -> [Type] -> TCvSubst
zipTvSubst [Id]
univ_tvs [Type]
arg_tys
(TCvSubst
subst, [Id]
_) <- TCvSubst -> [Id] -> UniqSupply -> (TCvSubst, [Id])
cloneTyVarBndrs TCvSubst
subst_univ [Id]
ex_tvs (UniqSupply -> (TCvSubst, [Id]))
-> IOEnv (Env DsGblEnv DsLclEnv) UniqSupply
-> IOEnv (Env DsGblEnv DsLclEnv) (TCvSubst, [Id])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env DsGblEnv DsLclEnv) UniqSupply
forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM
let field_tys' :: [Type]
field_tys' = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst [Type]
field_tys
[Id]
vars <- (Type -> DsM Id) -> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) [Id]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> DsM Id
mkPmId [Type]
field_tys'
let ty_cs :: [TyCt]
ty_cs = (Type -> TyCt) -> [Type] -> [TyCt]
forall a b. (a -> b) -> [a] -> [b]
map Type -> TyCt
TyCt (HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTheta TCvSubst
subst ([EqSpec] -> [Type]
eqSpecPreds [EqSpec]
eq_spec [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
thetas))
let arg_is_strict :: [Bool]
arg_is_strict
| RealDataCon DataCon
dc <- ConLike
con
, TyCon -> Bool
isNewTyCon (DataCon -> TyCon
dataConTyCon DataCon
dc)
= [Bool
True]
| Bool
otherwise
= (HsImplBang -> Bool) -> [HsImplBang] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map HsImplBang -> Bool
isBanged ([HsImplBang] -> [Bool]) -> [HsImplBang] -> [Bool]
forall a b. (a -> b) -> a -> b
$ ConLike -> [HsImplBang]
conLikeImplBangs ConLike
con
strict_arg_tys :: [Type]
strict_arg_tys = [Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList [Bool]
arg_is_strict [Type]
field_tys'
([Id], Bag TyCt, [Type]) -> DsM ([Id], Bag TyCt, [Type])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id]
vars, [TyCt] -> Bag TyCt
forall a. [a] -> Bag a
listToBag [TyCt]
ty_cs, [Type]
strict_arg_tys)
newtype SatisfiabilityCheck = SC (Delta -> DsM (Maybe Delta))
runSatisfiabilityCheck :: Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck :: Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck Delta
delta (SC Delta -> DsM (Maybe Delta)
chk) = Delta -> DsM (Maybe Delta)
chk Delta
delta
instance Semigroup SatisfiabilityCheck where
SC Delta -> DsM (Maybe Delta)
a <> :: SatisfiabilityCheck -> SatisfiabilityCheck -> SatisfiabilityCheck
<> SC Delta -> DsM (Maybe Delta)
b = (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
SC Delta -> DsM (Maybe Delta)
c
where
c :: Delta -> DsM (Maybe Delta)
c Delta
delta = Delta -> DsM (Maybe Delta)
a Delta
delta DsM (Maybe Delta)
-> (Maybe Delta -> DsM (Maybe Delta)) -> DsM (Maybe Delta)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe Delta
Nothing -> Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Delta
forall a. Maybe a
Nothing
Just Delta
delta' -> Delta -> DsM (Maybe Delta)
b Delta
delta'
instance Monoid SatisfiabilityCheck where
mempty :: SatisfiabilityCheck
mempty = (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
SC (Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Delta -> DsM (Maybe Delta))
-> (Delta -> Maybe Delta) -> Delta -> DsM (Maybe Delta)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Delta -> Maybe Delta
forall a. a -> Maybe a
Just)
pmIsSatisfiable
:: Delta
-> Bag TmCt
-> Bag TyCt
-> [Type]
-> DsM (Maybe Delta)
pmIsSatisfiable :: Delta -> Bag TmCt -> Bag TyCt -> [Type] -> DsM (Maybe Delta)
pmIsSatisfiable Delta
amb_cs Bag TmCt
new_tm_cs Bag TyCt
new_ty_cs [Type]
strict_arg_tys =
Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck Delta
amb_cs (SatisfiabilityCheck -> DsM (Maybe Delta))
-> SatisfiabilityCheck -> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ [SatisfiabilityCheck] -> SatisfiabilityCheck
forall a. Monoid a => [a] -> a
mconcat
[ Bool -> Bag TyCt -> SatisfiabilityCheck
tyIsSatisfiable Bool
True Bag TyCt
new_ty_cs
, Bag TmCt -> SatisfiabilityCheck
tmIsSatisfiable Bag TmCt
new_tm_cs
, RecTcChecker -> [Type] -> SatisfiabilityCheck
tysAreNonVoid RecTcChecker
initRecTc [Type]
strict_arg_tys
]
data TopNormaliseTypeResult
= NoChange Type
| NormalisedByConstraints Type
| HadRedexes Type [(Type, DataCon, Type)] Type
normalisedSourceType :: TopNormaliseTypeResult -> Type
normalisedSourceType :: TopNormaliseTypeResult -> Type
normalisedSourceType (NoChange Type
ty) = Type
ty
normalisedSourceType (NormalisedByConstraints Type
ty) = Type
ty
normalisedSourceType (HadRedexes Type
ty [(Type, DataCon, Type)]
_ Type
_) = Type
ty
tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts (NoChange Type
ty) = (Type
ty, [], Type
ty)
tntrGuts (NormalisedByConstraints Type
ty) = (Type
ty, [], Type
ty)
tntrGuts (HadRedexes Type
src_ty [(Type, DataCon, Type)]
ds Type
core_ty) = (Type
src_ty, [(Type, DataCon, Type)]
ds, Type
core_ty)
instance Outputable TopNormaliseTypeResult where
ppr :: TopNormaliseTypeResult -> SDoc
ppr (NoChange Type
ty) = String -> SDoc
text String
"NoChange" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
ppr (NormalisedByConstraints Type
ty) = String -> SDoc
text String
"NormalisedByConstraints" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
ppr (HadRedexes Type
src_ty [(Type, DataCon, Type)]
ds Type
core_ty) = String -> SDoc
text String
"HadRedexes" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces SDoc
fields
where
fields :: SDoc
fields = [SDoc] -> SDoc
fsep (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma [ String -> SDoc
text String
"src_ty =" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
src_ty
, String -> SDoc
text String
"newtype_dcs =" SDoc -> SDoc -> SDoc
<+> [(Type, DataCon, Type)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Type, DataCon, Type)]
ds
, String -> SDoc
text String
"core_ty =" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
core_ty ])
pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType (TySt Bag Id
inert) Type
typ
= do FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
(Messages
_, Maybe Type
mb_typ') <- TcM Type -> DsM (Messages, Maybe Type)
forall a. TcM a -> DsM (Messages, Maybe a)
initTcDsForSolver (TcM Type -> DsM (Messages, Maybe Type))
-> TcM Type -> DsM (Messages, Maybe Type)
forall a b. (a -> b) -> a -> b
$ Bag Id -> Type -> TcM Type
tcNormalise Bag Id
inert Type
typ
let typ' :: Type
typ' = Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe Type
typ Maybe Type
mb_typ'
TopNormaliseTypeResult -> DsM TopNormaliseTypeResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TopNormaliseTypeResult -> DsM TopNormaliseTypeResult)
-> TopNormaliseTypeResult -> DsM TopNormaliseTypeResult
forall a b. (a -> b) -> a -> b
$ case NormaliseStepper
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> (([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> ([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> ([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)]))
-> Type
-> Maybe
(([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)]),
Type)
forall ev.
NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX (FamInstEnvs
-> NormaliseStepper
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
stepper FamInstEnvs
env) ([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> ([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> ([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall b c b c a a.
(b -> c, b -> c) -> (a -> b, a -> b) -> (a -> c, a -> c)
comb Type
typ' of
Maybe
(([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)]),
Type)
Nothing
| Maybe Type
Nothing <- Maybe Type
mb_typ' -> Type -> TopNormaliseTypeResult
NoChange Type
typ
| Bool
otherwise -> Type -> TopNormaliseTypeResult
NormalisedByConstraints Type
typ'
Just (([Type] -> [Type]
ty_f,[(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tm_f), Type
ty) -> Type -> [(Type, DataCon, Type)] -> Type -> TopNormaliseTypeResult
HadRedexes Type
src_ty [(Type, DataCon, Type)]
newtype_dcs Type
core_ty
where
src_ty :: Type
src_ty = Type -> [Type] -> Type
eq_src_ty Type
ty (Type
typ' Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type] -> [Type]
ty_f [Type
ty])
newtype_dcs :: [(Type, DataCon, Type)]
newtype_dcs = [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tm_f []
core_ty :: Type
core_ty = Type
ty
where
eq_src_ty :: Type -> [Type] -> Type
eq_src_ty :: Type -> [Type] -> Type
eq_src_ty Type
ty [Type]
tys = Type -> (Type -> Type) -> Maybe Type -> Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Type
ty Type -> Type
forall a. a -> a
id ((Type -> Bool) -> [Type] -> Maybe Type
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Type -> Bool
is_closed_or_data_family [Type]
tys)
is_closed_or_data_family :: Type -> Bool
is_closed_or_data_family :: Type -> Bool
is_closed_or_data_family Type
ty = Type -> Bool
pmIsClosedType Type
ty Bool -> Bool -> Bool
|| Type -> Bool
isDataFamilyAppType Type
ty
comb :: (b -> c, b -> c) -> (a -> b, a -> b) -> (a -> c, a -> c)
comb (b -> c
tyf1, b -> c
tmf1) (a -> b
tyf2, a -> b
tmf2) = (b -> c
tyf1 (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
tyf2, b -> c
tmf1 (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
tmf2)
stepper :: FamInstEnvs
-> NormaliseStepper
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
stepper FamInstEnvs
env = NormaliseStepper
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
newTypeStepper NormaliseStepper
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> NormaliseStepper
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> NormaliseStepper
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev.
NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
`composeSteppers` FamInstEnvs
-> NormaliseStepper
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall a.
FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
tyFamStepper FamInstEnvs
env
newTypeStepper :: NormaliseStepper ([Type] -> [Type],[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
newTypeStepper :: NormaliseStepper
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
newTypeStepper RecTcChecker
rec_nts TyCon
tc [Type]
tys
| Just (Type
ty', Coercion
_co) <- TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe TyCon
tc [Type]
tys
, let orig_ty :: Type
orig_ty = TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys
= case RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_nts TyCon
tc of
Just RecTcChecker
rec_nts' -> let tyf :: [Type] -> [Type]
tyf = (Type
orig_tyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:)
tmf :: [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tmf = ((Type
orig_ty, TyCon -> DataCon
tyConSingleDataCon TyCon
tc, Type
ty')(Type, DataCon, Type)
-> [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
forall a. a -> [a] -> [a]
:)
in RecTcChecker
-> Type
-> ([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> NormaliseStepResult
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts' Type
ty' ([Type] -> [Type]
tyf, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tmf)
Maybe RecTcChecker
Nothing -> NormaliseStepResult
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev. NormaliseStepResult ev
NS_Abort
| Bool
otherwise
= NormaliseStepResult
([Type] -> [Type],
[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev. NormaliseStepResult ev
NS_Done
tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
tyFamStepper FamInstEnvs
env RecTcChecker
rec_nts TyCon
tc [Type]
tys
= let (Coercion
_args_co, [Type]
ntys, Coercion
_res_co) = FamInstEnvs
-> Role -> TyCon -> [Type] -> (Coercion, [Type], Coercion)
normaliseTcArgs FamInstEnvs
env Role
Representational TyCon
tc [Type]
tys in
case FamInstEnvs -> Role -> TyCon -> [Type] -> Maybe (Coercion, Type)
reduceTyFamApp_maybe FamInstEnvs
env Role
Representational TyCon
tc [Type]
ntys of
Just (Coercion
_co, Type
rhs) -> RecTcChecker
-> Type
-> ([Type] -> [Type], a -> a)
-> NormaliseStepResult ([Type] -> [Type], a -> a)
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts Type
rhs ((Type
rhsType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:), a -> a
forall a. a -> a
id)
Maybe (Coercion, Type)
_ -> NormaliseStepResult ([Type] -> [Type], a -> a)
forall ev. NormaliseStepResult ev
NS_Done
pmIsClosedType :: Type -> Bool
pmIsClosedType :: Type -> Bool
pmIsClosedType Type
ty
= case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
Just (TyCon
tc, [Type]
ty_args)
| TyCon -> Bool
is_algebraic_like TyCon
tc Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isFamilyTyCon TyCon
tc)
-> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
Maybe (TyCon, [Type])
_other -> Bool
False
where
is_algebraic_like :: TyCon -> Bool
is_algebraic_like :: TyCon -> Bool
is_algebraic_like TyCon
tc = TyCon -> Bool
isAlgTyCon TyCon
tc Bool -> Bool -> Bool
|| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tYPETyCon
newtype TyCt = TyCt PredType
instance Outputable TyCt where
ppr :: TyCt -> SDoc
ppr (TyCt Type
pred_ty) = Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred_ty
nameTyCt :: TyCt -> DsM EvVar
nameTyCt :: TyCt -> DsM Id
nameTyCt (TyCt Type
pred_ty) = do
Unique
unique <- IOEnv (Env DsGblEnv DsLclEnv) Unique
forall (m :: * -> *). MonadUnique m => m Unique
getUniqueM
let occname :: OccName
occname = FastString -> OccName
mkVarOccFS (String -> FastString
fsLit (String
"pm_"String -> String -> String
forall a. [a] -> [a] -> [a]
++Unique -> String
forall a. Show a => a -> String
show Unique
unique))
idname :: Name
idname = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
unique OccName
occname SrcSpan
noSrcSpan
Id -> DsM Id
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> Id
mkLocalId Name
idname Type
pred_ty)
tyOracle :: TyState -> Bag TyCt -> DsM (Maybe TyState)
tyOracle :: TyState -> Bag TyCt -> DsM (Maybe TyState)
tyOracle (TySt Bag Id
inert) Bag TyCt
cts
= do { Bag Id
evs <- (TyCt -> DsM Id)
-> Bag TyCt -> IOEnv (Env DsGblEnv DsLclEnv) (Bag Id)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse TyCt -> DsM Id
nameTyCt Bag TyCt
cts
; let new_inert :: Bag Id
new_inert = Bag Id
inert Bag Id -> Bag Id -> Bag Id
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Id
evs
; String -> SDoc -> DsM ()
tracePm String
"tyOracle" (Bag TyCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag TyCt
cts)
; ((WarningMessages
_warns, WarningMessages
errs), Maybe Bool
res) <- TcM Bool -> DsM (Messages, Maybe Bool)
forall a. TcM a -> DsM (Messages, Maybe a)
initTcDsForSolver (TcM Bool -> DsM (Messages, Maybe Bool))
-> TcM Bool -> DsM (Messages, Maybe Bool)
forall a b. (a -> b) -> a -> b
$ Bag Id -> TcM Bool
tcCheckSatisfiability Bag Id
new_inert
; case Maybe Bool
res of
Just Bool
True -> Maybe TyState -> DsM (Maybe TyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyState -> Maybe TyState
forall a. a -> Maybe a
Just (Bag Id -> TyState
TySt Bag Id
new_inert))
Just Bool
False -> Maybe TyState -> DsM (Maybe TyState)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TyState
forall a. Maybe a
Nothing
Maybe Bool
Nothing -> String -> SDoc -> DsM (Maybe TyState)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tyOracle" ([SDoc] -> SDoc
vcat ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ WarningMessages -> [SDoc]
pprErrMsgBagWithLoc WarningMessages
errs) }
tyIsSatisfiable :: Bool -> Bag TyCt -> SatisfiabilityCheck
tyIsSatisfiable :: Bool -> Bag TyCt -> SatisfiabilityCheck
tyIsSatisfiable Bool
recheck_complete_sets Bag TyCt
new_ty_cs = (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
SC ((Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck)
-> (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
forall a b. (a -> b) -> a -> b
$ \Delta
delta ->
if Bag TyCt -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag TyCt
new_ty_cs
then Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta -> Maybe Delta
forall a. a -> Maybe a
Just Delta
delta)
else TyState -> Bag TyCt -> DsM (Maybe TyState)
tyOracle (Delta -> TyState
delta_ty_st Delta
delta) Bag TyCt
new_ty_cs DsM (Maybe TyState)
-> (Maybe TyState -> DsM (Maybe Delta)) -> DsM (Maybe Delta)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe TyState
Nothing -> Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Delta
forall a. Maybe a
Nothing
Just TyState
ty_st' -> do
let delta' :: Delta
delta' = Delta
delta{ delta_ty_st :: TyState
delta_ty_st = TyState
ty_st' }
if Bool
recheck_complete_sets
then Delta -> DsM (Maybe Delta)
ensureAllPossibleMatchesInhabited Delta
delta'
else Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta -> Maybe Delta
forall a. a -> Maybe a
Just Delta
delta')
tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck
tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck
tmIsSatisfiable Bag TmCt
new_tm_cs = (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
SC ((Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck)
-> (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
forall a b. (a -> b) -> a -> b
$ \Delta
delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta -> DsM (Maybe Delta)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta -> DsM (Maybe Delta))
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
-> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ (Delta -> TmCt -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> Delta
-> Bag TmCt
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Delta -> TmCt -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
go Delta
delta Bag TmCt
new_tm_cs
where
go :: Delta -> TmCt -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
go Delta
delta TmCt
ct = DsM (Maybe Delta) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Delta -> TmCt -> DsM (Maybe Delta)
addTmCt Delta
delta TmCt
ct)
emptyVarInfo :: Id -> VarInfo
emptyVarInfo :: Id -> VarInfo
emptyVarInfo Id
x = Type
-> [(PmAltCon, [Id])] -> [PmAltCon] -> PossibleMatches -> VarInfo
VI (Id -> Type
idType Id
x) [] [] PossibleMatches
NoPM
lookupVarInfo :: TmState -> Id -> VarInfo
lookupVarInfo :: TmState -> Id -> VarInfo
lookupVarInfo (TmSt SharedDIdEnv VarInfo
env CoreMap Id
_) Id
x = VarInfo -> Maybe VarInfo -> VarInfo
forall a. a -> Maybe a -> a
fromMaybe (Id -> VarInfo
emptyVarInfo Id
x) (SharedDIdEnv VarInfo -> Id -> Maybe VarInfo
forall a. SharedDIdEnv a -> Id -> Maybe a
lookupSDIE SharedDIdEnv VarInfo
env Id
x)
initPossibleMatches :: TyState -> VarInfo -> DsM VarInfo
initPossibleMatches :: TyState -> VarInfo -> DsM VarInfo
initPossibleMatches TyState
ty_st vi :: VarInfo
vi@VI{ vi_ty :: VarInfo -> Type
vi_ty = Type
ty, vi_cache :: VarInfo -> PossibleMatches
vi_cache = PossibleMatches
NoPM } = do
TopNormaliseTypeResult
res <- TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType TyState
ty_st Type
ty
let ty' :: Type
ty' = TopNormaliseTypeResult -> Type
normalisedSourceType TopNormaliseTypeResult
res
case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty' of
Maybe (TyCon, [Type])
Nothing -> VarInfo -> DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi{ vi_ty :: Type
vi_ty = Type
ty' }
Just (TyCon
tc, [Type
_])
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tYPETyCon
-> VarInfo -> DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi{ vi_ty :: Type
vi_ty = Type
ty', vi_cache :: PossibleMatches
vi_cache = NonEmpty ConLikeSet -> PossibleMatches
PM (ConLikeSet -> NonEmpty ConLikeSet
forall (f :: * -> *) a. Applicative f => a -> f a
pure ConLikeSet
forall a. UniqDSet a
emptyUniqDSet) }
Just (TyCon
tc, [Type]
tc_args) -> do
(TyCon
tc_rep, TyCon
tc_fam) <- case TyCon -> Maybe (TyCon, [Type])
tyConFamInst_maybe TyCon
tc of
Just (TyCon
tc_fam, [Type]
_) -> (TyCon, TyCon) -> IOEnv (Env DsGblEnv DsLclEnv) (TyCon, TyCon)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon
tc, TyCon
tc_fam)
Maybe (TyCon, [Type])
Nothing -> do
FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
let (TyCon
tc_rep, [Type]
_tc_rep_args, Coercion
_co) = FamInstEnvs -> TyCon -> [Type] -> (TyCon, [Type], Coercion)
tcLookupDataFamInst FamInstEnvs
env TyCon
tc [Type]
tc_args
(TyCon, TyCon) -> IOEnv (Env DsGblEnv DsLclEnv) (TyCon, TyCon)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon
tc_rep, TyCon
tc)
let mb_rdcs :: Maybe [ConLike]
mb_rdcs = (DataCon -> ConLike) -> [DataCon] -> [ConLike]
forall a b. (a -> b) -> [a] -> [b]
map DataCon -> ConLike
RealDataCon ([DataCon] -> [ConLike]) -> Maybe [DataCon] -> Maybe [ConLike]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> Maybe [DataCon]
tyConDataCons_maybe TyCon
tc_rep
let rdcs :: [[ConLike]]
rdcs = Maybe [ConLike] -> [[ConLike]]
forall a. Maybe a -> [a]
maybeToList Maybe [ConLike]
mb_rdcs
[CompleteMatch]
pragmas <- TyCon -> DsM [CompleteMatch]
dsGetCompleteMatches TyCon
tc_fam
let fams :: CompleteMatch -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike]
fams = (Name -> IOEnv (Env DsGblEnv DsLclEnv) ConLike)
-> [Name] -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> IOEnv (Env DsGblEnv DsLclEnv) ConLike
dsLookupConLike ([Name] -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike])
-> (CompleteMatch -> [Name])
-> CompleteMatch
-> IOEnv (Env DsGblEnv DsLclEnv) [ConLike]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompleteMatch -> [Name]
completeMatchConLikes
[[ConLike]]
pscs <- (CompleteMatch -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike])
-> [CompleteMatch] -> IOEnv (Env DsGblEnv DsLclEnv) [[ConLike]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CompleteMatch -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike]
fams [CompleteMatch]
pragmas
case [[ConLike]] -> Maybe (NonEmpty [ConLike])
forall a. [a] -> Maybe (NonEmpty a)
NonEmpty.nonEmpty ([[ConLike]]
rdcs [[ConLike]] -> [[ConLike]] -> [[ConLike]]
forall a. [a] -> [a] -> [a]
++ [[ConLike]]
pscs) of
Maybe (NonEmpty [ConLike])
Nothing -> VarInfo -> DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi{ vi_ty :: Type
vi_ty = Type
ty' }
Just NonEmpty [ConLike]
cs -> VarInfo -> DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi{ vi_ty :: Type
vi_ty = Type
ty', vi_cache :: PossibleMatches
vi_cache = NonEmpty ConLikeSet -> PossibleMatches
PM ([ConLike] -> ConLikeSet
forall a. Uniquable a => [a] -> UniqDSet a
mkUniqDSet ([ConLike] -> ConLikeSet)
-> NonEmpty [ConLike] -> NonEmpty ConLikeSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty [ConLike]
cs) }
initPossibleMatches TyState
_ VarInfo
vi = VarInfo -> DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi
initLookupVarInfo :: Delta -> Id -> DsM VarInfo
initLookupVarInfo :: Delta -> Id -> DsM VarInfo
initLookupVarInfo MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmState
ts, delta_ty_st :: Delta -> TyState
delta_ty_st = TyState
ty_st } Id
x
= TyState -> VarInfo -> DsM VarInfo
initPossibleMatches TyState
ty_st (TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x)
canDiverge :: Delta -> Id -> Bool
canDiverge :: Delta -> Id -> Bool
canDiverge delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmState
ts } Id
x
| VI Type
_ [(PmAltCon, [Id])]
pos [PmAltCon]
neg PossibleMatches
_ <- TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x
= [PmAltCon] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PmAltCon]
neg Bool -> Bool -> Bool
&& ((PmAltCon, [Id]) -> Bool) -> [(PmAltCon, [Id])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (PmAltCon, [Id]) -> Bool
pos_can_diverge [(PmAltCon, [Id])]
pos
where
pos_can_diverge :: (PmAltCon, [Id]) -> Bool
pos_can_diverge (PmAltConLike (RealDataCon DataCon
dc), [Id
y])
| TyCon -> Bool
isNewTyCon (DataCon -> TyCon
dataConTyCon DataCon
dc) = Delta -> Id -> Bool
canDiverge Delta
delta Id
y
pos_can_diverge (PmAltCon, [Id])
_ = Bool
False
lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon]
lookupRefuts :: Delta -> k -> [PmAltCon]
lookupRefuts MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = ts :: TmState
ts@(TmSt (SDIE DIdEnv (Shared VarInfo)
env) CoreMap Id
_) } k
k =
case DIdEnv (Shared VarInfo) -> k -> Maybe (Shared VarInfo)
forall key elt. Uniquable key => UniqDFM elt -> key -> Maybe elt
lookupUDFM DIdEnv (Shared VarInfo)
env k
k of
Maybe (Shared VarInfo)
Nothing -> []
Just (Indirect Id
y) -> VarInfo -> [PmAltCon]
vi_neg (TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
y)
Just (Entry VarInfo
vi) -> VarInfo -> [PmAltCon]
vi_neg VarInfo
vi
isDataConSolution :: (PmAltCon, [Id]) -> Bool
isDataConSolution :: (PmAltCon, [Id]) -> Bool
isDataConSolution (PmAltConLike (RealDataCon DataCon
_), [Id]
_) = Bool
True
isDataConSolution (PmAltCon, [Id])
_ = Bool
False
lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [Id])
lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [Id])
lookupSolution Delta
delta Id
x = case VarInfo -> [(PmAltCon, [Id])]
vi_pos (TmState -> Id -> VarInfo
lookupVarInfo (Delta -> TmState
delta_tm_st Delta
delta) Id
x) of
[] -> Maybe (PmAltCon, [Id])
forall a. Maybe a
Nothing
[(PmAltCon, [Id])]
pos
| Just (PmAltCon, [Id])
sol <- ((PmAltCon, [Id]) -> Bool)
-> [(PmAltCon, [Id])] -> Maybe (PmAltCon, [Id])
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (PmAltCon, [Id]) -> Bool
isDataConSolution [(PmAltCon, [Id])]
pos -> (PmAltCon, [Id]) -> Maybe (PmAltCon, [Id])
forall a. a -> Maybe a
Just (PmAltCon, [Id])
sol
| Bool
otherwise -> (PmAltCon, [Id]) -> Maybe (PmAltCon, [Id])
forall a. a -> Maybe a
Just ([(PmAltCon, [Id])] -> (PmAltCon, [Id])
forall a. [a] -> a
head [(PmAltCon, [Id])]
pos)
data TmCt
= TmVarVar !Id !Id
| TmVarCon !Id !PmAltCon ![Id]
| TmVarNonVoid !Id
instance Outputable TmCt where
ppr :: TmCt -> SDoc
ppr (TmVarVar Id
x Id
y) = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<+> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
y
ppr (TmVarCon Id
x PmAltCon
con [Id]
args) = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<+> [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 Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
args)
ppr (TmVarNonVoid Id
x) = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"/~ ⊥"
addTypeEvidence :: Delta -> Bag EvVar -> DsM (Maybe Delta)
addTypeEvidence :: Delta -> Bag Id -> DsM (Maybe Delta)
addTypeEvidence Delta
delta Bag Id
dicts
= Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck Delta
delta (Bool -> Bag TyCt -> SatisfiabilityCheck
tyIsSatisfiable Bool
True (Type -> TyCt
TyCt (Type -> TyCt) -> (Id -> Type) -> Id -> TyCt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Type
evVarPred (Id -> TyCt) -> Bag Id -> Bag TyCt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bag Id
dicts))
addTmCt :: Delta -> TmCt -> DsM (Maybe Delta)
addTmCt :: Delta -> TmCt -> DsM (Maybe Delta)
addTmCt Delta
delta TmCt
ct = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta -> DsM (Maybe Delta)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta -> DsM (Maybe Delta))
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
-> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ case TmCt
ct of
TmVarVar Id
x Id
y -> Delta -> (Id, Id) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarVarCt Delta
delta (Id
x, Id
y)
TmVarCon Id
x PmAltCon
con [Id]
args -> Delta
-> Id
-> PmAltCon
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarConCt Delta
delta Id
x PmAltCon
con [Id]
args
TmVarNonVoid Id
x -> Delta -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarNonVoidCt Delta
delta Id
x
addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta)
addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta)
addRefutableAltCon delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps } Id
x PmAltCon
nalt = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta -> DsM (Maybe Delta)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta -> DsM (Maybe Delta))
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
-> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ do
vi :: VarInfo
vi@(VI Type
_ [(PmAltCon, [Id])]
pos [PmAltCon]
neg PossibleMatches
pm) <- DsM VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Delta -> Id -> DsM VarInfo
initLookupVarInfo Delta
delta Id
x)
let contradicts :: PmAltCon -> (PmAltCon, b) -> Bool
contradicts PmAltCon
nalt (PmAltCon
cl, b
_args) = PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
cl PmAltCon
nalt PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
Equal
Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (((PmAltCon, [Id]) -> Bool) -> [(PmAltCon, [Id])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PmAltCon -> (PmAltCon, [Id]) -> Bool
forall b. PmAltCon -> (PmAltCon, b) -> Bool
contradicts PmAltCon
nalt) [(PmAltCon, [Id])]
pos))
let implies :: PmAltCon -> (PmAltCon, b) -> Bool
implies PmAltCon
nalt (PmAltCon
cl, b
_args) = PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
cl PmAltCon
nalt PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
Disjoint
let neg' :: [PmAltCon]
neg'
| ((PmAltCon, [Id]) -> Bool) -> [(PmAltCon, [Id])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PmAltCon -> (PmAltCon, [Id]) -> Bool
forall b. PmAltCon -> (PmAltCon, b) -> Bool
implies PmAltCon
nalt) [(PmAltCon, [Id])]
pos = [PmAltCon]
neg
| PmAltCon -> Bool
hasRequiredTheta PmAltCon
nalt = [PmAltCon]
neg
| Bool
otherwise = [PmAltCon] -> [PmAltCon] -> [PmAltCon]
forall a.
(HasDebugCallStack, Outputable a, Eq a) =>
[a] -> [a] -> [a]
unionLists [PmAltCon]
neg [PmAltCon
nalt]
let vi_ext :: VarInfo
vi_ext = VarInfo
vi{ vi_neg :: [PmAltCon]
vi_neg = [PmAltCon]
neg' }
VarInfo
vi' <- case PmAltCon
nalt of
PmAltConLike ConLike
cl
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Delta -> VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
ensureInhabited Delta
delta VarInfo
vi_ext{ vi_cache :: PossibleMatches
vi_cache = ConLike -> PossibleMatches -> PossibleMatches
markMatched ConLike
cl PossibleMatches
pm })
PmAltCon
_ -> VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi_ext
Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt (SharedDIdEnv VarInfo -> Id -> VarInfo -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE SharedDIdEnv VarInfo
env Id
x VarInfo
vi') CoreMap Id
reps }
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta (PmAltConLike ConLike
cl) = [Type] -> Bool
forall a. [a] -> Bool
notNull [Type]
req_theta
where
([Id]
_,[Id]
_,[EqSpec]
_,[Type]
_,[Type]
req_theta,[Type]
_,Type
_) = ConLike -> ([Id], [Id], [EqSpec], [Type], [Type], [Type], Type)
conLikeFullSig ConLike
cl
hasRequiredTheta PmAltCon
_ = Bool
False
guessConLikeUnivTyArgsFromResTy :: FamInstEnvs -> Type -> ConLike -> Maybe [Type]
guessConLikeUnivTyArgsFromResTy :: FamInstEnvs -> Type -> ConLike -> Maybe [Type]
guessConLikeUnivTyArgsFromResTy FamInstEnvs
env Type
res_ty (RealDataCon DataCon
_) = do
(TyCon
tc, [Type]
tc_args) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
res_ty
let (TyCon
_, [Type]
tc_args', Coercion
_) = FamInstEnvs -> TyCon -> [Type] -> (TyCon, [Type], Coercion)
tcLookupDataFamInst FamInstEnvs
env TyCon
tc [Type]
tc_args
[Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
tc_args'
guessConLikeUnivTyArgsFromResTy FamInstEnvs
_ Type
res_ty (PatSynCon PatSyn
ps) = do
let ([Id]
univ_tvs,[Type]
_,[Id]
_,[Type]
_,[Type]
_,Type
con_res_ty) = PatSyn -> ([Id], [Type], [Id], [Type], [Type], Type)
patSynSig PatSyn
ps
TCvSubst
subst <- Type -> Type -> Maybe TCvSubst
tcMatchTy Type
con_res_ty Type
res_ty
(Id -> Maybe Type) -> [Id] -> Maybe [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (TCvSubst -> Id -> Maybe Type
lookupTyVar TCvSubst
subst) [Id]
univ_tvs
addVarNonVoidCt :: Delta -> Id -> MaybeT DsM Delta
addVarNonVoidCt :: Delta -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarNonVoidCt delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps } Id
x = do
VarInfo
vi <- DsM VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (DsM VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo)
-> DsM VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall a b. (a -> b) -> a -> b
$ Delta -> Id -> DsM VarInfo
initLookupVarInfo Delta
delta Id
x
VarInfo
vi' <- IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall a b. (a -> b) -> a -> b
$ Delta -> VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
ensureInhabited Delta
delta VarInfo
vi
Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt (SharedDIdEnv VarInfo -> Id -> VarInfo -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE SharedDIdEnv VarInfo
env Id
x VarInfo
vi') CoreMap Id
reps}
ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo)
ensureInhabited :: Delta -> VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
ensureInhabited Delta
delta VarInfo
vi = (PossibleMatches -> VarInfo)
-> Maybe PossibleMatches -> Maybe VarInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VarInfo -> PossibleMatches -> VarInfo
set_cache VarInfo
vi) (Maybe PossibleMatches -> Maybe VarInfo)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe PossibleMatches)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PossibleMatches
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe PossibleMatches)
test (VarInfo -> PossibleMatches
vi_cache VarInfo
vi)
where
set_cache :: VarInfo -> PossibleMatches -> VarInfo
set_cache VarInfo
vi PossibleMatches
cache = VarInfo
vi { vi_cache :: PossibleMatches
vi_cache = PossibleMatches
cache }
test :: PossibleMatches
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe PossibleMatches)
test PossibleMatches
NoPM = Maybe PossibleMatches
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe PossibleMatches)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PossibleMatches -> Maybe PossibleMatches
forall a. a -> Maybe a
Just PossibleMatches
NoPM)
test (PM NonEmpty ConLikeSet
ms) = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) PossibleMatches
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe PossibleMatches)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (NonEmpty ConLikeSet -> PossibleMatches
PM (NonEmpty ConLikeSet -> PossibleMatches)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (NonEmpty ConLikeSet)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) PossibleMatches
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ConLikeSet -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ConLikeSet)
-> NonEmpty ConLikeSet
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (NonEmpty ConLikeSet)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ConLikeSet -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ConLikeSet
one_set NonEmpty ConLikeSet
ms)
one_set :: ConLikeSet -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ConLikeSet
one_set ConLikeSet
cs = ConLikeSet
-> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ConLikeSet
find_one_inh ConLikeSet
cs (ConLikeSet -> [ConLike]
forall a. UniqDSet a -> [a]
uniqDSetToList ConLikeSet
cs)
find_one_inh :: ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet
find_one_inh :: ConLikeSet
-> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ConLikeSet
find_one_inh ConLikeSet
_ [] = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ConLikeSet
forall (m :: * -> *) a. MonadPlus m => m a
mzero
find_one_inh ConLikeSet
cs (ConLike
con:[ConLike]
cons) = IOEnv (Env DsGblEnv DsLclEnv) Bool
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ConLike -> IOEnv (Env DsGblEnv DsLclEnv) Bool
inh_test ConLike
con) MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Bool
-> (Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ConLikeSet)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ConLikeSet
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> ConLikeSet -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ConLikeSet
forall (f :: * -> *) a. Applicative f => a -> f a
pure ConLikeSet
cs
Bool
False -> ConLikeSet
-> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ConLikeSet
find_one_inh (ConLikeSet -> ConLike -> ConLikeSet
forall a. Uniquable a => UniqDSet a -> a -> UniqDSet a
delOneFromUniqDSet ConLikeSet
cs ConLike
con) [ConLike]
cons
inh_test :: ConLike -> DsM Bool
inh_test :: ConLike -> IOEnv (Env DsGblEnv DsLclEnv) Bool
inh_test ConLike
con = do
FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
case FamInstEnvs -> Type -> ConLike -> Maybe [Type]
guessConLikeUnivTyArgsFromResTy FamInstEnvs
env (VarInfo -> Type
vi_ty VarInfo
vi) ConLike
con of
Maybe [Type]
Nothing -> Bool -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
Just [Type]
arg_tys -> do
([Id]
_vars, Bag TyCt
ty_cs, [Type]
strict_arg_tys) <- [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type])
mkOneConFull [Type]
arg_tys ConLike
con
String -> SDoc -> DsM ()
tracePm String
"inh_test" (ConLike -> SDoc
forall a. Outputable a => a -> SDoc
ppr ConLike
con SDoc -> SDoc -> SDoc
$$ Bag TyCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag TyCt
ty_cs)
(Maybe Delta -> Bool)
-> DsM (Maybe Delta) -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe Delta -> Bool
forall a. Maybe a -> Bool
isJust (DsM (Maybe Delta) -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> (SatisfiabilityCheck -> DsM (Maybe Delta))
-> SatisfiabilityCheck
-> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck Delta
delta (SatisfiabilityCheck -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> SatisfiabilityCheck -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall a b. (a -> b) -> a -> b
$ [SatisfiabilityCheck] -> SatisfiabilityCheck
forall a. Monoid a => [a] -> a
mconcat
[ Bool -> Bag TyCt -> SatisfiabilityCheck
tyIsSatisfiable Bool
False Bag TyCt
ty_cs
, RecTcChecker -> [Type] -> SatisfiabilityCheck
tysAreNonVoid RecTcChecker
initRecTc [Type]
strict_arg_tys
]
ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta)
ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta)
ensureAllPossibleMatchesInhabited delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps }
= MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta -> DsM (Maybe Delta)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (Delta -> SharedDIdEnv VarInfo -> Delta
set_tm_cs_env Delta
delta (SharedDIdEnv VarInfo -> Delta)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (SharedDIdEnv VarInfo)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo)
-> SharedDIdEnv VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (SharedDIdEnv VarInfo)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)
traverseSDIE VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
go SharedDIdEnv VarInfo
env)
where
set_tm_cs_env :: Delta -> SharedDIdEnv VarInfo -> Delta
set_tm_cs_env Delta
delta SharedDIdEnv VarInfo
env = Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps }
go :: VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
go VarInfo
vi = IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Delta -> VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
ensureInhabited Delta
delta VarInfo
vi)
addVarVarCt :: Delta -> (Id, Id) -> MaybeT DsM Delta
addVarVarCt :: Delta -> (Id, Id) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarVarCt delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
_ } (Id
x, Id
y)
| SharedDIdEnv VarInfo -> Id -> Id -> Bool
forall a. SharedDIdEnv a -> Id -> Id -> Bool
sameRepresentativeSDIE SharedDIdEnv VarInfo
env Id
x Id
y = Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta
| Bool
otherwise = Delta -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
equate Delta
delta Id
x Id
y
equate :: Delta -> Id -> Id -> MaybeT DsM Delta
equate :: Delta -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
equate delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps } Id
x Id
y
= ASSERT( not (sameRepresentativeSDIE env x y) )
case (SharedDIdEnv VarInfo -> Id -> Maybe VarInfo
forall a. SharedDIdEnv a -> Id -> Maybe a
lookupSDIE SharedDIdEnv VarInfo
env Id
x, SharedDIdEnv VarInfo -> Id -> Maybe VarInfo
forall a. SharedDIdEnv a -> Id -> Maybe a
lookupSDIE SharedDIdEnv VarInfo
env Id
y) of
(Maybe VarInfo
Nothing, Maybe VarInfo
_) -> Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt (SharedDIdEnv VarInfo -> Id -> Id -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
setIndirectSDIE SharedDIdEnv VarInfo
env Id
x Id
y) CoreMap Id
reps })
(Maybe VarInfo
_, Maybe VarInfo
Nothing) -> Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt (SharedDIdEnv VarInfo -> Id -> Id -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
setIndirectSDIE SharedDIdEnv VarInfo
env Id
y Id
x) CoreMap Id
reps })
(Just VarInfo
vi_x, Just VarInfo
vi_y) -> do
MASSERT2( vi_ty vi_x `eqType` vi_ty vi_y, text "Not same type" )
let env_ind :: SharedDIdEnv VarInfo
env_ind = SharedDIdEnv VarInfo -> Id -> Id -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
setIndirectSDIE SharedDIdEnv VarInfo
env Id
x Id
y
let env_refs :: SharedDIdEnv VarInfo
env_refs = SharedDIdEnv VarInfo -> Id -> VarInfo -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE SharedDIdEnv VarInfo
env_ind Id
y VarInfo
vi_y
let delta_refs :: Delta
delta_refs = Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt SharedDIdEnv VarInfo
env_refs CoreMap Id
reps }
let add_fact :: Delta
-> (PmAltCon, [Id]) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
add_fact Delta
delta (PmAltCon
cl, [Id]
args) = Delta
-> Id
-> PmAltCon
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarConCt Delta
delta Id
y PmAltCon
cl [Id]
args
Delta
delta_pos <- (Delta
-> (PmAltCon, [Id])
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> Delta
-> [(PmAltCon, [Id])]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Delta
-> (PmAltCon, [Id]) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
add_fact Delta
delta_refs (VarInfo -> [(PmAltCon, [Id])]
vi_pos VarInfo
vi_x)
let add_refut :: Delta -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
add_refut Delta
delta PmAltCon
nalt = DsM (Maybe Delta) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Delta -> Id -> PmAltCon -> DsM (Maybe Delta)
addRefutableAltCon Delta
delta Id
y PmAltCon
nalt)
Delta
delta_neg <- (Delta -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> Delta
-> [PmAltCon]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Delta -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
add_refut Delta
delta_pos (VarInfo -> [PmAltCon]
vi_neg VarInfo
vi_x)
Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta_neg
addVarConCt :: Delta -> Id -> PmAltCon -> [Id] -> MaybeT DsM Delta
addVarConCt :: Delta
-> Id
-> PmAltCon
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarConCt delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps } Id
x PmAltCon
alt [Id]
args = do
VI Type
ty [(PmAltCon, [Id])]
pos [PmAltCon]
neg PossibleMatches
cache <- DsM VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Delta -> Id -> DsM VarInfo
initLookupVarInfo Delta
delta Id
x)
Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ((PmAltCon -> Bool) -> [PmAltCon] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
/= PmEquality
Equal) (PmEquality -> Bool)
-> (PmAltCon -> PmEquality) -> PmAltCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
alt) [PmAltCon]
neg)
Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (((PmAltCon, [Id]) -> Bool) -> [(PmAltCon, [Id])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
/= PmEquality
Disjoint) (PmEquality -> Bool)
-> ((PmAltCon, [Id]) -> PmEquality) -> (PmAltCon, [Id]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
alt (PmAltCon -> PmEquality)
-> ((PmAltCon, [Id]) -> PmAltCon) -> (PmAltCon, [Id]) -> PmEquality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PmAltCon, [Id]) -> PmAltCon
forall a b. (a, b) -> a
fst) [(PmAltCon, [Id])]
pos)
case ((PmAltCon, [Id]) -> Bool)
-> [(PmAltCon, [Id])] -> Maybe (PmAltCon, [Id])
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
Equal) (PmEquality -> Bool)
-> ((PmAltCon, [Id]) -> PmEquality) -> (PmAltCon, [Id]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
alt (PmAltCon -> PmEquality)
-> ((PmAltCon, [Id]) -> PmAltCon) -> (PmAltCon, [Id]) -> PmEquality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PmAltCon, [Id]) -> PmAltCon
forall a b. (a, b) -> a
fst) [(PmAltCon, [Id])]
pos of
Just (PmAltCon
_, [Id]
other_args) -> do
(Delta -> (Id, Id) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> Delta
-> [(Id, Id)]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Delta -> (Id, Id) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarVarCt Delta
delta ([Id] -> [Id] -> [(Id, Id)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Id]
args [Id]
other_args)
Maybe (PmAltCon, [Id])
Nothing -> do
let neg' :: [PmAltCon]
neg' = (PmAltCon -> Bool) -> [PmAltCon] -> [PmAltCon]
forall a. (a -> Bool) -> [a] -> [a]
filter ((PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
PossiblyOverlap) (PmEquality -> Bool)
-> (PmAltCon -> PmEquality) -> PmAltCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
alt) [PmAltCon]
neg
let pos' :: [(PmAltCon, [Id])]
pos' = (PmAltCon
alt,[Id]
args)(PmAltCon, [Id]) -> [(PmAltCon, [Id])] -> [(PmAltCon, [Id])]
forall a. a -> [a] -> [a]
:[(PmAltCon, [Id])]
pos
Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt (SharedDIdEnv VarInfo -> Id -> VarInfo -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE SharedDIdEnv VarInfo
env Id
x (Type
-> [(PmAltCon, [Id])] -> [PmAltCon] -> PossibleMatches -> VarInfo
VI Type
ty [(PmAltCon, [Id])]
pos' [PmAltCon]
neg' PossibleMatches
cache)) CoreMap Id
reps}
data InhabitationCandidate =
InhabitationCandidate
{ InhabitationCandidate -> Bag TmCt
ic_tm_cs :: Bag TmCt
, InhabitationCandidate -> Bag TyCt
ic_ty_cs :: Bag TyCt
, InhabitationCandidate -> [Type]
ic_strict_arg_tys :: [Type]
}
instance Outputable InhabitationCandidate where
ppr :: InhabitationCandidate -> SDoc
ppr (InhabitationCandidate Bag TmCt
tm_cs Bag TyCt
ty_cs [Type]
strict_arg_tys) =
String -> SDoc
text String
"InhabitationCandidate" SDoc -> SDoc -> SDoc
<+>
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"ic_tm_cs =" SDoc -> SDoc -> SDoc
<+> Bag TmCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag TmCt
tm_cs
, String -> SDoc
text String
"ic_ty_cs =" SDoc -> SDoc -> SDoc
<+> Bag TyCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag TyCt
ty_cs
, String -> SDoc
text String
"ic_strict_arg_tys =" SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
strict_arg_tys ]
mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate
mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate
mkInhabitationCandidate Id
x DataCon
dc = do
let cl :: ConLike
cl = DataCon -> ConLike
RealDataCon DataCon
dc
let tc_args :: [Type]
tc_args = Type -> [Type]
tyConAppArgs (Id -> Type
idType Id
x)
([Id]
arg_vars, Bag TyCt
ty_cs, [Type]
strict_arg_tys) <- [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type])
mkOneConFull [Type]
tc_args ConLike
cl
InhabitationCandidate -> DsM InhabitationCandidate
forall (f :: * -> *) a. Applicative f => a -> f a
pure InhabitationCandidate :: Bag TmCt -> Bag TyCt -> [Type] -> InhabitationCandidate
InhabitationCandidate
{ ic_tm_cs :: Bag TmCt
ic_tm_cs = TmCt -> Bag TmCt
forall a. a -> Bag a
unitBag (Id -> PmAltCon -> [Id] -> TmCt
TmVarCon Id
x (ConLike -> PmAltCon
PmAltConLike ConLike
cl) [Id]
arg_vars)
, ic_ty_cs :: Bag TyCt
ic_ty_cs = Bag TyCt
ty_cs
, ic_strict_arg_tys :: [Type]
ic_strict_arg_tys = [Type]
strict_arg_tys
}
inhabitationCandidates :: Delta -> Type
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
inhabitationCandidates :: Delta
-> Type -> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
inhabitationCandidates MkDelta{ delta_ty_st :: Delta -> TyState
delta_ty_st = TyState
ty_st } Type
ty = do
TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType TyState
ty_st Type
ty DsM TopNormaliseTypeResult
-> (TopNormaliseTypeResult
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate])))
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
NoChange Type
_ -> Type
-> Type
-> [(Type, DataCon, Type)]
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
alts_to_check Type
ty Type
ty []
NormalisedByConstraints Type
ty' -> Type
-> Type
-> [(Type, DataCon, Type)]
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
alts_to_check Type
ty' Type
ty' []
HadRedexes Type
src_ty [(Type, DataCon, Type)]
dcs Type
core_ty -> Type
-> Type
-> [(Type, DataCon, Type)]
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
alts_to_check Type
src_ty Type
core_ty [(Type, DataCon, Type)]
dcs
where
build_newtype :: (Type, DataCon, Type) -> Id -> DsM (Id, TmCt)
build_newtype :: (Type, DataCon, Type) -> Id -> DsM (Id, TmCt)
build_newtype (Type
ty, DataCon
dc, Type
_arg_ty) Id
x = do
Id
y <- Type -> DsM Id
mkPmId Type
ty
(Id, TmCt) -> DsM (Id, TmCt)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id
y, Id -> PmAltCon -> [Id] -> TmCt
TmVarCon Id
y (ConLike -> PmAltCon
PmAltConLike (DataCon -> ConLike
RealDataCon DataCon
dc)) [Id
x])
build_newtypes :: Id -> [(Type, DataCon, Type)] -> DsM (Id, [TmCt])
build_newtypes :: Id -> [(Type, DataCon, Type)] -> DsM (Id, [TmCt])
build_newtypes Id
x = ((Type, DataCon, Type) -> (Id, [TmCt]) -> DsM (Id, [TmCt]))
-> (Id, [TmCt]) -> [(Type, DataCon, Type)] -> DsM (Id, [TmCt])
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\(Type, DataCon, Type)
dc (Id
x, [TmCt]
cts) -> (Type, DataCon, Type) -> Id -> [TmCt] -> DsM (Id, [TmCt])
go (Type, DataCon, Type)
dc Id
x [TmCt]
cts) (Id
x, [])
where
go :: (Type, DataCon, Type) -> Id -> [TmCt] -> DsM (Id, [TmCt])
go (Type, DataCon, Type)
dc Id
x [TmCt]
cts = (TmCt -> [TmCt]) -> (Id, TmCt) -> (Id, [TmCt])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (TmCt -> [TmCt] -> [TmCt]
forall a. a -> [a] -> [a]
:[TmCt]
cts) ((Id, TmCt) -> (Id, [TmCt])) -> DsM (Id, TmCt) -> DsM (Id, [TmCt])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type, DataCon, Type) -> Id -> DsM (Id, TmCt)
build_newtype (Type, DataCon, Type)
dc Id
x
alts_to_check :: Type -> Type -> [(Type, DataCon, Type)]
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
alts_to_check :: Type
-> Type
-> [(Type, DataCon, Type)]
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
alts_to_check Type
src_ty Type
core_ty [(Type, DataCon, Type)]
dcs = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
core_ty of
Just (TyCon
tc, [Type]
_)
| TyCon -> Bool
isTyConTriviallyInhabited TyCon
tc
-> case [(Type, DataCon, Type)]
dcs of
[] -> Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Either Type (TyCon, Id, [InhabitationCandidate])
forall a b. a -> Either a b
Left Type
src_ty)
((Type, DataCon, Type)
_:[(Type, DataCon, Type)]
_) -> do Id
inner <- Type -> DsM Id
mkPmId Type
core_ty
(Id
outer, [TmCt]
new_tm_cts) <- Id -> [(Type, DataCon, Type)] -> DsM (Id, [TmCt])
build_newtypes Id
inner [(Type, DataCon, Type)]
dcs
Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate])))
-> Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall a b. (a -> b) -> a -> b
$ (TyCon, Id, [InhabitationCandidate])
-> Either Type (TyCon, Id, [InhabitationCandidate])
forall a b. b -> Either a b
Right (TyCon
tc, Id
outer, [InhabitationCandidate :: Bag TmCt -> Bag TyCt -> [Type] -> InhabitationCandidate
InhabitationCandidate
{ ic_tm_cs :: Bag TmCt
ic_tm_cs = [TmCt] -> Bag TmCt
forall a. [a] -> Bag a
listToBag [TmCt]
new_tm_cts
, ic_ty_cs :: Bag TyCt
ic_ty_cs = Bag TyCt
forall a. Bag a
emptyBag, ic_strict_arg_tys :: [Type]
ic_strict_arg_tys = [] }])
| Type -> Bool
pmIsClosedType Type
core_ty Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isAbstractTyCon TyCon
tc)
-> do
Id
inner <- Type -> DsM Id
mkPmId Type
core_ty
[InhabitationCandidate]
alts <- (DataCon -> DsM InhabitationCandidate)
-> [DataCon]
-> IOEnv (Env DsGblEnv DsLclEnv) [InhabitationCandidate]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Id -> DataCon -> DsM InhabitationCandidate
mkInhabitationCandidate Id
inner) (TyCon -> [DataCon]
tyConDataCons TyCon
tc)
(Id
outer, [TmCt]
new_tm_cts) <- Id -> [(Type, DataCon, Type)] -> DsM (Id, [TmCt])
build_newtypes Id
inner [(Type, DataCon, Type)]
dcs
let wrap_dcs :: InhabitationCandidate -> InhabitationCandidate
wrap_dcs InhabitationCandidate
alt = InhabitationCandidate
alt{ ic_tm_cs :: Bag TmCt
ic_tm_cs = [TmCt] -> Bag TmCt
forall a. [a] -> Bag a
listToBag [TmCt]
new_tm_cts Bag TmCt -> Bag TmCt -> Bag TmCt
forall a. Bag a -> Bag a -> Bag a
`unionBags` InhabitationCandidate -> Bag TmCt
ic_tm_cs InhabitationCandidate
alt}
Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate])))
-> Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall a b. (a -> b) -> a -> b
$ (TyCon, Id, [InhabitationCandidate])
-> Either Type (TyCon, Id, [InhabitationCandidate])
forall a b. b -> Either a b
Right (TyCon
tc, Id
outer, (InhabitationCandidate -> InhabitationCandidate)
-> [InhabitationCandidate] -> [InhabitationCandidate]
forall a b. (a -> b) -> [a] -> [b]
map InhabitationCandidate -> InhabitationCandidate
wrap_dcs [InhabitationCandidate]
alts)
Maybe (TyCon, [Type])
_other -> Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Either Type (TyCon, Id, [InhabitationCandidate])
forall a b. a -> Either a b
Left Type
src_ty)
triviallyInhabitedTyCons :: UniqSet TyCon
triviallyInhabitedTyCons :: UniqSet TyCon
triviallyInhabitedTyCons = [TyCon] -> UniqSet TyCon
forall a. Uniquable a => [a] -> UniqSet a
mkUniqSet [
TyCon
charTyCon, TyCon
doubleTyCon, TyCon
floatTyCon, TyCon
intTyCon, TyCon
wordTyCon, TyCon
word8TyCon
]
isTyConTriviallyInhabited :: TyCon -> Bool
isTyConTriviallyInhabited :: TyCon -> Bool
isTyConTriviallyInhabited TyCon
tc = TyCon -> UniqSet TyCon -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
elementOfUniqSet TyCon
tc UniqSet TyCon
triviallyInhabitedTyCons
tysAreNonVoid :: RecTcChecker -> [Type] -> SatisfiabilityCheck
tysAreNonVoid :: RecTcChecker -> [Type] -> SatisfiabilityCheck
tysAreNonVoid RecTcChecker
rec_env [Type]
strict_arg_tys = (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
SC ((Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck)
-> (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
forall a b. (a -> b) -> a -> b
$ \Delta
delta -> do
Bool
all_non_void <- RecTcChecker
-> Delta -> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) Bool
checkAllNonVoid RecTcChecker
rec_env Delta
delta [Type]
strict_arg_tys
Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Delta -> DsM (Maybe Delta))
-> Maybe Delta -> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ if Bool
all_non_void
then Delta -> Maybe Delta
forall a. a -> Maybe a
Just Delta
delta
else Maybe Delta
forall a. Maybe a
Nothing
checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> DsM Bool
checkAllNonVoid :: RecTcChecker
-> Delta -> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) Bool
checkAllNonVoid RecTcChecker
rec_ts Delta
amb_cs [Type]
strict_arg_tys = do
let definitely_inhabited :: Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
definitely_inhabited = TyState -> Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
definitelyInhabitedType (Delta -> TyState
delta_ty_st Delta
amb_cs)
[Type]
tys_to_check <- (Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) [Type]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterOutM Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
definitely_inhabited [Type]
strict_arg_tys
let rec_max_bound :: Int
rec_max_bound | [Type]
tys_to_check [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` Int
1
= Int
1
| Bool
otherwise
= Int
defaultRecTcMaxBound
rec_ts' :: RecTcChecker
rec_ts' = Int -> RecTcChecker -> RecTcChecker
setRecTcMaxBound Int
rec_max_bound RecTcChecker
rec_ts
(Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
allM (RecTcChecker -> Delta -> Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
nonVoid RecTcChecker
rec_ts' Delta
amb_cs) [Type]
tys_to_check
nonVoid
:: RecTcChecker
-> Delta
-> Type
-> DsM Bool
nonVoid :: RecTcChecker -> Delta -> Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
nonVoid RecTcChecker
rec_ts Delta
amb_cs Type
strict_arg_ty = do
Either Type (TyCon, Id, [InhabitationCandidate])
mb_cands <- Delta
-> Type -> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
inhabitationCandidates Delta
amb_cs Type
strict_arg_ty
case Either Type (TyCon, Id, [InhabitationCandidate])
mb_cands of
Right (TyCon
tc, Id
_, [InhabitationCandidate]
cands)
| Just RecTcChecker
rec_ts' <- RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_ts TyCon
tc
-> (InhabitationCandidate -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> [InhabitationCandidate] -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
anyM (RecTcChecker
-> Delta
-> InhabitationCandidate
-> IOEnv (Env DsGblEnv DsLclEnv) Bool
cand_is_inhabitable RecTcChecker
rec_ts' Delta
amb_cs) [InhabitationCandidate]
cands
Either Type (TyCon, Id, [InhabitationCandidate])
_ -> Bool -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
where
cand_is_inhabitable :: RecTcChecker -> Delta
-> InhabitationCandidate -> DsM Bool
cand_is_inhabitable :: RecTcChecker
-> Delta
-> InhabitationCandidate
-> IOEnv (Env DsGblEnv DsLclEnv) Bool
cand_is_inhabitable RecTcChecker
rec_ts Delta
amb_cs
(InhabitationCandidate{ ic_tm_cs :: InhabitationCandidate -> Bag TmCt
ic_tm_cs = Bag TmCt
new_tm_cs
, ic_ty_cs :: InhabitationCandidate -> Bag TyCt
ic_ty_cs = Bag TyCt
new_ty_cs
, ic_strict_arg_tys :: InhabitationCandidate -> [Type]
ic_strict_arg_tys = [Type]
new_strict_arg_tys }) =
(Maybe Delta -> Bool)
-> DsM (Maybe Delta) -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe Delta -> Bool
forall a. Maybe a -> Bool
isJust (DsM (Maybe Delta) -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> DsM (Maybe Delta) -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall a b. (a -> b) -> a -> b
$ Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck Delta
amb_cs (SatisfiabilityCheck -> DsM (Maybe Delta))
-> SatisfiabilityCheck -> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ [SatisfiabilityCheck] -> SatisfiabilityCheck
forall a. Monoid a => [a] -> a
mconcat
[ Bool -> Bag TyCt -> SatisfiabilityCheck
tyIsSatisfiable Bool
False Bag TyCt
new_ty_cs
, Bag TmCt -> SatisfiabilityCheck
tmIsSatisfiable Bag TmCt
new_tm_cs
, RecTcChecker -> [Type] -> SatisfiabilityCheck
tysAreNonVoid RecTcChecker
rec_ts [Type]
new_strict_arg_tys
]
definitelyInhabitedType :: TyState -> Type -> DsM Bool
definitelyInhabitedType :: TyState -> Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
definitelyInhabitedType TyState
ty_st Type
ty = do
TopNormaliseTypeResult
res <- TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType TyState
ty_st Type
ty
Bool -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> Bool -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall a b. (a -> b) -> a -> b
$ case TopNormaliseTypeResult
res of
HadRedexes Type
_ [(Type, DataCon, Type)]
cons Type
_ -> ((Type, DataCon, Type) -> Bool) -> [(Type, DataCon, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Type, DataCon, Type) -> Bool
meets_criteria [(Type, DataCon, Type)]
cons
TopNormaliseTypeResult
_ -> Bool
False
where
meets_criteria :: (Type, DataCon, Type) -> Bool
meets_criteria :: (Type, DataCon, Type) -> Bool
meets_criteria (Type
_, DataCon
con, Type
_) =
[EqSpec] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> [EqSpec]
dataConEqSpec DataCon
con) Bool -> Bool -> Bool
&&
[HsImplBang] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> [HsImplBang]
dataConImplBangs DataCon
con)
provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta]
provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta]
provideEvidence = [Id] -> Int -> Delta -> DsM [Delta]
go
where
go :: [Id] -> Int -> Delta -> DsM [Delta]
go [Id]
_ Int
0 Delta
_ = [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
go [] Int
_ Delta
delta = [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Delta
delta]
go (Id
x:[Id]
xs) Int
n Delta
delta = do
String -> SDoc -> DsM ()
tracePm String
"provideEvidence" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
$$ [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
xs SDoc -> SDoc -> SDoc
$$ Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta SDoc -> SDoc -> SDoc
$$ Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n)
VI Type
_ [(PmAltCon, [Id])]
pos [PmAltCon]
neg PossibleMatches
_ <- Delta -> Id -> DsM VarInfo
initLookupVarInfo Delta
delta Id
x
case [(PmAltCon, [Id])]
pos of
(PmAltCon, [Id])
_:[(PmAltCon, [Id])]
_ -> do
let arg_vas :: [Id]
arg_vas = ((PmAltCon, [Id]) -> [Id]) -> [(PmAltCon, [Id])] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(PmAltCon
_cl, [Id]
args) -> [Id]
args) [(PmAltCon, [Id])]
pos
[Id] -> Int -> Delta -> DsM [Delta]
go ([Id]
arg_vas [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id]
xs) Int
n Delta
delta
[]
| [PmLit] -> Bool
forall a. [a] -> Bool
notNull [ PmLit
l | PmAltLit PmLit
l <- [PmAltCon]
neg ]
-> [Id] -> Int -> Delta -> DsM [Delta]
go [Id]
xs Int
n Delta
delta
[] -> Id -> [Id] -> Int -> Delta -> DsM [Delta]
try_instantiate Id
x [Id]
xs Int
n Delta
delta
try_instantiate :: Id -> [Id] -> Int -> Delta -> DsM [Delta]
try_instantiate :: Id -> [Id] -> Int -> Delta -> DsM [Delta]
try_instantiate Id
x [Id]
xs Int
n Delta
delta = do
(Type
_src_ty, [(Type, DataCon, Type)]
dcs, Type
core_ty) <- TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts (TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type))
-> DsM TopNormaliseTypeResult
-> IOEnv
(Env DsGblEnv DsLclEnv) (Type, [(Type, DataCon, Type)], Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType (Delta -> TyState
delta_ty_st Delta
delta) (Id -> Type
idType Id
x)
let build_newtype :: (Id, Delta)
-> (a, DataCon, Type)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta)
build_newtype (Id
x, Delta
delta) (a
_ty, DataCon
dc, Type
arg_ty) = do
Id
y <- DsM Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (DsM Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id)
-> DsM Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
forall a b. (a -> b) -> a -> b
$ Type -> DsM Id
mkPmId Type
arg_ty
Delta
delta' <- Delta
-> Id
-> PmAltCon
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarConCt Delta
delta Id
x (ConLike -> PmAltCon
PmAltConLike (DataCon -> ConLike
RealDataCon DataCon
dc)) [Id
y]
(Id, Delta) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id
y, Delta
delta')
MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe (Id, Delta))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (((Id, Delta)
-> (Type, DataCon, Type)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta))
-> (Id, Delta)
-> [(Type, DataCon, Type)]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (Id, Delta)
-> (Type, DataCon, Type)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta)
forall a.
(Id, Delta)
-> (a, DataCon, Type)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta)
build_newtype (Id
x, Delta
delta) [(Type, DataCon, Type)]
dcs) IOEnv (Env DsGblEnv DsLclEnv) (Maybe (Id, Delta))
-> (Maybe (Id, Delta) -> DsM [Delta]) -> DsM [Delta]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe (Id, Delta)
Nothing -> [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Just (Id
y, Delta
newty_delta) -> do
PossibleMatches
pm <- VarInfo -> PossibleMatches
vi_cache (VarInfo -> PossibleMatches)
-> DsM VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) PossibleMatches
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delta -> Id -> DsM VarInfo
initLookupVarInfo Delta
newty_delta Id
y
Maybe ConLikeSet
mb_cls <- Delta -> PossibleMatches -> DsM (Maybe ConLikeSet)
pickMinimalCompleteSet Delta
newty_delta PossibleMatches
pm
case ConLikeSet -> [ConLike]
forall a. UniqDSet a -> [a]
uniqDSetToList (ConLikeSet -> [ConLike]) -> Maybe ConLikeSet -> Maybe [ConLike]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ConLikeSet
mb_cls of
Just cls :: [ConLike]
cls@(ConLike
_:[ConLike]
_) -> Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta]
instantiate_cons Id
y Type
core_ty [Id]
xs Int
n Delta
newty_delta [ConLike]
cls
Just [] | Bool -> Bool
not (Delta -> Id -> Bool
canDiverge Delta
newty_delta Id
y) -> [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Maybe [ConLike]
_ -> [Id] -> Int -> Delta -> DsM [Delta]
go [Id]
xs Int
n Delta
newty_delta
instantiate_cons :: Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta]
instantiate_cons :: Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta]
instantiate_cons Id
_ Type
_ [Id]
_ Int
_ Delta
_ [] = [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
instantiate_cons Id
_ Type
_ [Id]
_ Int
0 Delta
_ [ConLike]
_ = [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
instantiate_cons Id
_ Type
ty [Id]
xs Int
n Delta
delta [ConLike]
_
| ((TyCon, [Type]) -> Bool) -> Maybe (TyCon, [Type]) -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TyCon -> Bool
isTyConTriviallyInhabited (TyCon -> Bool)
-> ((TyCon, [Type]) -> TyCon) -> (TyCon, [Type]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon, [Type]) -> TyCon
forall a b. (a, b) -> a
fst) (HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty) Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
= [Id] -> Int -> Delta -> DsM [Delta]
go [Id]
xs Int
n Delta
delta
instantiate_cons Id
x Type
ty [Id]
xs Int
n Delta
delta (ConLike
cl:[ConLike]
cls) = do
FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
case FamInstEnvs -> Type -> ConLike -> Maybe [Type]
guessConLikeUnivTyArgsFromResTy FamInstEnvs
env Type
ty ConLike
cl of
Maybe [Type]
Nothing -> [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Delta
delta]
Just [Type]
arg_tys -> do
([Id]
arg_vars, Bag TyCt
new_ty_cs, [Type]
strict_arg_tys) <- [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type])
mkOneConFull [Type]
arg_tys ConLike
cl
let new_tm_cs :: Bag TmCt
new_tm_cs = TmCt -> Bag TmCt
forall a. a -> Bag a
unitBag (Id -> PmAltCon -> [Id] -> TmCt
TmVarCon Id
x (ConLike -> PmAltCon
PmAltConLike ConLike
cl) [Id]
arg_vars)
Maybe Delta
mb_delta <- Delta -> Bag TmCt -> Bag TyCt -> [Type] -> DsM (Maybe Delta)
pmIsSatisfiable Delta
delta Bag TmCt
new_tm_cs Bag TyCt
new_ty_cs [Type]
strict_arg_tys
String -> SDoc -> DsM ()
tracePm String
"instantiate_cons" ([SDoc] -> SDoc
vcat [ Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id -> Type
idType Id
x)
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
, ConLike -> SDoc
forall a. Outputable a => a -> SDoc
ppr ConLike
cl
, [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
arg_tys
, Bag TmCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag TmCt
new_tm_cs
, Bag TyCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag TyCt
new_ty_cs
, [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
strict_arg_tys
, Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta
, Maybe Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe Delta
mb_delta
, Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n ])
[Delta]
con_deltas <- case Maybe Delta
mb_delta of
Maybe Delta
Nothing -> [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
Just Delta
delta' -> [Id] -> Int -> Delta -> DsM [Delta]
go [Id]
xs Int
n Delta
delta'
[Delta]
other_cons_deltas <- Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta]
instantiate_cons Id
x Type
ty [Id]
xs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Delta] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Delta]
con_deltas) Delta
delta [ConLike]
cls
[Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Delta]
con_deltas [Delta] -> [Delta] -> [Delta]
forall a. [a] -> [a] -> [a]
++ [Delta]
other_cons_deltas)
pickMinimalCompleteSet :: Delta -> PossibleMatches -> DsM (Maybe ConLikeSet)
pickMinimalCompleteSet :: Delta -> PossibleMatches -> DsM (Maybe ConLikeSet)
pickMinimalCompleteSet Delta
_ PossibleMatches
NoPM = Maybe ConLikeSet -> DsM (Maybe ConLikeSet)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ConLikeSet
forall a. Maybe a
Nothing
pickMinimalCompleteSet Delta
_ (PM NonEmpty ConLikeSet
clss) = do
String -> SDoc -> DsM ()
tracePm String
"pickMinimalCompleteSet" ([ConLikeSet] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([ConLikeSet] -> SDoc) -> [ConLikeSet] -> SDoc
forall a b. (a -> b) -> a -> b
$ NonEmpty ConLikeSet -> [ConLikeSet]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty ConLikeSet
clss)
Maybe ConLikeSet -> DsM (Maybe ConLikeSet)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ConLikeSet -> Maybe ConLikeSet
forall a. a -> Maybe a
Just ((ConLikeSet -> ConLikeSet -> Ordering)
-> NonEmpty ConLikeSet -> ConLikeSet
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy ((ConLikeSet -> Int) -> ConLikeSet -> ConLikeSet -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ConLikeSet -> Int
forall a. UniqDSet a -> Int
sizeUniqDSet) NonEmpty ConLikeSet
clss))
representCoreExpr :: Delta -> CoreExpr -> DsM (Delta, Id)
representCoreExpr :: Delta -> CoreExpr -> DsM (Delta, Id)
representCoreExpr delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = ts :: TmState
ts@TmSt{ ts_reps :: TmState -> CoreMap Id
ts_reps = CoreMap Id
reps } } CoreExpr
e = do
DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
let e' :: CoreExpr
e' = DynFlags -> CoreExpr -> CoreExpr
simpleOptExpr DynFlags
dflags CoreExpr
e
case CoreMap Id -> CoreExpr -> Maybe Id
forall a. CoreMap a -> CoreExpr -> Maybe a
lookupCoreMap CoreMap Id
reps CoreExpr
e' of
Just Id
rep -> (Delta, Id) -> DsM (Delta, Id)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta
delta, Id
rep)
Maybe Id
Nothing -> do
Id
rep <- Type -> DsM Id
mkPmId (CoreExpr -> Type
exprType CoreExpr
e')
let reps' :: CoreMap Id
reps' = CoreMap Id -> CoreExpr -> Id -> CoreMap Id
forall a. CoreMap a -> CoreExpr -> a -> CoreMap a
extendCoreMap CoreMap Id
reps CoreExpr
e' Id
rep
let delta' :: Delta
delta' = Delta
delta{ delta_tm_st :: TmState
delta_tm_st = TmState
ts{ ts_reps :: CoreMap Id
ts_reps = CoreMap Id
reps' } }
(Delta, Id) -> DsM (Delta, Id)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta
delta', Id
rep)
addVarCoreCt :: Delta -> Id -> CoreExpr -> DsM (Maybe Delta)
addVarCoreCt :: Delta -> Id -> CoreExpr -> DsM (Maybe Delta)
addVarCoreCt Delta
delta Id
x CoreExpr
e = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta -> DsM (Maybe Delta)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
-> Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Id
-> CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x CoreExpr
e) Delta
delta)
where
core_expr :: Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
core_expr :: Id
-> CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x (Cast CoreExpr
e Coercion
_co) = Id
-> CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x CoreExpr
e
core_expr Id
x (Tick Tickish Id
_t CoreExpr
e) = Id
-> CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x CoreExpr
e
core_expr Id
x CoreExpr
e
| Just (PmLit -> Maybe FastString
pmLitAsStringLit -> Just FastString
s) <- CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
e
, Type
expr_ty Type -> Type -> Bool
`eqType` Type
stringTy
= case FastString -> String
unpackFS FastString
s of
[] -> Id
-> DataCon
-> [Id]
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
data_con_app Id
x DataCon
nilDataCon []
String
s' -> Id
-> CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x (Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
charTy ((Char -> CoreExpr) -> String -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map Char -> CoreExpr
mkCharExpr String
s'))
| Just PmLit
lit <- CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
e
= Id
-> PmLit
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_lit Id
x PmLit
lit
| Just (InScopeSet
_in_scope, _empty_floats :: [FloatBind]
_empty_floats@[], DataCon
dc, [Type]
_arg_tys, [CoreExpr]
args)
<- InScopeEnv
-> CoreExpr
-> Maybe (InScopeSet, [FloatBind], DataCon, [Type], [CoreExpr])
exprIsConApp_maybe InScopeEnv
forall b. (InScopeSet, b -> Unfolding)
in_scope_env CoreExpr
e
= do { [Id]
arg_ids <- (CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id)
-> [CoreExpr]
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) [Id]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
bind_expr [CoreExpr]
args
; Id
-> DataCon
-> [Id]
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
data_con_app Id
x DataCon
dc [Id]
arg_ids }
| Var Id
y <- CoreExpr
e, Maybe DataCon
Nothing <- Id -> Maybe DataCon
isDataConId_maybe Id
x
= (Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT (\Delta
delta -> Delta -> (Id, Id) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarVarCt Delta
delta (Id
x, Id
y))
| Bool
otherwise
= do { Id
rep <- CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
represent_expr CoreExpr
e
; (Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT (\Delta
delta -> Delta -> (Id, Id) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarVarCt Delta
delta (Id
x, Id
rep)) }
where
expr_ty :: Type
expr_ty = CoreExpr -> Type
exprType CoreExpr
e
expr_in_scope :: InScopeSet
expr_in_scope = VarSet -> InScopeSet
mkInScopeSet (CoreExpr -> VarSet
exprFreeVars CoreExpr
e)
in_scope_env :: (InScopeSet, b -> Unfolding)
in_scope_env = (InScopeSet
expr_in_scope, Unfolding -> b -> Unfolding
forall a b. a -> b -> a
const Unfolding
NoUnfolding)
bind_expr :: CoreExpr -> StateT Delta (MaybeT DsM) Id
bind_expr :: CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
bind_expr CoreExpr
e = do
Id
x <- MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (DsM Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Type -> DsM Id
mkPmId (CoreExpr -> Type
exprType CoreExpr
e)))
Id
-> CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x CoreExpr
e
Id -> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
forall (f :: * -> *) a. Applicative f => a -> f a
pure Id
x
represent_expr :: CoreExpr -> StateT Delta (MaybeT DsM) Id
represent_expr :: CoreExpr
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
represent_expr CoreExpr
e = (Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta))
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta))
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id)
-> (Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta))
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
forall a b. (a -> b) -> a -> b
$ \Delta
delta ->
(Delta, Id) -> (Id, Delta)
forall a b. (a, b) -> (b, a)
swap ((Delta, Id) -> (Id, Delta))
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Delta, Id)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Delta)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DsM (Delta, Id)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Delta, Id)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Delta -> CoreExpr -> DsM (Delta, Id)
representCoreExpr Delta
delta CoreExpr
e)
data_con_app :: Id -> DataCon -> [Id] -> StateT Delta (MaybeT DsM) ()
data_con_app :: Id
-> DataCon
-> [Id]
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
data_con_app Id
x DataCon
dc [Id]
args = Id
-> PmAltCon
-> [Id]
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_alt_con_app Id
x (ConLike -> PmAltCon
PmAltConLike (DataCon -> ConLike
RealDataCon DataCon
dc)) [Id]
args
pm_lit :: Id -> PmLit -> StateT Delta (MaybeT DsM) ()
pm_lit :: Id
-> PmLit
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_lit Id
x PmLit
lit = Id
-> PmAltCon
-> [Id]
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_alt_con_app Id
x (PmLit -> PmAltCon
PmAltLit PmLit
lit) []
pm_alt_con_app :: Id -> PmAltCon -> [Id] -> StateT Delta (MaybeT DsM) ()
pm_alt_con_app :: Id
-> PmAltCon
-> [Id]
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_alt_con_app Id
x PmAltCon
con [Id]
args = (Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT ((Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ())
-> (Delta -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta)
-> StateT Delta (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
forall a b. (a -> b) -> a -> b
$ \Delta
delta -> Delta
-> Id
-> PmAltCon
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Delta
addVarConCt Delta
delta Id
x PmAltCon
con [Id]
args
modifyT :: Monad m => (s -> m s) -> StateT s m ()
modifyT :: (s -> m s) -> StateT s m ()
modifyT s -> m s
f = (s -> m ((), s)) -> StateT s m ()
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((s -> m ((), s)) -> StateT s m ())
-> (s -> m ((), s)) -> StateT s m ()
forall a b. (a -> b) -> a -> b
$ (s -> ((), s)) -> m s -> m ((), s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) ()) (m s -> m ((), s)) -> (s -> m s) -> s -> m ((), s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> m s
f