Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Compiler.UHC.CompileState
Description
Contains the state monad that the compiler works in and some functions for tampering with the state.
- data CompileT m a
- type Compile = CompileT TCM
- runCompileT :: MonadIO m => ModuleName -> CompileT m a -> m a
- data 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
- getConstrFun :: QName -> Compile HsName
- moduleNameToCoreName :: ModuleName -> HsName
- moduleNameToCoreNameParts :: ModuleName -> [String]
- freshLocalName :: Monad m => CompileT m HsName
- conArityAndPars :: QName -> TCM (Nat, Nat)
- dataRecCons :: Defn -> [QName]
Documentation
Compiler monad
Instances
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,
addExports :: Monad m => [HsName] -> CompileT m () #
addMetaCon :: QName -> CDataCon -> 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.
moduleNameToCoreNameParts :: ModuleName -> [String] #
freshLocalName :: Monad m => CompileT m HsName #
dataRecCons :: Defn -> [QName] #