{-# 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.Errors
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.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)
import           Language.Haskell.Liquid.UX.Config

-- Template

data Template a
  = Asserted a
  | Assumed a
  | Internal a
  | Unknown
  deriving ((forall a b. (a -> b) -> Template a -> Template b)
-> (forall a b. a -> Template b -> Template a) -> Functor Template
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
$cfmap :: forall a b. (a -> b) -> Template a -> Template b
fmap :: forall a b. (a -> b) -> Template a -> Template b
$c<$ :: forall a b. a -> Template b -> Template a
<$ :: forall a b. a -> Template b -> Template a
Functor, (forall m. Monoid m => Template m -> m)
-> (forall m a. Monoid m => (a -> m) -> Template a -> m)
-> (forall m a. Monoid m => (a -> m) -> Template a -> m)
-> (forall a b. (a -> b -> b) -> b -> Template a -> b)
-> (forall a b. (a -> b -> b) -> b -> Template a -> b)
-> (forall b a. (b -> a -> b) -> b -> Template a -> b)
-> (forall b a. (b -> a -> b) -> b -> Template a -> b)
-> (forall a. (a -> a -> a) -> Template a -> a)
-> (forall a. (a -> a -> a) -> Template a -> a)
-> (forall a. Template a -> [a])
-> (forall a. Template a -> Bool)
-> (forall a. Template a -> Int)
-> (forall a. Eq a => a -> Template a -> Bool)
-> (forall a. Ord a => Template a -> a)
-> (forall a. Ord a => Template a -> a)
-> (forall a. Num a => Template a -> a)
-> (forall a. Num a => Template a -> a)
-> Foldable Template
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
$cfold :: forall m. Monoid m => Template m -> m
fold :: forall m. Monoid m => Template m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> Template a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> Template a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Template a -> a
foldr1 :: forall a. (a -> a -> a) -> Template a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Template a -> a
foldl1 :: forall a. (a -> a -> a) -> Template a -> a
$ctoList :: forall a. Template a -> [a]
toList :: forall a. Template a -> [a]
$cnull :: forall a. Template a -> Bool
null :: forall a. Template a -> Bool
$clength :: forall a. Template a -> Int
length :: forall a. Template a -> Int
$celem :: forall a. Eq a => a -> Template a -> Bool
elem :: forall a. Eq a => a -> Template a -> Bool
$cmaximum :: forall a. Ord a => Template a -> a
maximum :: forall a. Ord a => Template a -> a
$cminimum :: forall a. Ord a => Template a -> a
minimum :: forall a. Ord a => Template a -> a
$csum :: forall a. Num a => Template a -> a
sum :: forall a. Num a => Template a -> a
$cproduct :: forall a. Num a => Template a -> a
product :: forall a. Num a => Template a -> a
F.Foldable, Functor Template
Foldable Template
(Functor Template, Foldable Template) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Template a -> f (Template b))
-> (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 (m :: * -> *) a.
    Monad m =>
    Template (m a) -> m (Template a))
