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

Safe Haskell | None

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

- data CompileState = CompileState {
  - nameSupply :: [Var]
  - compiledModules :: Map TopLevelModuleName (EInterface, Set FilePath)
  - curModule :: EInterface
  - importedModules :: EInterface
  - curFun :: String
  }
- initCompileState :: CompileState
- type Compile = StateT CompileState
- epicError :: String -> Compile TCM a
- modifyEI :: (EInterface -> EInterface) -> Compile TCM ()
- getsEI :: (EInterface -> a) -> Compile TCM a
- getType :: QName -> Compile TCM Type
- unqname :: QName -> Var
- 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 :: Int -> [a] -> [a] -> [a]
- constructorArity :: Num a => QName -> TCM a
- bindExpr :: Expr -> (Var -> Compile TCM Expr) -> Compile TCM Expr

# 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