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

Safe HaskellNone




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.


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.

withoutCache :: TCM a -> TCM a Source #

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

Restoring the PostScopeState