Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 :: CompileStateSource
The initial (empty) state
type Compile = StateT CompileStateSource
Compiler monad
epicError :: MonadTCM m => String -> Compile m aSource
unqname :: QName -> VarSource
Create a name which can be used in Epic code from a QName.
State modifiers
getDelayed :: MonadTCM m => QName -> Compile m BoolSource
putDelayed :: Monad m => QName -> Bool -> Compile m ()Source
newName :: Monad m => Compile m VarSource
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 TagSource
addDefName :: Monad m => QName -> Compile m ()Source
topBindings :: Monad m => Compile m (Set Var)Source
getConPar :: MonadTCM m => QName -> Compile m IntSource
putConPar :: Monad m => QName -> Int -> Compile m ()Source
putMain :: Monad m => QName -> Compile m ()Source
getMain :: MonadTCM m => Compile m VarSource
getIrrFilter :: Monad m => QName -> Compile m IrrFilterSource
putIrrFilter :: Monad m => QName -> IrrFilter -> Compile m ()Source
replaceAtSource
:: Intreplace at
-> [a]to replace
-> [a]replace with
-> [a]result?
constructorArity :: (MonadTCM tcm, Num a) => QName -> tcm aSource
Copy pasted from MAlonzo, HAHA!!! Move somewhere else!
Produced by Haddock version 2.6.1