| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Compiler.MAlonzo.Compiler
Synopsis
- ghcBackend :: Backend
- ghcBackend' :: Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
- data GHCFlags = GHCFlags {}
- defaultGHCFlags :: GHCFlags
- ghcCommandLineFlags :: [OptDescr (Flag GHCFlags)]
- withCompilerFlag :: FilePath -> Flag GHCFlags
- class Monad m => ReadGHCOpts m where
- askGhcOpts :: m GHCOptions
- data GHCModule = GHCModule {}
- data GHCDefinition = GHCDefinition {}
- ghcPreCompile :: GHCFlags -> TCM GHCEnv
- ghcPostCompile :: GHCEnv -> IsMain -> Map ModuleName GHCModule -> TCM ()
- ghcPreModule :: GHCEnv -> IsMain -> ModuleName -> Maybe FilePath -> TCM (Recompile GHCModuleEnv GHCModule)
- ghcPostModule :: GHCEnv -> GHCModuleEnv -> IsMain -> ModuleName -> [GHCDefinition] -> TCM GHCModule
- ghcCompileDef :: GHCEnv -> GHCModuleEnv -> IsMain -> Definition -> TCM GHCDefinition
- ghcMayEraseType :: QName -> TCM Bool
- imports :: BuiltinThings PrimFun -> Set ModuleName -> [Definition] -> [ImportDecl]
- newtype UsesFloat = UsesFloat Bool
- pattern YesFloat :: UsesFloat
- pattern NoFloat :: UsesFloat
- mazRTEFloatImport :: UsesFloat -> [ImportDecl]
- definition :: Definition -> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
- constructorCoverageCode :: QName -> Int -> [QName] -> HaskellType -> [HaskellCode] -> HsCompileM [Decl]
- data CCEnv = CCEnv {}
- type NameSupply = [Name]
- type CCContext = [Name]
- ccNameSupply :: Lens' NameSupply CCEnv
- ccContext :: Lens' CCContext CCEnv
- initCCEnv :: CCEnv
- lookupIndex :: Int -> CCContext -> Name
- type CCT m = ReaderT CCEnv (WriterT UsesFloat (HsCompileT m))
- type CC = CCT TCM
- liftCC :: Monad m => HsCompileT m a -> CCT m a
- freshNames :: Monad m => Int -> ([Name] -> CCT m a) -> CCT m a
- intros :: Monad m => Int -> ([Name] -> CCT m a) -> CCT m a
- checkConstructorType :: QName -> HaskellCode -> HsCompileM [Decl]
- checkCover :: HasConstInfo m => QName -> HaskellType -> Nat -> [QName] -> [HaskellCode] -> m [Decl]
- closedTerm_ :: TTerm -> HsCompileM Exp
- closedTerm :: TTerm -> HsCompileM (Exp, UsesFloat)
- mkIf :: TTerm -> CC TTerm
- term :: TTerm -> CC Exp
- noApplication :: TTerm -> CC Exp
- hsCoerce :: Exp -> Exp
- compilePrim :: TPrim -> Exp
- alt :: Int -> TAlt -> CC Alt
- literal :: forall m. Monad m => Literal -> CCT m Exp
- hslit :: Literal -> Literal
- litString :: Text -> Exp
- litqname :: QName -> Exp
- litqnamepat :: QName -> Pat
- condecl :: QName -> Induction -> HsCompileM ConDecl
- compiledcondecl :: Maybe Nat -> QName -> HsCompileM Decl
- compiledTypeSynonym :: QName -> String -> Nat -> Decl
- tvaldecl :: QName -> Induction -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
- infodecl :: QName -> [Decl] -> [Decl]
- type MonadGHCIO m = (MonadIO m, ReadGHCOpts m)
- copyRTEModules :: MonadGHCIO m => m ()
- writeModule :: MonadGHCIO m => Module -> m ()
- outFileAndDir :: MonadGHCIO m => ModuleName -> m (FilePath, FilePath)
- curOutFileAndDir :: (MonadGHCIO m, ReadGHCModuleEnv m) => m (FilePath, FilePath)
- curOutFile :: (MonadGHCIO m, ReadGHCModuleEnv m) => m FilePath
- callGHC :: ReaderT GHCModule TCM ()
Documentation
ghcBackend :: Backend Source #
Constructors
| GHCFlags | |
Fields
| |
Instances
class Monad m => ReadGHCOpts m where Source #
Monads that can read GHCOptions
Methods
askGhcOpts :: m GHCOptions Source #
Instances
| Monad m => ReadGHCOpts (ReaderT GHCModule m) Source # | |
Defined in Agda.Compiler.MAlonzo.Compiler Methods askGhcOpts :: ReaderT GHCModule m GHCOptions Source # | |
| Monad m => ReadGHCOpts (ReaderT GHCEnv m) Source # | |
Defined in Agda.Compiler.MAlonzo.Compiler Methods askGhcOpts :: ReaderT GHCEnv m GHCOptions Source # | |
| Monad m => ReadGHCOpts (ReaderT GHCModuleEnv m) Source # | |
Defined in Agda.Compiler.MAlonzo.Compiler Methods askGhcOpts :: ReaderT GHCModuleEnv m GHCOptions Source # | |
| Monad m => ReadGHCOpts (ReaderT GHCOptions m) Source # | |
Defined in Agda.Compiler.MAlonzo.Compiler Methods askGhcOpts :: ReaderT GHCOptions m GHCOptions Source # | |
Constructors
| GHCModule | |
Fields
| |
Instances
| Monad m => ReadGHCOpts (ReaderT GHCModule m) Source # | |
Defined in Agda.Compiler.MAlonzo.Compiler Methods askGhcOpts :: ReaderT GHCModule m GHCOptions Source # | |
| Monad m => ReadGHCModuleEnv (ReaderT GHCModule m) Source # | |
Defined in Agda.Compiler.MAlonzo.Compiler Methods askGHCModuleEnv :: ReaderT GHCModule m GHCModuleEnv Source # askHsModuleEnv :: ReaderT GHCModule m HsModuleEnv Source # | |
data GHCDefinition Source #
Constructors
| GHCDefinition | |
Fields | |
ghcPostCompile :: GHCEnv -> IsMain -> Map ModuleName GHCModule -> TCM () Source #
Arguments
| :: GHCEnv | |
| -> IsMain | Are we looking at the main module? |
| -> ModuleName | |
| -> Maybe FilePath | Path to the |
| -> TCM (Recompile GHCModuleEnv GHCModule) | Could we confirm the existence of a main function? |
Arguments
| :: GHCEnv | |
| -> GHCModuleEnv | |
| -> IsMain | Are we looking at the main module? |
| -> ModuleName | |
| -> [GHCDefinition] | Compiled module content. |
| -> TCM GHCModule |
ghcCompileDef :: GHCEnv -> GHCModuleEnv -> IsMain -> Definition -> TCM GHCDefinition Source #
ghcMayEraseType :: QName -> TCM Bool Source #
We do not erase types that have a HsData pragma.
This is to ensure a stable interface to third-party code.
imports :: BuiltinThings PrimFun -> Set ModuleName -> [Definition] -> [ImportDecl] Source #
mazRTEFloatImport :: UsesFloat -> [ImportDecl] Source #
definition :: Definition -> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef) Source #
constructorCoverageCode :: QName -> Int -> [QName] -> HaskellType -> [HaskellCode] -> HsCompileM [Decl] Source #
Environment for naming of local variables.
Invariant: reverse ccCxt ++ ccNameSupply
Constructors
| CCEnv | |
Fields
| |
type NameSupply = [Name] Source #
type CCT m = ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) Source #
Constructor coverage monad transformer
intros :: Monad m => Int -> ([Name] -> CCT m a) -> CCT m a Source #
Introduce n variables into the context.
checkConstructorType :: QName -> HaskellCode -> HsCompileM [Decl] Source #
checkCover :: HasConstInfo m => QName -> HaskellType -> Nat -> [QName] -> [HaskellCode] -> m [Decl] Source #
closedTerm_ :: TTerm -> HsCompileM Exp Source #
closedTerm :: TTerm -> HsCompileM (Exp, UsesFloat) Source #
term :: TTerm -> CC Exp Source #
Extract Agda term to Haskell expression.
Erased arguments are extracted as ().
Types are extracted as ().
noApplication :: TTerm -> CC Exp Source #
Translate a non-application, non-coercion, non-constructor, non-definition term.
compilePrim :: TPrim -> Exp Source #
litqnamepat :: QName -> Pat Source #
Arguments
| :: Maybe Nat | The constructor's arity (after erasure). |
| -> QName | |
| -> HsCompileM Decl |
type MonadGHCIO m = (MonadIO m, ReadGHCOpts m) Source #
copyRTEModules :: MonadGHCIO m => m () Source #
writeModule :: MonadGHCIO m => Module -> m () Source #
outFileAndDir :: MonadGHCIO m => ModuleName -> m (FilePath, FilePath) Source #
curOutFileAndDir :: (MonadGHCIO m, ReadGHCModuleEnv m) => m (FilePath, FilePath) Source #
curOutFile :: (MonadGHCIO m, ReadGHCModuleEnv m) => m FilePath Source #