{-# LANGUAGE FlexibleContexts         #-}


module Language.Haskell.Liquid.Bare.Misc
  ( joinVar
  , mkVarExpr
  , vmap
  , runMapTyVars
  , matchKindArgs
  , symbolRTyVar
  , simpleSymbolVar
  , hasBoolResult
  , isKind
  ) where

import           Prelude                               hiding (error)

import           Liquid.GHC.API       as Ghc  hiding (Located, showPpr)

import           Control.Monad.Except                  (MonadError, throwError)
import           Control.Monad.State
import qualified Data.Maybe                            as Mb --(fromMaybe, isNothing)

import qualified Text.PrettyPrint.HughesPJ             as PJ
import qualified Data.List                             as L
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.GHC.Misc
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.Types

-- import           Language.Haskell.Liquid.Bare.Env

-- import           Language.Haskell.Liquid.WiredIn       (dcPrefix)


-- TODO: This is where unsorted stuff is for now. Find proper places for what follows.

{-
-- WTF does this function do?
makeSymbols :: (Id -> Bool) -> [Id] -> [F.Symbol] -> BareM [(F.Symbol, Var)]
makeSymbols f vs xs
  = do svs <- M.toList <$> gets varEnv
       return $ L.nub ([ (x,v') | (x,v) <- svs, x `elem` xs, let (v',_,_) = joinVar vs (v,x,x)]
                   ++  [ (F.symbol v, v) | v <- vs, f v, isDataConId v, hasBasicArgs $ varType v ])
    where
      -- arguments should be basic so that autogenerated singleton types are well formed
      hasBasicArgs (ForAllTy _ t) = hasBasicArgs t
      hasBasicArgs (FunTy _ tx t)   = isBaseTy tx && hasBasicArgs t
      hasBasicArgs _              = True

-}

{-
HEAD
freeSymbols :: (F.Reftable r, F.Reftable r1, F.Reftable r2, TyConable c, TyConable c1, TyConable c2)
            => [F.Symbol]
            -> [(a1, Located (RType c2 tv2 r2))]
            -> [(a, Located (RType c1 tv1 r1))]
            -> [Located (RType c tv r)]
            -> [LocSymbol]
freeSymbols xs' xts yts ivs =  [ lx | lx <- Misc.sortNub $ zs ++ zs' ++ zs'' , not (M.member (val lx) knownM) ]
  where
    knownM                  = M.fromList [ (x, ()) | x <- xs' ]
    zs                      = concatMap freeSyms (snd <$> xts)
    zs'                     = concatMap freeSyms (snd <$> yts)
    zs''                    = concatMap freeSyms ivs



-------------------------------------------------------------------------------
freeSyms :: (F.Reftable r, TyConable c) => Located (RType c tv r) -> [LocSymbol]
-------------------------------------------------------------------------------
freeSyms ty    = [ F.atLoc ty x | x <- tySyms ]
  where
    tySyms     = Misc.sortNub $ concat $ efoldReft (\_ _ -> True) False (\_ _ -> []) (const []) (const ()) f (const id) F.emptySEnv [] (val ty)
    f γ _ r xs = let F.Reft (v, _) = F.toReft r in
                 [ x | x <- F.syms r, x /= v, not (x `F.memberSEnv` γ)] : xs

--- ABOVE IS THE T1773 STUFF
--- BELOW IS THE develop-classes STUFF

-- freeSymbols :: (F.Reftable r, F.Reftable r1, F.Reftable r2, TyConable c, TyConable c1, TyConable c2)
--             => [F.Symbol]
--             -> [(a1, Located (RType c2 tv2 r2))]
--             -> [(a, Located (RType c1 tv1 r1))]
--             -> [(Located (RType c tv r))]
--             -> [LocSymbol]
-- freeSymbols xs' xts yts ivs =  [ lx | lx <- Misc.sortNub $ zs ++ zs' ++ zs'' , not (M.member (val lx) knownM) ]
--   where
--     knownM                  = M.fromList [ (x, ()) | x <- xs' ]
--     zs                      = concatMap freeSyms (snd <$> xts)
--     zs'                     = concatMap freeSyms (snd <$> yts)
--     zs''                    = concatMap freeSyms ivs



-- freeSyms :: (F.Reftable r, TyConable c) => Located (RType c tv r) -> [LocSymbol]
-- freeSyms ty    = [ F.atLoc ty x | x <- tySyms ]
--   where
--     tySyms     = Misc.sortNub $ concat $ efoldReft (\_ _ -> True) False (\_ _ -> []) (\_ -> []) (const ()) f (const id) F.emptySEnv [] (val ty)
--     f γ _ r xs = let F.Reft (v, _) = F.toReft r in
--                  [ x | x <- F.syms r, x /= v, not (x `F.memberSEnv` γ)] : xs

-}
-------------------------------------------------------------------------------
-- Renaming Type Variables in Haskell Signatures ------------------------------
-------------------------------------------------------------------------------
runMapTyVars :: Bool -> Type -> SpecType -> (PJ.Doc -> PJ.Doc -> Error) -> Either Error MapTyVarST
runMapTyVars :: Bool
-> Type
-> SpecType
-> (Doc -> Doc -> Error)
-> Either Error MapTyVarST
runMapTyVars Bool
allowTC Type
τ SpecType
t Doc -> Doc -> Error
err = forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ SpecType
t) ([(Var, RTyVar)] -> (Doc -> Doc -> Error) -> MapTyVarST
MTVST [] Doc -> Doc -> Error
err)

