Safe Haskell	None
Language	Haskell2010

Agda.Compiler.Backend

Description

Interface for compiler backend writers.

Synopsis

module Agda.Compiler.Backend.Base
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
crInterface :: CheckResult -> Interface
crMode :: CheckResult -> ModuleCheckMode
crWarnings :: CheckResult -> Set TCWarning
data CheckResult where
- pattern CheckResult :: Interface -> Set TCWarning -> ModuleCheckMode -> Source -> CheckResult
backendInteraction :: AbsolutePath -> [Backend] -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM ()
parseBackendOptions :: [Backend] -> [String] -> CommandLineOptions -> OptM ([Backend], CommandLineOptions)
callBackend :: BackendName -> IsMain -> CheckResult -> TCM ()
callBackendInteractTop :: BackendName -> String -> CommandM ()
callBackendInteractHole :: BackendName -> String -> InteractionId -> Range -> String -> CommandM ()

Documentation

module Agda.Compiler.Backend.Base

data Recompile menv mod Source #

Constructors

Recompile menv
Skip mod

data IsMain Source #

Constructors

IsMain
NotMain

Instances

Instances details

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

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 #

module Agda.Syntax.Treeless

module Agda.TypeChecking.Monad

crInterface :: CheckResult -> Interface Source #

crMode :: CheckResult -> ModuleCheckMode Source #

crWarnings :: CheckResult -> Set TCWarning Source #

data CheckResult where Source #

The result and associated parameters of a type-checked file, when invoked directly via interaction or a backend. Note that the constructor is not exported.

Bundled Patterns

pattern CheckResult :: Interface -> Set TCWarning -> ModuleCheckMode -> Source -> CheckResult

Flattened unidirectional pattern for CheckResult for destructuring inside the ModuleInfo field.

backendInteraction :: AbsolutePath -> [Backend] -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM () Source #

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

callBackend :: BackendName -> IsMain -> CheckResult -> TCM () Source #

Call the compilerMain function of the given backend.

callBackendInteractTop :: BackendName -> String -> CommandM () Source #

Call the backendInteractTop function of the given backend.

callBackendInteractHole :: BackendName -> String -> InteractionId -> Range -> String -> CommandM () Source #

Call the backendInteractHole function of the given backend.