ModuleAgda-2.8.0.2Haskell2010

Agda.Compiler.MAlonzo.Misc

Synopsis

data HsModuleEnv
data GHCOptions
data GHCEnv
data GHCModuleEnv
class ReadGHCModuleEnv
newtype HsCompileState
type HsCompileT
type HsCompileM
value runHsCompileT'
value runHsCompileT
value ghcBackendError
value curIsMainModule
value curAgdaMod
value curHsMod
data FunctionKind
data VariableKind
data NameKind
value encodeString
value ihname
value unqhname
value tlmodOf
value xqual
value xhqn
value hsName
value conhqn
value bltQual
value dname
value duname
value hsPrimOp
value hsPrimOpApp
value hsInt
value hsTypedInt
value hsTypedDouble
value hsLet
value hsVarUQ
value hsAppView
value hsOpToExp
value hsLambda
value hsMapAlt
value hsMapRHS
value mazstr
value mazName
value mazMod'
value mazMod
value mazCoerceName
value mazErasedName
value mazAnyTypeName
value mazCoerce
value mazUnreachableError
value rtmUnreachableError
value mazHole
value rtmHole
value mazAnyType
value mazRTE
value mazRTEFloat
value rtmQual
value rtmVar
value rtmError
value unsafeCoerceMod
value fakeD
value fakeDS
value fakeDQ
value fakeType
value fakeExp
value fakeDecl
value emptyBinds
value isModChar

PackageAgda-2.8.0.2
Exports67
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

Source#

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.8.0.2 · Agda.Compiler.MAlonzo.Compiler

datadata GHCEnv

Source#

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
- ghcEnvIsTCBuiltin :: QName -> Bool
- ghcEnvListArity :: Maybe Int
- ghcEnvMaybeArity :: Maybe Int

Instances1ReadGHCOpts

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

datadata GHCModuleEnv

Source#

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

Constructors

GHCModuleEnv
- ghcModEnv :: GHCEnv
- ghcModHsModuleEnv :: HsModuleEnv

Instances2ReadGHCOpts, ReadGHCModuleEnv

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

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

Source#

Monads that can produce a GHCModuleEnv.

Instances6ReadGHCModuleEnv

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

newtypenewtype HsCompileState

Constructors

HsCompileState
- mazAccumlatedImports :: Set TopLevelModuleName

Instances3Eq, Semigroup, Monoid

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

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

Source#

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

typetype HsCompileM = HsCompileT TCM

Source#

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)

valueghcBackendError :: (HasCallStack, MonadTCError m) => GHCBackendError -> m a

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

valuecurAgdaMod :: 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)

valuecurHsMod :: ReadGHCModuleEnv m => m ModuleName

Source#

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

datadata FunctionKind

Source#

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

NoUnused PossiblyUnused

datadata VariableKind

Source#

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

A V X

datadata NameKind

Source#

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

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.

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

Source#

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

Source#

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