Agda.Compiler.Epic.CompileState

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

Documentation

data CompileState

Stuff we need in our compiler

Constructors

CompileState

Fields

nameSupply :: [Var]

compiledModules :: Map TopLevelModuleName (EInterface, Set FilePath)

curModule :: EInterface

importedModules :: EInterface

curFun :: String

Instances

Show CompileState

initCompileState :: CompileState

The initial (empty) state

type Compile = StateT CompileState

Compiler monad

epicError :: String -> Compile TCM a

When normal errors are not enough

modifyEI :: (EInterface -> EInterface) -> Compile TCM ()

Modify the state of the current module's Epic Interface

getsEI :: (EInterface -> a) -> Compile TCM a

Get the state of the current module's Epic Interface

getType :: QName -> Compile TCM Type

Returns the type of a definition given its name

unqname :: QName -> Var

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

State modifiers

resetNameSupply :: Compile TCM ()

getDelayed :: QName -> Compile TCM Bool

putDelayed :: QName -> Bool -> Compile TCM ()

newName :: Compile TCM Var

putConstrTag :: QName -> Tag -> Compile TCM ()

assignConstrTag :: QName -> Compile TCM Tag

assignConstrTag' :: QName -> [QName] -> Compile TCM Tag

getConData :: QName -> Compile TCM QName

getDataCon :: QName -> Compile TCM [QName]

getConstrTag :: QName -> Compile TCM Tag

getConstrTag' :: QName -> Compile TCM (Maybe Tag)

addDefName :: QName -> Compile TCM ()

topBindings :: Compile TCM (Set Var)

getConArity :: QName -> Compile TCM Int

putConArity :: QName -> Int -> Compile TCM ()

putMain :: QName -> Compile TCM ()

getMain :: Compile TCM Var

lookInterface :: (EInterface -> Maybe a) -> Compile TCM a -> Compile TCM a

constrInScope :: QName -> Compile TCM Bool

getForcedArgs :: QName -> Compile TCM ForcedArgs

putForcedArgs :: QName -> ForcedArgs -> Compile TCM ()

replaceAt

Arguments

:: Int

replace at

-> [a]

to replace

-> [a]

replace with

-> [a]

result?

constructorArity :: Num a => QName -> TCM a

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

bindExpr :: Expr -> (Var -> Compile TCM Expr) -> Compile TCM Expr

Bind an expression to a fresh variable name