{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE ConstraintKinds       #-}

{-# OPTIONS_GHC -Wno-orphans #-}

module Language.Haskell.Liquid.Constraint.Fresh
  ( -- module Language.Haskell.Liquid.Types.Fresh
    -- , 
    refreshArgsTop
  , freshTyType
  , freshTyExpr
  , trueTy
  , addKuts
  )
  where

-- import           Data.Maybe                    (catMaybes) -- , fromJust, isJust)
-- import           Data.Bifunctor
-- import qualified Data.List                      as L
import qualified Data.HashMap.Strict            as M
import qualified Data.HashSet                   as S
import           Data.Hashable
import           Control.Monad.State            (gets, get, put, modify)
import           Control.Monad                  (when, (>=>))
import           Prelude                        hiding (error)

import           Language.Fixpoint.Misc  ((=>>))
import qualified Language.Fixpoint.Types as F
import           Language.Fixpoint.Types.Visitor (kvarsExpr)
import           Language.Haskell.Liquid.Types
-- import           Language.Haskell.Liquid.Types.RefType
-- import           Language.Haskell.Liquid.Types.Fresh
import           Language.Haskell.Liquid.Constraint.Types
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import           Liquid.GHC.API as Ghc

--------------------------------------------------------------------------------
-- | This is all hardwiring stuff to CG ----------------------------------------
--------------------------------------------------------------------------------
instance Freshable CG Integer where
  fresh :: CG Integer
fresh = do CGInfo
s <- forall s (m :: * -> *). MonadState s m => m s
get
             let n :: Integer
n = CGInfo -> Integer
freshIndex CGInfo
s
             forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ CGInfo
s { freshIndex :: Integer
freshIndex = Integer
n forall a. Num a => a -> a -> a
+ Integer
1 }
             forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n

--------------------------------------------------------------------------------
refreshArgsTop :: (Var, SpecType) -> CG SpecType
--------------------------------------------------------------------------------
refreshArgsTop :: (Var, SpecType) -> CG SpecType
refreshArgsTop (Var
x, SpecType
t)
  = do (SpecType
t', Subst
su) <- forall (m :: * -> *). FreshM m => SpecType -> m (SpecType, Subst)
refreshArgsSub SpecType
t
       forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s {termExprs :: HashMap Var [Located Expr]
termExprs = forall k v.
(Eq k, Hashable k) =>
(v -> v) -> k -> HashMap k v -> HashMap k v
M.adjust (forall a. Subable a => Subst -> a -> a
F.subst Subst
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) Var
x forall a b. (a -> b) -> a -> b
$ CGInfo -> HashMap Var [Located Expr]
termExprs CGInfo
s}
       forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t'

--------------------------------------------------------------------------------
-- | Generation: Freshness -----------------------------------------------------
--------------------------------------------------------------------------------

-- | Right now, we generate NO new pvars. Rather than clutter code
--   with `uRType` calls, put it in one place where the above
--   invariant is /obviously/ enforced.
--   Constraint generation should ONLY use @freshTyType@ and @freshTyExpr@

freshTyType        :: Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType :: Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyType Bool
allowTC KVKind
k CoreExpr
e Type
τ  =  forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"freshTyType: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp KVKind
k forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr CoreExpr
e)
                   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> KVKind -> SpecType -> CG SpecType
freshTyReftype Bool
allowTC KVKind
k (forall r. Monoid r => Type -> RRType r
ofType Type
τ)

freshTyExpr        :: Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyExpr :: Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyExpr Bool
allowTC KVKind
k CoreExpr
e Type
_  = Bool -> KVKind -> SpecType -> CG SpecType
freshTyReftype Bool
allowTC KVKind
k forall a b. (a -> b) -> a -> b
$ CoreExpr -> SpecType
exprRefType CoreExpr
e

