Safe Haskell	None
Language	Haskell2010

Agda.Compiler.MAlonzo.Misc

Contents

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.

Synopsis

data HsModuleEnv = HsModuleEnv {
- mazModuleName :: ModuleName
- mazIsMainModule :: Bool
}
class Monad m => ReadHsModuleEnv m where
- askHsModuleEnv :: m HsModuleEnv
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 mazModuleName :: ModuleName The name of the Agda module mazIsMainModule :: Bool Whether this is the compilation root and therefore should have the `main` function. This corresponds to the `IsMain` flag provided to the backend, not necessarily whether the GHC module has a `main` function defined.

Instances

Instances details

Monad m => ReadHsModuleEnv (ReaderT HsModuleEnv m) Source #
Instance details 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

Instances details

ReadHsModuleEnv m => ReadHsModuleEnv (MaybeT m) Source #
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods askHsModuleEnv :: MaybeT m HsModuleEnv Source #
ReadHsModuleEnv m => ReadHsModuleEnv (IdentityT m) Source #
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods askHsModuleEnv :: IdentityT m HsModuleEnv Source #
ReadHsModuleEnv m => ReadHsModuleEnv (ExceptT e m) Source #
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods askHsModuleEnv :: ExceptT e m HsModuleEnv Source #
Monad m => ReadHsModuleEnv (ReaderT HsModuleEnv m) Source #
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods askHsModuleEnv :: ReaderT HsModuleEnv m HsModuleEnv Source #
Monad m => ReadHsModuleEnv (ReaderT GHCModule m) Source #
Instance details Defined in Agda.Compiler.MAlonzo.Compiler Methods askHsModuleEnv :: ReaderT GHCModule m HsModuleEnv Source #
Monad m => ReadHsModuleEnv (ReaderT GHCModuleEnv m) Source #
Instance details Defined in Agda.Compiler.MAlonzo.Compiler Methods askHsModuleEnv :: ReaderT GHCModuleEnv m HsModuleEnv Source #
ReadHsModuleEnv m => ReadHsModuleEnv (StateT s m) Source #
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods askHsModuleEnv :: StateT s m HsModuleEnv Source #

newtype HsCompileState Source #

Constructors

HsCompileState
Fields mazAccumlatedImports :: Set ModuleName

Instances

Instances details

Eq HsCompileState Source #
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods (==) :: HsCompileState -> HsCompileState -> Bool # (/=) :: HsCompileState -> HsCompileState -> Bool #
Semigroup HsCompileState Source #
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods (<>) :: HsCompileState -> HsCompileState -> HsCompileState # sconcat :: NonEmpty HsCompileState -> HsCompileState # stimes :: Integral b => b -> HsCompileState -> HsCompileState #
Monoid HsCompileState Source #
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods mempty :: HsCompileState # 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