{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
module Wingman.GHC where
import Bag (bagToList)
import Class (classTyVars)
import ConLike
import Control.Monad.State
import Control.Monad.Trans.Maybe (MaybeT(..))
import CoreUtils (exprType)
import Data.Bool (bool)
import Data.Function (on)
import Data.Functor ((<&>))
import Data.List (isPrefixOf)
import qualified Data.Map as M
import Data.Maybe (isJust)
import Data.Set (Set)
import qualified Data.Set as S
import Data.Traversable
import DataCon
import Development.IDE.GHC.Compat hiding (exprType)
import DsExpr (dsExpr)
import DsMonad (initDs)
import FamInst (tcLookupDataFamInst_maybe)
import FamInstEnv (normaliseType)
import GHC.SourceGen (lambda)
import Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
import GhcPlugins (Role (Nominal))
import OccName
import TcRnMonad
import TcType
import TyCoRep
import Type
import TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon)
import Unify
import Unique
import Var
import Wingman.StaticPlugin (pattern MetaprogramSyntax)
import Wingman.Types
tcTyVar_maybe :: Type -> Maybe Var
tcTyVar_maybe :: Type -> Maybe Var
tcTyVar_maybe Type
ty | Just Type
ty' <- Type -> Maybe Type
tcView Type
ty = Type -> Maybe Var
tcTyVar_maybe Type
ty'
tcTyVar_maybe (CastTy Type
ty KindCoercion
_) = Type -> Maybe Var
tcTyVar_maybe Type
ty
tcTyVar_maybe (TyVarTy Var
v) = Var -> Maybe Var
forall a. a -> Maybe a
Just Var
v
tcTyVar_maybe Type
_ = Maybe Var
forall a. Maybe a
Nothing
instantiateType :: Type -> ([TyVar], Type)
instantiateType :: Type -> ([Var], Type)
instantiateType Type
t = do
let vs :: [Var]
vs = Type -> [Var]
tyCoVarsOfTypeList Type
t
vs' :: [Var]
vs' = (Var -> Var) -> [Var] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Var -> Var
cloneTyVar [Var]
vs
subst :: TCvSubst
subst = ((Var, Var) -> TCvSubst -> TCvSubst)
-> TCvSubst -> [(Var, Var)] -> TCvSubst
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Var
v,Var
t) TCvSubst
a -> TCvSubst -> Var -> Type -> TCvSubst
extendTCvSubst TCvSubst
a Var
v (Type -> TCvSubst) -> Type -> TCvSubst
forall a b. (a -> b) -> a -> b
$ Var -> Type
TyVarTy Var
t) TCvSubst
emptyTCvSubst
([(Var, Var)] -> TCvSubst) -> [(Var, Var)] -> TCvSubst
forall a b. (a -> b) -> a -> b
$ [Var] -> [Var] -> [(Var, Var)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
vs [Var]
vs'
in ([Var]
vs', HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
t)
cloneTyVar :: TyVar -> TyVar
cloneTyVar :: Var -> Var
cloneTyVar Var
t =
let uniq :: Unique
uniq = Var -> Unique
forall a. Uniquable a => a -> Unique
getUnique Var
t
some_magic_number :: Int
some_magic_number = Int
49
in Var -> Unique -> Var
setVarUnique Var
t (Unique -> Var) -> Unique -> Var
forall a b. (a -> b) -> a -> b
$ Unique -> Int -> Unique
deriveUnique Unique
uniq Int
some_magic_number
isFunction :: Type -> Bool
isFunction :: Type -> Bool
isFunction (Type -> ([Var], ThetaType, ThetaType, Type)
tacticsSplitFunTy -> ([Var]
_, ThetaType
_, [], Type
_)) = Bool
False
isFunction Type
_ = Bool
True
tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type)
tacticsSplitFunTy :: Type -> ([Var], ThetaType, ThetaType, Type)
tacticsSplitFunTy Type
t
= let ([Var]
vars, ThetaType
theta, Type
t') = Type -> ([Var], ThetaType, Type)
tcSplitNestedSigmaTys Type
t
(ThetaType
args, Type
res) = Type -> (ThetaType, Type)
tcSplitFunTys Type
t'
in ([Var]
vars, ThetaType
theta, ThetaType
args, Type
res)
tacticsThetaTy :: Type -> ThetaType
tacticsThetaTy :: Type -> ThetaType
tacticsThetaTy (Type -> ([Var], ThetaType, Type)
tcSplitSigmaTy -> ([Var]
_, ThetaType
theta, Type
_)) = ThetaType
theta
tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
tacticsGetDataCons :: Type -> Maybe ([DataCon], ThetaType)
tacticsGetDataCons Type
ty
| Just (TyVarBinder
_, Type
ty') <- Type -> Maybe (TyVarBinder, Type)
tcSplitForAllTy_maybe Type
ty
= Type -> Maybe ([DataCon], ThetaType)
tacticsGetDataCons Type
ty'
tacticsGetDataCons Type
ty
| Just TyCon
_ <- Type -> Maybe TyCon
algebraicTyCon Type
ty
= HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty Maybe (TyCon, ThetaType)
-> ((TyCon, ThetaType) -> ([DataCon], ThetaType))
-> Maybe ([DataCon], ThetaType)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(TyCon
tc, ThetaType
apps) ->
( (DataCon -> Bool) -> [DataCon] -> [DataCon]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (DataCon -> Bool) -> DataCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThetaType -> DataCon -> Bool
dataConCannotMatch ThetaType
apps) ([DataCon] -> [DataCon]) -> [DataCon] -> [DataCon]
forall a b. (a -> b) -> a -> b
$ TyCon -> [DataCon]
tyConDataCons TyCon
tc
, ThetaType
apps
)
tacticsGetDataCons Type
_ = Maybe ([DataCon], ThetaType)
forall a. Maybe a
Nothing
freshTyvars :: MonadState TacticState m => Type -> m Type
freshTyvars :: Type -> m Type
freshTyvars Type
t = do
let ([Var]
tvs, ThetaType
_, ThetaType
_, Type
_) = Type -> ([Var], ThetaType, ThetaType, Type)
tacticsSplitFunTy Type
t
Map Var Var
reps <- ([(Var, Var)] -> Map Var Var) -> m [(Var, Var)] -> m (Map Var Var)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Var, Var)] -> Map Var Var
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
(m [(Var, Var)] -> m (Map Var Var))
-> m [(Var, Var)] -> m (Map Var Var)
forall a b. (a -> b) -> a -> b
$ [Var] -> (Var -> m (Var, Var)) -> m [(Var, Var)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Var]
tvs ((Var -> m (Var, Var)) -> m [(Var, Var)])
-> (Var -> m (Var, Var)) -> m [(Var, Var)]
forall a b. (a -> b) -> a -> b
$ \Var
tv -> do
Unique
uniq <- m Unique
forall (m :: * -> *). MonadState TacticState m => m Unique
freshUnique
(Var, Var) -> m (Var, Var)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Var
tv, Var -> Unique -> Var
setTyVarUnique Var
tv Unique
uniq)
Type -> m Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$
(forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere
((Var -> Var) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT ((Var -> Var) -> a -> a) -> (Var -> Var) -> a -> a
forall a b. (a -> b) -> a -> b
$ \Var
tv ->
case Var -> Map Var Var -> Maybe Var
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Var
tv Map Var Var
reps of
Just Var
tv' -> Var
tv'
Maybe Var
Nothing -> Var
tv
) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ ([Var], Type) -> Type
forall a b. (a, b) -> b
snd (([Var], Type) -> Type) -> ([Var], Type) -> Type
forall a b. (a -> b) -> a -> b
$ Type -> ([Var], Type)
tcSplitForAllTys Type
t
getRecordFields :: ConLike -> Maybe [(OccName, CType)]
getRecordFields :: ConLike -> Maybe [(OccName, CType)]
getRecordFields ConLike
dc =
case ConLike -> [FieldLabel]
conLikeFieldLabels ConLike
dc of
[] -> Maybe [(OccName, CType)]
forall a. Maybe a
Nothing
[FieldLabel]
lbls -> [FieldLabel]
-> (FieldLabel -> Maybe (OccName, CType))
-> Maybe [(OccName, CType)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [FieldLabel]
lbls ((FieldLabel -> Maybe (OccName, CType))
-> Maybe [(OccName, CType)])
-> (FieldLabel -> Maybe (OccName, CType))
-> Maybe [(OccName, CType)]
forall a b. (a -> b) -> a -> b
$ \FieldLabel
lbl -> do
let ty :: Type
ty = ConLike -> FieldLabelString -> Type
conLikeFieldType ConLike
dc (FieldLabelString -> Type) -> FieldLabelString -> Type
forall a b. (a -> b) -> a -> b
$ FieldLabel -> FieldLabelString
forall a. FieldLbl a -> FieldLabelString
flLabel FieldLabel
lbl
(OccName, CType) -> Maybe (OccName, CType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FieldLabelString -> OccName
mkVarOccFS (FieldLabelString -> OccName) -> FieldLabelString -> OccName
forall a b. (a -> b) -> a -> b
$ FieldLabel -> FieldLabelString
forall a. FieldLbl a -> FieldLabelString
flLabel FieldLabel
lbl, Type -> CType
CType Type
ty)
algebraicTyCon :: Type -> Maybe TyCon
algebraicTyCon :: Type -> Maybe TyCon
algebraicTyCon Type
ty
| Just (TyVarBinder
_, Type
ty') <- Type -> Maybe (TyVarBinder, Type)
tcSplitForAllTy_maybe Type
ty
= Type -> Maybe TyCon
algebraicTyCon Type
ty'
algebraicTyCon (HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe -> Just (TyCon
tycon, ThetaType
_))
| TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
intTyCon = Maybe TyCon
forall a. Maybe a
Nothing
| TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
floatTyCon = Maybe TyCon
forall a. Maybe a
Nothing
| TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
doubleTyCon = Maybe TyCon
forall a. Maybe a
Nothing
| TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
charTyCon = Maybe TyCon
forall a. Maybe a
Nothing
| TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
funTyCon = Maybe TyCon
forall a. Maybe a
Nothing
| Bool
otherwise = TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
tycon
algebraicTyCon Type
_ = Maybe TyCon
forall a. Maybe a
Nothing
eqRdrName :: RdrName -> RdrName -> Bool
eqRdrName :: RdrName -> RdrName -> Bool
eqRdrName = String -> String -> Bool
forall a. Eq a => a -> a -> Bool
(==) (String -> String -> Bool)
-> (RdrName -> String) -> RdrName -> RdrName -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` OccName -> String
occNameString (OccName -> String) -> (RdrName -> OccName) -> RdrName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RdrName -> OccName
forall name. HasOccName name => name -> OccName
occName
sloppyEqOccName :: OccName -> OccName -> Bool
sloppyEqOccName :: OccName -> OccName -> Bool
sloppyEqOccName = String -> String -> Bool
forall a. Eq a => a -> a -> Bool
(==) (String -> String -> Bool)
-> (OccName -> String) -> OccName -> OccName -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` OccName -> String
occNameString
containsHsVar :: Data a => RdrName -> a -> Bool
containsHsVar :: RdrName -> a -> Bool
containsHsVar RdrName
name a
x = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [HsExpr GhcPs] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([HsExpr GhcPs] -> Bool) -> [HsExpr GhcPs] -> Bool
forall a b. (a -> b) -> a -> b
$ (HsExpr GhcPs -> Bool) -> a -> [HsExpr GhcPs]
forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify (
\case
((HsVar XVar GhcPs
_ (L SrcSpan
_ IdP GhcPs
a)) :: HsExpr GhcPs) | RdrName -> RdrName -> Bool
eqRdrName IdP GhcPs
RdrName
a RdrName
name -> Bool
True
HsExpr GhcPs
_ -> Bool
False
) a
x
containsHole :: Data a => a -> Bool
containsHole :: a -> Bool
containsHole a
x = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [HsExpr GhcPs] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([HsExpr GhcPs] -> Bool) -> [HsExpr GhcPs] -> Bool
forall a b. (a -> b) -> a -> b
$ (HsExpr GhcPs -> Bool) -> a -> [HsExpr GhcPs]
forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify (
\case
((HsVar XVar GhcPs
_ (L SrcSpan
_ IdP GhcPs
name)) :: HsExpr GhcPs) -> OccName -> Bool
isHole (OccName -> Bool) -> OccName -> Bool
forall a b. (a -> b) -> a -> b
$ RdrName -> OccName
forall name. HasOccName name => name -> OccName
occName IdP GhcPs
RdrName
name
MetaprogramSyntax FieldLabelString
_ -> Bool
True
HsExpr GhcPs
_ -> Bool
False
) a
x
isHole :: OccName -> Bool
isHole :: OccName -> Bool
isHole = String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
"_" (String -> Bool) -> (OccName -> String) -> OccName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> String
occNameString
allOccNames :: Data a => a -> Set OccName
allOccNames :: a -> Set OccName
allOccNames = (Set OccName -> Set OccName -> Set OccName)
-> GenericQ (Set OccName) -> GenericQ (Set OccName)
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything Set OccName -> Set OccName -> Set OccName
forall a. Semigroup a => a -> a -> a
(<>) (GenericQ (Set OccName) -> GenericQ (Set OccName))
-> GenericQ (Set OccName) -> GenericQ (Set OccName)
forall a b. (a -> b) -> a -> b
$ Set OccName -> (OccName -> Set OccName) -> a -> Set OccName
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ Set OccName
forall a. Monoid a => a
mempty ((OccName -> Set OccName) -> a -> Set OccName)
-> (OccName -> Set OccName) -> a -> Set OccName
forall a b. (a -> b) -> a -> b
$ \case
OccName
a -> OccName -> Set OccName
forall a. a -> Set a
S.singleton OccName
a
pattern AMatch :: HsMatchContext (NameOrRdrName (IdP GhcPs)) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
pattern $mAMatch :: forall r.
Match GhcPs (LHsExpr GhcPs)
-> (HsMatchContext (NameOrRdrName (IdP GhcPs))
-> [Pat GhcPs] -> HsExpr GhcPs -> r)
-> (Void# -> r)
-> r
AMatch ctx pats body <-
Match { m_ctxt = ctx
, m_pats = fmap fromPatCompat -> pats
, m_grhss = UnguardedRHSs (unLoc -> body)
}
pattern SingleLet :: IdP GhcPs -> [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs -> HsExpr GhcPs
pattern $mSingleLet :: forall r.
HsExpr GhcPs
-> (IdP GhcPs -> [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs -> r)
-> (Void# -> r)
-> r
SingleLet bind pats val expr <-
HsLet _
(L _ (HsValBinds _
(ValBinds _ (bagToList ->
[(L _ (FunBind _ (L _ bind) (MG _ (L _ [L _ (AMatch _ pats val)]) _) _ _))]) _)))
(L _ expr)
pattern Lambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs
pattern $bLambda :: [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs
$mLambda :: forall r.
HsExpr GhcPs
-> ([Pat GhcPs] -> HsExpr GhcPs -> r) -> (Void# -> r) -> r
Lambda pats body <-
HsLam _
(MG {mg_alts = L _ [L _ (AMatch _ pats body) ]})
where
Lambda [] HsExpr GhcPs
body = HsExpr GhcPs
body
Lambda [Pat GhcPs]
pats HsExpr GhcPs
body = [Pat GhcPs] -> HsExpr GhcPs -> HsExpr GhcPs
lambda [Pat GhcPs]
pats HsExpr GhcPs
body
pattern UnguardedRHSs :: LHsExpr p -> GRHSs p (LHsExpr p)
pattern $mUnguardedRHSs :: forall r p.
GRHSs p (LHsExpr p) -> (LHsExpr p -> r) -> (Void# -> r) -> r
UnguardedRHSs body <-
GRHSs {grhssGRHSs = [L _ (GRHS _ [] body)]}
pattern SinglePatMatch :: PatCompattable p => Pat p -> LHsExpr p -> Match p (LHsExpr p)
pattern $mSinglePatMatch :: forall r p.
PatCompattable p =>
Match p (LHsExpr p)
-> (Pat p -> LHsExpr p -> r) -> (Void# -> r) -> r
SinglePatMatch pat body <-
Match { m_pats = [fromPatCompat -> pat]
, m_grhss = UnguardedRHSs body
}
unpackMatches :: PatCompattable p => [Match p (LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)]
unpackMatches :: [Match p (LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)]
unpackMatches [] = [(Pat p, LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)]
forall a. a -> Maybe a
Just []
unpackMatches (SinglePatMatch Pat p
pat LHsExpr p
body : [Match p (LHsExpr p)]
matches) =
(:) ((Pat p, LHsExpr p)
-> [(Pat p, LHsExpr p)] -> [(Pat p, LHsExpr p)])
-> Maybe (Pat p, LHsExpr p)
-> Maybe ([(Pat p, LHsExpr p)] -> [(Pat p, LHsExpr p)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pat p, LHsExpr p) -> Maybe (Pat p, LHsExpr p)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat p
pat, LHsExpr p
body) Maybe ([(Pat p, LHsExpr p)] -> [(Pat p, LHsExpr p)])
-> Maybe [(Pat p, LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Match p (LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)]
forall p.
PatCompattable p =>
[Match p (LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)]
unpackMatches [Match p (LHsExpr p)]
matches
unpackMatches [Match p (LHsExpr p)]
_ = Maybe [(Pat p, LHsExpr p)]
forall a. Maybe a
Nothing
pattern Case :: PatCompattable p => HsExpr p -> [(Pat p, LHsExpr p)] -> HsExpr p
pattern $mCase :: forall r p.
PatCompattable p =>
HsExpr p
-> (HsExpr p -> [(Pat p, LHsExpr p)] -> r) -> (Void# -> r) -> r
Case scrutinee matches <-
HsCase _ (L _ scrutinee)
(MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})
pattern LamCase :: PatCompattable p => [(Pat p, LHsExpr p)] -> HsExpr p
pattern $mLamCase :: forall r p.
PatCompattable p =>
HsExpr p -> ([(Pat p, LHsExpr p)] -> r) -> (Void# -> r) -> r
LamCase matches <-
HsLamCase _
(MG {mg_alts = L _ (fmap unLoc -> unpackMatches -> Just matches)})
lambdaCaseable :: Type -> Maybe Bool
lambdaCaseable :: Type -> Maybe Bool
lambdaCaseable (Type -> Maybe (Type, Type)
splitFunTy_maybe -> Just (Type
arg, Type
res))
| Maybe TyCon -> Bool
forall a. Maybe a -> Bool
isJust (Type -> Maybe TyCon
algebraicTyCon Type
arg)
= Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ Maybe TyCon -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TyCon -> Bool) -> Maybe TyCon -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> Maybe TyCon
algebraicTyCon Type
res
lambdaCaseable Type
_ = Maybe Bool
forall a. Maybe a
Nothing
class PatCompattable p where
fromPatCompat :: PatCompat p -> Pat p
toPatCompat :: Pat p -> PatCompat p
#if __GLASGOW_HASKELL__ == 808
instance PatCompattable GhcTc where
fromPatCompat = id
toPatCompat = id
instance PatCompattable GhcPs where
fromPatCompat = id
toPatCompat = id
type PatCompat pass = Pat pass
#else
instance PatCompattable GhcTc where
fromPatCompat :: PatCompat GhcTc -> Pat GhcTc
fromPatCompat = PatCompat GhcTc -> Pat GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc
toPatCompat :: Pat GhcTc -> PatCompat GhcTc
toPatCompat = Pat GhcTc -> PatCompat GhcTc
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc
instance PatCompattable GhcPs where
fromPatCompat :: PatCompat GhcPs -> Pat GhcPs
fromPatCompat = PatCompat GhcPs -> Pat GhcPs
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc
toPatCompat :: Pat GhcPs -> PatCompat GhcPs
toPatCompat = Pat GhcPs -> PatCompat GhcPs
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc
type PatCompat pass = LPat pass
#endif
pattern TopLevelRHS
:: OccName
-> [PatCompat GhcTc]
-> LHsExpr GhcTc
-> HsLocalBindsLR GhcTc GhcTc
-> Match GhcTc (LHsExpr GhcTc)
pattern $mTopLevelRHS :: forall r.
Match GhcTc (LHsExpr GhcTc)
-> (OccName
-> [PatCompat GhcTc]
-> LHsExpr GhcTc
-> HsLocalBindsLR GhcTc GhcTc
-> r)
-> (Void# -> r)
-> r
TopLevelRHS name ps body where_binds <-
Match _
(FunRhs (L _ (occName -> name)) _ _)
ps
(GRHSs _
[L _ (GRHS _ [] body)] (L _ where_binds))
dataConExTys :: DataCon -> [TyCoVar]
#if __GLASGOW_HASKELL__ >= 808
dataConExTys :: DataCon -> [Var]
dataConExTys = DataCon -> [Var]
DataCon.dataConExTyCoVars
#else
dataConExTys = DataCon.dataConExTyVars
#endif
unXPat :: Pat GhcPs -> Pat GhcPs
#if __GLASGOW_HASKELL__ == 808
unXPat (XPat (L _ pat)) = unXPat pat
#endif
unXPat :: Pat GhcPs -> Pat GhcPs
unXPat Pat GhcPs
pat = Pat GhcPs
pat
liftMaybe :: Monad m => Maybe a -> MaybeT m a
liftMaybe :: Maybe a -> MaybeT m a
liftMaybe Maybe a
a = m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe a) -> MaybeT m a) -> m (Maybe a) -> MaybeT m a
forall a b. (a -> b) -> a -> b
$ Maybe a -> m (Maybe a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe a
a
typeCheck :: HscEnv -> TcGblEnv -> HsExpr GhcTc -> IO (Maybe Type)
typeCheck :: HscEnv -> TcGblEnv -> HsExpr GhcTc -> IO (Maybe Type)
typeCheck HscEnv
hscenv TcGblEnv
tcg = ((Messages, Maybe Type) -> Maybe Type)
-> IO (Messages, Maybe Type) -> IO (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Messages, Maybe Type) -> Maybe Type
forall a b. (a, b) -> b
snd (IO (Messages, Maybe Type) -> IO (Maybe Type))
-> (HsExpr GhcTc -> IO (Messages, Maybe Type))
-> HsExpr GhcTc
-> IO (Maybe Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HscEnv -> TcGblEnv -> DsM Type -> IO (Messages, Maybe Type)
forall a. HscEnv -> TcGblEnv -> DsM a -> IO (Messages, Maybe a)
initDs HscEnv
hscenv TcGblEnv
tcg (DsM Type -> IO (Messages, Maybe Type))
-> (HsExpr GhcTc -> DsM Type)
-> HsExpr GhcTc
-> IO (Messages, Maybe Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoreExpr -> Type)
-> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr -> DsM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CoreExpr -> Type
exprType (IOEnv (Env DsGblEnv DsLclEnv) CoreExpr -> DsM Type)
-> (HsExpr GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr)
-> HsExpr GhcTc
-> DsM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsExpr GhcTc -> IOEnv (Env DsGblEnv DsLclEnv) CoreExpr
dsExpr
mkFunTys' :: [Type] -> Type -> Type
mkFunTys' :: ThetaType -> Type -> Type
mkFunTys' =
#if __GLASGOW_HASKELL__ <= 808
mkFunTys
#else
ThetaType -> Type -> Type
mkVisFunTys
#endif
normalizeType :: Context -> Type -> Type
normalizeType :: Context -> Type -> Type
normalizeType Context
ctx Type
ty =
let ty' :: Type
ty' = Context -> Type -> Type
expandTyFam Context
ctx Type
ty
in case HasCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
tcSplitTyConApp_maybe Type
ty' of
Just (TyCon
tc, ThetaType
tys) ->
case FamInstEnvs
-> TyCon -> ThetaType -> Maybe (TyCon, ThetaType, KindCoercion)
tcLookupDataFamInst_maybe (Context -> FamInstEnvs
ctxFamInstEnvs Context
ctx) TyCon
tc ThetaType
tys of
Just (TyCon
dtc, ThetaType
dtys, KindCoercion
_) -> Type -> ThetaType -> Type
mkAppTys (TyCon -> Type
mkTyConTy TyCon
dtc) ThetaType
dtys
Maybe (TyCon, ThetaType, KindCoercion)
Nothing -> Type
ty'
Maybe (TyCon, ThetaType)
Nothing -> Type
ty'
expandTyFam :: Context -> Type -> Type
expandTyFam :: Context -> Type -> Type
expandTyFam Context
ctx = (KindCoercion, Type) -> Type
forall a b. (a, b) -> b
snd ((KindCoercion, Type) -> Type)
-> (Type -> (KindCoercion, Type)) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FamInstEnvs -> Role -> Type -> (KindCoercion, Type)
normaliseType (Context -> FamInstEnvs
ctxFamInstEnvs Context
ctx) Role
Nominal
tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems :: Set Var -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems Set Var
skolems CType
goal CType
inst =
case (Var -> BindFlag) -> ThetaType -> ThetaType -> UnifyResult
tcUnifyTysFG
(BindFlag -> BindFlag -> Bool -> BindFlag
forall a. a -> a -> Bool -> a
bool BindFlag
BindMe BindFlag
Skolem (Bool -> BindFlag) -> (Var -> Bool) -> Var -> BindFlag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> Set Var -> Bool) -> Set Var -> Var -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Set Var
skolems)
[CType -> Type
unCType CType
inst]
[CType -> Type
unCType CType
goal] of
Unifiable TCvSubst
subst -> TCvSubst -> Maybe TCvSubst
forall (f :: * -> *) a. Applicative f => a -> f a
pure TCvSubst
subst
UnifyResult
_ -> Maybe TCvSubst
forall a. Maybe a
Nothing
updateSubst :: TCvSubst -> TacticState -> TacticState
updateSubst :: TCvSubst -> TacticState -> TacticState
updateSubst TCvSubst
subst TacticState
s = TacticState
s { ts_unifier :: TCvSubst
ts_unifier = TCvSubst -> TCvSubst -> TCvSubst
unionTCvSubst TCvSubst
subst (TacticState -> TCvSubst
ts_unifier TacticState
s) }
methodHypothesis :: PredType -> Maybe [HyInfo CType]
methodHypothesis :: Type -> Maybe [HyInfo CType]
methodHypothesis Type
ty = do
(TyCon
tc, ThetaType
apps) <- HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty
Class
cls <- TyCon -> Maybe Class
tyConClass_maybe TyCon
tc
let methods :: [Var]
methods = Class -> [Var]
classMethods Class
cls
tvs :: [Var]
tvs = Class -> [Var]
classTyVars Class
cls
subst :: TCvSubst
subst = [Var] -> ThetaType -> TCvSubst
HasDebugCallStack => [Var] -> ThetaType -> TCvSubst
zipTvSubst [Var]
tvs ThetaType
apps
[HyInfo CType] -> Maybe [HyInfo CType]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([HyInfo CType] -> Maybe [HyInfo CType])
-> [HyInfo CType] -> Maybe [HyInfo CType]
forall a b. (a -> b) -> a -> b
$ [Var]
methods [Var] -> (Var -> HyInfo CType) -> [HyInfo CType]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Var
method ->
let ([Var]
_, ThetaType
_, Type
ty) = Type -> ([Var], ThetaType, Type)
tcSplitSigmaTy (Type -> ([Var], ThetaType, Type))
-> Type -> ([Var], ThetaType, Type)
forall a b. (a -> b) -> a -> b
$ Var -> Type
idType Var
method
in ( OccName -> Provenance -> CType -> HyInfo CType
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo (Var -> OccName
forall name. HasOccName name => name -> OccName
occName Var
method) (Uniquely Class -> Provenance
ClassMethodPrv (Uniquely Class -> Provenance) -> Uniquely Class -> Provenance
forall a b. (a -> b) -> a -> b
$ Class -> Uniquely Class
forall a. a -> Uniquely a
Uniquely Class
cls) (CType -> HyInfo CType) -> CType -> HyInfo CType
forall a b. (a -> b) -> a -> b
$ Type -> CType
CType (Type -> CType) -> Type -> CType
forall a b. (a -> b) -> a -> b
$ HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
ty
)