module Agda.TypeChecking.Monad.State where
import Control.Applicative
import qualified Control.Exception as E
import Control.Monad.State
import Data.Set (Set)
import Data.Map as Map
import qualified Data.Set as Set
import Agda.Interaction.Response
(InteractionOutputCallback, Response)
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.TypeChecking.Monad.Base.Benchmark
import Agda.TypeChecking.Monad.Options
import Agda.Utils.Hash
import Agda.Utils.Monad (bracket_)
import Agda.Utils.Pretty
resetState :: TCM ()
resetState = do
pers <- gets stPersistent
put $ initState { stPersistent = pers }
resetAllState :: TCM ()
resetAllState = do
b <- getBenchmark
put $ updatePersistentState (\ s -> s { stBenchmark = b }) initState
localTCState :: TCM a -> TCM a
localTCState = bracket_ get $ \ s -> do
b <- getBenchmark
put s
modifyBenchmark $ const b
updatePersistentState :: (PersistentTCState -> PersistentTCState) -> (TCState -> TCState)
updatePersistentState f s = s { stPersistent = f (stPersistent s) }
modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
modifyPersistentState = modify . updatePersistentState
getScope :: TCM ScopeInfo
getScope = gets stScope
setScope :: ScopeInfo -> TCM ()
setScope scope = modifyScope (const scope)
modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()
modifyScope f = modify $ \ s -> s { stScope = f (stScope 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
notInScope :: C.QName -> TCM a
notInScope x = do
printScope "unbound" 5 ""
typeError $ NotInScope [x]
printScope :: String -> Int -> String -> TCM ()
printScope tag v s = verboseS ("scope." ++ tag) v $ do
scope <- getScope
reportSDoc ("scope." ++ tag) v $ return $ vcat [ text s, text $ show scope ]
setTopLevelModule :: C.QName -> TCM ()
setTopLevelModule x =
modify $ \s -> s
{ stFreshThings = (stFreshThings s)
{ fName = NameId 0 $ hashString (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
getInteractionOutputCallback :: TCM InteractionOutputCallback
getInteractionOutputCallback
= gets $ stInteractionOutputCallback . stPersistent
appInteractionOutputCallback :: Response -> TCM ()
appInteractionOutputCallback r
= getInteractionOutputCallback >>= \ cb -> cb r
setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
setInteractionOutputCallback cb
= modifyPersistentState $ \ s -> s { stInteractionOutputCallback = cb }
getPatternSyns :: TCM PatternSynDefns
getPatternSyns = gets stPatternSyns
setPatternSyns :: PatternSynDefns -> TCM ()
setPatternSyns m = modifyPatternSyns (const m)
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns f = modify $ \s -> s { stPatternSyns = f (stPatternSyns 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 -> notInScope $ qnameToConcrete x
theBenchmark :: TCState -> Benchmark
theBenchmark = stBenchmark . stPersistent
updateBenchmark :: (Benchmark -> Benchmark) -> TCState -> TCState
updateBenchmark f = updatePersistentState $ \ s -> s { stBenchmark = f (stBenchmark s) }
getBenchmark :: TCM Benchmark
getBenchmark = gets $ theBenchmark
modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
modifyBenchmark = modify . updateBenchmark
freshTCM :: TCM a -> TCM (Either TCErr a)
freshTCM m = do
b <- getBenchmark
let s = updateBenchmark (const b) initState
r <- liftIO $ (Right <$> runTCM initEnv s m) `E.catch` (return . Left)
case r of
Left err -> return $ Left err
Right (a, s) -> do
modifyBenchmark $ const $ theBenchmark s
return $ Right a