Copyright | disco team and contributors |
---|---|
License | BSD-3-Clause |
Maintainer | byorgey@gmail.com |
Safe Haskell | None |
Language | Haskell2010 |
Top-level evaluation utilities.
Synopsis
- type EvalEffects = [Error EvalError, Random, LFresh, Output Message, State Mem]
- type DiscoEffects = AppendEffects EvalEffects TopEffects
- data DiscoConfig
- initDiscoConfig :: DiscoConfig
- debugMode :: Iso' DiscoConfig Bool
- data TopInfo
- replModInfo :: Lens' TopInfo ModuleInfo
- topEnv :: Lens' TopInfo Env
- topModMap :: Lens' TopInfo (Map ModuleName ModuleInfo)
- lastFile :: Lens' TopInfo (Maybe FilePath)
- discoConfig :: Lens' TopInfo DiscoConfig
- runDisco :: DiscoConfig -> (forall r. Members DiscoEffects r => Sem r ()) -> IO ()
- runTCM :: Member (Error DiscoError) r => TyCtx -> TyDefCtx -> Sem (Reader TyCtx ': (Reader TyDefCtx ': (Fresh ': (Error LocTCError ': r)))) a -> Sem r a
- inputTopEnv :: Member (Input TopInfo) r => Sem (Input Env ': r) a -> Sem r a
- parseDiscoModule :: Members '[Error DiscoError, Embed IO] r => FilePath -> Sem r Module
- typecheckTop :: Members '[Input TopInfo, Error DiscoError] r => Sem (Reader TyCtx ': (Reader TyDefCtx ': (Fresh ': (Error TCError ': r)))) a -> Sem r a
- loadDiscoModule :: Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r => Bool -> Resolver -> FilePath -> Sem r ModuleInfo
- loadParsedDiscoModule :: Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r => Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo
- loadFile :: Members '[Output Message, Embed IO] r => FilePath -> Sem r (Maybe String)
- addToREPLModule :: Members '[Error DiscoError, State TopInfo, Random, State Mem, Output Message] r => ModuleInfo -> Sem r ()
- setREPLModule :: Members '[State TopInfo, Random, Error EvalError, State Mem, Output Message] r => ModuleInfo -> Sem r ()
- loadDefsFrom :: Members '[State TopInfo, Random, Error EvalError, State Mem] r => ModuleInfo -> Sem r ()
- loadDef :: Members '[State TopInfo, Random, Error EvalError, State Mem] r => QName Core -> Core -> Sem r ()
Effects
type EvalEffects = [Error EvalError, Random, LFresh, Output Message, State Mem] Source #
Effects needed for evaluation.
type DiscoEffects = AppendEffects EvalEffects TopEffects Source #
All effects needed for the top level + evaluation.
Top-level info record and associated lenses
data DiscoConfig Source #
Running things
runDisco :: DiscoConfig -> (forall r. Members DiscoEffects r => Sem r ()) -> IO () Source #
Run a top-level computation.
runTCM :: Member (Error DiscoError) r => TyCtx -> TyDefCtx -> Sem (Reader TyCtx ': (Reader TyDefCtx ': (Fresh ': (Error LocTCError ': r)))) a -> Sem r a Source #
Run a typechecking computation, providing it with local contexts (initialized to the provided arguments) for variable types and type definitions.
inputTopEnv :: Member (Input TopInfo) r => Sem (Input Env ': r) a -> Sem r a Source #
Run a computation that needs an input environment, grabbing the
current top-level environment from the TopInfo
records.
parseDiscoModule :: Members '[Error DiscoError, Embed IO] r => FilePath -> Sem r Module Source #
Parse a module from a file, re-throwing a parse error if it fails.
typecheckTop :: Members '[Input TopInfo, Error DiscoError] r => Sem (Reader TyCtx ': (Reader TyDefCtx ': (Fresh ': (Error TCError ': r)))) a -> Sem r a Source #
Run a typechecking computation in the context of the top-level REPL module, re-throwing a wrapped error if it fails.
Loading modules
loadDiscoModule :: Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r => Bool -> Resolver -> FilePath -> Sem r ModuleInfo Source #
Recursively loads a given module by first recursively loading and
typechecking its imported modules, adding the obtained
ModuleInfo
records to a map from module names to info records,
and then typechecking the parent module in an environment with
access to this map. This is really just a depth-first search.
The Resolver
argument specifies where to look for imported
modules.
loadParsedDiscoModule :: Members '[State TopInfo, Output Message, Random, State Mem, Error DiscoError, Embed IO] r => Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo Source #
Like loadDiscoModule
, but start with an already parsed Module
instead of loading a module from disk by name. Also, check it in
a context that includes the current top-level context (unlike a
module loaded from disk). Used for e.g. blocks/modules entered
at the REPL prompt.
loadFile :: Members '[Output Message, Embed IO] r => FilePath -> Sem r (Maybe String) Source #
Try loading the contents of a file from the filesystem, emitting an error if it's not found.
addToREPLModule :: Members '[Error DiscoError, State TopInfo, Random, State Mem, Output Message] r => ModuleInfo -> Sem r () Source #
Add things from the given module to the set of currently loaded things.
setREPLModule :: Members '[State TopInfo, Random, Error EvalError, State Mem, Output Message] r => ModuleInfo -> Sem r () Source #
Set the given ModuleInfo
record as the currently loaded
module. This also includes updating the top-level state with new
term definitions, documentation, types, and type definitions.
Replaces any previously loaded module.
loadDefsFrom :: Members '[State TopInfo, Random, Error EvalError, State Mem] r => ModuleInfo -> Sem r () Source #
Populate various pieces of the top-level info record (docs, type
context, type and term definitions) from the ModuleInfo
record
corresponding to the currently loaded module, and load all the
definitions into the current top-level environment.