Disco.Eval

Top-level evaluation utilities.

Effects

type EvalEffects = [Error EvalError, Random, LFresh, Output Message, State Mem]

Effects needed for evaluation.

type DiscoEffects = AppendEffects EvalEffects TopEffects

All effects needed for the top level + evaluation.

Top-level info record and associated lenses

data DiscoConfig

initDiscoConfig :: DiscoConfig

debugMode :: Iso' DiscoConfig Bool

data TopInfo

A record of information about the current top-level environment.

replModInfo :: Lens' TopInfo ModuleInfo

topEnv :: Lens' TopInfo Env

topModMap :: Lens' TopInfo (Map ModuleName ModuleInfo)

lastFile :: Lens' TopInfo (Maybe FilePath)

discoConfig :: Lens' TopInfo DiscoConfig

Running things

runDisco :: DiscoConfig -> (forall r. Members DiscoEffects r => Sem r ()) -> IO ()

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

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

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

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

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

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

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)

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 ()

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 ()

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 ()

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.

loadDef :: Members '[State TopInfo, Random, Error EvalError, State Mem] r => QName Core -> Core -> Sem r ()