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

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 -> IsMain -> Definition -> TCM [Decl]
- 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
- 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 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 :: GHCOptions -> ModuleName -> FilePath -> TCM (Recompile GHCModuleEnv IsMain) Source #

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

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

imports :: TCM [ImportDecl] Source #

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

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

data CCEnv Source #

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] Source #

type CCContext = [Name] Source #

ccNameSupply :: Lens' NameSupply CCEnv Source #

ccContext :: Lens' CCContext CCEnv Source #

initCCEnv :: CCEnv Source #

Initial environment for expression generation.

lookupIndex :: Int -> CCContext -> Name Source #

Term variables are de Bruijn indices.

type CC = ReaderT CCEnv TCM Source #

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

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

Introduce n variables into the context.

checkConstructorType :: QName -> HaskellCode -> TCM [Decl] Source #

checkCover :: QName -> HaskellType -> Nat -> [QName] -> [HaskellCode] -> TCM [Decl] Source #

closedTerm :: TTerm -> TCM Exp Source #

mkIf :: TTerm -> CC TTerm Source #

term :: TTerm -> CC Exp Source #

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

hsCoerce :: Exp -> Exp Source #

compilePrim :: TPrim -> Exp Source #

alt :: Int -> TAlt -> CC Alt Source #

literal :: Literal -> Exp Source #

hslit :: Literal -> Literal Source #

litString :: String -> Exp Source #

litqname :: QName -> Exp Source #

litqnamepat :: QName -> Pat Source #

erasedArity :: QName -> TCM Nat Source #

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

compiledcondecl :: QName -> TCM Decl Source #

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

tvaldecl Source #

Arguments

:: QName |
-> Induction | Is the type inductive or coinductive?
-> Nat |
-> [ConDecl] |
-> Maybe Clause |
-> [Decl] |

infodecl :: QName -> [Decl] -> [Decl] Source #

copyRTEModules :: TCM () Source #

writeModule :: Module -> TCM () Source #

outFile' :: Pretty a => a -> TCM (FilePath, FilePath) Source #

outFile :: ModuleName -> TCM FilePath Source #

outFile_ :: TCM FilePath Source #

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