{-# 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  -- 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_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


------------------------------------------------------------------------------
-- | 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, [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)
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

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


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


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


------------------------------------------------------------------------------
-- | 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, 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


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

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


dataConExTys :: DataCon -> [TyCoVar]
#if __GLASGOW_HASKELL__ >= 808
dataConExTys :: DataCon -> [Var]
dataConExTys = DataCon -> [Var]
DataCon.dataConExTyCoVars
#else
dataConExTys = DataCon.dataConExTyVars
#endif


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


mkFunTys' :: [Type] -> Type -> Type
mkFunTys' :: ThetaType -> Type -> Type
mkFunTys' =
#if __GLASGOW_HASKELL__ <= 808
  mkFunTys
#else
  ThetaType -> Type -> Type
mkVisFunTys
#endif


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


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