Agda-2.5.4: 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

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

Semigroup IsMain Source # 
Instance details

Defined in Agda.Compiler.Common

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 :: 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.