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

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

The initial (empty) state

type Compile = StateT CompileStateSource

Compiler monad

epicError :: String -> Compile TCM aSource

When normal errors are not enough

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

Modify the state of the current module's Epic Interface

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

Get the state of the current module's Epic Interface

getType :: QName -> Compile TCM TypeSource

Returns the type of a definition given its name

unqname :: QName -> VarSource

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

State modifiers

replaceAtSource

Arguments

:: Int

replace at

-> [a]

to replace

-> [a]

replace with

-> [a]

result?

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

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

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

Bind an expression to a fresh variable name