Safe Haskell	None
Language	Haskell2010

Agda.Compiler.Backend.Base

Synopsis

type BackendVersion = Text
data Backend_boot definition (tcm :: Type -> Type) where
- Backend :: forall opts definition (tcm :: Type -> Type) env menv mod def. NFData opts => Backend'_boot definition tcm opts env menv mod def -> Backend_boot definition tcm
data Backend'_boot definition (tcm :: Type -> Type) opts env menv mod def = Backend' {
- backendName :: BackendName
- backendVersion :: Maybe BackendVersion
- options :: opts
- commandLineFlags :: [OptDescr (Flag opts)]
- isEnabled :: opts -> Bool
- preCompile :: opts -> tcm env
- postCompile :: env -> IsMain -> Map TopLevelModuleName mod -> tcm ()
- preModule :: env -> IsMain -> TopLevelModuleName -> Maybe FilePath -> tcm (Recompile menv mod)
- postModule :: env -> menv -> IsMain -> TopLevelModuleName -> [def] -> tcm mod
- compileDef :: env -> menv -> IsMain -> definition -> tcm def
- scopeCheckingSuffices :: Bool
- mayEraseType :: QName -> tcm Bool
- backendInteractTop :: Maybe (BackendCommandTop tcm)
- backendInteractHole :: Maybe (BackendCommandHole tcm)
}
data Recompile menv mod
- = Recompile menv
- | Skip mod
type CommandPayload = String
type BackendCommandTop (tcm :: Type -> Type) = CommandPayload -> CommandM' tcm ()
type BackendCommandHole (tcm :: Type -> Type) = CommandPayload -> InteractionId -> Range -> String -> CommandM' tcm ()

Documentation

type BackendVersion = Text Source #

data Backend_boot definition (tcm :: Type -> Type) where Source #

Constructors

Backend :: forall opts definition (tcm :: Type -> Type) env menv mod def. NFData opts => Backend'_boot definition tcm opts env menv mod def -> Backend_boot definition tcm

Instances

Instances details

NFData (Backend_boot definition tcm) Source #
Instance details Defined in Agda.Compiler.Backend.Base Methods rnf :: Backend_boot definition tcm -> () #

data Backend'_boot definition (tcm :: Type -> Type) opts env menv mod def Source #

Constructors

Backend'

Fields

backendName :: BackendName
the name of the backend
backendVersion :: Maybe BackendVersion
Optional version information to be printed with --version.
options :: opts
Default options
commandLineFlags :: [OptDescr (Flag opts)]
Backend-specific command-line flags. Should at minimum contain a flag to enable the backend.
isEnabled :: opts -> Bool
Unless the backend has been enabled, runAgda will fall back to vanilla Agda behaviour.
preCompile :: opts -> tcm env
Called after type checking completes, but before compilation starts.
postCompile :: env -> IsMain -> Map TopLevelModuleName mod -> tcm ()
Called after module compilation has completed. The IsMain argument is NotMain if the --no-main flag is present.
preModule :: env -> IsMain -> TopLevelModuleName -> Maybe FilePath -> tcm (Recompile menv mod)
Called before compilation of each module. Gets the path to the .agdai file to allow up-to-date checking of previously written compilation results. Should return Skip m if compilation is not required. Will be Nothing if only scope checking.
postModule :: env -> menv -> IsMain -> TopLevelModuleName -> [def] -> tcm mod
Called after all definitions of a module have been compiled.
compileDef :: env -> menv -> IsMain -> definition -> tcm def
Compile a single definition.
scopeCheckingSuffices :: Bool
True if the backend works if --only-scope-checking is used.
mayEraseType :: QName -> tcm Bool
The treeless compiler may ask the Backend if elements of the given type maybe possibly erased. The answer should be False if the compilation of the type is used by a third party, e.g. in a FFI binding.
backendInteractTop :: Maybe (BackendCommandTop tcm)
Backend-specific top-level interactive command.
backendInteractHole :: Maybe (BackendCommandHole tcm)
Backend-specific hole-level interactive command.

Instances

Instances details

Generic (Backend'_boot definition tcm opts env menv mod def) Source #

Instance details

Defined in Agda.Compiler.Backend.Base

Associated Types

type Rep (Backend'_boot definition tcm opts env menv mod def)

Instance details

Defined in Agda.Compiler.Backend.Base

Methods

from :: Backend'_boot definition tcm opts env menv mod def -> Rep (Backend'_boot definition tcm opts env menv mod def) x #

to :: Rep (Backend'_boot definition tcm opts env menv mod def) x -> Backend'_boot definition tcm opts env menv mod def #

NFData opts => NFData (Backend'_boot definition tcm opts env menv mod def) Source #

Instance details

Defined in Agda.Compiler.Backend.Base

Methods

rnf :: Backend'_boot definition tcm opts env menv mod def -> () #

type Rep (Backend'_boot definition tcm opts env menv mod def) Source #

Instance details

Defined in Agda.Compiler.Backend.Base

data Recompile menv mod Source #

Constructors

Recompile menv
Skip mod

type CommandPayload = String Source #

For the sake of flexibility, we parametrize interactive commands with an arbitrary string payload, e.g. to allow extra user input, or have backends provide multiple commands with a single record field.

type BackendCommandTop (tcm :: Type -> Type) Source #

Arguments

= CommandPayload	arbitrary user payload
-> CommandM' tcm ()

The type of top-level backend interactive commmands.

type BackendCommandHole (tcm :: Type -> Type) Source #

Arguments

= CommandPayload	arbitrary user payload
-> InteractionId	the hole's ID
-> Range	the hole's range
-> String	the hole's contents
-> CommandM' tcm ()

The type of top-level backend interactive commmands.