Agda.Compiler.Backend.Base · Agda-2.8.0.2

typetype BackendVersion = Text

#

datadata Backend_boot definition (tcm :: Type -> Type) where

#

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

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

#

Constructors

Backend'
- 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.

Instances3Generic, NFData, Rep

Generic (Backend'_boot definition tcm opts env menv mod def)Defined in Agda-2.8.0.2 · Agda.Compiler.Backend.Base
NFData opts => NFData (Backend'_boot definition tcm opts env menv mod def)Defined in Agda-2.8.0.2 · Agda.Compiler.Backend.Base
type Rep (Backend'_boot definition tcm opts env menv mod def) = D1 ('MetaData "Backend'_boot" "Agda.Compiler.Backend.Base" "Agda-2.8.0.2-3KZoCGOoan2Kayji4DU37s" '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))))))))Defined in Agda-2.8.0.2 · Agda.Compiler.Backend.Base

datadata Recompile menv mod

#

Constructors

Recompile menv
Skip mod

typetype CommandPayload = String

#

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.

typetype BackendCommandTop (tcm :: Type -> Type) = CommandPayload -> CommandM' tcm ()

#

The type of top-level backend interactive commmands.

typetype BackendCommandHole (tcm :: Type -> Type) = CommandPayload -> InteractionId -> Range -> String -> CommandM' tcm ()

#

The type of top-level backend interactive commmands.