-- | This module contains various functions that add/update in the CG monad.

{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE BangPatterns              #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE ImplicitParams            #-}
{-# LANGUAGE FlexibleContexts          #-}

module Language.Haskell.Liquid.Constraint.Monad  where

import           Var
import           Name (getSrcSpan)
import           SrcLoc
import           Outputable hiding (showPpr, panic, (<>), showSDoc, text)

import qualified TyCon as TC

import qualified Data.HashMap.Strict as M
import qualified Data.Text           as T

import           Control.Monad
import           Control.Monad.State (get, modify)
import           Language.Haskell.Liquid.Types hiding (loc)
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Constraint.Env
import           Language.Fixpoint.Misc hiding (errorstar)
import           Language.Haskell.Liquid.GHC.Misc -- (concatMapM)
import           Language.Haskell.Liquid.GHC.SpanStack (srcSpan)

--------------------------------------------------------------------------------
-- | `addC` adds a subtyping constraint into the global pool.
--------------------------------------------------------------------------------
addC :: SubC -> String -> CG ()
--------------------------------------------------------------------------------
addC :: SubC -> String -> CG ()
addC c :: SubC
c@(SubC CGEnv
γ SpecType
t1 SpecType
t2) String
_msg
  | SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= SpecType -> Type
forall r. ToTypeable r => RRType r -> Type
toType SpecType
t2
  = Maybe SrcSpan -> String -> CG ()
forall a. Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ CGEnv -> SrcSpan
getLocation CGEnv
γ) (String -> CG ()) -> String -> CG ()
forall a b. (a -> b) -> a -> b
$ String
"addC: malformed constraint:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
_msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. PPrint a => a -> String
showpp SpecType
t1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n <: \n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. PPrint a => a -> String
showpp SpecType
t2 
  | Bool
otherwise
  = (CGInfo -> CGInfo) -> CG ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> CG ()) -> (CGInfo -> CGInfo) -> CG ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { hsCs :: [SubC]
hsCs  = SubC
c SubC -> [SubC] -> [SubC]
forall a. a -> [a] -> [a]
: (CGInfo -> [SubC]
hsCs CGInfo
s) }
 

addC SubC
c String
_msg
  = (CGInfo -> CGInfo) -> CG ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> CG ()) -> (CGInfo -> CGInfo) -> CG ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { hsCs :: [SubC]
hsCs  = SubC
c SubC -> [SubC] -> [SubC]
forall a. a -> [a] -> [a]
: CGInfo -> [SubC]
hsCs CGInfo
s }

--------------------------------------------------------------------------------
-- | addPost: RJ: what DOES this function do?
--------------------------------------------------------------------------------
addPost :: CGEnv -> SpecType -> CG SpecType
--------------------------------------------------------------------------------
addPost :: CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ (RRTy [(Symbol, SpecType)]
e RReft
r Oblig
OInv SpecType
t)
  = do CGEnv
γ' <- (CGEnv -> (Symbol, SpecType) -> StateT CGInfo Identity CGEnv)
-> CGEnv -> [(Symbol, SpecType)] -> StateT CGInfo Identity CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\CGEnv
γ (Symbol
x, SpecType
t) -> CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> StateT CGInfo Identity CGEnv
`addSEnv` (String
"addPost", Symbol
x,SpecType
t)) CGEnv
γ [(Symbol, SpecType)]
e
       SubC -> String -> CG ()
addC (CGEnv -> Oblig -> RReft -> SubC
SubR CGEnv
γ' Oblig
OInv RReft
r) String
"precondition-oinv" CG () -> CG SpecType -> CG SpecType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SpecType -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

addPost CGEnv
γ (RRTy [(Symbol, SpecType)]
e RReft
r Oblig
OTerm SpecType
t)
  = do CGEnv
γ' <- (CGEnv -> (Symbol, SpecType) -> StateT CGInfo Identity CGEnv)
-> CGEnv -> [(Symbol, SpecType)] -> StateT CGInfo Identity CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\CGEnv
γ (Symbol
x, SpecType
t) -> CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> StateT CGInfo Identity CGEnv
+= (String
"addPost", Symbol
x, SpecType
t)) CGEnv
γ [(Symbol, SpecType)]
e
       SubC -> String -> CG ()
addC (CGEnv -> Oblig -> RReft -> SubC
SubR CGEnv
γ' Oblig
OTerm RReft
r) String
"precondition-oterm" CG () -> CG SpecType -> CG SpecType
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SpecType -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

addPost CGEnv
γ (RRTy [(Symbol, SpecType)]
cts RReft
_ Oblig
OCons SpecType
t)
  = do CGEnv
