{-# LANGUAGE CPP               #-}
{-# LANGUAGE OverloadedStrings #-}

module Wingman.GHC where

import           Control.Monad.State
import           Control.Monad.Trans.Maybe (MaybeT(..))
import           Data.Bool (bool)
import           Data.Coerce (coerce)
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           Development.IDE.GHC.Compat
import           Development.IDE.GHC.Compat.Util
import           GHC.SourceGen (lambda)
import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
import           Wingman.StaticPlugin (pattern MetaprogramSyntax)
import           Wingman.Types

#if __GLASGOW_HASKELL__ >= 900
import GHC.Tc.Utils.TcType
#endif


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  -- look through casts, as
                                                -- this is only used for
                                                -- e.g., FlexibleContexts
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_char :: Char
some_magic_char = Char
'w' -- 'w' for wingman ;D
   in Var -> Unique -> Var
setVarUnique Var
t (Unique -> Var) -> Unique -> Var
forall a b. (a -> b) -> a -> b
$ Unique -> Char -> Unique
newTagUnique Unique
uniq Char
some_magic_char


------------------------------------------------------------------------------
-- | Is this a function type?
isFunction :: Type -> Bool
isFunction :: Type -> Bool
isFunction (Type -> ([Var], ThetaType, ThetaType, Type)
tacticsSplitFunTy -> ([Var]
_, ThetaType
_, [], Type
_)) = Bool
False
isFunction Type
_                                    = Bool
True


------------------------------------------------------------------------------
-- | Split a function, also splitting out its quantified variables and theta
-- context.
tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Scaled 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)


------------------------------------------------------------------------------
-- | Rip the theta context out of a regular type.
tacticsThetaTy :: Type -> ThetaType
tacticsThetaTy :: Type -> ThetaType
tacticsThetaTy (Type -> ([Var], ThetaType, Type)
tcSplitSigmaTy -> ([Var]
_, ThetaType
theta,  Type
_)) = ThetaType
theta


------------------------------------------------------------------------------
-- | Get the data cons of a type, if it has any.
tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
tacticsGetDataCons :: Type -> Maybe ([DataCon], ThetaType)
tacticsGetDataCons Type
ty
  | Just (TyVarBinder
_, Type
ty') <- Type -> Maybe (TyVarBinder, Type)
tcSplitForAllTyVarBinder_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

------------------------------------------------------------------------------
-- | Instantiate all of the quantified type variables in a type with fresh
-- skolems.
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 -> Var -> Var -> Map Var Var -> Var
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault Var
tv Var
tv Map Var Var
reps
      ) (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)
tcSplitForAllTyVars Type
t


------------------------------------------------------------------------------
-- | Given a datacon, extract its record fields' names and types. Returns
-- nothing if the datacon is not a record.
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)


------------------------------------------------------------------------------
-- | Is this an algebraic type?
algebraicTyCon :: Type -> Maybe TyCon
algebraicTyCon :: Type -> Maybe TyCon
algebraicTyCon Type
ty
  | Just (TyVarBinder
_, Type
ty') <- Type -> Maybe (TyVarBinder, Type)
tcSplitForAllTyVarBinder_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


------------------------------------------------------------------------------
-- | We can't compare 'RdrName' for equality directly. Instead, sloppily
-- compare them by their 'OccName's.
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


------------------------------------------------------------------------------
-- | Compare two 'OccName's for unqualified equality.
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


------------------------------------------------------------------------------
-- | Does this thing contain any references to 'HsVar's with the given
-- 'RdrName'?
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


------------------------------------------------------------------------------
-- | Does this thing contain any holes?
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


------------------------------------------------------------------------------
-- | Check if an 'OccName' is a hole
isHole :: OccName -> Bool
-- TODO(sandy): Make this more robust
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


------------------------------------------------------------------------------
-- | Get all of the referenced occnames.
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


------------------------------------------------------------------------------
-- | Unpack the relevant parts of a 'Match'
#if __GLASGOW_HASKELL__ >= 900
pattern AMatch :: HsMatchContext (NoGhcTc GhcPs) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
#else
pattern AMatch :: HsMatchContext (NameOrRdrName (IdP GhcPs)) -> [Pat GhcPs] -> HsExpr GhcPs -> Match GhcPs (LHsExpr GhcPs)
#endif
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 _
    (HsValBinds _
      (ValBinds _ (bagToList ->
        [L _ (FunBind {fun_id = (L _ bind), fun_matches = (MG _ (L _ [L _ (AMatch _ pats val)]) _)})]) _))
    (L _ expr)


------------------------------------------------------------------------------
-- | A pattern over the otherwise (extremely) messy AST for lambdas.
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
    -- If there are no patterns to bind, just stick in the body
    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


------------------------------------------------------------------------------
-- | A GRHS that caontains no guards.
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)]}


