rzk-0.7.4: An experimental proof assistant for synthetic ∞-categories

Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.Rzk.VSCode.Env

Synopsis

data RzkCachedModule = RzkCachedModule {
- cachedModuleDecls :: [Decl']
- cachedModuleErrors :: [TypeErrorInScopedContext VarIdent]
}
type RzkTypecheckCache = [(FilePath, RzkCachedModule)]
newtype RzkEnv = RzkEnv {
- rzkEnvTypecheckCache :: TVar RzkTypecheckCache
}
defaultRzkEnv :: IO RzkEnv
type LSP = LspT ServerConfig (ReaderT RzkEnv IO)
cacheTypecheckedModules :: RzkTypecheckCache -> LSP ()
resetCacheForAllFiles :: LSP ()
resetCacheForFiles :: [FilePath] -> LSP ()
getCachedTypecheckedModules :: LSP RzkTypecheckCache

Documentation

data RzkCachedModule Source #

Constructors

RzkCachedModule
Fields cachedModuleDecls :: [Decl'] cachedModuleErrors :: [TypeErrorInScopedContext VarIdent]

type RzkTypecheckCache = [(FilePath, RzkCachedModule)] Source #

newtype RzkEnv Source #

Constructors

RzkEnv
Fields rzkEnvTypecheckCache :: TVar RzkTypecheckCache

defaultRzkEnv :: IO RzkEnv Source #

type LSP = LspT ServerConfig (ReaderT RzkEnv IO) Source #

cacheTypecheckedModules :: RzkTypecheckCache -> LSP () Source #

Override the cache with given typechecked modules.

resetCacheForAllFiles :: LSP () Source #

Completely invalidate the cache of typechecked files.

resetCacheForFiles :: [FilePath] -> LSP () Source #

Invalidate the cache for a list of file paths.

getCachedTypecheckedModules :: LSP RzkTypecheckCache Source #

Get the current state of the cache.