Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.MAlonzo.Misc

Synopsis

Documentation

data HsModuleEnv Source #

Constructors

HsModuleEnv 

Fields

  • 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.

data GHCOptions Source #

The options derived from GHCFlags and other shared options.

Constructors

GHCOptions 

Fields

data GHCModuleEnv Source #

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

Instances

Instances details
Monad m => ReadGHCModuleEnv (ReaderT GHCModuleEnv m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Misc

class Monad m => ReadGHCModuleEnv (m :: Type -> Type) where Source #

Monads that can produce a GHCModuleEnv.

Minimal complete definition

Nothing

Methods

askGHCModuleEnv :: m GHCModuleEnv Source #

default askGHCModuleEnv :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, Monad n, m ~ t n, ReadGHCModuleEnv n) => m GHCModuleEnv Source #

askHsModuleEnv :: m HsModuleEnv Source #

askGHCEnv :: m GHCEnv Source #

Instances

Instances details
ReadGHCModuleEnv m => ReadGHCModuleEnv (MaybeT m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Misc

ReadGHCModuleEnv m => ReadGHCModuleEnv (ExceptT e m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Misc

Methods

askGHCModuleEnv :: ExceptT e m GHCModuleEnv Source #

askHsModuleEnv :: ExceptT e m HsModuleEnv Source #

askGHCEnv :: ExceptT e m GHCEnv Source #

ReadGHCModuleEnv m => ReadGHCModuleEnv (IdentityT m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Misc

Methods

askGHCModuleEnv :: IdentityT m GHCModuleEnv Source #

askHsModuleEnv :: IdentityT m HsModuleEnv Source #

askGHCEnv :: IdentityT m GHCEnv Source #

Monad m => ReadGHCModuleEnv (ReaderT GHCModuleEnv m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Misc

ReadGHCModuleEnv m => ReadGHCModuleEnv (StateT s m) Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Misc

type HsCompileT (m :: Type -> Type) = 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

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.

Constructors

A 
V 
X 

data 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.

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.

hsName :: String -> QName Source #

duname :: QName -> Name Source #

Name for definition stripped of unused arguments

hsPrimOp :: String -> QOp Source #

hsPrimOpApp :: String -> Exp -> Exp -> Exp Source #

hsInt :: Integer -> Exp Source #

hsTypedInt :: Integral a => a -> Exp Source #

hsTypedDouble :: Real a => a -> Exp Source #

hsLet :: Name -> Exp -> Exp -> Exp Source #

hsLambda :: [Pat] -> Exp -> Exp Source #

hsMapAlt :: (Exp -> Exp) -> Alt -> Alt Source #

hsMapRHS :: (Exp -> Exp) -> Rhs -> Rhs Source #

mazstr :: String Source #

mazMod' :: String -> ModuleName Source #

rtmHole :: String -> Exp Source #

rtmQual :: String -> QName Source #

rtmVar :: String -> Exp Source #

rtmError :: Text -> Exp Source #

fakeD :: Name -> String -> Decl Source #

fakeDS :: String -> String -> Decl Source #

fakeDQ :: QName -> String -> Decl Source #

fakeType :: String -> Type Source #

fakeExp :: String -> Exp Source #

fakeDecl :: String -> Decl Source #

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