data MapTyVarST = MTVST
  { MapTyVarST -> [(Var, RTyVar)]
vmap   :: [(Var, RTyVar)]
  , MapTyVarST -> Doc -> Doc -> Error
errmsg :: PJ.Doc -> PJ.Doc -> Error
  }

mapTyVars :: Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars :: Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC (FunTy { ft_arg :: Type -> Type
ft_arg = Type
τ, ft_res :: Type -> Type
ft_res = Type
τ'}) SpecType
t
  | Type -> Bool
isErasable Type
τ
  = Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ' SpecType
t
  where isErasable :: Type -> Bool
isErasable = if Bool
allowTC then Type -> Bool
isEmbeddedDictType else Type -> Bool
isClassPred
mapTyVars Bool
allowTC (FunTy { ft_arg :: Type -> Type
ft_arg = Type
τ, ft_res :: Type -> Type
ft_res = Type
τ'}) (RFun Symbol
_ RFInfo
_ SpecType
t SpecType
t' UReft Reft
_)
   = Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ SpecType
t forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ' SpecType
t'
mapTyVars Bool
allowTC Type
τ (RAllT RTVU RTyCon RTyVar
_ SpecType
t UReft Reft
_)
  = Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ SpecType
t
mapTyVars Bool
allowTC (TyConApp TyCon
_ [Type]
τs) (RApp RTyCon
_ [SpecType]
ts [RTProp RTyCon RTyVar (UReft Reft)]
_ UReft Reft
_)
   = forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC) [Type]
τs ([Type] -> [SpecType] -> [SpecType]
matchKindArgs' [Type]
τs [SpecType]
ts)
mapTyVars Bool
_ (TyVarTy Var
α) (RVar RTyVar
a UReft Reft
_)
   = do MapTyVarST
s  <- forall s (m :: * -> *). MonadState s m => m s
get
        MapTyVarST
s' <- forall (m :: * -> *).
MonadError Error m =>
Var -> RTyVar -> MapTyVarST -> m MapTyVarST
mapTyRVar Var
α RTyVar
a MapTyVarST
s
        forall s (m :: * -> *). MonadState s m => s -> m ()
put MapTyVarST
s'
mapTyVars Bool
allowTC Type
τ (RAllP PVU RTyCon RTyVar
_ SpecType
t)
  = Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ SpecType
t
mapTyVars Bool
allowTC Type
τ (RAllE Symbol
_ SpecType
_ SpecType
t)
  = Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ SpecType
t
mapTyVars Bool
allowTC Type
τ (RRTy [(Symbol, SpecType)]
_ UReft Reft
_ Oblig
_ SpecType
t)
  = Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ SpecType
t
mapTyVars Bool
allowTC Type
τ (REx Symbol
_ SpecType
_ SpecType
t)
  = Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ SpecType
t
mapTyVars Bool
_ Type
_ (RExprArg Located Expr
_)
  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
mapTyVars Bool
allowTC (AppTy Type
τ Type
τ') (RAppTy SpecType
t SpecType
t' UReft Reft
_)
  = do  Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ SpecType
t
        Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ' SpecType
t'
mapTyVars Bool
_ Type
_ (RHole UReft Reft
_)
  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
mapTyVars Bool
_ Type
k SpecType
_ | Type -> Bool
isKind Type
k
  = forall (m :: * -> *) a. Monad m => a -> m a
return ()
mapTyVars Bool
allowTC (ForAllTy TyCoVarBinder
_ Type
τ) SpecType
t
  = Bool -> Type -> SpecType -> StateT MapTyVarST (Either Error) ()
mapTyVars Bool
allowTC Type
τ SpecType
t
mapTyVars Bool
_ Type
hsT SpecType
lqT
  = do Doc -> Doc -> Error
err <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets MapTyVarST -> Doc -> Doc -> Error
errmsg
       forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Doc -> Doc -> Error
err (forall a. PPrint a => a -> Doc
F.pprint Type
hsT) (forall a. PPrint a => a -> Doc
F.pprint SpecType
lqT))

isKind :: Kind -> Bool
isKind :: Type -> Bool
isKind = Type -> Bool
classifiesTypeWithValues -- TODO:GHC-863 isStarKind k --  typeKind k


mapTyRVar :: MonadError Error m
          => Var -> RTyVar -> MapTyVarST -> m MapTyVarST
mapTyRVar :: forall (m :: * -> *).
MonadError Error m =>
Var -> RTyVar -> MapTyVarST -> m MapTyVarST
mapTyRVar Var
α RTyVar
a s :: MapTyVarST
s@(MTVST [(Var, RTyVar)]
αas Doc -> Doc -> Error
err)
  = case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
α [(Var, RTyVar)]
αas of
      Just RTyVar
a' | RTyVar
a forall a. Eq a => a -> a -> Bool
== RTyVar
a'   -> forall (m :: * -> *) a. Monad m => a -> m a
return MapTyVarST
s
              | Bool
otherwise -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Doc -> Doc -> Error
err (forall a. PPrint a => a -> Doc
F.pprint RTyVar
a) (forall a. PPrint a => a -> Doc
F.pprint RTyVar
a'))
      Maybe RTyVar
Nothing             -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(Var, RTyVar)] -> (Doc -> Doc -> Error) -> MapTyVarST
MTVST ((Var
α,RTyVar
a)forall a. a -> [a] -> [a]
:[(Var, RTyVar)]
αas) Doc -> Doc -> Error
err

matchKindArgs' :: [Type] -> [SpecType] -> [SpecType]
matchKindArgs' :: [Type] -> [SpecType] -> [SpecType]
matchKindArgs' [Type]
ts1' = forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> [SpecType] -> [SpecType]
go (forall a. [a] -> [a]
reverse [Type]
ts1') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse
  where
    go :: [Type] -> [SpecType] -> [SpecType]
go (Type
_:[Type]
ts1) (SpecType
t2:[SpecType]
ts2) = SpecType
t2forall a. a -> [a] -> [a]
:[Type] -> [SpecType] -> [SpecType]
go [Type]
ts1 [SpecType]
ts2
    go [Type]
ts      []       | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Type -> Bool
isKind [Type]
ts
                        = (forall r. Monoid r => Type -> RRType r
ofType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts) :: [SpecType]
    go [Type]
_       [SpecType]
ts       = [SpecType]
ts


matchKindArgs :: [SpecType] -> [SpecType] -> [SpecType]
matchKindArgs :: [SpecType] -> [SpecType] -> [SpecType]
matchKindArgs [SpecType]
ts1' = forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. [a] -> [a] -> [a]
go (forall a. [a] -> [a]
reverse [SpecType]
ts1') forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse
  where
    go :: [a] -> [a] -> [a]
go (a
_:[a]
ts1) (a
t2:[a]
ts2) = a
t2forall a. a -> [a] -> [a]
:[a] -> [a] -> [a]
go [a]
ts1 [a]
ts2
    go [a]
ts      []       = [a]
ts
    go [a]
_       [a]
ts       = [a]
ts

mkVarExpr :: Id -> F.Expr
mkVarExpr :: Var -> Expr
mkVarExpr Var
v
  | Var -> Bool
isFunVar Var
v = LocSymbol -> [Expr] -> Expr
F.mkEApp (Var -> LocSymbol
varFunSymbol Var
v) []
  | Bool
otherwise  = forall a. Symbolic a => a -> Expr
F.eVar Var
v -- EVar (symbol v)

varFunSymbol :: Id -> Located F.Symbol
varFunSymbol :: Var -> LocSymbol
varFunSymbol = forall a. a -> Located a
dummyLoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> DataCon
idDataCon

isFunVar :: Id -> Bool
isFunVar :: Var -> Bool
isFunVar Var
v   = Var -> Bool
isDataConId Var
v Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
αs) Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
Mb.isNothing Maybe (Type, Type, Type)
tf
  where
    ([Var]
αs, Type
t)  = Type -> ([Var], Type)
splitForAllTyCoVars forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
v
    tf :: Maybe (Type, Type, Type)
tf       = Type -> Maybe (Type, Type, Type)
splitFunTy_maybe Type
t

-- the Vars we lookup in GHC don't always have the same tyvars as the Vars
-- we're given, so return the original var when possible.
-- see tests/pos/ResolvePred.hs for an example
joinVar :: [Var] -> (Var, s, t) -> (Var, s, t)
joinVar :: forall s t. [Var] -> (Var, s, t) -> (Var, s, t)
joinVar [Var]
vs (Var
v,s
s,t
t) = case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find ((forall a. Eq a => a -> a -> Bool
== forall a. Outputable a => a -> String
showPpr Var
v) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> String
showPpr) [Var]
vs of
                       Just Var
v' -> (Var
v',s
s,t
t)
                       Maybe Var
Nothing -> (Var
v,s
s,t
t)

simpleSymbolVar :: Var -> F.Symbol
simpleSymbolVar :: Var -> Symbol
simpleSymbolVar  = Symbol -> Symbol
dropModuleNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> String
showPpr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedThing a => a -> Name
getName

hasBoolResult :: Type -> Bool
hasBoolResult :: Type -> Bool
hasBoolResult (ForAllTy TyCoVarBinder
_ Type
t) = Type -> Bool
hasBoolResult Type
t
hasBoolResult (FunTy { ft_res :: Type -> Type
ft_res = Type
t} )    | Type -> Type -> Bool
eqType Type
boolTy Type
t = Bool
True
hasBoolResult (FunTy { ft_res :: Type -> Type
ft_res = Type
t} )    = Type -> Bool
hasBoolResult Type
t
hasBoolResult Type
_              = Bool
False