ModuleAgda-2.7.0.1Haskell2010

Agda.Compiler.MAlonzo.Misc

10 types
1 class
55 values

PackageAgda-2.7.0.1
Exports66
LanguageHaskell2010
LicenceMIT
SourceMisc.hs

datadata HsModuleEnv

Constructors

HsModuleEnv
- mazModuleName :: TopLevelModuleName
  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.

datadata GHCOptions

The options derived from Agda.Compiler.MAlonzo.Compiler.GHCFlags and other shared options.

Constructors

GHCOptions
- optGhcCallGhc :: Bool
- optGhcBin :: FilePath
  Use the compiler at PATH instead of "ghc"
- optGhcFlags :: [String]
- optGhcCompileDir :: FilePath
- optGhcStrictData :: Bool
  Make inductive constructors strict?
- optGhcStrict :: Bool
  Make functions strict?

Instances1ReadGHCOpts

Monad m => ReadGHCOpts (ReaderT GHCOptions m)Defined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Compiler

datadata GHCEnv

A static part of the GHC backend's environment that does not change from module to module.

Constructors

GHCEnv
- ghcEnvOpts :: GHCOptions
- ghcEnvBool :: Maybe QName
- ghcEnvTrue :: Maybe QName
- ghcEnvFalse :: Maybe QName
- ghcEnvMaybe :: Maybe QName
- ghcEnvNothing :: Maybe QName
- ghcEnvJust :: Maybe QName
- ghcEnvList :: Maybe QName
- ghcEnvNil :: Maybe QName
- ghcEnvCons :: Maybe QName
- ghcEnvNat :: Maybe QName
- ghcEnvInteger :: Maybe QName
- ghcEnvWord64 :: Maybe QName
- ghcEnvInf :: Maybe QName
- ghcEnvSharp :: Maybe QName
- ghcEnvFlat :: Maybe QName
- ghcEnvInterval :: Maybe QName
- ghcEnvIZero :: Maybe QName
- ghcEnvIOne :: Maybe QName
- ghcEnvIsOne :: Maybe QName
- ghcEnvItIsOne :: Maybe QName
- ghcEnvIsOne1 :: Maybe QName
- ghcEnvIsOne2 :: Maybe QName
- ghcEnvIsOneEmpty :: Maybe QName
- ghcEnvPathP :: Maybe QName
- ghcEnvSub :: Maybe QName
- ghcEnvSubIn :: Maybe QName
- ghcEnvId :: Maybe QName
- ghcEnvConId :: Maybe QName
- ghcEnvIsTCBuiltin :: QName -> Bool
- ghcEnvListArity :: Maybe Int
- ghcEnvMaybeArity :: Maybe Int

Instances1ReadGHCOpts

Monad m => ReadGHCOpts (ReaderT GHCEnv m)Defined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Compiler

datadata GHCModuleEnv

Module compilation environment, bundling the overall backend session options along with the module's basic readable properties.

Constructors

GHCModuleEnv
- ghcModEnv :: GHCEnv
- ghcModHsModuleEnv :: HsModuleEnv

Instances2ReadGHCModuleEnv, ReadGHCOpts

Monad m => ReadGHCModuleEnv (ReaderT GHCModuleEnv m)Defined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Misc
Monad m => ReadGHCOpts (ReaderT GHCModuleEnv m)Defined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Compiler

classclass Monad m => ReadGHCModuleEnv (m :: Type -> Type) where

Monads that can produce a GHCModuleEnv.

Instances6ReadGHCModuleEnv

ReadGHCModuleEnv m => ReadGHCModuleEnv (MaybeT m)Defined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Misc
ReadGHCModuleEnv m => ReadGHCModuleEnv (ExceptT e m)Defined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Misc
ReadGHCModuleEnv m => ReadGHCModuleEnv (IdentityT m)Defined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Misc
ReadGHCModuleEnv m => ReadGHCModuleEnv (StateT s m)Defined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Misc
Monad m => ReadGHCModuleEnv (ReaderT GHCModule m)Defined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Compiler
Monad m => ReadGHCModuleEnv (ReaderT GHCModuleEnv m)Defined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Misc