------------------------------------------------------------------------------
-- | A match with a single pattern. Case matches are always 'SinglePatMatch'es.
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
        }


------------------------------------------------------------------------------
-- | Helper function for defining the 'Case' pattern.
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
pat, LHsExpr p
body)(Pat p, LHsExpr p) -> [(Pat p, LHsExpr p)] -> [(Pat p, LHsExpr p)]
forall a. a -> [a] -> [a]
:) ([(Pat p, LHsExpr p)] -> [(Pat p, LHsExpr p)])
-> Maybe [(Pat p, LHsExpr p)] -> Maybe [(Pat p, LHsExpr p)]
forall (f :: * -> *) a b. Functor 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


------------------------------------------------------------------------------
-- | A pattern over the otherwise (extremely) messy AST for lambdas.
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)}

------------------------------------------------------------------------------
-- | Like 'Case', but for lambda cases.
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)}


------------------------------------------------------------------------------
-- | Can ths type be lambda-cased?
--
-- Return: 'Nothing' if no
--         @Just False@ if it can't be homomorphic
--         @Just True@ if it can
lambdaCaseable :: Type -> Maybe Bool
#if __GLASGOW_HASKELL__ >= 900
lambdaCaseable (splitFunTy_maybe -> Just (_multiplicity, arg, res))
#else
lambdaCaseable :: Type -> Maybe Bool
lambdaCaseable (Type -> Maybe (Type, Type)
splitFunTy_maybe -> Just (Type
arg, Type
res))
#endif
  | 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

------------------------------------------------------------------------------
-- | Should make sure it's a fun bind
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))

------------------------------------------------------------------------------
-- | In GHC 8.8, sometimes patterns are wrapped in 'XPat'.
-- The nitty gritty details are explained at
-- https://blog.shaynefletcher.org/2020/03/ghc-haskell-pats-and-lpats.html
--
-- We need to remove these in order to succesfull find patterns.
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


------------------------------------------------------------------------------
-- | Get the type of an @HsExpr GhcTc@. This is slow and you should prefer to
-- not use it, but sometimes it can't be helped.
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

------------------------------------------------------------------------------
-- | Expand type and data families
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) ->
          -- try to expand any data families
          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'

------------------------------------------------------------------------------
-- | Expand type families
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


------------------------------------------------------------------------------
-- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of.
tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems :: Set Var -> CType -> CType -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolems Set Var
skolems CType
goal CType
inst =
  Set Var -> [(Type, Type)] -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolemsMany Set Var
skolems ([(Type, Type)] -> Maybe TCvSubst)
-> [(Type, Type)] -> Maybe TCvSubst
forall a b. (a -> b) -> a -> b
$ [(CType, CType)] -> [(Type, Type)]
coerce [(CType
goal, CType
inst)]

------------------------------------------------------------------------------
-- | Like 'tryUnifyUnivarsButNotSkolems', but takes a list
-- of pairs of types to unify.
tryUnifyUnivarsButNotSkolemsMany :: Set TyVar -> [(Type, Type)] -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolemsMany :: Set Var -> [(Type, Type)] -> Maybe TCvSubst
tryUnifyUnivarsButNotSkolemsMany Set Var
skolems ([(Type, Type)] -> (ThetaType, ThetaType)
forall a b. [(a, b)] -> ([a], [b])
unzip -> (ThetaType
goal, ThetaType
inst)) =
  (Var -> BindFlag) -> ThetaType -> ThetaType -> Maybe TCvSubst
tcUnifyTys
    (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)
    ThetaType
inst
    ThetaType
goal


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) }


------------------------------------------------------------------------------
-- | Get the class methods of a 'PredType', correctly dealing with
-- instantiation of quantified class types.
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
       )