Agda-2.2.10: A dependently typed functional programming language and proof assistant

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]

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!