module Agda.TypeChecking.Monad.State where
import Control.Applicative
import Control.Monad.State
import Data.Set (Set)
import Data.Map as Map
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 (PatternSynDefn, PatternSynDefns)
import Agda.Syntax.Abstract.Name
import Agda.TypeChecking.Monad.Base
import Agda.Utils.Hash
resetState :: TCM ()
resetState = do
pers <- stPersistent <$> get
put $ initState { stPersistent = pers }
resetAllState :: TCM ()
resetAllState = put initState
setScope :: ScopeInfo -> TCM ()
setScope scope = modify $ \s -> s { stScope = scope }
getScope :: TCM ScopeInfo
getScope = gets stScope
getPatternSyns :: TCM PatternSynDefns
getPatternSyns = gets stPatternSyns
setPatternSyns :: PatternSynDefns -> TCM ()
setPatternSyns m = modify $ \s -> s { stPatternSyns = m }
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns f = do
s <- getPatternSyns
setPatternSyns $ f s
getPatternSynImports :: TCM PatternSynDefns
getPatternSynImports = gets stPatternSynImports
lookupPatternSyn :: QName -> TCM PatternSynDefn
lookupPatternSyn x = do
s <- getPatternSyns
case Map.lookup x s of
Just d -> return d
Nothing -> do
si <- getPatternSynImports
case Map.lookup x si of
Just d -> return d
Nothing -> typeError $ NotInScope [qnameToConcrete x]
setExtLambdaTele :: Map QName (Int , Int) -> TCM ()
setExtLambdaTele tele = modify $ \s -> s { stExtLambdaTele = tele }
getExtLambdaTele :: TCM (Map QName (Int , Int))
getExtLambdaTele = gets stExtLambdaTele
addExtLambdaTele :: QName -> (Int , Int) -> TCM ()
addExtLambdaTele id x = getExtLambdaTele >>= setExtLambdaTele . (insert id x)
modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()
modifyScope f = do
s <- getScope
setScope $ f s
withScope :: ScopeInfo -> TCM a -> TCM (a, ScopeInfo)
withScope s m = do
s' <- getScope
setScope s
x <- m
s'' <- getScope
setScope s'
return (x, s'')
withScope_ :: ScopeInfo -> TCM a -> TCM a
withScope_ s m = fst <$> withScope s m
localScope :: TCM a -> TCM a
localScope m = do
scope <- getScope
x <- m
setScope scope
return x
setTopLevelModule :: C.QName -> TCM ()
setTopLevelModule x =
modify $ \s -> s
{ stFreshThings = (stFreshThings s)
{ fName = NameId 0 $ hash (show x)
}
}
withTopLevelModule :: 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 :: String -> TCM ()
addHaskellImport i =
modify $ \s -> s { stHaskellImports = Set.insert i $ stHaskellImports s }
getHaskellImports :: TCM (Set String)
getHaskellImports = gets stHaskellImports