{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE DeriveTraversable         #-}
{-# LANGUAGE StandaloneDeriving        #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Language.Haskell.Liquid.Constraint.Template (
  Template(..)
, unTemplate
, varTemplate
, addPostTemplate
, safeFromAsserted
, topSpecType
, derivedVar
, extender
) where

import           Prelude hiding (error)
import qualified Data.Foldable                                 as F
import qualified Data.Traversable                              as T
import qualified Data.HashSet                                  as S
import           Control.Monad.State ( gets )
import           Text.PrettyPrint.HughesPJ ( text, (<+>) )
import           GHC.Types.Var (Var)
import           GHC.Core (CoreExpr)
import           GHC.Core.Utils ( exprType )
import qualified Language.Fixpoint.Types                       as F
import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Constraint.Env ( lookupREnv, (+=) )
import           Language.Haskell.Liquid.Constraint.Monad (addPost, addW)
import           Language.Haskell.Liquid.Constraint.Fresh (refreshArgsTop, freshTyExpr)

-- Template

data Template a
  = Asserted a
  | Assumed a
  | Internal a
  | Unknown
  deriving (forall a b. a -> Template b -> Template a
forall a b. (a -> b) -> Template a -> Template b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Template b -> Template a
$c<$ :: forall a b. a -> Template b -> Template a
fmap :: forall a b. (a -> b) -> Template a -> Template b
$cfmap :: forall a b. (a -> b) -> Template a -> Template b
Functor, forall a. Eq a => a -> Template a -> Bool
forall a. Num a => Template a -> a
forall a. Ord a => Template a -> a
forall m. Monoid m => Template m -> m
forall a. Template a -> Bool
forall a. Template a -> Int
forall a. Template a -> [a]
forall a. (a -> a -> a) -> Template a -> a
forall m a. Monoid m => (a -> m) -> Template a -> m
forall b a. (b -> a -> b) -> b -> Template a -> b
forall a b. (a -> b -> b) -> b -> Template a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Template a -> a
$cproduct :: forall a. Num a => Template a -> a
sum :: forall a. Num a => Template a -> a
$csum :: forall a. Num a => Template a -> a
minimum :: forall a. Ord a => Template a -> a
$cminimum :: forall a. Ord a => Template a -> a
maximum :: forall a. Ord a => Template a -> a
$cmaximum :: forall a. Ord a => Template a -> a
elem :: forall a. Eq a => a -> Template a -> Bool
$celem :: forall a. Eq a => a -> Template a -> Bool
length :: forall a. Template a -> Int
$clength :: forall a. Template a -> Int
null :: forall a. Template a -> Bool
$cnull :: forall a. Template a -> Bool
toList :: forall a. Template a -> [a]
$ctoList :: forall a. Template a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Template a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Template a -> a
foldr1 :: forall a. (a -> a -> a) -> Template a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Template a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Template a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Template a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Template a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Template a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Template a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Template a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Template a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Template a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Template a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Template a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Template a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Template a -> m
fold :: forall m. Monoid m => Template m -> m
$cfold :: forall m. Monoid m => Template m -> m
F.Foldable, Functor Template
Foldable Template
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Template (m a) -> m (Template a)
forall (f :: * -> *) a.
Applicative f =>
Template (f a) -> f (Template a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Template a -> m (Template b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Template a -> f (Template b)
sequence :: forall (m :: * -> *) a. Monad m => Template (m a) -> m (Template a)
$csequence :: forall (m :: * -> *) a. Monad m => Template (m a) -> m (Template a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Template a -> m (Template b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Template a -> m (Template b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Template (f a) -> f (Template a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Template (f a) -> f (Template a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Template a -> f (Template b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Template a -> f (Template b)
T.Traversable)

deriving instance (Show a) => (Show (Template a))

instance PPrint a => PPrint (Template a) where
  pprintTidy :: Tidy -> Template a -> Doc
pprintTidy Tidy
k (Asserted a
t) = String -> Doc
text String
"Asserted" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a
t
  pprintTidy Tidy
k (Assumed  a
t) = String -> Doc
text String
"Assumed"  Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a
t
  pprintTidy Tidy
k (Internal a
t) = String -> Doc
text String
"Internal" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a
t
  pprintTidy Tidy
_ Template a
Unknown      = String -> Doc
text String
"Unknown"

unTemplate :: Template t -> t
unTemplate :: forall t. Template t -> t
unTemplate (Asserted t
t) = t
t
unTemplate (Assumed t
t)  = t
t
unTemplate (Internal t
t) = t
t
unTemplate Template t
_            = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"Constraint.Template.unTemplate called on `Unknown`"

addPostTemplate :: CGEnv
                -> Template SpecType
                -> CG (Template SpecType)
addPostTemplate :: CGEnv -> Template SpecType -> CG (Template SpecType)
addPostTemplate CGEnv
γ (Asserted SpecType
t) = forall a. a -> Template a
Asserted forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ SpecType
t
addPostTemplate CGEnv
γ (Assumed  SpecType
t) = forall a. a -> Template a
Assumed  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ SpecType
t
addPostTemplate CGEnv
γ (Internal SpecType
t) = forall a. a -> Template a
Internal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ SpecType
t
addPostTemplate CGEnv
_ Template SpecType
Unknown      = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Template a
Unknown

safeFromAsserted :: [Char] -> Template t -> t
safeFromAsserted :: forall t. String -> Template t -> t
safeFromAsserted String
_   (Asserted t
t) = t
t
safeFromAsserted String
msg  Template t
_           = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ String
"safeFromAsserted:" forall a. [a] -> [a] -> [a]
++ String
msg

-- | @varTemplate@ is only called with a `Just e` argument when the `e`
-- corresponds to the body of a @Rec@ binder.
varTemplate :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate CGEnv
γ (Var
x, Maybe CoreExpr
eo) = CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate' CGEnv
γ (Var
x, Maybe CoreExpr
eo) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Var -> SpecType -> CG SpecType
topSpecType Var
x)

-- | @lazVarTemplate@ is like `varTemplate` but for binders that are *not*
--   termination checked and hence, the top-level refinement / KVar is
--   stripped out. e.g. see tests/neg/T743.hs
-- varTemplate :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
-- lazyVarTemplate γ (x, eo) = dbg <$> (topRTypeBase <$>) <$> varTemplate' γ (x, eo)
--   where
--    dbg   = traceShow ("LAZYVAR-TEMPLATE: " ++ show x)

varTemplate' :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate' :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate' CGEnv
γ (Var
x, Maybe CoreExpr
eo)
  = case (Maybe CoreExpr
eo, Symbol -> REnv -> Maybe SpecType
lookupREnv (forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (CGEnv -> REnv
grtys CGEnv
γ), Symbol -> REnv -> Maybe SpecType
lookupREnv (forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (CGEnv -> REnv
assms CGEnv
γ), Symbol -> REnv -> Maybe SpecType
lookupREnv (forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (CGEnv -> REnv
intys CGEnv
γ)) of
      (Maybe CoreExpr
_, Just SpecType
t, Maybe SpecType
_, Maybe SpecType
_) -> forall a. a -> Template a
Asserted forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> CG SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Maybe CoreExpr
_, Maybe SpecType
_, Maybe SpecType
_, Just SpecType
t) -> forall a. a -> Template a
Internal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> CG SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Maybe CoreExpr
_, Maybe SpecType
_, Just SpecType
t, Maybe SpecType
_) -> forall a. a -> Template a
Assumed  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> CG SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Just CoreExpr
e, Maybe SpecType
_, Maybe SpecType
_, Maybe SpecType
_) -> do SpecType
t <- Bool -> KVKind -> CoreExpr -> Type -> CG SpecType
freshTyExpr (Config -> Bool
typeclass (forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (Var -> KVKind
RecBindE Var
x) CoreExpr
e (CoreExpr -> Type
exprType CoreExpr
e)
                              WfC -> CG ()
addW (CGEnv -> SpecType -> WfC
WfC CGEnv
γ SpecType
t)
                              forall a. a -> Template a
Asserted forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> CG SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Maybe CoreExpr
_,      Maybe SpecType
_, Maybe SpecType
_, Maybe SpecType
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Template a
Unknown

-- | @topSpecType@ strips out the top-level refinement of "derived var"
topSpecType :: Var -> SpecType -> CG SpecType
topSpecType :: Var -> SpecType -> CG SpecType
topSpecType Var
x SpecType
t = do
  TargetInfo
info <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> TargetInfo
ghcI
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if TargetSrc -> Var -> Bool
derivedVar (TargetInfo -> TargetSrc
giSrc TargetInfo
info) Var
x then forall r c tv. Reftable r => RType c tv r -> RType c tv r
topRTypeBase SpecType
t else SpecType
t

derivedVar :: TargetSrc -> Var -> Bool
derivedVar :: TargetSrc -> Var -> Bool
derivedVar TargetSrc
src Var
x = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Var
x (TargetSrc -> HashSet Var
giDerVars TargetSrc
src)

extender :: F.Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender :: forall a. Symbolic a => CGEnv -> (a, Template SpecType) -> CG CGEnv
extender CGEnv
γ (a
x, Asserted SpecType
t)
  = case Symbol -> REnv -> Maybe SpecType
lookupREnv (forall a. Symbolic a => a -> Symbol
F.symbol a
x) (CGEnv -> REnv
assms CGEnv
γ) of
      Just SpecType
t' -> CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"extender", forall a. Symbolic a => a -> Symbol
F.symbol a
x, SpecType
t')
      Maybe SpecType
_       -> CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"extender", forall a. Symbolic a => a -> Symbol
F.symbol a
x, SpecType
t)
extender CGEnv
γ (a
x, Assumed SpecType
t)
  = CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"extender", forall a. Symbolic a => a -> Symbol
F.symbol a
x, SpecType
t)
extender CGEnv
γ (a, Template SpecType)
_
  = forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