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 -> ModuleName -> FilePath -> TCM (Recompile GHCModuleEnv IsMain)
ghcPostModule :: GHCOptions -> GHCModuleEnv -> IsMain -> ModuleName -> [[Decl]] -> TCM IsMain
ghcCompileDef :: GHCOptions -> GHCModuleEnv -> Definition -> TCM [Decl]
imports :: TCM [ImportDecl]
definition :: GHCModuleEnv -> 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
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
erasedArity :: QName -> TCM Nat
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 #

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

data GHCOptions #

Constructors

GHCOptions
Fields 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 = () #

This environment is no longer used for anything.

ghcPreModule :: GHCOptions -> ModuleName -> FilePath -> TCM (Recompile GHCModuleEnv IsMain) #

ghcPostModule :: GHCOptions -> GHCModuleEnv -> IsMain -> ModuleName -> [[Decl]] -> TCM IsMain #

ghcCompileDef :: GHCOptions -> GHCModuleEnv -> Definition -> TCM [Decl] #

imports :: TCM [ImportDecl] #

definition :: GHCModuleEnv -> Definition -> TCM [Decl] #

constructorCoverageCode :: QName -> Int -> [QName] -> HaskellType -> [HaskellCode] -> TCM [Decl] #

data CCEnv #

Environment for naming of local variables. Invariant: reverse ccCxt ++ ccNameSupply

Constructors

CCEnv
Fields _ccNameSupply :: NameSupply Supply of fresh names _ccContext :: CCContext Names currently in scope

type NameSupply = [Name] #

type CCContext = [Name] #

ccNameSupply :: Lens' NameSupply CCEnv #

ccContext :: Lens' CCContext CCEnv #

initCCEnv :: CCEnv #

Initial environment for expression generation.

lookupIndex :: Int -> CCContext -> Name #

Term variables are de Bruijn indices.

type CC = ReaderT CCEnv TCM #

freshNames :: Int -> ([Name] -> CC a) -> CC a #

intros :: Int -> ([Name] -> CC a) -> CC a #

Introduce n variables into the context.

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 #

Extract Agda term to Haskell expression. Erased arguments are extracted as (). Types are extracted as ().

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 #

erasedArity :: QName -> TCM Nat #

condecl :: QName -> Induction -> TCM ConDecl #

compiledcondecl :: QName -> TCM Decl #

compiledTypeSynonym :: QName -> String -> Nat -> Decl #

tvaldecl #

Arguments

:: QName
-> Induction	Is the type inductive or coinductive?
-> 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 () #