{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
module Agda.TypeChecking.Monad.State where
import Control.Arrow (first)
import qualified Control.Exception as E
import Control.Monad.Reader (asks)
import Control.Monad.State (put, get, gets, modify, modify')
import Control.Monad.Trans (liftIO)
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Traversable (traverse)
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.PatternSynonyms
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Warnings
import {-# SOURCE #-} Agda.TypeChecking.Monad.Debug
import {-# SOURCE #-} Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.CompiledClause
import Agda.Utils.Hash
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Lens
import Agda.Utils.Monad (bracket_)
import Agda.Utils.NonemptyList
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
backends <- use stBackends
put $ updatePersistentState (\ s -> s { stBenchmark = b }) initState
stBackends .= backends
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)
freshTCM :: TCM a -> TCM (Either TCErr a)
freshTCM m = do
ps <- use lensPersistentState
let s = set lensPersistentState ps initState
r <- liftIO $ (Right <$> runTCM initEnv s m) `E.catch` (return . Left)
case r of
Right (a, s) -> do
lensPersistentState .= s ^. lensPersistentState
return $ Right a
Left err -> do
case err of
TypeError { tcErrState = s } ->
lensPersistentState .= s ^. lensPersistentState
IOException s _ _ ->
lensPersistentState .= s ^. lensPersistentState
_ -> return ()
return $ Left err
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, pretty scope ]
modifySignature :: (Signature -> Signature) -> TCM ()
modifySignature f = stSignature %= f
modifyImportedSignature :: (Signature -> Signature) -> TCM ()
modifyImportedSignature f = stImports %= f
getSignature :: TCM Signature
getSignature = use stSignature
modifyGlobalDefinition :: QName -> (Definition -> Definition) -> TCM ()
modifyGlobalDefinition q f = do
modifySignature $ updateDefinition q f
modifyImportedSignature $ updateDefinition q f
setSignature :: Signature -> TCM ()
setSignature sig = modifySignature $ const sig
withSignature :: Signature -> TCM a -> TCM a
withSignature sig m = do
sig0 <- getSignature
setSignature sig
r <- m
setSignature sig0
return r
addRewriteRulesFor :: QName -> RewriteRules -> [QName] -> Signature -> Signature
addRewriteRulesFor f rews matchables =
(over sigRewriteRules $ HMap.insertWith mappend f rews)
. (updateDefinition f $ updateTheDef setNotInjective)
. (foldr (.) id $ map (\g -> updateDefinition g setMatchable) matchables)
where
setNotInjective def@Function{} = def { funInv = NotInjective }
setNotInjective def = def
setMatchable def = def { defMatchable = True }
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) }
addCompilerPragma :: BackendName -> CompilerPragma -> Definition -> Definition
addCompilerPragma backend pragma = updateDefCompiledRep $ Map.insertWith (++) backend [pragma]
updateFunClauses :: ([Clause] -> [Clause]) -> (Defn -> Defn)
updateFunClauses f def@Function{ funClauses = cs} = def { funClauses = f cs }
updateFunClauses f _ = __IMPOSSIBLE__
updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> (Defn -> Defn)
updateCompiledClauses f def@Function{ funCompiled = cc} = def { funCompiled = f cc }
updateCompiledClauses f _ = __IMPOSSIBLE__
updateFunCopatternLHS :: (Bool -> Bool) -> Defn -> Defn
updateFunCopatternLHS f def@Function{ funCopatternLHS = b } = def { funCopatternLHS = f b }
updateFunCopatternLHS f _ = __IMPOSSIBLE__
setTopLevelModule :: C.QName -> TCM ()
setTopLevelModule x = stFreshNameId .= NameId 0 (hashString $ prettyShow x)
withTopLevelModule :: C.QName -> TCM a -> TCM a
withTopLevelModule x m = do
next <- use stFreshNameId
setTopLevelModule x
y <- m
stFreshNameId .= next
return y
addForeignCode :: BackendName -> String -> TCM ()
addForeignCode backend code = do
r <- asks envRange
stForeignCode . key backend %= Just . (ForeignCode r code :) . fromMaybe []
addDeprecatedForeignCode :: String -> BackendName -> String -> TCM ()
addDeprecatedForeignCode old backend code = do
warning $ DeprecationWarning (unwords ["The", old, "pragma"])
foreignPragma "2.6"
addForeignCode backend code
where
spc | length (lines code) > 1 = "\n"
| otherwise = " "
foreignPragma =
"{-# FOREIGN " ++ backend ++ spc ++ code ++ spc ++ "#-}"
addHaskellImport :: String -> TCM ()
addHaskellImport i = addDeprecatedForeignCode "IMPORT" ghcBackendName $ "import qualified " ++ i
addHaskellImportUHC :: String -> TCM ()
addHaskellImportUHC i = addDeprecatedForeignCode "IMPORT_UHC" ghcBackendName $ "__IMPORT__ " ++ i
addInlineHaskell :: String -> TCM ()
addInlineHaskell s = addDeprecatedForeignCode "HASKELL" ghcBackendName s
getInteractionOutputCallback :: TCM InteractionOutputCallback
getInteractionOutputCallback
= gets $ stInteractionOutputCallback . stPersistentState
appInteractionOutputCallback :: Response -> TCM ()
appInteractionOutputCallback r
= getInteractionOutputCallback >>= \ cb -> liftIO $ 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
getAllPatternSyns :: TCM PatternSynDefns
getAllPatternSyns = Map.union <$> getPatternSyns <*> getPatternSynImports
lookupPatternSyn :: AmbiguousQName -> TCM PatternSynDefn
lookupPatternSyn (AmbQ xs) = do
defs <- traverse lookupSinglePatternSyn xs
case mergePatternSynDefs defs of
Just def -> return def
Nothing -> typeError $ CannotResolveAmbiguousPatternSynonym (zipNe xs defs)
lookupSinglePatternSyn :: QName -> TCM PatternSynDefn
lookupSinglePatternSyn 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
addImportedInstances :: Signature -> TCM ()
addImportedInstances sig = do
let itable = Map.fromListWith Set.union
[ (c, Set.singleton i)
| (i, Defn{ defInstance = Just c }) <- HMap.toList $ sig ^. sigDefinitions ]
stImportedInstanceDefs %= Map.unionWith Set.union itable
updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> (TCState -> TCState)
updateInstanceDefs = over stInstanceDefs
modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs = modify . updateInstanceDefs
getAllInstanceDefs :: TCM TempInstanceTable
getAllInstanceDefs = do
(table,xs) <- use stInstanceDefs
itable <- use stImportedInstanceDefs
let !table' = Map.unionWith Set.union itable table
return (table', xs)
getAnonInstanceDefs :: TCM (Set QName)
getAnonInstanceDefs = snd <$> getAllInstanceDefs
clearAnonInstanceDefs :: TCM ()
clearAnonInstanceDefs = modifyInstanceDefs $ mapSnd $ const Set.empty
addUnknownInstance :: QName -> TCM ()
addUnknownInstance x = do
reportSLn "tc.decl.instance" 10 $
"adding definition " ++ prettyShow x ++
" to the instance table (the type is not yet known)"
modifyInstanceDefs $ mapSnd $ Set.insert x
addNamedInstance
:: QName
-> QName
-> TCM ()
addNamedInstance x n = do
reportSLn "tc.decl.instance" 10 $
"adding definition " ++ prettyShow x ++ " to instance table for " ++ prettyShow n
modifySignature $ updateDefinition x $ \ d -> d { defInstance = Just n }
modifyInstanceDefs $ mapFst $ Map.insertWith Set.union n $ Set.singleton x