Safe Haskell	None
Language	Haskell2010

Agda.Compiler.MAlonzo.Compiler

Synopsis

ghcBackend :: Backend
ghcBackend' :: Backend' GHCOptions GHCOptions GHCModuleEnv IsMain [Decl]
data GHCOptions = GHCOptions {
- optGhcCompile :: Bool
- optGhcCallGhc :: Bool
- optGhcFlags :: [String]
}
defaultGHCOptions :: GHCOptions
ghcCommandLineFlags :: [OptDescr (Flag GHCOptions)]
ghcPreCompile :: GHCOptions -> TCM GHCOptions
ghcPostCompile :: GHCOptions -> IsMain -> Map ModuleName IsMain -> TCM ()
type GHCModuleEnv = ()
ghcPreModule :: GHCOptions -> IsMain -> ModuleName -> FilePath -> TCM (Recompile GHCModuleEnv IsMain)
ghcPostModule :: GHCOptions -> GHCModuleEnv -> IsMain -> ModuleName -> [[Decl]] -> TCM IsMain
ghcCompileDef :: GHCOptions -> GHCModuleEnv -> IsMain -> Definition -> TCM [Decl]
ghcMayEraseType :: QName -> TCM Bool
imports :: TCM [ImportDecl]
definition :: GHCModuleEnv -> IsMain -> Definition -> TCM [Decl]
constructorCoverageCode :: QName -> Int -> [QName] -> HaskellType -> [HaskellCode] -> TCM [Decl]
data CCEnv = CCEnv {
- _ccNameSupply :: NameSupply
- _ccContext :: CCContext
}
type NameSupply = [Name]
type CCContext = [Name]
ccNameSupply :: Lens' NameSupply CCEnv
ccContext :: Lens' CCContext CCEnv
initCCEnv :: CCEnv
lookupIndex :: Int -> CCContext -> Name
type CC = ReaderT CCEnv TCM
freshNames :: Int -> ([Name] -> CC a) -> CC a
intros :: Int -> ([Name] -> CC a) -> CC a
checkConstructorType :: QName -> HaskellCode -> TCM [Decl]
checkCover :: QName -> HaskellType -> Nat -> [QName] -> [HaskellCode] -> TCM [Decl]
closedTerm :: TTerm -> TCM Exp
mkIf :: TTerm -> CC TTerm
term :: TTerm -> CC Exp
noApplication :: TTerm -> CC Exp
hsCoerce :: Exp -> Exp
compilePrim :: TPrim -> Exp
alt :: Int -> TAlt -> CC Alt
literal :: Literal -> Exp
hslit :: Literal -> Literal
litString :: String -> Exp
litqname :: QName -> Exp
litqnamepat :: QName -> Pat
condecl :: QName -> Induction -> TCM ConDecl
compiledcondecl :: QName -> TCM Decl
compiledTypeSynonym :: QName -> String -> Nat -> Decl
tvaldecl :: QName -> Induction -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
infodecl :: QName -> [Decl] -> [Decl]
copyRTEModules :: TCM ()
writeModule :: Module -> TCM ()
outFile' :: Pretty a => a -> TCM (FilePath, FilePath)
outFile :: ModuleName -> TCM FilePath
outFile_ :: TCM FilePath
callGHC :: GHCOptions -> IsMain -> Map ModuleName IsMain -> TCM ()

Documentation

ghcBackend :: Backend Source #

ghcBackend' :: Backend' GHCOptions GHCOptions GHCModuleEnv IsMain [Decl] Source #

data GHCOptions Source #

Constructors

GHCOptions
Fields optGhcCompile :: Bool optGhcCallGhc :: Bool optGhcFlags :: [String]

defaultGHCOptions :: GHCOptions Source #

ghcCommandLineFlags :: [OptDescr (Flag GHCOptions)] Source #

ghcPreCompile :: GHCOptions -> TCM GHCOptions Source #

ghcPostCompile :: GHCOptions -> IsMain -> Map ModuleName IsMain -> TCM () Source #

type GHCModuleEnv = () Source #

This environment is no longer used for anything.

ghcPreModule Source #

Arguments

:: GHCOptions
-> IsMain	Are we looking at the main module?
-> ModuleName
-> FilePath	Path to the `.agdai` file.
-> TCM (Recompile GHCModuleEnv IsMain)	Could we confirm the existence of a main function?

ghcPostModule Source #

Arguments

:: GHCOptions
-> GHCModuleEnv
-> IsMain	Are we looking at the main module?
-> ModuleName
-> [[Decl]]	Compiled module content.
-> TCM IsMain	Could we confirm the existence of a main function?