Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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



initCompileState :: CompileState Source #

The initial (empty) state

type Compile = StateT CompileState Source #

Compiler monad

epicError :: String -> Compile TCM a Source #

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 a Source #

Get the state of the current module's Epic Interface

getType :: QName -> Compile TCM Type Source #

Returns the type of a definition given its name

unqname :: QName -> Var Source #

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

State modifiers

replaceAt Source #


:: Int

replace at

-> [a]

to replace

-> [a]

replace with

-> [a]


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

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

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

Bind an expression to a fresh variable name