freshTyReftype     :: Bool -> KVKind -> SpecType -> CG SpecType
freshTyReftype :: Bool -> KVKind -> SpecType -> CG SpecType
freshTyReftype Bool
allowTC KVKind
k SpecType
_t = (SpecType -> CG SpecType
fixTy SpecType
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
refresh Bool
allowTC) forall (m :: * -> *) b a. Monad m => m b -> (b -> m a) -> m b
=>> KVKind -> SpecType -> StateT CGInfo Identity ()
addKVars KVKind
k
  where
    t :: SpecType
t                = {- F.tracepp ("freshTyReftype:" ++ show k) -} SpecType
_t

-- | Used to generate "cut" kvars for fixpoint. Typically, KVars for recursive
--   definitions, and also to update the KVar profile.
addKVars        :: KVKind -> SpecType -> CG ()
addKVars :: KVKind -> SpecType -> StateT CGInfo Identity ()
addKVars !KVKind
k !SpecType
t  = do
    Config
cfg <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall t. HasConfig t => t -> Config
getConfig forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGInfo -> TargetInfo
ghcI)
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
True          forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { kvProf :: KVProf
kvProf = KVKind -> Kuts -> KVProf -> KVProf
updKVProf KVKind
k Kuts
ks (CGInfo -> KVProf
kvProf CGInfo
s) }
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> KVKind -> Bool
isKut Config
cfg KVKind
k) forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> SpecType -> StateT CGInfo Identity ()
addKuts KVKind
k SpecType
t
  where
    ks :: Kuts
ks         = HashSet KVar -> Kuts
F.KS forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ SpecType -> [KVar]
specTypeKVars SpecType
t

isKut :: Config -> KVKind -> Bool
isKut :: Config -> KVKind -> Bool
isKut Config
_  (RecBindE Var
_) = Bool
True
isKut Config
cfg KVKind
ProjectE    = Bool -> Bool
not (forall t. HasConfig t => t -> Bool
higherOrderFlag Config
cfg) -- see ISSUE 1034, tests/pos/T1034.hs
isKut Config
_    KVKind
_          = Bool
False

addKuts :: (PPrint a) => a -> SpecType -> CG ()
addKuts :: forall a. PPrint a => a -> SpecType -> StateT CGInfo Identity ()
addKuts a
_x SpecType
t = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { kuts :: Kuts
kuts = forall a. Monoid a => a -> a -> a
mappend (HashSet KVar -> Kuts
F.KS HashSet KVar
ks) (CGInfo -> Kuts
kuts CGInfo
s)   }
  where
     ks' :: HashSet KVar
ks'     = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ SpecType -> [KVar]
specTypeKVars SpecType
t
     ks :: HashSet KVar
ks
       | forall a. HashSet a -> Bool
S.null HashSet KVar
ks' = HashSet KVar
ks'
       | Bool
otherwise  = {- F.tracepp ("addKuts: " ++ showpp _x) -} HashSet KVar
ks'

specTypeKVars :: SpecType -> [F.KVar]
specTypeKVars :: SpecType -> [KVar]
specTypeKVars = forall r c tv a.
(Reftable r, TyConable c) =>
Bool
-> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
foldReft Bool
False (\ SEnv SpecType
_ RReft
r [KVar]
ks -> Expr -> [KVar]
kvarsExpr (Reft -> Expr
F.reftPred forall a b. (a -> b) -> a -> b
$ forall r. UReft r -> r
ur_reft RReft
r) forall a. [a] -> [a] -> [a]
++ [KVar]
ks) []

--------------------------------------------------------------------------------
trueTy  :: Bool -> Type -> CG SpecType
--------------------------------------------------------------------------------
trueTy :: Bool -> Type -> CG SpecType
trueTy Bool
allowTC = Type -> CG SpecType
ofType' forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> forall (m :: * -> *) a. Freshable m a => Bool -> a -> m a
true Bool
allowTC

