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

{-# LANGUAGE BangPatterns              #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE FlexibleContexts          #-}

module Language.Haskell.Liquid.Constraint.Monad  where

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

import           Control.Monad
import           Control.Monad.State (gets, modify)
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.Types
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           Liquid.GHC.API as Ghc hiding (panic, showPpr)

--------------------------------------------------------------------------------
-- | `addC` adds a subtyping constraint into the global pool.
--------------------------------------------------------------------------------
addC :: SubC -> String -> CG ()
--------------------------------------------------------------------------------
addC :: SubC -> [Char] -> CG ()
addC c :: SubC
c@(SubC CGEnv
γ SpecType
t1 SpecType
t2) [Char]
_msg =
  let tt1 :: Type
tt1 = Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
t1
      tt2 :: Type
tt2 = Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
t2
   in if Type
tt1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
/= Type
tt2 then
        Maybe SrcSpan -> [Char] -> CG ()
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> 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
γ) ([Char] -> CG ()) -> [Char] -> CG ()
forall a b. (a -> b) -> a -> b
$
          [Char]
"addC: malformed constraint:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
_msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n---------\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
          Type -> [Char]
forall a. PPrint a => a -> [Char]
showpp Type
tt1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
          [Char]
"\n <: \n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
          Type -> [Char]
forall a. PPrint a => a -> [Char]
showpp Type
tt2
      else
        (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  = c : hsCs s }


addC SubC
c [Char]
_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  = c : hsCs s }

--------------------------------------------------------------------------------
-- | addPost: RJ: what DOES this function do?
--------------------------------------------------------------------------------
addPost :: CGEnv -> SpecType -> CG SpecType
--------------------------------------------------------------------------------
addPost :: CGEnv -> SpecType -> CG SpecType
addPost CGEnv
cgenv (RRTy [(Symbol, SpecType)]
e RReft
r Oblig
OInv SpecType
rt)
  = do γ' <- (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 -> ([Char], Symbol, SpecType) -> StateT CGInfo Identity CGEnv
`addSEnv` ([Char]
"addPost", Symbol
x,SpecType
t)) CGEnv
cgenv [(Symbol, SpecType)]
e
       addC (SubR γ' OInv r) "precondition-oinv" >> return rt

addPost CGEnv
cgenv (RRTy [(Symbol, SpecType)]
e RReft
r Oblig
OTerm SpecType
rt)
  = do γ' <- (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 -> ([Char], Symbol, SpecType) -> StateT CGInfo Identity CGEnv
+= ([Char]
"addPost", Symbol
x, SpecType
t)) CGEnv
cgenv [(Symbol, SpecType)]
e
       addC (SubR γ' OTerm r) "precondition-oterm" >> return rt

addPost CGEnv
cgenv (RRTy [(Symbol, SpecType)]
cts RReft
_ Oblig
OCons SpecType
rt)
  = do γ' <- (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 -> ([Char], Symbol, SpecType) -> StateT CGInfo Identity CGEnv
`addSEnv` ([Char]
"splitS", Symbol
x,SpecType
t)) CGEnv
cgenv [(Symbol, SpecType)]
xts
       addC (SubC  γ' t1 t2)  "precondition-ocons"
       addPost cgenv rt
  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 a. a -> StateT CGInfo Identity a
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 = w : hsWfs 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 = w : logErrors 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 = upd $ annotMap 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 :: forall a. 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 a. [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 = addA l xo t $ annotMap s }

--------------------------------------------------------------------------------
-- | 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 a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
addA :: (Outputable a) => SrcSpan -> Maybe a -> b -> AnnInfo b -> AnnInfo b
--------------------------------------------------------------------------------
addA :: forall a b.
Outputable a =>
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 ([Char] -> Text
T.pack ([Char] -> Text) -> (a -> [Char]) -> a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Char]
forall a. Outputable a => a -> [Char]
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 ([Char] -> Text
T.pack ([Char] -> Text) -> (a -> [Char]) -> a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Char]
forall a. Outputable a => a -> [Char]
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 :: Ghc.TyCon -> CG (Maybe SpecType)
lookupNewType :: TyCon -> CG (Maybe SpecType)
lookupNewType TyCon
tc
  = (CGInfo -> Maybe SpecType) -> CG (Maybe SpecType)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (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)


--------------------------------------------------------------------------------
{-@ envToSub :: {v:[(a, b)] | 2 <= len v} -> ([(a, b)], b, b) @-}
envToSub :: [(a, b)] -> ([(a, b)], b, b)
--------------------------------------------------------------------------------
envToSub :: forall a b. [(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 -> [Char] -> ([(a, c)], c, c)
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"This cannot happen: envToSub on 0 elems"
    go [(a, c)]
_   [(a
_,c
_)]         = Maybe SrcSpan -> [Char] -> ([(a, c)], c, c)
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"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