ModuleAgda-2.8.0.2Haskell2010
Agda.Compiler.Backend.Base
Synopsis
- type BackendVersion
- data Backend_boot
- data Backend'_boot
- data Recompile
- type CommandPayload
- type BackendCommandTop
- type BackendCommandHole
- PackageAgda-2.8.0.2
- Exports7
- LanguageHaskell2010
- LicenceMIT
- SourceBase.hs
Constructors
Backend :: NFData opts => Backend'_boot definition tcm opts env menv mod def -> Backend_boot definition tcm
Instances1NFData
NFData (Backend_boot definition tcm)Defined in Agda-2.8.0.2 · Agda.Compiler.Backend.Base
Constructors
Backend'backendName :: BackendNamethe name of the backend
backendVersion :: Maybe BackendVersionOptional version information to be printed with
--version.options :: optsDefault options
commandLineFlags :: [OptDescr (Flag opts)]Backend-specific command-line flags. Should at minimum contain a flag to enable the backend.
isEnabled :: opts -> BoolUnless the backend has been enabled,
runAgdawill fall back to vanilla Agda behaviour.preCompile :: opts -> tcm envCalled after type checking completes, but before compilation starts.
postCompile :: env -> IsMain -> Map TopLevelModuleName mod -> tcm ()Called after module compilation has completed. The
IsMainargument isNotMainif the--no-mainflag is present.preModule :: env -> IsMain -> TopLevelModuleName -> Maybe FilePath -> tcm (Recompile menv mod)Called before compilation of each module. Gets the path to the
.agdaifile to allow up-to-date checking of previously written compilation results. Should returnSkip mif compilation is not required. Will beNothingif only scope checking.postModule :: env -> menv -> IsMain -> TopLevelModuleName -> [def] -> tcm modCalled after all definitions of a module have been compiled.
compileDef :: env -> menv -> IsMain -> definition -> tcm defCompile a single definition.
scopeCheckingSuffices :: BoolTrue if the backend works if
--only-scope-checkingis used.mayEraseType :: QName -> tcm BoolThe 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.
Instances3Generic, NFData, Rep
Generic (Backend'_boot definition tcm opts env menv mod def)Defined in Agda-2.8.0.2 · Agda.Compiler.Backend.BaseNFData opts => NFData (Backend'_boot definition tcm opts env menv mod def)Defined in Agda-2.8.0.2 · Agda.Compiler.Backend.Basetype Rep (Backend'_boot definition tcm opts env menv mod def) = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.Compiler.Backend.Base"Backend'_boot"
"Agda.Compiler.Backend.Base"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"Backend'"
'PrefixI 'True) (((S1 ('MetaSel ('Just"backendName"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BackendName) :*: (S1 ('MetaSel ('Just"backendVersion"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe BackendVersion)) :*: S1 ('MetaSel ('Just"options"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 opts))) :*: ((S1 ('MetaSel ('Just"commandLineFlags"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [OptDescr (Flag opts)]) :*: S1 ('MetaSel ('Just"isEnabled"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (opts -> Bool))) :*: (S1 ('MetaSel ('Just"preCompile"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (opts -> tcm env)) :*: S1 ('MetaSel ('Just"postCompile"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> IsMain -> Map TopLevelModuleName mod -> tcm ()))))) :*: ((S1 ('MetaSel ('Just"preModule"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> IsMain -> TopLevelModuleName -> Maybe FilePath -> tcm (Recompile menv mod))) :*: (S1 ('MetaSel ('Just"postModule"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> menv -> IsMain -> TopLevelModuleName -> [def] -> tcm mod)) :*: S1 ('MetaSel ('Just"compileDef"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (env -> menv -> IsMain -> definition -> tcm def)))) :*: ((S1 ('MetaSel ('Just"scopeCheckingSuffices"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just"mayEraseType"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (QName -> tcm Bool))) :*: (S1 ('MetaSel ('Just"backendInteractTop"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (BackendCommandTop tcm))) :*: S1 ('MetaSel ('Just"backendInteractHole"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (BackendCommandHole tcm))))))))
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.
The type of top-level backend interactive commmands.
type BackendCommandHole (tcm :: Type -> Type) = CommandPayload -> InteractionId -> Range -> String -> CommandM' tcm ()The type of top-level backend interactive commmands.