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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Caching

Contents

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

Synopsis

- writeToCurrentLog :: TypeCheckAction -> TCM ()
- readFromCachedLog :: TCM (Maybe (TypeCheckAction, PostScopeState))
- cleanCachedLog :: TCM ()
- cacheCurrentLog :: TCM ()
- activateLoadedFileCache :: TCM ()
- cachingStarts :: TCM ()
- areWeCaching :: TCM Bool
- withoutCache :: TCM a -> TCM a
- restorePostScopeState :: PostScopeState -> TCM ()

# Log reading/writing operations

writeToCurrentLog :: TypeCheckAction -> TCM () Source #

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

readFromCachedLog :: TCM (Maybe (TypeCheckAction, PostScopeState)) Source #

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

cleanCachedLog :: TCM () Source #

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

cacheCurrentLog :: TCM () Source #

Caches the current type check log. Discardes the old cache. Does nothing if caching is inactive.

# Activating/deactivating

activateLoadedFileCache :: TCM () 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 :: TCM () Source #

To be called before any write or restore calls.

areWeCaching :: TCM Bool Source #

withoutCache :: TCM a -> TCM a Source #

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

# Restoring the `PostScopeState`

restorePostScopeState :: PostScopeState -> TCM () Source #