-> Traversable 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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Template a -> f (Template b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Template a -> f (Template b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Template (f a) -> f (Template a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Template (f a) -> f (Template a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Template a -> m (Template b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Template a -> m (Template b)
$csequence :: forall (m :: * -> *) a. Monad m => Template (m a) -> m (Template a)
sequence :: forall (m :: * -> *) a. Monad m => Template (m a) -> m (Template a)
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
<+> Tidy -> a -> 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
<+> Tidy -> a -> 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
<+> Tidy -> a -> 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
_            = Maybe SrcSpan -> String -> t
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
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) = SpecType -> Template SpecType
forall a. a -> Template a
Asserted (SpecType -> Template SpecType)
-> StateT CGInfo Identity SpecType -> CG (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> StateT CGInfo Identity SpecType
addPost CGEnv
γ SpecType
t
addPostTemplate CGEnv
γ (Assumed  SpecType
t) = SpecType -> Template SpecType
forall a. a -> Template a
Assumed  (SpecType -> Template SpecType)
-> StateT CGInfo Identity SpecType -> CG (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> StateT CGInfo Identity SpecType
addPost CGEnv
γ SpecType
t
addPostTemplate CGEnv
γ (Internal SpecType
t) = SpecType -> Template SpecType
forall a. a -> Template a
Internal (SpecType -> Template SpecType)
-> StateT CGInfo Identity SpecType -> CG (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CGEnv -> SpecType -> StateT CGInfo Identity SpecType
addPost CGEnv
γ SpecType
t
addPostTemplate CGEnv
_ Template SpecType
Unknown      = Template SpecType -> CG (Template SpecType)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Template SpecType
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
_           = Maybe SrcSpan -> String -> t
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> t) -> String -> t
forall a b. (a -> b) -> a -> b
$ String
"safeFromAsserted:" String -> ShowS
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) CG (Template SpecType)
-> (Template SpecType -> CG (Template SpecType))
-> CG (Template SpecType)
forall a b.
StateT CGInfo Identity a
-> (a -> StateT CGInfo Identity b) -> StateT CGInfo Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SpecType -> StateT CGInfo Identity SpecType)
-> Template SpecType -> CG (Template SpecType)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Template a -> m (Template b)
mapM (Var -> SpecType -> StateT CGInfo Identity 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 (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (CGEnv -> REnv
grtys CGEnv
γ), Symbol -> REnv -> Maybe SpecType
lookupREnv (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (CGEnv -> REnv
assms CGEnv
γ), Symbol -> REnv -> Maybe SpecType
lookupREnv (Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Var
x) (CGEnv -> REnv
intys CGEnv
γ)) of
      (Maybe CoreExpr
_, Just SpecType
t, Maybe SpecType
_, Maybe SpecType
_) -> SpecType -> Template SpecType
forall a. a -> Template a
Asserted (SpecType -> Template SpecType)
-> StateT CGInfo Identity SpecType -> CG (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> StateT CGInfo Identity SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Maybe CoreExpr
_, Maybe SpecType
_, Maybe SpecType
_, Just SpecType
t) -> SpecType -> Template SpecType
forall a. a -> Template a
Internal (SpecType -> Template SpecType)
-> StateT CGInfo Identity SpecType -> CG (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> StateT CGInfo Identity SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Maybe CoreExpr
_, Maybe SpecType
_, Just SpecType
t, Maybe SpecType
_) -> SpecType -> Template SpecType
forall a. a -> Template a
Assumed  (SpecType -> Template SpecType)
-> StateT CGInfo Identity SpecType -> CG (Template SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, SpecType) -> StateT CGInfo Identity SpecType
refreshArgsTop (Var
x, SpecType
t)
      (Just CoreExpr
e, Maybe SpecType
_, Maybe SpecType
_, Maybe SpecType
_) -> do t <- Bool
-> KVKind -> CoreExpr -> Type -> StateT CGInfo Identity SpecType
freshTyExpr (Config -> Bool
typeclass (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ)) (Var -> KVKind
RecBindE Var
x) CoreExpr
e (HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e)
                              addW (WfC γ t)
                              Asserted <$> refreshArgsTop (x, t)
      (Maybe CoreExpr
_,      Maybe SpecType
_, Maybe SpecType
_, Maybe SpecType
_) -> Template SpecType -> CG (Template SpecType)
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Template SpecType
forall a. Template a
Unknown

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

derivedVar :: TargetSrc -> Var -> Bool
derivedVar :: TargetSrc -> Var -> Bool
derivedVar TargetSrc
src Var
x = Var -> HashSet Var -> Bool
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 (a -> Symbol
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", a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
x, SpecType
t')
      Maybe SpecType
_       -> CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> CG CGEnv
+= (String
"extender", a -> Symbol
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", a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
x, SpecType
t)
extender CGEnv
γ (a, Template SpecType)
_
  = CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