Agda.Compiler.Backend

Interface for compiler backend writers.

Documentation

data Backend where

Constructors

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

data Backend' opts env menv mod def

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 -> Definition -> TCM def

  Compile a single definition.

• scopeCheckingSuffices :: Bool

  True if the backend works if --only-scope-checking is used.

data Recompile menv mod

Constructors

Recompile menv

Skip mod

data IsMain

Constructors

IsMain

NotMain

Instances

Eq IsMain

Methods

(==) :: IsMain -> IsMain -> Bool

(/=) :: IsMain -> IsMain -> Bool

Show IsMain

Methods

showsPrec :: Int -> IsMain -> ShowS

show :: IsMain -> String

showList :: [IsMain] -> ShowS

Semigroup IsMain

Methods

(<>) :: IsMain -> IsMain -> IsMain

sconcat :: NonEmpty IsMain -> IsMain

stimes :: Integral b => b -> IsMain -> IsMain

Monoid IsMain

Methods

mempty :: IsMain

mappend :: IsMain -> IsMain -> IsMain

mconcat :: [IsMain] -> IsMain

type Flag opts = opts -> OptM opts

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 :: QName -> TCM (Maybe TTerm)

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

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

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