Agda-2.2.10: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.Compiler.Epic.CompileState

Contents State modifiers

Description

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

Synopsis

type IrrFilter = [Bool] data CompileState = CompileState { dataDecls :: Map QName Tag nameSupply :: [Var] definitions :: Set Var defDelayed :: Map QName Bool conPars :: Map QName Int mainName :: Maybe QName irrFilters :: Map QName IrrFilter } initCompileState :: CompileState type Compile = StateT CompileState epicError :: MonadTCM m => String -> Compile m a unqname :: QName -> Var 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 () 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 :: Int -> [a] -> [a] -> [a] constructorArity :: (MonadTCM tcm, Num a) => QName -> tcm a

Documentation

type IrrFilter = [Bool] Source

data CompileState Source

Stuff we need in our compiler Constructors CompileState dataDecls :: Map QName Tag nameSupply :: [Var] definitions :: Set Var defDelayed :: Map QName Bool conPars :: Map QName Int mainName :: Maybe QName irrFilters :: Map QName IrrFilter

initCompileState :: CompileState Source

The initial (empty) state

type Compile = StateT CompileState Source

Compiler monad

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

unqname :: QName -> Var Source

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

State modifiers

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

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

newName :: Monad m => Compile m Var Source

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

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

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

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

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

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

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

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

getMain :: MonadTCM m => Compile m Var Source

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

putIrrFilter :: Monad m => QName -> IrrFilter -> Compile m () Source

replaceAt Source

:: Int replace at -> [a] to replace -> [a] replace with -> [a] result?

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

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

Produced by Haddock version 2.6.1