module Agda.TypeChecking.Monad.State where
import Control.Arrow (first)
import Control.Applicative
import qualified Control.Exception as E
import Control.Monad.State (put, get, gets, modify)
import Control.Monad.Trans (liftIO)
import Data.Map as Map
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import Agda.Benchmarking
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.Options
import Agda.TypeChecking.Positivity.Occurrence
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 = disableDestructiveUpdate . bracket_ get (\ s -> do
b <- getBenchmark
put s
modifyBenchmark $ const b)
localTCStateSaving :: TCM a -> TCM (a, TCState)
localTCStateSaving compute = do
oldState <- get
result <- compute
newState <- get
do
b <- getBenchmark
put oldState
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
modifyScope :: (ScopeInfo -> ScopeInfo) -> TCM ()
modifyScope f = modifyScope_ (recomputeInverseScopeMaps . 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
modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM ()
modifyGlobalDefinition q f = modifySignature (updateDefinition q f) >>
modifyImportedSignature (updateDefinition q f)
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
addRewriteRulesFor :: QName -> RewriteRules -> Signature -> Signature
addRewriteRulesFor f rews =
(over sigRewriteRules $ HMap.insertWith mappend f rews)
. (updateDefinition f $ updateTheDef setNotInjective)
where
setNotInjective def@Function{} = def { funInv = NotInjective }
setNotInjective def = def
lookupDefinition :: QName -> Signature -> Maybe Definition
lookupDefinition q sig = HMap.lookup q $ sig ^. sigDefinitions
updateDefinitions :: (Definitions -> Definitions) -> Signature -> Signature
updateDefinitions = over sigDefinitions
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
addHaskellImportUHC :: String -> TCM ()
addHaskellImportUHC i = stHaskellImportsUHC %= Set.insert i
getHaskellImportsUHC :: TCM (Set String)
getHaskellImportsUHC = use stHaskellImportsUHC
addInlineHaskell :: String -> TCM ()
addInlineHaskell s = stHaskellCode %= (s :)
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 $ sig ^. sigDefinitions ]
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]