Agda.Compiler.Epic.CompileState

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

Documentation

type IrrFilter = [Bool]

data CompileState

Stuff we need in our compiler

Constructors

CompileState

Fields

dataDecls :: Map QName Tag

nameSupply :: [Var]

definitions :: Set Var

defDelayed :: Map QName Bool

conPars :: Map QName Int

mainName :: Maybe QName

irrFilters :: Map QName IrrFilter

Instances

Show CompileState

initCompileState :: CompileState

The initial (empty) state

type Compile = StateT CompileState

Compiler monad

epicError :: MonadTCM m => String -> Compile m a

unqname :: QName -> Var

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

State modifiers

getDelayed :: MonadTCM m => QName -> Compile m Bool

putDelayed :: Monad m => QName -> Bool -> Compile m ()

newName :: Monad m => Compile m Var

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

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

getConstrTag :: Monad m => QName -> Compile m Tag

addDefName :: Monad m => QName -> Compile m ()

topBindings :: Monad m => Compile m (Set Var)

getConPar :: MonadTCM m => QName -> Compile m Int

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

putMain :: Monad m => QName -> Compile m ()

getMain :: MonadTCM m => Compile m Var

getIrrFilter :: Monad m => QName -> Compile m IrrFilter

putIrrFilter :: Monad m => QName -> IrrFilter -> 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!