newtypenewtype HsCompileState

Constructors

HsCompileState
- mazAccumlatedImports :: Set TopLevelModuleName

Instances3Eq, Semigroup, Monoid

Eq HsCompileStateDefined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Misc
Semigroup HsCompileStateDefined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Misc
Monoid HsCompileStateDefined in Agda-2.7.0.1 · Agda.Compiler.MAlonzo.Misc

typetype HsCompileT (m :: Type -> Type) = ReaderT GHCModuleEnv (StateT HsCompileState m)

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

typetype HsCompileM = HsCompileT TCM

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

valuerunHsCompileT'

:: HsCompileT m a
-> GHCModuleEnv
-> HsCompileState
-> m (a, HsCompileState)

valuerunHsCompileT :: HsCompileT m a -> GHCModuleEnv -> m (a, HsCompileState)

valuecurIsMainModule :: ReadGHCModuleEnv 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.

valuecurAgdaMod :: ReadGHCModuleEnv m => m TopLevelModuleName

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)

valuecurHsMod :: ReadGHCModuleEnv m => m ModuleName

Get the Haskell module name of the currently-focused Agda module

datadata FunctionKind

There are two kinds of functions: those definitely without unused arguments, and those that might have unused arguments.

NoUnused PossiblyUnused

datadata VariableKind

Different kinds of variables: those starting with a, those starting with v, and those starting with x.

A V X

datadata NameKind

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.

valueencodeString :: NameKind -> String -> String

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.

valueihname :: VariableKind -> Nat -> Name

valueunqhname :: NameKind -> QName -> Name

valuetlmodOf :: ReadTCState m => ModuleName -> m ModuleName

valuexqual :: QName -> Name -> HsCompileM QName

valuexhqn :: NameKind -> QName -> HsCompileM QName

valuehsName :: String -> QName

valueconhqn :: QName -> HsCompileM QName

valuebltQual :: BuiltinId -> String -> HsCompileM QName

valuedname :: QName -> Name

valueduname :: QName -> Name

Name for definition stripped of unused arguments

valuehsPrimOp :: String -> QOp

valuehsPrimOpApp :: String -> Exp -> Exp -> Exp

valuehsInt :: Integer -> Exp

valuehsTypedInt :: Integral a => a -> Exp

valuehsTypedDouble :: Real a => a -> Exp

valuehsLet :: Name -> Exp -> Exp -> Exp

valuehsVarUQ :: Name -> Exp

valuehsAppView :: Exp -> [Exp]

valuehsOpToExp :: QOp -> Exp

valuehsLambda :: [Pat] -> Exp -> Exp

valuehsMapAlt :: (Exp -> Exp) -> Alt -> Alt

valuehsMapRHS :: (Exp -> Exp) -> Rhs -> Rhs

valuemazstr :: String

valuemazName :: Name

valuemazMod' :: String -> ModuleName

valuemazMod :: TopLevelModuleName -> ModuleName

valuemazCoerceName :: String

valuemazErasedName :: String

valuemazAnyTypeName :: String

valuemazCoerce :: Exp

valuemazUnreachableError :: Exp

valuertmUnreachableError :: Exp

valuemazHole :: Exp

valuertmHole :: String -> Exp

valuemazAnyType :: Type

valuemazRTE :: ModuleName

valuemazRTEFloat :: ModuleName

valuertmQual :: String -> QName

valuertmVar :: String -> Exp

valuertmError :: Text -> Exp

valueunsafeCoerceMod :: ModuleName

valuefakeD :: Name -> String -> Decl

valuefakeDS :: String -> String -> Decl

valuefakeDQ :: QName -> String -> Decl

valuefakeType :: String -> Type

valuefakeExp :: String -> Exp

valuefakeDecl :: String -> Decl

valueemptyBinds :: Maybe Binds

valueisModChar :: 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.