| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Monad.Caching
Synopsis
- writeToCurrentLog :: TypeCheckAction -> TCM ()
- readFromCachedLog :: TCM (Maybe (TypeCheckAction, PostScopeState))
- cleanCachedLog :: TCM ()
- cacheCurrentLog :: TCM ()
- activateLoadedFileCache :: TCM ()
- cachingStarts :: TCM ()
- areWeCaching :: TCM Bool
- noCacheForImportedModule :: TCM a -> TCM a
- restorePostScopeState :: PostScopeState -> TCM ()
Log reading/writing operations
writeToCurrentLog :: TypeCheckAction -> TCM () #
Writes a TypeCheckAction to the current log, using the current
PostScopeState
readFromCachedLog :: TCM (Maybe (TypeCheckAction, PostScopeState)) #
Reads the next entry in the cached type check log, if present.
cleanCachedLog :: TCM () #
Empties the "to read" CachedState. To be used when it gets invalid.
cacheCurrentLog :: TCM () #
Caches the current type check log. Discardes the old cache. Does nothing if caching is inactive.
Activating/deactivating
activateLoadedFileCache :: TCM () #
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 () #
To be called before any write or restore calls.
areWeCaching :: TCM Bool #
noCacheForImportedModule :: TCM a -> TCM a #
The cache should not be used for an imported module, and it should be restored after the module has been type-checked. This combinator takes care of that.
Restoring the PostScopeState
restorePostScopeState :: PostScopeState -> TCM () #