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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Backend

Description

Interface for compiler backend writers.

Synopsis

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

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

Show IsMain Source # 
Instance details

Defined in Agda.Compiler.Common

Methods

showsPrec :: Int -> IsMain -> ShowS

show :: IsMain -> String

showList :: [IsMain] -> ShowS

Semigroup IsMain Source #

Conjunctive semigroup (NotMain is absorbing).

Instance details

Defined in Agda.Compiler.Common

Methods

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

sconcat :: NonEmpty IsMain -> IsMain

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

Monoid IsMain Source # 
Instance details

Defined in Agda.Compiler.Common

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.

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

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