Safe Haskell | None |
---|---|
Language | Haskell2010 |
Interface for compiler backend writers.
Synopsis
- data Backend where
- 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 -> Definition -> TCM def
- scopeCheckingSuffices :: Bool
- data Recompile menv mod
- data IsMain
- type Flag opts = opts -> OptM opts
- toTreeless :: 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] -> OptM ([Backend], CommandLineOptions)
- callBackend :: String -> IsMain -> Interface -> TCM ()
Documentation
data Backend' opts env menv mod def Source #
Backend' | |
|
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 :: 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] -> OptM ([Backend], CommandLineOptions) Source #