Agda.Compiler.UHC.CompileState

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

Documentation

data CompileT m a

Compiler monad

Instances

MonadTrans CompileT

MonadState s m => MonadState s (CompileT m)

MonadReader r m => MonadReader r (CompileT m)

Monad m => Monad (CompileT m)

Functor m => Functor (CompileT m)

Monad m => Applicative (CompileT m)

MonadIO m => MonadIO (CompileT m)

MonadTCM m => MonadTCM (CompileT m)

type Compile = CompileT TCM

runCompileT

Arguments

:: MonadIO m

=> ModuleName

The module to compile.

-> CompileT m a

-> m a

Used to run the Agda-to-UHC Core transformation. During this transformation,

data CoreMeta

Instances

Monoid CoreMeta

addExports :: Monad m => [HsName] -> CompileT m ()

addMetaCon :: QName -> CDataCon -> Compile ()

addMetaData :: QName -> ([CDataCon] -> CDeclMeta) -> Compile ()

getExports :: Compile [CExport]

getDeclMetas :: Compile [CDeclMeta]

getCoreName :: QName -> Compile HsName

getCoreName1 :: QName -> TCM HsName

getConstrCTag :: QName -> Compile CTag

Returns the CTag for a constructor. Not defined for Sharp and magic UNIT constructor.

getConstrFun :: QName -> Compile HsName

Returns the expression to use to build a value of the given datatype/constructor.

moduleNameToCoreName :: ModuleName -> HsName

moduleNameToCoreNameParts :: ModuleName -> [String]

freshLocalName :: Monad m => CompileT m HsName

conArityAndPars :: QName -> TCM (Nat, Nat)

Copy pasted from MAlonzo.... Move somewhere else!

dataRecCons :: Defn -> [QName]