{-# LANGUAGE CPP #-}
{-# LANGUAGE ViewPatterns #-}
module Wingman.Judgements.Theta
( Evidence
, getEvidenceAtHole
, mkEvidence
, evidenceToSubst
, evidenceToHypothesis
, evidenceToThetaType
) where
import Class (classTyVars)
import Control.Applicative (empty)
import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
import Data.Set (Set)
import qualified Data.Set as S
import Development.IDE.Core.UseStale
import Development.IDE.GHC.Compat
import Generics.SYB hiding (tyConName, empty)
import GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst)
#if __GLASGOW_HASKELL__ > 806
import GhcPlugins (eqTyCon)
#else
import GhcPlugins (nameRdrName, tyConName)
import PrelNames (eqTyCon_RDR)
#endif
import TcEvidence
import TcType (substTy)
import TcType (tcTyConAppTyCon_maybe)
import TysPrim (eqPrimTyCon)
import Wingman.Machinery
import Wingman.Types
data Evidence
= EqualityOfTypes Type Type
| HasInstance PredType
deriving (Int -> Evidence -> ShowS
[Evidence] -> ShowS
Evidence -> String
(Int -> Evidence -> ShowS)
-> (Evidence -> String) -> ([Evidence] -> ShowS) -> Show Evidence
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Evidence] -> ShowS
$cshowList :: [Evidence] -> ShowS
show :: Evidence -> String
$cshow :: Evidence -> String
showsPrec :: Int -> Evidence -> ShowS
$cshowsPrec :: Int -> Evidence -> ShowS
Show)
mkEvidence :: PredType -> [Evidence]
mkEvidence :: PredType -> [Evidence]
mkEvidence (PredType -> Maybe (PredType, PredType)
getEqualityTheta -> Just (PredType
a, PredType
b))
= Evidence -> [Evidence]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Evidence -> [Evidence]) -> Evidence -> [Evidence]
forall a b. (a -> b) -> a -> b
$ PredType -> PredType -> Evidence
EqualityOfTypes PredType
a PredType
b
mkEvidence inst :: PredType
inst@(PredType -> Maybe TyCon
tcTyConAppTyCon_maybe -> Just (TyCon -> Maybe Class
tyConClass_maybe -> Just Class
cls)) = do
(TyCon
_, [PredType]
apps) <- Maybe (TyCon, [PredType]) -> [(TyCon, [PredType])]
forall a. Maybe a -> [a]
maybeToList (Maybe (TyCon, [PredType]) -> [(TyCon, [PredType])])
-> Maybe (TyCon, [PredType]) -> [(TyCon, [PredType])]
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe PredType
inst
let tvs :: [TyVar]
tvs = Class -> [TyVar]
classTyVars Class
cls
subst :: TCvSubst
subst = [TyVar] -> [PredType] -> TCvSubst
HasDebugCallStack => [TyVar] -> [PredType] -> TCvSubst
zipTvSubst [TyVar]
tvs [PredType]
apps
[Evidence]
sc_ev <- (PredType -> [Evidence]) -> [PredType] -> [[Evidence]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (PredType -> [Evidence]
mkEvidence (PredType -> [Evidence])
-> (PredType -> PredType) -> PredType -> [Evidence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => TCvSubst -> PredType -> PredType
TCvSubst -> PredType -> PredType
substTy TCvSubst
subst) ([PredType] -> [[Evidence]]) -> [PredType] -> [[Evidence]]
forall a b. (a -> b) -> a -> b
$ Class -> [PredType]
classSCTheta Class
cls
PredType -> Evidence
HasInstance PredType
inst Evidence -> [Evidence] -> [Evidence]
forall a. a -> [a] -> [a]
: [Evidence]
sc_ev
mkEvidence PredType
_ = [Evidence]
forall (f :: * -> *) a. Alternative f => f a
empty
evidenceToThetaType :: [Evidence] -> Set CType
evidenceToThetaType :: [Evidence] -> Set CType
evidenceToThetaType [Evidence]
evs = [CType] -> Set CType
forall a. Ord a => [a] -> Set a
S.fromList ([CType] -> Set CType) -> [CType] -> Set CType
forall a b. (a -> b) -> a -> b
$ do
HasInstance PredType
t <- [Evidence]
evs
CType -> [CType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CType -> [CType]) -> CType -> [CType]
forall a b. (a -> b) -> a -> b
$ PredType -> CType
CType PredType
t
getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]
getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]
getEvidenceAtHole (Tracked age SrcSpan -> SrcSpan
forall (age :: Age) a. Tracked age a -> a
unTrack -> SrcSpan
dst)
= (PredType -> [Evidence]) -> [PredType] -> [Evidence]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PredType -> [Evidence]
mkEvidence
([PredType] -> [Evidence])
-> (Tracked age (LHsBinds GhcTc) -> [PredType])
-> Tracked age (LHsBinds GhcTc)
-> [Evidence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([PredType] -> [PredType] -> [PredType])
-> GenericQ [PredType] -> GenericQ [PredType]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything [PredType] -> [PredType] -> [PredType]
forall a. Semigroup a => a -> a -> a
(<>) (GenericQ [PredType] -> GenericQ [PredType])
-> GenericQ [PredType] -> GenericQ [PredType]
forall a b. (a -> b) -> a -> b
$
[PredType]
-> (LHsBindLR GhcTc GhcTc -> [PredType]) -> a -> [PredType]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ [PredType]
forall a. Monoid a => a
mempty (SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
absBinds SrcSpan
dst) (a -> [PredType])
-> (LHsExpr GhcTc -> [PredType]) -> a -> [PredType]
forall a b q.
(Typeable a, Typeable b) =>
(a -> q) -> (b -> q) -> a -> q
`extQ` SrcSpan -> LHsExpr GhcTc -> [PredType]
wrapperBinds SrcSpan
dst (a -> [PredType])
-> (LMatch GhcTc (LHsExpr GhcTc) -> [PredType]) -> a -> [PredType]
forall a b q.
(Typeable a, Typeable b) =>
(a -> q) -> (b -> q) -> a -> q
`extQ` SrcSpan -> LMatch GhcTc (LHsExpr GhcTc) -> [PredType]
matchBinds SrcSpan
dst)
(LHsBinds GhcTc -> [PredType])
-> (Tracked age (LHsBinds GhcTc) -> LHsBinds GhcTc)
-> Tracked age (LHsBinds GhcTc)
-> [PredType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tracked age (LHsBinds GhcTc) -> LHsBinds GhcTc
forall (age :: Age) a. Tracked age a -> a
unTrack
evidenceToSubst :: Evidence -> TacticState -> TacticState
evidenceToSubst :: Evidence -> TacticState -> TacticState
evidenceToSubst (EqualityOfTypes PredType
a PredType
b) TacticState
ts =
let tyvars :: Set TyVar
tyvars = [TyVar] -> Set TyVar
forall a. Ord a => [a] -> Set a
S.fromList ([TyVar] -> Set TyVar) -> [TyVar] -> Set TyVar
forall a b. (a -> b) -> a -> b
$ (PredType -> Maybe TyVar) -> [PredType] -> [TyVar]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe PredType -> Maybe TyVar
getTyVar_maybe [PredType
a, PredType
b]
skolems :: Set TyVar
skolems = TacticState -> Set TyVar
ts_skolems TacticState
ts Set TyVar -> Set TyVar -> Set TyVar
forall a. Ord a => Set a -> Set a -> Set a
S.\\ Set TyVar
tyvars
in
case Set TyVar -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems Set TyVar
skolems (PredType -> CType
CType PredType
a) (PredType -> CType
CType PredType
b) of
Just TCvSubst
subst -> TCvSubst -> TacticState -> TacticState
updateSubst TCvSubst
subst TacticState
ts
Maybe TCvSubst
Nothing -> TacticState
ts
evidenceToSubst HasInstance{} TacticState
ts = TacticState
ts
evidenceToHypothesis :: Evidence -> Hypothesis CType
evidenceToHypothesis :: Evidence -> Hypothesis CType
evidenceToHypothesis EqualityOfTypes{} = Hypothesis CType
forall a. Monoid a => a
mempty
evidenceToHypothesis (HasInstance PredType
t) =
[HyInfo CType] -> Hypothesis CType
forall a. [HyInfo a] -> Hypothesis a
Hypothesis ([HyInfo CType] -> Hypothesis CType)
-> (Maybe [HyInfo CType] -> [HyInfo CType])
-> Maybe [HyInfo CType]
-> Hypothesis CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HyInfo CType] -> [HyInfo CType]
forall a. [HyInfo a] -> [HyInfo a]
excludeForbiddenMethods ([HyInfo CType] -> [HyInfo CType])
-> (Maybe [HyInfo CType] -> [HyInfo CType])
-> Maybe [HyInfo CType]
-> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HyInfo CType] -> Maybe [HyInfo CType] -> [HyInfo CType]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [HyInfo CType] -> Hypothesis CType)
-> Maybe [HyInfo CType] -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ PredType -> Maybe [HyInfo CType]
methodHypothesis PredType
t
getEqualityTheta :: PredType -> Maybe (Type, Type)
getEqualityTheta :: PredType -> Maybe (PredType, PredType)
getEqualityTheta (HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe -> Just (TyCon
tc, [PredType
_k, PredType
a, PredType
b]))
#if __GLASGOW_HASKELL__ > 806
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
eqTyCon
#else
| nameRdrName (tyConName tc) == eqTyCon_RDR
#endif
= (PredType, PredType) -> Maybe (PredType, PredType)
forall a. a -> Maybe a
Just (PredType
a, PredType
b)
getEqualityTheta (HasDebugCallStack => PredType -> Maybe (TyCon, [PredType])
PredType -> Maybe (TyCon, [PredType])
splitTyConApp_maybe -> Just (TyCon
tc, [PredType
_k1, PredType
_k2, PredType
a, PredType
b]))
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
eqPrimTyCon = (PredType, PredType) -> Maybe (PredType, PredType)
forall a. a -> Maybe a
Just (PredType
a, PredType
b)
getEqualityTheta PredType
_ = Maybe (PredType, PredType)
forall a. Maybe a
Nothing
excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
excludeForbiddenMethods = (HyInfo a -> Bool) -> [HyInfo a] -> [HyInfo a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (HyInfo a -> Bool) -> HyInfo a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OccName -> Set OccName -> Bool) -> Set OccName -> OccName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip OccName -> Set OccName -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Set OccName
forbiddenMethods (OccName -> Bool) -> (HyInfo a -> OccName) -> HyInfo a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo a -> OccName
forall a. HyInfo a -> OccName
hi_name)
where
forbiddenMethods :: Set OccName
forbiddenMethods :: Set OccName
forbiddenMethods = (String -> OccName) -> Set String -> Set OccName
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map String -> OccName
mkVarOcc (Set String -> Set OccName) -> Set String -> Set OccName
forall a b. (a -> b) -> a -> b
$ [String] -> Set String
forall a. Ord a => [a] -> Set a
S.fromList
[
String
"fail"
, String
"showsPrec", String
"showList"
, String
"<$"
, String
"liftA2", String
"<*", String
"*>"
, String
"return", String
">>"
, String
"some", String
"many"
, String
"foldr1", String
"foldl1", String
"elem", String
"maximum", String
"minimum", String
"sum", String
"product"
, String
"sequenceA", String
"mapM", String
"sequence"
, String
"sconcat", String
"stimes"
, String
"mconcat"
]
absBinds :: SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
absBinds :: SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
absBinds SrcSpan
dst (L SrcSpan
src (AbsBinds XAbsBinds GhcTc GhcTc
_ [TyVar]
_ [TyVar]
h [ABExport GhcTc]
_ [TcEvBinds]
_ LHsBinds GhcTc
_ Bool
_))
| SrcSpan
dst SrcSpan -> SrcSpan -> Bool
`isSubspanOf` SrcSpan
src = (TyVar -> PredType) -> [TyVar] -> [PredType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyVar -> PredType
idType [TyVar]
h
absBinds SrcSpan
_ LHsBindLR GhcTc GhcTc
_ = []
wrapperBinds :: SrcSpan -> LHsExpr GhcTc -> [PredType]
wrapperBinds :: SrcSpan -> LHsExpr GhcTc -> [PredType]
wrapperBinds SrcSpan
dst (L SrcSpan
src (HsWrap XWrap GhcTc
_ HsWrapper
h HsExpr GhcTc
_))
| SrcSpan
dst SrcSpan -> SrcSpan -> Bool
`isSubspanOf` SrcSpan
src = HsWrapper -> [PredType]
wrapper HsWrapper
h
wrapperBinds SrcSpan
_ LHsExpr GhcTc
_ = []
matchBinds :: SrcSpan -> LMatch GhcTc (LHsExpr GhcTc) -> [PredType]
matchBinds :: SrcSpan -> LMatch GhcTc (LHsExpr GhcTc) -> [PredType]
matchBinds SrcSpan
dst (L SrcSpan
src (Match XCMatch GhcTc (LHsExpr GhcTc)
_ HsMatchContext (NameOrRdrName (IdP GhcTc))
_ [LPat GhcTc]
pats GRHSs GhcTc (LHsExpr GhcTc)
_))
| SrcSpan
dst SrcSpan -> SrcSpan -> Bool
`isSubspanOf` SrcSpan
src = ([PredType] -> [PredType] -> [PredType])
-> GenericQ [PredType] -> [Located (Pat GhcTc)] -> [PredType]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything [PredType] -> [PredType] -> [PredType]
forall a. Semigroup a => a -> a -> a
(<>) ([PredType] -> (Pat GhcTc -> [PredType]) -> a -> [PredType]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ [PredType]
forall a. Monoid a => a
mempty Pat GhcTc -> [PredType]
patBinds) [LPat GhcTc]
[Located (Pat GhcTc)]
pats
matchBinds SrcSpan
_ LMatch GhcTc (LHsExpr GhcTc)
_ = []
patBinds :: Pat GhcTc -> [PredType]
patBinds :: Pat GhcTc -> [PredType]
patBinds (ConPatOut { pat_dicts :: forall p. Pat p -> [TyVar]
pat_dicts = [TyVar]
dicts })
= (TyVar -> PredType) -> [TyVar] -> [PredType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyVar -> PredType
idType [TyVar]
dicts
patBinds Pat GhcTc
_ = []
wrapper :: HsWrapper -> [PredType]
wrapper :: HsWrapper -> [PredType]
wrapper (WpCompose HsWrapper
h HsWrapper
h2) = HsWrapper -> [PredType]
wrapper HsWrapper
h [PredType] -> [PredType] -> [PredType]
forall a. Semigroup a => a -> a -> a
<> HsWrapper -> [PredType]
wrapper HsWrapper
h2
wrapper (WpEvLam TyVar
v) = [TyVar -> PredType
idType TyVar
v]
wrapper HsWrapper
_ = []