module Agda.TypeChecking.Monad.State where
import Control.Arrow ((***), first, second)
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.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Base.Benchmark
import Agda.TypeChecking.Monad.Options
import Agda.Utils.Hash
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Lens
import Agda.Utils.Monad (bracket_, modify')
import Agda.Utils.Pretty
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
resetState :: TCM ()
resetState = do
pers <- gets stPersistentState
put $ initState { stPersistentState = 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
localTCStateSaving :: TCM a -> TCM (a, TCState)
localTCStateSaving compute = do
state <- get
result <- compute
newState <- get
do
b <- getBenchmark
put state
modifyBenchmark $ const b
return (result, newState)
lensPersistentState :: Lens' PersistentTCState TCState
lensPersistentState f s =
f (stPersistentState s) <&> \ p -> s { stPersistentState = p }
updatePersistentState
:: (PersistentTCState -> PersistentTCState) -> (TCState -> TCState)
updatePersistentState f s = s { stPersistentState = f (stPersistentState s) }
modifyPersistentState :: (PersistentTCState -> PersistentTCState) -> TCM ()
modifyPersistentState = modify . updatePersistentState
lensAccumStatisticsP :: Lens' Statistics PersistentTCState
lensAccumStatisticsP f s = f (stAccumStatistics s) <&> \ a ->
s { stAccumStatistics = a }
lensAccumStatistics :: Lens' Statistics TCState
lensAccumStatistics = lensPersistentState . lensAccumStatisticsP
getScope :: TCM ScopeInfo
getScope = use stScope
setScope :: ScopeInfo -> TCM ()
setScope scope = modifyScope (const scope)
modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()
modifyScope f = stScope %= f
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 ]
modifySignature :: (Signature -> Signature) -> TCM ()
modifySignature f = stSignature %= f
modifyImportedSignature :: (Signature -> Signature) -> TCM ()
modifyImportedSignature f = stImports %= f
getSignature :: TCM Signature
getSignature = use stSignature
getImportedSignature :: TCM Signature
getImportedSignature = use stImports
setSignature :: Signature -> TCM ()
setSignature sig = modifySignature $ const sig
setImportedSignature :: Signature -> TCM ()
setImportedSignature sig = stImports .= sig
withSignature :: Signature -> TCM a -> TCM a
withSignature sig m = do
sig0 <- getSignature
setSignature sig
r <- m
setSignature sig0
return r
lookupDefinition :: QName -> Signature -> Maybe Definition
lookupDefinition q sig = HMap.lookup q $ sigDefinitions sig
updateDefinitions :: (Definitions -> Definitions) -> Signature -> Signature
updateDefinitions f sig = sig { sigDefinitions = f (sigDefinitions sig) }
updateDefinition :: QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition q f = updateDefinitions $ HMap.adjust f q
updateTheDef :: (Defn -> Defn) -> (Definition -> Definition)
updateTheDef f def = def { theDef = f (theDef def) }
updateDefType :: (Type -> Type) -> (Definition -> Definition)
updateDefType f def = def { defType = f (defType def) }
updateDefArgOccurrences :: ([Occurrence] -> [Occurrence]) -> (Definition -> Definition)
updateDefArgOccurrences f def = def { defArgOccurrences = f (defArgOccurrences def) }
updateDefPolarity :: ([Polarity] -> [Polarity]) -> (Definition -> Definition)
updateDefPolarity f def = def { defPolarity = f (defPolarity def) }
updateDefCompiledRep :: (CompiledRepresentation -> CompiledRepresentation) -> (Definition -> Definition)
updateDefCompiledRep f def = def { defCompiledRep = f (defCompiledRep def) }
updateFunClauses :: ([Clause] -> [Clause]) -> (Defn -> Defn)
updateFunClauses f def@Function{ funClauses = cs} = def { funClauses = f cs }
updateFunClauses f _ = __IMPOSSIBLE__
setTopLevelModule :: C.QName -> TCM ()
setTopLevelModule x = stFreshNameId .= NameId 0 (hashString (show x))
withTopLevelModule :: C.QName -> TCM a -> TCM a
withTopLevelModule x m = do
next <- use stFreshNameId
setTopLevelModule x
y <- m
stFreshNameId .= next
return y
addHaskellImport :: String -> TCM ()
addHaskellImport i = stHaskellImports %= Set.insert i
getHaskellImports :: TCM (Set String)
getHaskellImports = use stHaskellImports
getInteractionOutputCallback :: TCM InteractionOutputCallback
getInteractionOutputCallback
= gets $ stInteractionOutputCallback . stPersistentState
appInteractionOutputCallback :: Response -> TCM ()
appInteractionOutputCallback r
= getInteractionOutputCallback >>= \ cb -> cb r
setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
setInteractionOutputCallback cb
= modifyPersistentState $ \ s -> s { stInteractionOutputCallback = cb }
getPatternSyns :: TCM PatternSynDefns
getPatternSyns = use stPatternSyns
setPatternSyns :: PatternSynDefns -> TCM ()
setPatternSyns m = modifyPatternSyns (const m)
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns f = stPatternSyns %= f
getPatternSynImports :: TCM PatternSynDefns
getPatternSynImports = use 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 . stPersistentState
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
a <- use lensAccumStatistics
let s = updateBenchmark (const b)
. set lensAccumStatistics a
$ 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
lensAccumStatistics .= (s^.lensAccumStatistics)
return $ Right a
addSignatureInstances :: Signature -> TCM ()
addSignatureInstances sig = do
let itable = Map.fromListWith (++)
[ (c, [i]) | (i, Defn{ defInstance = Just c }) <- HMap.toList $ sigDefinitions sig ]
modifyInstanceDefs $ first $ Map.unionWith (++) itable
updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> (TCState -> TCState)
updateInstanceDefs = over stInstanceDefs
modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs = modify . updateInstanceDefs
getAllInstanceDefs :: TCM TempInstanceTable
getAllInstanceDefs = use stInstanceDefs
getAnonInstanceDefs :: TCM [QName]
getAnonInstanceDefs = snd <$> getAllInstanceDefs
clearAnonInstanceDefs :: TCM ()
clearAnonInstanceDefs = modifyInstanceDefs $ mapSnd $ const []
addUnknownInstance :: QName -> TCM ()
addUnknownInstance x = do
reportSLn "tc.decl.instance" 10 $ "adding definition " ++ show x ++ " to the instance table (the type is not yet known)"
modifyInstanceDefs $ mapSnd (x:)
addNamedInstance
:: QName
-> QName
-> TCM ()
addNamedInstance x n = do
reportSLn "tc.decl.instance" 10 $ ("adding definition " ++ show x ++ " to instance table for " ++ show n)
modifySignature $ updateDefinition x $ \ d -> d { defInstance = Just n }
modifyInstanceDefs $ mapFst $ Map.insertWith (++) n [x]