{-# LANGUAGE BangPatterns #-}
module Agda.TypeChecking.Monad.State where
import qualified Control.Exception as E
import Control.Monad.State (void)
import Control.Monad.Trans (liftIO)
import Data.Maybe
import qualified Data.Map as Map
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.HashMap.Strict as HMap
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 Agda.TypeChecking.Monad.Debug (reportSDoc, reportSLn, verboseS)
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.CompiledClause
import Agda.Utils.Hash
import Agda.Utils.Lens
import Agda.Utils.Monad (bracket_)
import Agda.Utils.Pretty
import Agda.Utils.Tuple
import Agda.Utils.Impossible
resetState :: TCM ()
resetState = do
pers <- getsTC stPersistentState
putTC $ initState { stPersistentState = pers }
resetAllState :: TCM ()
resetAllState = do
b <- getBenchmark
backends <- useTC stBackends
putTC $ updatePersistentState (\ s -> s { stBenchmark = b }) initState
stBackends `setTCLens` backends
localTCState :: TCM a -> TCM a
localTCState = bracket_ getTC (\ s -> do
b <- getBenchmark
putTC s
modifyBenchmark $ const b)
localTCStateSaving :: TCM a -> TCM (a, TCState)
localTCStateSaving compute = do
oldState <- getTC
result <- compute
newState <- getTC
do
b <- getBenchmark
putTC oldState
modifyBenchmark $ const b
return (result, newState)
localTCStateSavingWarnings :: TCM a -> TCM a
localTCStateSavingWarnings compute = do
(result, newState) <- localTCStateSaving compute
modifyTC $ over stTCWarnings $ const $ newState ^. stTCWarnings
return result
data SpeculateResult = SpeculateAbort | SpeculateCommit
speculateTCState :: TCM (a, SpeculateResult) -> TCM a
speculateTCState m = do
((x, res), newState) <- localTCStateSaving m
case res of
SpeculateAbort -> return x
SpeculateCommit -> x <$ putTC newState
speculateTCState_ :: TCM SpeculateResult -> TCM ()
speculateTCState_ m = void $ speculateTCState $ ((),) <$> m
freshTCM :: TCM a -> TCM (Either TCErr a)
freshTCM m = do
ps <- useTC 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
setTCLens lensPersistentState $ s ^. lensPersistentState
return $ Right a
Left err -> do
case err of
TypeError { tcErrState = s } ->
setTCLens lensPersistentState $ s ^. lensPersistentState
IOException s _ _ ->
setTCLens 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 = modifyTC . updatePersistentState
lensAccumStatisticsP :: Lens' Statistics PersistentTCState
lensAccumStatisticsP f s = f (stAccumStatistics s) <&> \ a ->
s { stAccumStatistics = a }
lensAccumStatistics :: Lens' Statistics TCState
lensAccumStatistics = lensPersistentState . lensAccumStatisticsP
getScope :: ReadTCState m => m ScopeInfo
getScope = useR stScope
setScope :: ScopeInfo -> TCM ()
setScope scope = modifyScope (const scope)
modifyScope_ :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
modifyScope_ f = stScope `modifyTCLens` f
modifyScope :: MonadTCState m => (ScopeInfo -> ScopeInfo) -> m ()
modifyScope f = modifyScope_ (recomputeInverseScopeMaps . f)
useScope :: ReadTCState m => Lens' a ScopeInfo -> m a
useScope l = useR $ stScope . l
locallyScope :: ReadTCState m => Lens' a ScopeInfo -> (a -> a) -> m b -> m b
locallyScope l = locallyTCState $ stScope . l
withScope :: ReadTCState m => ScopeInfo -> m a -> m (a, ScopeInfo)
withScope s m = locallyTCState stScope (recomputeInverseScopeMaps . const s) $ (,) <$> m <*> getScope
withScope_ :: ReadTCState m => ScopeInfo -> m a -> m a
withScope_ s m = fst <$> withScope s m
localScope :: TCM a -> TCM a
localScope m = do
scope <- getScope
x <- m
setScope scope
return x
notInScopeError :: C.QName -> TCM a
notInScopeError x = do
printScope "unbound" 5 ""
typeError $ NotInScope [x]
notInScopeWarning :: C.QName -> TCM ()
notInScopeWarning x = do
printScope "unbound" 5 ""
warning $ NotInScopeW [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 `modifyTCLens` f
modifyImportedSignature :: (Signature -> Signature) -> TCM ()
modifyImportedSignature f = stImports `modifyTCLens` f
getSignature :: ReadTCState m => m Signature
getSignature = useR 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 . setCopatternLHS)
. (setMatchableSymbols f matchables)
where
setNotInjective def@Function{} = def { funInv = NotInjective }
setNotInjective def = def
setCopatternLHS =
updateDefCopatternLHS (|| any hasProjectionPattern rews)
hasProjectionPattern rew = any (isJust . isProjElim) $ rewPats rew
setMatchableSymbols :: QName -> [QName] -> Signature -> Signature
setMatchableSymbols f matchables =
foldr (.) id $ map (\g -> updateDefinition g $ setMatchable) matchables
where
setMatchable def = def { defMatchable = Set.insert f $ defMatchable 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) }
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__
updateCovering :: ([Clause] -> [Clause]) -> (Defn -> Defn)
updateCovering f def@Function{ funCovering = cs} = def { funCovering = f cs }
updateCovering f _ = __IMPOSSIBLE__
updateCompiledClauses :: (Maybe CompiledClauses -> Maybe CompiledClauses) -> (Defn -> Defn)
updateCompiledClauses f def@Function{ funCompiled = cc} = def { funCompiled = f cc }
updateCompiledClauses f _ = __IMPOSSIBLE__
updateDefCopatternLHS :: (Bool -> Bool) -> Definition -> Definition
updateDefCopatternLHS f def@Defn{ defCopatternLHS = b } = def { defCopatternLHS = f b }
updateDefBlocked :: (Blocked_ -> Blocked_) -> Definition -> Definition
updateDefBlocked f def@Defn{ defBlocked = b } = def { defBlocked = f b }
setTopLevelModule :: C.QName -> TCM ()
setTopLevelModule x = stFreshNameId `setTCLens` NameId 0 (hashString $ prettyShow x)
withTopLevelModule :: C.QName -> TCM a -> TCM a
withTopLevelModule x m = do
next <- useTC stFreshNameId
setTopLevelModule x
y <- m
stFreshNameId `setTCLens` next
return y
addForeignCode :: BackendName -> String -> TCM ()
addForeignCode backend code = do
r <- asksTC envRange
modifyTCLens (stForeignCode . key backend) $ Just . (ForeignCode r code :) . fromMaybe []
getInteractionOutputCallback :: TCM InteractionOutputCallback
getInteractionOutputCallback
= getsTC $ stInteractionOutputCallback . stPersistentState
appInteractionOutputCallback :: Response -> TCM ()
appInteractionOutputCallback r
= getInteractionOutputCallback >>= \ cb -> cb r
setInteractionOutputCallback :: InteractionOutputCallback -> TCM ()
setInteractionOutputCallback cb
= modifyPersistentState $ \ s -> s { stInteractionOutputCallback = cb }
getPatternSyns :: ReadTCState m => m PatternSynDefns
getPatternSyns = useR stPatternSyns
setPatternSyns :: PatternSynDefns -> TCM ()
setPatternSyns m = modifyPatternSyns (const m)
modifyPatternSyns :: (PatternSynDefns -> PatternSynDefns) -> TCM ()
modifyPatternSyns f = stPatternSyns `modifyTCLens` f
getPatternSynImports :: ReadTCState m => m PatternSynDefns
getPatternSynImports = useR stPatternSynImports
getAllPatternSyns :: ReadTCState m => m 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 (NonEmpty.zip 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 -> notInScopeError $ 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 = getsTC $ theBenchmark
modifyBenchmark :: (Benchmark -> Benchmark) -> TCM ()
modifyBenchmark = modifyTC' . 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 `modifyTCLens` Map.unionWith Set.union itable
updateInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> (TCState -> TCState)
updateInstanceDefs = over stInstanceDefs
modifyInstanceDefs :: (TempInstanceTable -> TempInstanceTable) -> TCM ()
modifyInstanceDefs = modifyTC . updateInstanceDefs
getAllInstanceDefs :: TCM TempInstanceTable
getAllInstanceDefs = do
(table,xs) <- useTC stInstanceDefs
itable <- useTC 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