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

Methods

showsPrec :: Int -> CompileState -> ShowS

show :: CompileState -> String

showList :: [CompileState] -> ShowS

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