Agda.Compiler.MAlonzo.Misc

Documentation

data HsModuleEnv

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

Monad m => ReadHsModuleEnv (ReaderT HsModuleEnv m)

Defined in Agda.Compiler.MAlonzo.Misc

Methods

askHsModuleEnv :: ReaderT HsModuleEnv m HsModuleEnv

class Monad m => ReadHsModuleEnv m where

Monads that can produce an HsModuleEnv

Minimal complete definition

Nothing

Methods

askHsModuleEnv :: m HsModuleEnv

default askHsModuleEnv :: (MonadTrans t, Monad n, m ~ t n, ReadHsModuleEnv n) => m HsModuleEnv

Instances

ReadHsModuleEnv m => ReadHsModuleEnv (MaybeT m)

Defined in Agda.Compiler.MAlonzo.Misc

Methods

askHsModuleEnv :: MaybeT m HsModuleEnv

ReadHsModuleEnv m => ReadHsModuleEnv (IdentityT m)

Defined in Agda.Compiler.MAlonzo.Misc

Methods

askHsModuleEnv :: IdentityT m HsModuleEnv

ReadHsModuleEnv m => ReadHsModuleEnv (ExceptT e m)

Defined in Agda.Compiler.MAlonzo.Misc

Methods

askHsModuleEnv :: ExceptT e m HsModuleEnv

Monad m => ReadHsModuleEnv (ReaderT HsModuleEnv m)

Defined in Agda.Compiler.MAlonzo.Misc

Methods

askHsModuleEnv :: ReaderT HsModuleEnv m HsModuleEnv

Monad m => ReadHsModuleEnv (ReaderT GHCModule m)

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askHsModuleEnv :: ReaderT GHCModule m HsModuleEnv

Monad m => ReadHsModuleEnv (ReaderT GHCModuleEnv m)

Defined in Agda.Compiler.MAlonzo.Compiler

Methods

askHsModuleEnv :: ReaderT GHCModuleEnv m HsModuleEnv

ReadHsModuleEnv m => ReadHsModuleEnv (StateT s m)

Defined in Agda.Compiler.MAlonzo.Misc

Methods

askHsModuleEnv :: StateT s m HsModuleEnv

newtype HsCompileState

Constructors

HsCompileState

Fields

• mazAccumlatedImports :: Set ModuleName

Instances

Eq HsCompileState

Defined in Agda.Compiler.MAlonzo.Misc

Methods

(==) :: HsCompileState -> HsCompileState -> Bool

(/=) :: HsCompileState -> HsCompileState -> Bool

Semigroup HsCompileState

Defined in Agda.Compiler.MAlonzo.Misc

Methods

(<>) :: HsCompileState -> HsCompileState -> HsCompileState

sconcat :: NonEmpty HsCompileState -> HsCompileState

stimes :: Integral b => b -> HsCompileState -> HsCompileState

Monoid HsCompileState

Defined in Agda.Compiler.MAlonzo.Misc

Methods

mempty :: HsCompileState

mappend :: HsCompileState -> HsCompileState -> HsCompileState

mconcat :: [HsCompileState] -> HsCompileState

type HsCompileT m = ReaderT HsModuleEnv (StateT HsCompileState m)

Transformer adding read-only module info and a writable set of imported modules

type HsCompileM = HsCompileT TCM

The default compilation monad is the entire TCM (☹️) enriched with our state and module info

runHsCompileT' :: HsCompileT m a -> HsModuleEnv -> HsCompileState -> m (a, HsCompileState)

runHsCompileT :: HsCompileT m a -> HsModuleEnv -> m (a, HsCompileState)

curIsMainModule :: ReadHsModuleEnv m => m Bool

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

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

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.

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

Name for definition stripped of unused arguments

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

Can the character be used in a Haskell module name part (conid)? This function is more restrictive than what the Haskell report allows.