Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.MAlonzo.Compiler

Synopsis

Documentation

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?

ghcMayEraseType :: QName -> TCM Bool Source #

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

data CCEnv Source #

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

Constructors

CCEnv 

Fields

initCCEnv :: CCEnv Source #

Initial environment for expression generation.

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

Term variables are de Bruijn indices.

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

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

Introduce n variables into the context.

term :: TTerm -> CC Exp Source #

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

noApplication :: TTerm -> CC Exp Source #

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

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

tvaldecl Source #

Arguments

:: QName 
-> Induction

Is the type inductive or coinductive?

-> Nat 
-> [ConDecl] 
-> Maybe Clause 
-> [Decl]