| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Caching
Synopsis
- writeToCurrentLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => TypeCheckAction -> m ()
- readFromCachedLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => m (Maybe (TypeCheckAction, PostScopeState))
- cleanCachedLog :: (MonadDebug m, MonadTCState m) => m ()
- cacheCurrentLog :: (MonadDebug m, MonadTCState m) => m ()
- activateLoadedFileCache :: (HasOptions m, MonadDebug m, MonadTCState m) => m ()
- cachingStarts :: (MonadTCState m, ReadTCState m) => m ()
- areWeCaching :: ReadTCState m => m Bool
- localCache :: (MonadTCState m, ReadTCState m) => m a -> m a
- withoutCache :: (MonadTCState m, ReadTCState m) => m a -> m a
- restorePostScopeState :: (MonadDebug m, MonadTCState m) => PostScopeState -> m ()
Log reading/writing operations
writeToCurrentLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => TypeCheckAction -> m () Source #
Writes a TypeCheckAction to the current log, using the current
PostScopeState
readFromCachedLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => m (Maybe (TypeCheckAction, PostScopeState)) Source #
Reads the next entry in the cached type check log, if present.
cleanCachedLog :: (MonadDebug m, MonadTCState m) => m () Source #
Empties the "to read" CachedState. To be used when it gets invalid.
cacheCurrentLog :: (MonadDebug m, MonadTCState m) => m () Source #
Caches the current type check log. Discardes the old cache. Does nothing if caching is inactive.
Activating/deactivating
activateLoadedFileCache :: (HasOptions m, MonadDebug m, MonadTCState m) => m () Source #
Makes sure that the stLoadedFileCache is Just, with a clean
current log. Crashes is stLoadedFileCache is already active with a
dirty log. Should be called when we start typechecking the current
file.
cachingStarts :: (MonadTCState m, ReadTCState m) => m () Source #
To be called before any write or restore calls.
areWeCaching :: ReadTCState m => m Bool Source #
localCache :: (MonadTCState m, ReadTCState m) => m a -> m a Source #
Runs the action and restores the current cache at the end of it.
withoutCache :: (MonadTCState m, ReadTCState m) => m a -> m a Source #
Runs the action without cache and restores the current cache at the end of it.
Restoring the PostScopeState
restorePostScopeState :: (MonadDebug m, MonadTCState m) => PostScopeState -> m () Source #