Safe Haskell | None |
---|---|
Language | Haskell98 |
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
MonadTrans CompileT Source | |
MonadState s m => MonadState s (CompileT m) Source | |
MonadReader r m => MonadReader r (CompileT m) Source | |
Monad m => Monad (CompileT m) Source | |
Functor m => Functor (CompileT m) Source | |
Monad m => Applicative (CompileT m) Source | |
MonadIO m => MonadIO (CompileT m) Source | |
MonadTCM m => MonadTCM (CompileT m) Source |
:: 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 () Source
addMetaCon :: QName -> CDataCon -> Compile () Source
getExports :: Compile [CExport] Source
getCoreName :: QName -> Compile HsName Source
getCoreName1 :: QName -> TCM HsName Source
getConstrCTag :: QName -> Compile CTag Source
Returns the CTag for a constructor. Not defined for Sharp and magic UNIT constructor.
getConstrFun :: QName -> Compile HsName Source
Returns the expression to use to build a value of the given datatype/constructor.
freshLocalName :: Monad m => CompileT m HsName Source
dataRecCons :: Defn -> [QName] Source