ofType' :: Type -> CG SpecType
ofType' :: Type -> CG SpecType
ofType' = SpecType -> CG SpecType
fixTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Monoid r => Type -> RRType r
ofType

fixTy :: SpecType -> CG SpecType
fixTy :: SpecType -> CG SpecType
fixTy SpecType
t = do TyConMap
tyi   <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> TyConMap
tyConInfo
             TCEmb TyCon
tce   <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> TCEmb TyCon
tyConEmbed
             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> TyConMap -> RRType r -> RRType r
addTyConInfo TCEmb TyCon
tce TyConMap
tyi SpecType
t

exprRefType :: CoreExpr -> SpecType
exprRefType :: CoreExpr -> SpecType
exprRefType = HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ forall k v. HashMap k v
M.empty

exprRefType_ :: M.HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ :: HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ HashMap Var SpecType
γ (Let Bind Var
b CoreExpr
e)
  = HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ (HashMap Var SpecType -> Bind Var -> HashMap Var SpecType
bindRefType_ HashMap Var SpecType
γ Bind Var
b) CoreExpr
e

exprRefType_ HashMap Var SpecType
γ (Lam Var
α CoreExpr
e) | Var -> Bool
isTyVar Var
α
  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv s. tv -> RTVar tv s
makeRTVar forall a b. (a -> b) -> a -> b
$ Var -> RTyVar
rTyVar Var
α) (HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ HashMap Var SpecType
γ CoreExpr
e) forall a. Monoid a => a
mempty

exprRefType_ HashMap Var SpecType
γ (Lam Var
x CoreExpr
e)
  = forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun (forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (forall r. Monoid r => Type -> RRType r
ofType forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x) (HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ HashMap Var SpecType
γ CoreExpr
e)

exprRefType_ HashMap Var SpecType
γ (Tick CoreTickish
_ CoreExpr
e)
  = HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ HashMap Var SpecType
γ CoreExpr
e

exprRefType_ HashMap Var SpecType
γ (Var Var
x)
  = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault (forall r. Monoid r => Type -> RRType r
ofType forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
x) Var
x HashMap Var SpecType
γ

exprRefType_ HashMap Var SpecType
_ CoreExpr
e
  = forall r. Monoid r => Type -> RRType r
ofType forall a b. (a -> b) -> a -> b
$ CoreExpr -> Type
exprType CoreExpr
e

bindRefType_ :: M.HashMap Var SpecType -> Bind Var -> M.HashMap Var SpecType
bindRefType_ :: HashMap Var SpecType -> Bind Var -> HashMap Var SpecType
bindRefType_ HashMap Var SpecType
γ (Rec [(Var, CoreExpr)]
xes)
  = forall k (t :: * -> *) v.
(Eq k, Foldable t, Hashable k) =>
HashMap k v -> t (k, v) -> HashMap k v
extendγ HashMap Var SpecType
γ [(Var
x, HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ HashMap Var SpecType
γ CoreExpr
e) | (Var
x,CoreExpr
e) <- [(Var, CoreExpr)]
xes]

bindRefType_ HashMap Var SpecType
γ (NonRec Var
x CoreExpr
e)
  = forall k (t :: * -> *) v.
(Eq k, Foldable t, Hashable k) =>
HashMap k v -> t (k, v) -> HashMap k v
extendγ HashMap Var SpecType
γ [(Var
x, HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ HashMap Var SpecType
γ CoreExpr
e)]

extendγ :: (Eq k, Foldable t, Hashable k)
        => M.HashMap k v
        -> t (k, v)
        -> M.HashMap k v
extendγ :: forall k (t :: * -> *) v.
(Eq k, Foldable t, Hashable k) =>
HashMap k v -> t (k, v) -> HashMap k v
extendγ HashMap k v
γ t (k, v)
xts
  = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(k
x,v
t) HashMap k v
m -> forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert k
x v
t HashMap k v
m) HashMap k v
γ t (k, v)
xts