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

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
- data CheckResult where
  - pattern CheckResult :: Interface -> Set TCWarning -> ModuleCheckMode -> Source -> CheckResult
- crInterface :: CheckResult -> Interface
- crWarnings :: CheckResult -> Set TCWarning
- crMode :: CheckResult -> ModuleCheckMode
- 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 Source # mappend :: IsMain -> IsMain -> IsMain Source # mconcat :: [IsMain] -> IsMain Source #
Semigroup IsMain Source # | Conjunctive semigroup (`NotMain` is absorbing).
Instance details Defined in Agda.Syntax.Common Methods (<>) :: IsMain -> IsMain -> IsMain Source # sconcat :: NonEmpty IsMain -> IsMain Source # stimes :: Integral b => b -> IsMain -> IsMain Source #
Show IsMain Source # |
Instance details Defined in Agda.Syntax.Common Methods showsPrec :: Int -> IsMain -> ShowS Source # show :: IsMain -> String Source # showList :: [IsMain] -> ShowS Source #
Eq IsMain Source # |
Instance details Defined in Agda.Syntax.Common Methods (==) :: IsMain -> IsMain -> Bool Source # (/=) :: IsMain -> IsMain -> Bool Source #

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

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.

crInterface :: CheckResult -> Interface Source #

crWarnings :: CheckResult -> Set TCWarning Source #

crMode :: CheckResult -> ModuleCheckMode Source #

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.