γ' <- (CGEnv -> (Symbol, SpecType) -> StateT CGInfo Identity CGEnv)
-> CGEnv -> [(Symbol, SpecType)] -> StateT CGInfo Identity CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\CGEnv
γ (Symbol
x, SpecType
t) -> CGEnv
γ CGEnv -> (String, Symbol, SpecType) -> StateT CGInfo Identity CGEnv
`addSEnv` (String
"splitS", Symbol
x,SpecType
t)) CGEnv
γ [(Symbol, SpecType)]
xts
       SubC -> String -> CG ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC  CGEnv
γ' SpecType
t1 SpecType
t2)  String
"precondition-ocons"
       CGEnv -> SpecType -> CG SpecType
addPost CGEnv
γ SpecType
t
  where
    ([(Symbol, SpecType)]
xts, SpecType
t1, SpecType
t2) = [(Symbol, SpecType)] -> ([(Symbol, SpecType)], SpecType, SpecType)
forall a b. [(a, b)] -> ([(a, b)], b, b)
envToSub [(Symbol, SpecType)]
cts
addPost CGEnv
_ SpecType
t 
  = SpecType -> CG SpecType
forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t 

--------------------------------------------------------------------------------
-- | Add Well formedness Constraint
--------------------------------------------------------------------------------
addW   :: WfC -> CG ()
--------------------------------------------------------------------------------
addW :: WfC -> CG ()
addW !WfC
w = (CGInfo -> CGInfo) -> CG ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> CG ()) -> (CGInfo -> CGInfo) -> CG ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { hsWfs :: [WfC]
hsWfs = WfC
w WfC -> [WfC] -> [WfC]
forall a. a -> [a] -> [a]
: (CGInfo -> [WfC]
hsWfs CGInfo
s) }

--------------------------------------------------------------------------------
-- | Add a warning
--------------------------------------------------------------------------------
addWarning   :: Error -> CG ()
--------------------------------------------------------------------------------
addWarning :: Error -> CG ()
addWarning Error
w = (CGInfo -> CGInfo) -> CG ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> CG ()) -> (CGInfo -> CGInfo) -> CG ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { logErrors :: [Error]
logErrors = Error
w Error -> [Error] -> [Error]
forall a. a -> [a] -> [a]
: CGInfo -> [Error]
logErrors CGInfo
s }

-- | Add Identifier Annotations, used for annotation binders (i.e. at binder sites)
addIdA            :: Var -> Annot SpecType -> CG ()
addIdA :: Var -> Annot SpecType -> CG ()
addIdA !Var
x !Annot SpecType
t      = (CGInfo -> CGInfo) -> CG ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> CG ()) -> (CGInfo -> CGInfo) -> CG ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { annotMap :: AnnInfo (Annot SpecType)
annotMap = AnnInfo (Annot SpecType) -> AnnInfo (Annot SpecType)
upd (AnnInfo (Annot SpecType) -> AnnInfo (Annot SpecType))
-> AnnInfo (Annot SpecType) -> AnnInfo (Annot SpecType)
forall a b. (a -> b) -> a -> b
$ CGInfo -> AnnInfo (Annot SpecType)
annotMap CGInfo
s }
  where
    l :: SrcSpan
l             = Var -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan Var
x
    upd :: AnnInfo (Annot SpecType) -> AnnInfo (Annot SpecType)
upd m :: AnnInfo (Annot SpecType)
m@(AI HashMap SrcSpan [(Maybe Text, Annot SpecType)]
_)  = if SrcSpan -> AnnInfo (Annot SpecType) -> Bool
forall a. SrcSpan -> AnnInfo (Annot a) -> Bool
boundRecVar SrcSpan
l AnnInfo (Annot SpecType)
m then AnnInfo (Annot SpecType)
m else SrcSpan
-> Maybe Var
-> Annot SpecType
-> AnnInfo (Annot SpecType)
-> AnnInfo (Annot SpecType)
forall a b.
Outputable a =>
SrcSpan -> Maybe a -> b -> AnnInfo b -> AnnInfo b
addA SrcSpan
l (Var -> Maybe Var
forall a. a -> Maybe a
Just Var
x) Annot SpecType
t AnnInfo (Annot SpecType)
m

boundRecVar :: SrcSpan -> AnnInfo (Annot a) -> Bool
boundRecVar :: SrcSpan -> AnnInfo (Annot a) -> Bool
boundRecVar SrcSpan
l (AI HashMap SrcSpan [(Maybe Text, Annot a)]
m) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a
t | (Maybe Text
_, AnnRDf a
t) <- [(Maybe Text, Annot a)]
-> SrcSpan
-> HashMap SrcSpan [(Maybe Text, Annot a)]
-> [(Maybe Text, Annot a)]
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] SrcSpan
l HashMap SrcSpan [(Maybe Text, Annot a)]
m]


