-- | 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 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           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
  | forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
t1 forall a. Eq a => a -> a -> Bool
/= forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
t2
  = forall a. Maybe SrcSpan -> [Char] -> a
panic (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ CGEnv -> SrcSpan
getLocation CGEnv
γ) forall a b. (a -> b) -> a -> b
$ [Char]
"addC: malformed constraint:\n" forall a. [a] -> [a] -> [a]
++ [Char]
_msg forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp SpecType
t1 forall a. [a] -> [a] -> [a]
++ [Char]
"\n <: \n" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp SpecType
t2
  | Bool
otherwise
  = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { hsCs :: [SubC]
hsCs  = SubC
c forall a. a -> [a] -> [a]
: CGInfo -> [SubC]
hsCs CGInfo
s }


addC SubC
c [Char]
_msg
  = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { hsCs :: [SubC]
hsCs  = SubC
c 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
cgenv (RRTy [(Symbol, SpecType)]
e RReft
r Oblig
OInv SpecType
rt)
  = do 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
       SubC -> [Char] -> CG ()
addC (CGEnv -> Oblig -> RReft -> SubC
SubR CGEnv
γ' Oblig
OInv RReft
r) [Char]
"precondition-oinv" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
rt

addPost CGEnv
cgenv (RRTy [(Symbol, SpecType)]
e RReft
r Oblig
OTerm SpecType
rt)
  = do 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
       SubC -> [Char] -> CG ()
addC (CGEnv -> Oblig -> RReft -> SubC
SubR CGEnv
γ' Oblig
OTerm RReft
r) [Char]
"precondition-oterm" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
rt

addPost CGEnv
cgenv (RRTy [(Symbol, SpecType)]
cts RReft
_ Oblig
OCons SpecType
rt)
  = do 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
       SubC -> [Char] -> CG ()
addC (CGEnv -> SpecType -> SpecType -> SubC
SubC  CGEnv
γ' SpecType
t1 SpecType
t2)  [Char]
"precondition-ocons"
       CGEnv -> SpecType -> CG SpecType
addPost CGEnv
cgenv SpecType
rt
  where
    ([(Symbol, SpecType)]
xts, SpecType
t1, SpecType
t2) = forall a b. [(a, b)] -> ([(a, b)], b, b)
envToSub [(Symbol, SpecType)]
cts
addPost CGEnv
_ SpecType
t
  = forall (m :: * -> *) a. Monad m => a -> m a
return SpecType
t

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

--------------------------------------------------------------------------------
-- | Add a warning
--------------------------------------------------------------------------------
addWarning   :: Error -> CG ()
--------------------------------------------------------------------------------
addWarning :: Error -> CG ()
addWarning Error
w = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { logErrors :: [Error]
logErrors = Error
w 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      = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { annotMap :: AnnInfo (Annot SpecType)
annotMap = AnnInfo (Annot SpecType) -> AnnInfo (Annot SpecType)
upd forall a b. (a -> b) -> a -> b
$ CGInfo -> AnnInfo (Annot SpecType)
annotMap CGInfo
s }
  where
    l :: SrcSpan
l             = 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 forall a. SrcSpan -> AnnInfo (Annot a) -> Bool
boundRecVar SrcSpan
l AnnInfo (Annot SpecType)
m then AnnInfo (Annot SpecType)
m else forall a b.
Outputable a =>
SrcSpan -> Maybe a -> b -> AnnInfo b -> AnnInfo b
addA SrcSpan
l (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 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a
t | (Maybe Text
_, AnnRDf a
t) <- 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
  = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CGInfo
s -> CGInfo
s { annotMap :: AnnInfo (Annot SpecType)
annotMap = forall a b.
Outputable a =>
SrcSpan -> Maybe a -> b -> AnnInfo b -> AnnInfo b
addA SrcSpan
l Maybe Var
xo Annot SpecType
t forall a b. (a -> b) -> a -> b
$ CGInfo -> AnnInfo (Annot SpecType)
annotMap CGInfo
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 forall a. Maybe a
Nothing SrcSpan
l (forall t. t -> Annot t
AnnUse SpecType
t)
updateLocA Maybe SrcSpan
_        SpecType
_ = 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
  = forall a. HashMap SrcSpan [(Maybe Text, a)] -> AnnInfo a
AI forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k [v] -> HashMap k [v]
inserts SrcSpan
l ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> [Char]
showPpr 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 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
  = forall a. HashMap SrcSpan [(Maybe Text, a)] -> AnnInfo a
AI forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k [v] -> HashMap k [v]
inserts SrcSpan
l ([Char] -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> [Char]
showPpr 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
  = forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup TyCon
tc 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 = 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)]
_   []              = forall a. Maybe SrcSpan -> [Char] -> a
impossible forall a. Maybe a
Nothing [Char]
"This cannot happen: envToSub on 0 elems"
    go [(a, c)]
_   [(a
_,c
_)]         = forall a. Maybe SrcSpan -> [Char] -> a
impossible forall a. Maybe a
Nothing [Char]
"This cannot happen: envToSub on 1 elem"
    go [(a, c)]
ack [(a
_,c
l), (a
_, c
r)] = (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)
xforall a. a -> [a] -> [a]
:[(a, c)]
ack) [(a, c)]
xs