Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Agda.Compiler.MAlonzo.Misc
Synopsis
- data HsModuleEnv = HsModuleEnv {}
- data GHCOptions = GHCOptions {}
- data GHCEnv = GHCEnv {
- ghcEnvOpts :: GHCOptions
- ghcEnvBool, ghcEnvTrue, ghcEnvFalse, ghcEnvMaybe, ghcEnvNothing, ghcEnvJust, ghcEnvList, ghcEnvNil, ghcEnvCons, ghcEnvNat, ghcEnvInteger, ghcEnvWord64, ghcEnvInf, ghcEnvSharp, ghcEnvFlat, ghcEnvInterval, ghcEnvIZero, ghcEnvIOne, ghcEnvIsOne, ghcEnvItIsOne, ghcEnvIsOne1, ghcEnvIsOne2, ghcEnvIsOneEmpty, ghcEnvPathP, ghcEnvSub, ghcEnvSubIn, ghcEnvId, ghcEnvConId :: Maybe QName
- ghcEnvIsTCBuiltin :: QName -> Bool
- ghcEnvListArity :: Maybe Int
- ghcEnvMaybeArity :: Maybe Int
- data GHCModuleEnv = GHCModuleEnv {}
- class Monad m => ReadGHCModuleEnv m where
- askGHCModuleEnv :: m GHCModuleEnv
- askHsModuleEnv :: m HsModuleEnv
- askGHCEnv :: m GHCEnv
- newtype HsCompileState = HsCompileState {}
- type HsCompileT m = ReaderT GHCModuleEnv (StateT HsCompileState m)
- type HsCompileM = HsCompileT TCM
- runHsCompileT' :: HsCompileT m a -> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState)
- runHsCompileT :: HsCompileT m a -> GHCModuleEnv -> m (a, HsCompileState)
- curIsMainModule :: ReadGHCModuleEnv m => m Bool
- curAgdaMod :: ReadGHCModuleEnv m => m TopLevelModuleName
- curHsMod :: ReadGHCModuleEnv m => m ModuleName
- data FunctionKind
- data VariableKind
- data NameKind
- = TypeK
- | ConK
- | VarK VariableKind
- | CoverK
- | CheckK
- | FunK FunctionKind
- encodeString :: NameKind -> String -> String
- ihname :: VariableKind -> Nat -> Name
- unqhname :: NameKind -> QName -> Name
- tlmodOf :: ReadTCState m => ModuleName -> m ModuleName
- xqual :: QName -> Name -> HsCompileM QName
- xhqn :: NameKind -> QName -> HsCompileM QName
- hsName :: String -> QName
- conhqn :: QName -> HsCompileM QName
- bltQual :: BuiltinId -> 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 :: TopLevelModuleName -> ModuleName
- mazCoerceName :: String
- mazErasedName :: String
- mazAnyTypeName :: String
- mazCoerce :: 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
|
data GHCOptions Source #
The options derived from
GHCFlags
and other shared options.
Constructors
GHCOptions | |
Fields
|
A static part of the GHC backend's environment that does not change from module to module.
Constructors
data GHCModuleEnv Source #
Module compilation environment, bundling the overall backend session options along with the module's basic readable properties.
Constructors
GHCModuleEnv | |
Fields |
Instances
Monad m => ReadGHCModuleEnv (ReaderT GHCModuleEnv m) Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods askGHCModuleEnv :: ReaderT GHCModuleEnv m GHCModuleEnv Source # askHsModuleEnv :: ReaderT GHCModuleEnv m HsModuleEnv Source # |
class Monad m => ReadGHCModuleEnv m where Source #
Monads that can produce a GHCModuleEnv
.
Minimal complete definition
Nothing
Methods
askGHCModuleEnv :: m GHCModuleEnv Source #
default askGHCModuleEnv :: (MonadTrans t, Monad n, m ~ t n, ReadGHCModuleEnv n) => m GHCModuleEnv Source #
askHsModuleEnv :: m HsModuleEnv Source #
Instances
ReadGHCModuleEnv m => ReadGHCModuleEnv (MaybeT m) Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods askGHCModuleEnv :: MaybeT m GHCModuleEnv Source # | |
ReadGHCModuleEnv m => ReadGHCModuleEnv (ExceptT e m) Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods askGHCModuleEnv :: ExceptT e m GHCModuleEnv Source # askHsModuleEnv :: ExceptT e m HsModuleEnv Source # | |
ReadGHCModuleEnv m => ReadGHCModuleEnv (IdentityT m) Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods askGHCModuleEnv :: IdentityT m GHCModuleEnv Source # | |
Monad m => ReadGHCModuleEnv (ReaderT GHCModuleEnv m) Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods askGHCModuleEnv :: ReaderT GHCModuleEnv m GHCModuleEnv Source # askHsModuleEnv :: ReaderT GHCModuleEnv m HsModuleEnv Source # | |
ReadGHCModuleEnv m => ReadGHCModuleEnv (StateT s m) Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods askGHCModuleEnv :: StateT s m GHCModuleEnv Source # askHsModuleEnv :: StateT s m HsModuleEnv Source # |
newtype HsCompileState Source #
Constructors
HsCompileState | |
Fields |
Instances
Monoid HsCompileState Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods mappend :: HsCompileState -> HsCompileState -> HsCompileState # mconcat :: [HsCompileState] -> HsCompileState # | |
Semigroup HsCompileState Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods (<>) :: HsCompileState -> HsCompileState -> HsCompileState # sconcat :: NonEmpty HsCompileState -> HsCompileState # stimes :: Integral b => b -> HsCompileState -> HsCompileState # | |
Eq HsCompileState Source # | |
Defined in Agda.Compiler.MAlonzo.Misc Methods (==) :: HsCompileState -> HsCompileState -> Bool # (/=) :: HsCompileState -> HsCompileState -> Bool # |
type HsCompileT m = ReaderT GHCModuleEnv (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 -> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState) Source #
runHsCompileT :: HsCompileT m a -> GHCModuleEnv -> m (a, HsCompileState) Source #
curIsMainModule :: ReadGHCModuleEnv 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 :: ReadGHCModuleEnv m => m TopLevelModuleName 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 :: ReadGHCModuleEnv m => m ModuleName Source #
Get the Haskell module name of the currently-focused Agda module
data FunctionKind Source #
There are two kinds of functions: those definitely without unused arguments, and those that might have unused arguments.
Constructors
NoUnused | |
PossiblyUnused |
data VariableKind Source #
Different kinds of variables: those starting with a
, those
starting with v
, and those starting with x
.
Different kinds of names.
Constructors
TypeK | Types. |
ConK | Constructors. |
VarK VariableKind | Variables. |
CoverK | Used for coverage checking. |
CheckK | Used for constructor type checking. |
FunK FunctionKind | Other functions. |
encodeString :: NameKind -> String -> String Source #
Turns strings into valid Haskell identifiers.
In order to avoid clashes with names of regular Haskell definitions (those not generated from Agda definitions), make sure that the Haskell names are always used qualified, with the exception of names from the prelude.
tlmodOf :: ReadTCState m => ModuleName -> m ModuleName Source #
hsTypedInt :: Integral a => a -> Exp Source #
hsTypedDouble :: Real a => a -> Exp Source #
mazMod' :: String -> ModuleName Source #
mazAnyType :: Type Source #
mazRTE :: ModuleName Source #
emptyBinds :: Maybe Binds Source #