-- | Used for annotating reads (i.e. at Var x sites)

addLocA :: Maybe Var -> SrcSpan -> Annot SpecType -> CG ()
addLocA :: Maybe Var -> SrcSpan -> Annot SpecType -> CG ()
addLocA !Maybe Var
xo !SrcSpan
l !Annot SpecType
t
  = (CGInfo -> CGInfo) -> CG ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> CG ()) -> (CGInfo -> CGInfo) -> CG ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { annotMap :: AnnInfo (Annot SpecType)
annotMap = SrcSpan
-> Maybe Var
-> Annot SpecType
-> AnnInfo (Annot SpecType)
-> AnnInfo (Annot SpecType)
forall a b.
Outputable a =>
SrcSpan -> Maybe a -> b -> AnnInfo b -> AnnInfo b
addA SrcSpan
l Maybe Var
xo Annot SpecType
t (AnnInfo (Annot SpecType) -> AnnInfo (Annot SpecType))
-> AnnInfo (Annot SpecType) -> AnnInfo (Annot SpecType)
forall a b. (a -> b) -> a -> b
$ CGInfo -> AnnInfo (Annot SpecType)
annotMap CGInfo
s }


-- | Used for annotating holes 

addHole :: Var -> SpecType -> CGEnv -> CG () 
addHole :: Var -> SpecType -> CGEnv -> CG ()
addHole Var
x SpecType
t CGEnv
γ 
  | Config -> Bool
typedHoles (CGEnv -> Config
forall t. HasConfig t => t -> Config
getConfig CGEnv
γ) = 
      do  CGInfo
st <- StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get 
          (CGInfo -> CGInfo) -> CG ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CGInfo -> CGInfo) -> CG ()) -> (CGInfo -> CGInfo) -> CG ()
forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s {holesMap :: HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
holesMap = Var
-> HoleInfo (CGInfo, CGEnv) SpecType
-> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
-> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Var
x ((CGInfo, CGEnv) -> HoleInfo (CGInfo, CGEnv) SpecType
forall i. i -> HoleInfo i SpecType
hinfo (CGInfo
st, CGEnv
γ)) (HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
 -> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType))
-> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
-> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
forall a b. (a -> b) -> a -> b
$ CGInfo -> HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType)
holesMap CGInfo
s}
          -- addWarning $ ErrHole loc ("hole found") (reGlobal env <> reLocal env) x' t 
  | Bool
otherwise = () -> CG ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    where 
      hinfo :: i -> HoleInfo i SpecType
hinfo = SpecType -> SrcSpan -> AREnv SpecType -> i -> HoleInfo i SpecType
forall i t. t -> SrcSpan -> AREnv t -> i -> HoleInfo i t
HoleInfo SpecType
t SrcSpan
loc AREnv SpecType
env
      loc :: SrcSpan
loc   = SpanStack -> SrcSpan
srcSpan (SpanStack -> SrcSpan) -> SpanStack -> SrcSpan
forall a b. (a -> b) -> a -> b
$ CGEnv -> SpanStack
cgLoc CGEnv
γ
      env :: AREnv SpecType
env   = [AREnv SpecType] -> AREnv SpecType
forall a. Monoid a => [a] -> a
mconcat [CGEnv -> AREnv SpecType
renv CGEnv
γ, CGEnv -> AREnv SpecType
grtys CGEnv
γ, CGEnv -> AREnv SpecType
assms CGEnv
γ, CGEnv -> AREnv SpecType
intys CGEnv
γ]

--------------------------------------------------------------------------------
-- | Update annotations for a location, due to (ghost) predicate applications
--------------------------------------------------------------------------------
updateLocA :: Maybe SrcSpan -> SpecType -> CG ()
--------------------------------------------------------------------------------
updateLocA :: Maybe SrcSpan -> SpecType -> CG ()
updateLocA (Just SrcSpan
l) SpecType
t = Maybe Var -> SrcSpan -> Annot SpecType -> CG ()
addLocA Maybe Var
forall a. Maybe a
Nothing SrcSpan
l (SpecType -> Annot SpecType
forall t. t -> Annot t
AnnUse SpecType
t)
updateLocA Maybe SrcSpan
_        SpecType
_ = () -> CG ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
addA :: (Outputable a) => SrcSpan -> Maybe a -> b -> AnnInfo b -> AnnInfo b
--------------------------------------------------------------------------------
addA :: SrcSpan -> Maybe a -> b -> AnnInfo b -> AnnInfo b
addA !SrcSpan
l xo :: Maybe a
xo@(Just a
_) !b
t (AI HashMap SrcSpan [(Maybe Text, b)]
m)
  | SrcSpan -> Bool
