Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 # | |
MonadReader r m => MonadReader r (CompileT m) Source # | |
MonadState s m => MonadState s (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,
getExports :: Compile [CExport] Source #
getDeclMetas :: Compile [CDeclMeta] 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.
moduleNameToCoreNameParts :: ModuleName -> [String] Source #
conArityAndPars :: QName -> TCM (Nat, Nat) Source #
Copy pasted from MAlonzo.... Move somewhere else!
dataRecCons :: Defn -> [QName] Source #