Agda-2.8.0: A dependently typed functional programming language and proof assistant

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

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

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

type Rep (Backend'_boot definition tcm opts env menv mod def) = D1 ('MetaData "Backend'_boot" "Agda.Compiler.Backend.Base" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))))))

Methods

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

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

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

Instance details

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-DJrTbcOFazJDzri4fKrI2F" '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))))))))

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.