Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Monad.Caching

Contents

- Log reading/writing operations
- Activating/deactivating
- Restoring the `PostScopeState`

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 :: (MonadDebug m, 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 :: (MonadDebug m, 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 #