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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Epic.CompileState

Contents

Description

Contains the state monad that the compiler works in and some functions for tampering with the state.

Synopsis

Documentation

initCompileState :: CompileState #

The initial (empty) state

type Compile = StateT CompileState #

Compiler monad

epicError :: String -> Compile TCM a #

When normal errors are not enough

modifyEI :: (EInterface -> EInterface) -> Compile TCM () #

Modify the state of the current module's Epic Interface

getsEI :: (EInterface -> a) -> Compile TCM a #

Get the state of the current module's Epic Interface

getType :: QName -> Compile TCM Type #

Returns the type of a definition given its name

unqname :: QName -> Var #

Create a name which can be used in Epic code from a QName.

State modifiers

replaceAt #

Arguments

:: Int

replace at

-> [a]

to replace

-> [a]

replace with

-> [a]

result?

constructorArity :: Num a => QName -> TCM a #

Copy pasted from MAlonzo, HAHA!!! Move somewhere else!

bindExpr :: Expr -> (Var -> Compile TCM Expr) -> Compile TCM Expr #

Bind an expression to a fresh variable name