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

Safe Haskell | None
Language | Haskell2010

Agda.Compiler.Backend

Description

Interface for compiler backend writers.

Synopsis

- data Backend where
  - Backend :: Backend' opts env menv mod def -> Backend
- data Backend' opts env menv mod def = Backend' {
  - backendName :: String
  - backendVersion :: Maybe String
  - options :: opts
  - commandLineFlags :: [OptDescr (Flag opts)]
  - isEnabled :: opts -> Bool
  - preCompile :: opts -> TCM env
  - postCompile :: env -> IsMain -> Map ModuleName mod -> TCM ()
  - preModule :: env -> ModuleName -> FilePath -> TCM (Recompile menv mod)
  - postModule :: env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod
  - compileDef :: env -> menv -> IsMain -> Definition -> TCM def
  - scopeCheckingSuffices :: Bool
  }
- data Recompile menv mod
  - = Recompile menv
  - | Skip mod
- data IsMain
  - = IsMain
  - | NotMain
- type Flag opts = opts -> OptM opts
- toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm)
- module Agda.Syntax.Treeless
- module Agda.TypeChecking.Monad
- backendInteraction :: [Backend] -> (TCM (Maybe Interface) -> TCM ()) -> TCM (Maybe Interface) -> TCM ()
- parseBackendOptions :: [Backend] -> [String] -> CommandLineOptions -> OptM ([Backend], CommandLineOptions)
- callBackend :: String -> IsMain -> Interface -> TCM ()

# Documentation

data Backend where Source #

Constructors

Backend :: Backend' opts env menv mod def -> Backend |

data Backend' opts env menv mod def Source #

Constructors

Backend' |

Fields

- backendName :: String
- backendVersion :: Maybe String

  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 ModuleName mod -> TCM ()

  Called after module compilation has completed. The `IsMain` argument is `NotMain` if the `--no-main` flag is present.

- preModule :: env -> ModuleName -> 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.

- postModule :: env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod

  Called after all definitions of a module has 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.

data Recompile menv mod Source #

Constructors

Recompile menv |
Skip mod |

data IsMain Source #

Constructors

IsMain |
NotMain |

Instances

Eq IsMain Source # |
Instance details Defined in Agda.Compiler.Common Methods (==) :: IsMain -> IsMain -> Bool Source # (/=) :: IsMain -> IsMain -> Bool Source #
Show IsMain Source # |
Instance details Defined in Agda.Compiler.Common Methods showsPrec :: Int -> IsMain -> ShowS Source # show :: IsMain -> String Source # showList :: [IsMain] -> ShowS Source #
Semigroup IsMain Source # | Conjunctive semigroup (`NotMain` is absorbing).
Instance details Defined in Agda.Compiler.Common Methods (<>) :: IsMain -> IsMain -> IsMain Source # sconcat :: NonEmpty IsMain -> IsMain Source # stimes :: Integral b => b -> IsMain -> IsMain Source #
Monoid IsMain Source # |
Instance details Defined in Agda.Compiler.Common Methods mempty :: IsMain Source # mappend :: IsMain -> IsMain -> IsMain Source # mconcat :: [IsMain] -> IsMain Source #

type Flag opts = opts -> OptM opts Source #

`f :: Flag opts` is an action on the option record that results from parsing an option. `f opts` produces either an error message or an updated options record

toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm) Source #

Converts compiled clauses to treeless syntax.

Note: Do not use any of the concrete names in the returned term for identification purposes! If you wish to do so, first apply the Agda.Compiler.Treeless.NormalizeNames transformation.

module Agda.Syntax.Treeless

module Agda.TypeChecking.Monad

backendInteraction :: [Backend] -> (TCM (Maybe Interface) -> TCM ()) -> TCM (Maybe Interface) -> TCM () Source #

parseBackendOptions :: [Backend] -> [String] -> CommandLineOptions -> OptM ([Backend], CommandLineOptions) Source #

callBackend :: String -> IsMain -> Interface -> TCM () Source #