Writes a TypeCheckAction to the current log, using the current PostScopeState
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Monad.Caching
Synopsis
- value writeToCurrentLog
- value readFromCachedLog
- value cleanCachedLog
- value cacheCurrentLog
- value activateLoadedFileCache
- value cachingStarts
- value areWeCaching
- value localCache
- value withoutCache
- value restorePostScopeState
- PackageAgda-2.8.0.2
- Exports10
- LanguageHaskell2010
- LicenceMIT
- SourceCaching.hs
Log reading/writing operations
value
readFromCachedLog :: (MonadDebug m, MonadTCState m, ReadTCState m) => m (Maybe (TypeCheckAction, PostScopeState))Reads the next entry in the cached type check log, if present.
Empties the "to read" CachedState. To be used when it gets invalid.
Caches the current type check log. Discardes the old cache. Does nothing if caching is inactive.
Activating/deactivating
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.
To be called before any write or restore calls.
Runs the action and restores the current cache at the end of it.
Runs the action without cache and restores the current cache at the end of it.