Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Compiler.MAlonzo.Misc

Synopsis

- data HsModuleEnv = HsModuleEnv {
  - mazModuleName :: TopLevelModuleName
  - mazIsMainModule :: Bool
  }
- data GHCOptions = GHCOptions {
  - optGhcCallGhc :: Bool
  - optGhcBin :: FilePath
  - optGhcFlags :: [String]
  - optGhcCompileDir :: FilePath
  - optGhcStrictData :: Bool
  - optGhcStrict :: Bool
  }
- data GHCEnv = 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
  }
- data GHCModuleEnv = GHCModuleEnv {
  - ghcModEnv :: GHCEnv
  - ghcModHsModuleEnv :: HsModuleEnv
  }
- class Monad m => ReadGHCModuleEnv (m :: Type -> Type) where
  - askGHCModuleEnv :: m GHCModuleEnv
  - askHsModuleEnv :: m HsModuleEnv
  - askGHCEnv :: m GHCEnv
- newtype HsCompileState = HsCompileState {
  - mazAccumlatedImports :: Set TopLevelModuleName
  }
- type HsCompileT (m :: Type -> Type) = 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)
- ghcBackendError :: (HasCallStack, MonadTCError m) => GHCBackendError -> m a
- curIsMainModule :: ReadGHCModuleEnv m => m Bool
- curAgdaMod :: ReadGHCModuleEnv m => m TopLevelModuleName
- curHsMod :: ReadGHCModuleEnv m => m ModuleName
- data FunctionKind
  - = NoUnused
  - | PossiblyUnused
- data VariableKind
  - = A
  - | V
  - | X
- 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

- 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

- 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?

data GHCEnv Source #

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

Constructors

GHCEnv |

Fields

- 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

data GHCModuleEnv Source #

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

Constructors

GHCModuleEnv |

Fields

- ghcModEnv :: GHCEnv
- ghcModHsModuleEnv :: HsModuleEnv

#### Instances

Instances details

Monad m => ReadGHCModuleEnv (ReaderT GHCModuleEnv m) Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods askGHCModuleEnv :: ReaderT GHCModuleEnv m GHCModuleEnv Source # askHsModuleEnv :: ReaderT GHCModuleEnv m HsModuleEnv Source # askGHCEnv :: ReaderT GHCModuleEnv m GHCEnv Source #

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 Methods askGHCModuleEnv :: MaybeT m GHCModuleEnv Source # askHsModuleEnv :: MaybeT m HsModuleEnv Source # askGHCEnv :: MaybeT m GHCEnv Source #
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 Methods askGHCModuleEnv :: ReaderT GHCModuleEnv m GHCModuleEnv Source # askHsModuleEnv :: ReaderT GHCModuleEnv m HsModuleEnv Source # askGHCEnv :: ReaderT GHCModuleEnv m GHCEnv Source #
ReadGHCModuleEnv m => ReadGHCModuleEnv (StateT s m) Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods askGHCModuleEnv :: StateT s m GHCModuleEnv Source # askHsModuleEnv :: StateT s m HsModuleEnv Source # askGHCEnv :: StateT s m GHCEnv Source #

newtype HsCompileState Source #

Constructors

HsCompileState |

Fields

- mazAccumlatedImports :: Set TopLevelModuleName

#### Instances

Instances details

Monoid HsCompileState Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods mempty :: HsCompileState Source # mappend :: HsCompileState -> HsCompileState -> HsCompileState Source # mconcat :: [HsCompileState] -> HsCompileState Source #
Semigroup HsCompileState Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods (<>) :: HsCompileState -> HsCompileState -> HsCompileState Source # sconcat :: NonEmpty HsCompileState -> HsCompileState Source # stimes :: Integral b => b -> HsCompileState -> HsCompileState Source #
Eq HsCompileState Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Misc Methods (==) :: HsCompileState -> HsCompileState -> Bool Source # (/=) :: HsCompileState -> HsCompileState -> Bool Source #

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

runHsCompileT' :: HsCompileT m a -> GHCModuleEnv -> HsCompileState -> m (a, HsCompileState) Source #

runHsCompileT :: HsCompileT m a -> GHCModuleEnv -> m (a, HsCompileState) Source #

ghcBackendError :: (HasCallStack, MonadTCError m) => GHCBackendError -> m a 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`.

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.

ihname :: VariableKind -> Nat -> Name Source #

unqhname :: NameKind -> QName -> Name Source #

tlmodOf :: ReadTCState m => ModuleName -> m ModuleName Source #

xqual :: QName -> Name -> HsCompileM QName Source #

xhqn :: NameKind -> QName -> HsCompileM QName Source #

hsName :: String -> QName Source #

conhqn :: QName -> HsCompileM QName Source #

bltQual :: BuiltinId -> String -> HsCompileM QName Source #

dname :: QName -> Name 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 #

hsVarUQ :: Name -> Exp Source #

hsAppView :: Exp -> [Exp] Source #

hsOpToExp :: QOp -> Exp Source #

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

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

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

mazstr :: String Source #

mazName :: Name Source #

mazMod' :: String -> ModuleName Source #

mazMod :: TopLevelModuleName -> ModuleName Source #

mazCoerceName :: String Source #

mazErasedName :: String Source #

mazAnyTypeName :: String Source #

mazCoerce :: Exp Source #

mazUnreachableError :: Exp Source #

rtmUnreachableError :: Exp Source #

mazHole :: Exp Source #

rtmHole :: String -> Exp Source #

mazAnyType :: Type Source #

mazRTE :: ModuleName Source #

mazRTEFloat :: ModuleName Source #

rtmQual :: String -> QName Source #

rtmVar :: String -> Exp Source #

rtmError :: Text -> Exp Source #

unsafeCoerceMod :: ModuleName 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 #

emptyBinds :: Maybe Binds 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.