isGoodSrcSpan SrcSpan
l
  = HashMap SrcSpan [(Maybe Text, b)] -> AnnInfo b
forall a. HashMap SrcSpan [(Maybe Text, a)] -> AnnInfo a
AI (HashMap SrcSpan [(Maybe Text, b)] -> AnnInfo b)
-> HashMap SrcSpan [(Maybe Text, b)] -> AnnInfo b
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> (Maybe Text, b)
-> HashMap SrcSpan [(Maybe Text, b)]
-> HashMap SrcSpan [(Maybe Text, b)]
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k [v] -> HashMap k [v]
inserts SrcSpan
l (String -> Text
T.pack (String -> Text) -> (a -> String) -> a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Outputable a => a -> String
showPpr (a -> Text) -> Maybe a -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
xo, b
t) HashMap SrcSpan [(Maybe Text, b)]
m
addA !SrcSpan
l xo :: Maybe a
xo@Maybe a
Nothing  !b
t (AI HashMap SrcSpan [(Maybe Text, b)]
m)
  | SrcSpan
l SrcSpan -> HashMap SrcSpan [(Maybe Text, b)] -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
`M.member` HashMap SrcSpan [(Maybe Text, b)]
m                  -- only spans known to be variables
  = HashMap SrcSpan [(Maybe Text, b)] -> AnnInfo b
forall a. HashMap SrcSpan [(Maybe Text, a)] -> AnnInfo a
AI (HashMap SrcSpan [(Maybe Text, b)] -> AnnInfo b)
-> HashMap SrcSpan [(Maybe Text, b)] -> AnnInfo b
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> (Maybe Text, b)
-> HashMap SrcSpan [(Maybe Text, b)]
-> HashMap SrcSpan [(Maybe Text, b)]
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k [v] -> HashMap k [v]
inserts SrcSpan
l (String -> Text
T.pack (String -> Text) -> (a -> String) -> a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Outputable a => a -> String
showPpr (a -> Text) -> Maybe a -> Maybe Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe a
xo, b
t) HashMap SrcSpan [(Maybe Text, b)]
m
addA SrcSpan
_ Maybe a
_ b
_ !AnnInfo b
a
  = AnnInfo b
a


lookupNewType :: TC.TyCon -> CG (Maybe SpecType)
lookupNewType :: TyCon -> CG (Maybe SpecType)
lookupNewType TyCon
tc
  = TyCon -> HashMap TyCon SpecType -> Maybe SpecType
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup TyCon
tc (HashMap TyCon SpecType -> Maybe SpecType)
-> (CGInfo -> HashMap TyCon SpecType) -> CGInfo -> Maybe SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGInfo -> HashMap TyCon SpecType
newTyEnv (CGInfo -> Maybe SpecType)
-> StateT CGInfo Identity CGInfo -> CG (Maybe SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get


--------------------------------------------------------------------------------
{-@ envToSub :: {v:[(a, b)] | 2 <= len v} -> ([(a, b)], b, b) @-}
envToSub :: [(a, b)] -> ([(a, b)], b, b)
--------------------------------------------------------------------------------
envToSub :: [(a, b)] -> ([(a, b)], b, b)
envToSub = [(a, b)] -> [(a, b)] -> ([(a, b)], b, b)
forall a c. [(a, c)] -> [(a, c)] -> ([(a, c)], c, c)
go []
  where
    go :: [(a, c)] -> [(a, c)] -> ([(a, c)], c, c)
go [(a, c)]
_   []              = Maybe SrcSpan -> String -> ([(a, c)], c, c)
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"This cannot happen: envToSub on 0 elems"
    go [(a, c)]
_   [(a
_,c
_)]         = Maybe SrcSpan -> String -> ([(a, c)], c, c)
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"This cannot happen: envToSub on 1 elem"
    go [(a, c)]
ack [(a
_,c
l), (a
_, c
r)] = ([(a, c)] -> [(a, c)]
forall a. [a] -> [a]
reverse [(a, c)]
ack, c
l, c
r)
    go [(a, c)]
ack ((a, c)
x:[(a, c)]
xs)          = [(a, c)] -> [(a, c)] -> ([(a, c)], c, c)
go ((a, c)
x(a, c) -> [(a, c)] -> [(a, c)]
forall a. a -> [a] -> [a]
:[(a, c)]
ack) [(a, c)]
xs