ModuleAgda-2.8.0.2Haskell2010

Agda.Compiler.Backend

Interface for compiler backend writers.

4 types
9 values

PackageAgda-2.8.0.2
Exports14
LanguageHaskell2010
LicenceMIT
SourceBackend.hs

module Agda.Compiler.Backend.Base

datadata Recompile menv mod

Constructors

Recompile menv
Skip mod

datadata IsMain

IsMain NotMain

Instances4Eq, Show, Semigroup, Monoid

Eq IsMainDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Show IsMainDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Semigroup IsMainDefined in Agda-2.8.0.2 · Agda.Syntax.Common
Conjunctive semigroup (NotMain is absorbing).
Monoid IsMainDefined in Agda-2.8.0.2 · Agda.Syntax.Common

typetype 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

valuetoTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm)

module Agda.Syntax.Treeless

module Agda.TypeChecking.Monad

valuecrInterface :: CheckResult -> Interface

valuecrMode :: CheckResult -> ModuleCheckMode

valuecrWarnings :: CheckResult -> Set TCWarning

datadata CheckResult

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.

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

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

valuebackendInteraction

:: AbsolutePath
-> [Backend]
-> TCM ()
-> AbsolutePath -> TCM CheckResult
-> TCM ()

valueparseBackendOptions

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

valuecallBackend :: BackendName -> IsMain -> CheckResult -> TCM ()

Call the compilerMain function of the given backend.

valuecallBackendInteractTop :: BackendName -> String -> CommandM ()

Call the backendInteractTop function of the given backend.

valuecallBackendInteractHole

:: BackendName
-> String
-> InteractionId
-> Range
-> String
-> CommandM ()

Call the backendInteractHole function of the given backend.