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

type IrrFilter = [Bool]

data CompileState

Stuff we need in our compiler

Instances

initCompileState :: CompileState

The initial (empty) state

type Compile = StateT CompileState

Compiler monad

unqname :: QName -> Var

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

State modifiers

addDataDecl :: Monad m => [QName] -> Compile m ()

Add a data declaration by giving a list of its constructors. Tags will be created and saved.

putConPar :: Monad m => QName -> Int -> Compile m ()

replaceAt

Arguments

:: Int

replace at

-> [a]

to replace

-> [a]

replace with

-> [a]

result?

constructorArity :: (MonadTCM tcm, Num a) => QName -> tcm a

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