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 = Maybe CoinductionKit

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 :: Maybe CoinductionKit -> Definition -> TCM [Decl]

Note that the INFINITY, SHARP and FLAT builtins are translated as follows (if a CoinductionKit is given):

  type Infinity a b = b

  sharp :: a -> a
  sharp x = x

  flat :: a -> a
  flat x = x

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

• ccCxt :: CCContext

  Names currently in scope

type NameSupply = [Name]

type CCContext = [Name]

mapNameSupply :: (NameSupply -> NameSupply) -> CCEnv -> CCEnv

mapContext :: (CCContext -> CCContext) -> CCEnv -> 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

term :: TTerm -> CC Exp

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

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 -> TCM (Nat, ConDecl)

cdecl :: QName -> Nat -> ConDecl

compiledcondecl :: QName -> TCM Decl

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

tvaldecl

Arguments

:: QName

-> Induction

Is the type inductive or coinductive?

-> Nat

-> Nat

-> [ConDecl]

-> Maybe Clause

-> [Decl]

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

hsCast :: Exp -> Exp

hsCast' :: Exp -> Exp

hsCastApp :: Exp -> Exp

hsCoerce :: Exp -> Exp

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