| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Compiler.MAlonzo.Misc
Synopsis
- data HsModuleEnv = HsModuleEnv {
- mazModuleName :: ModuleName
- mazIsMainModule :: Bool
- class Monad m => ReadHsModuleEnv m where
- newtype HsCompileState = HsCompileState {
- mazAccumlatedImports :: Set ModuleName
- type HsCompileT m = ReaderT HsModuleEnv (StateT HsCompileState m)
- type HsCompileM = HsCompileT TCM
- runHsCompileT' :: HsCompileT m a -> HsModuleEnv -> HsCompileState -> m (a, HsCompileState)
- runHsCompileT :: HsCompileT m a -> HsModuleEnv -> m (a, HsCompileState)
- curIsMainModule :: ReadHsModuleEnv m => m Bool
- curAgdaMod :: ReadHsModuleEnv m => m ModuleName
- curHsMod :: ReadHsModuleEnv m => m ModuleName
- ihname :: String -> Nat -> Name
- unqhname :: String -> QName -> Name
- tlmodOf :: ReadTCState m => ModuleName -> m ModuleName
- xqual :: QName -> Name -> HsCompileM QName
- xhqn :: String -> QName -> HsCompileM QName
- hsName :: String -> QName
- conhqn :: QName -> HsCompileM QName
- bltQual :: String -> String -> HsCompileM QName
- dname :: QName -> Name
- duname :: QName -> Name
- hsPrimOp :: String -> QOp
- hsPrimOpApp :: String -> Exp -> Exp -> Exp
- hsInt :: Integer -> Exp
- hsTypedInt :: Integral a => a -> Exp
- hsTypedDouble :: Real a => a -> Exp
- hsLet :: Name -> Exp -> Exp -> Exp
- hsVarUQ :: Name -> Exp
- hsAppView :: Exp -> [Exp]
- hsOpToExp :: QOp -> Exp
- hsLambda :: [Pat] -> Exp -> Exp
- hsMapAlt :: (Exp -> Exp) -> Alt -> Alt
- hsMapRHS :: (Exp -> Exp) -> Rhs -> Rhs
- mazstr :: String
- mazName :: Name
- mazMod' :: String -> ModuleName
- mazMod :: ModuleName -> ModuleName
- mazCoerceName :: String
- mazErasedName :: String
- mazAnyTypeName :: String
- mazCoerce :: Exp
- mazIncompleteMatch :: Exp
- rtmIncompleteMatch :: QName -> Exp
- mazUnreachableError :: Exp
- rtmUnreachableError :: Exp
- mazHole :: Exp
- rtmHole :: String -> Exp
- mazAnyType :: Type
- mazRTE :: ModuleName
- mazRTEFloat :: ModuleName
- rtmQual :: String -> QName
- rtmVar :: String -> Exp
- rtmError :: Text -> Exp
- unsafeCoerceMod :: ModuleName
- fakeD :: Name -> String -> Decl
- fakeDS :: String -> String -> Decl
- fakeDQ :: QName -> String -> Decl
- fakeType :: String -> Type
- fakeExp :: String -> Exp
- fakeDecl :: String -> Decl
- emptyBinds :: Maybe Binds
- isModChar :: Char -> Bool
Documentation
data HsModuleEnv Source #
Constructors
| HsModuleEnv | |
Fields
| |
Instances
| Monad m => ReadHsModuleEnv (ReaderT HsModuleEnv m) Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods askHsModuleEnv :: ReaderT HsModuleEnv m HsModuleEnv Source # | |
class Monad m => ReadHsModuleEnv m where Source #
Monads that can produce an HsModuleEnv
Minimal complete definition
Nothing
Methods
askHsModuleEnv :: m HsModuleEnv Source #
default askHsModuleEnv :: (MonadTrans t, Monad n, m ~ t n, ReadHsModuleEnv n) => m HsModuleEnv Source #
Instances
newtype HsCompileState Source #
Constructors
| HsCompileState | |
Fields
| |
Instances
| Eq HsCompileState Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods (==) :: HsCompileState -> HsCompileState -> Bool (/=) :: HsCompileState -> HsCompileState -> Bool | |
| Semigroup HsCompileState Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods (<>) :: HsCompileState -> HsCompileState -> HsCompileState # sconcat :: NonEmpty HsCompileState -> HsCompileState stimes :: Integral b => b -> HsCompileState -> HsCompileState | |
| Monoid HsCompileState Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods mappend :: HsCompileState -> HsCompileState -> HsCompileState mconcat :: [HsCompileState] -> HsCompileState | |
type HsCompileT m = ReaderT HsModuleEnv (StateT HsCompileState m) Source #
Transformer adding read-only module info and a writable set of imported modules
type HsCompileM = HsCompileT TCM Source #
The default compilation monad is the entire TCM (☹️) enriched with our state and module info
runHsCompileT' :: HsCompileT m a -> HsModuleEnv -> HsCompileState -> m (a, HsCompileState) Source #
runHsCompileT :: HsCompileT m a -> HsModuleEnv -> m (a, HsCompileState) Source #
curIsMainModule :: ReadHsModuleEnv m => m Bool Source #
Whether the current module is expected to have the main function.
This corresponds to the IsMain flag provided to the backend,
not necessarily whether the GHC module actually has a main function defined.
curAgdaMod :: ReadHsModuleEnv m => m ModuleName Source #
This is the same value as curMName, but does not rely on the TCM's state.
(curMName and co. should be removed, but the current Backend interface
is not sufficient yet to allow that)
curHsMod :: ReadHsModuleEnv m => m ModuleName Source #
Get the Haskell module name of the currently-focused Agda module
Types coming from Agda are named "T<number>".
Other definitions coming from Agda are named "d<number>".
Names coming from Haskell must always be used qualified.
tlmodOf :: ReadTCState m => ModuleName -> m ModuleName Source #
bltQual :: String -> String -> HsCompileM QName Source #
hsTypedInt :: Integral a => a -> Exp Source #
hsTypedDouble :: Real a => a -> Exp Source #
mazMod' :: String -> ModuleName Source #
mazMod :: ModuleName -> ModuleName Source #
mazCoerceName :: String Source #
mazErasedName :: String Source #
mazAnyTypeName :: String Source #
rtmIncompleteMatch :: QName -> Exp Source #
mazAnyType :: Type Source #
mazRTE :: ModuleName Source #
emptyBinds :: Maybe Binds Source #