Agda.TypeChecking.Monad.Caching

Log reading/writing operations

writeToCurrentLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => TypeCheckAction -> m ()

Writes a TypeCheckAction to the current log, using the current PostScopeState

readFromCachedLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => m (Maybe (TypeCheckAction, PostScopeState))

Reads the next entry in the cached type check log, if present.

cleanCachedLog :: (MonadDebug m, MonadTCState m) => m ()

Empties the "to read" CachedState. To be used when it gets invalid.

cacheCurrentLog :: (MonadDebug m, MonadTCState m) => m ()

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 ()

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 :: (MonadDebug m, MonadTCState m, ReadTCState m) => m ()

To be called before any write or restore calls.

areWeCaching :: ReadTCState m => m Bool

localCache :: (MonadTCState m, ReadTCState m) => m a -> m a

Runs the action and restores the current cache at the end of it.

withoutCache :: (MonadTCState m, ReadTCState m) => m a -> m a

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 ()