module Agda.TypeChecking.Monad.State where
import Control.Applicative
import Control.Monad.State
import Data.Set (Set)
import qualified Data.Set as Set
import Agda.Syntax.Common
import Agda.Syntax.Scope.Base
import qualified Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Abstract.Name
import Agda.TypeChecking.Monad.Base
import Agda.Utils.Hash
resetState :: MonadTCM tcm => tcm ()
resetState = liftTCM $ do
opts <- stPersistentOptions <$> get
put $ initState { stPersistentOptions = opts }
setScope :: MonadTCM tcm => ScopeInfo -> tcm ()
setScope scope = liftTCM $ modify $ \s -> s { stScope = scope }
getScope :: MonadTCM tcm => tcm ScopeInfo
getScope = liftTCM $ gets stScope
modifyScope :: MonadTCM tcm => (ScopeInfo -> ScopeInfo) -> tcm ()
modifyScope f = do
s <- getScope
setScope $ f s
withScope :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm (a, ScopeInfo)
withScope s m = do
s' <- getScope
setScope s
x <- m
s'' <- getScope
setScope s'
return (x, s'')
withScope_ :: MonadTCM tcm => ScopeInfo -> tcm a -> tcm a
withScope_ s m = fst <$> withScope s m
localScope :: MonadTCM tcm => tcm a -> tcm a
localScope m = do
scope <- getScope
x <- m
setScope scope
return x
setTopLevelModule :: MonadTCM tcm => C.QName -> tcm ()
setTopLevelModule x =
modify $ \s -> s
{ stFreshThings = (stFreshThings s)
{ fName = NameId 0 $ hash (show x)
}
}
withTopLevelModule :: MonadTCM tcm => C.QName -> tcm a -> tcm a
withTopLevelModule x m = do
next <- gets $ fName . stFreshThings
setTopLevelModule x
y <- m
modify $ \s -> s { stFreshThings = (stFreshThings s) { fName = next } }
return y
addHaskellImport :: MonadTCM tcm => String -> tcm ()
addHaskellImport i =
modify $ \s -> s { stHaskellImports = Set.insert i $ stHaskellImports s }
getHaskellImports :: MonadTCM tcm => tcm (Set String)
getHaskellImports = gets stHaskellImports