Writes a TypeCheckAction to the current log, using the current PostScopeState
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Monad.Caching
- 10 values
- PackageAgda-2.8.0.2
- Exports10
- LanguageHaskell2010
- LicenceMIT
- SourceCaching.hs
Log reading/writing operations
4 declarationsvalue
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
5 declarationsMakes 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.