Agda.Compiler.MAlonzo.Compiler

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

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

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?

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

ghcMayEraseType :: QName -> TCM Bool

We do not erase types that have a HsData pragma. This is to ensure a stable interface to third-party code.

imports :: TCM [ImportDecl]

definition :: GHCModuleEnv -> IsMain -> 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 ().

noApplication :: TTerm -> CC Exp

Translate a non-application, non-coercion, non-constructor, non-definition term.

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

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 ()