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
- 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
NFData (Backend_boot definition tcm) Source # | |
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
|
Instances
Generic (Backend'_boot definition tcm opts env menv mod def) Source # | |||||
Defined in Agda.Compiler.Backend.Base Associated Types
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 # | |||||
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 # | |||||
Defined in 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-ES80446w7YfI1YRCZGcXTm" '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)))))))) |
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.