| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Compiler.MAlonzo.Compiler

Synopsis

compilerMain :: Interface -> TCM ()
compile :: Interface -> TCM ()
imports :: TCM [HsImportDecl]
definitions :: Definitions -> TCM [HsDecl]
definition :: Definition -> TCM [HsDecl]
checkConstructorType :: QName -> TCM [HsDecl]
checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [HsDecl]
constructorArity :: MonadTCM tcm => QName -> tcm Nat
clause :: QName -> (Nat, Bool, Clause) -> TCM HsDecl
argpatts :: [Arg Pattern] -> [HsPat] -> TCM [HsPat]
clausebody :: ClauseBody -> TCM HsExp
term :: Term -> ReaderT Nat TCM HsExp
literal :: Literal -> TCM HsExp
hslit :: Literal -> HsLiteral
condecl :: QName -> TCM (Nat, HsConDecl)
cdecl :: QName -> Nat -> HsConDecl
tvaldecl :: QName -> Induction -> Nat -> Nat -> [HsConDecl] -> Maybe Clause -> [HsDecl]
infodecl :: QName -> HsDecl
hsCast :: HsExp -> HsExp
writeModule :: HsModule -> TCM ()
malonzoDir :: TCM FilePath
outFile :: TCM FilePath
callGHC :: Interface -> TCM ()

Documentation

compilerMain :: Interface -> TCM () | Source

compile :: Interface -> TCM () | Source

imports :: TCM [HsImportDecl] | Source

definitions :: Definitions -> TCM [HsDecl] | Source

definition :: Definition -> TCM [HsDecl] | Source

checkConstructorType :: QName -> TCM [HsDecl] | Source

checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [HsDecl] | Source

constructorArity :: MonadTCM tcm => QName -> tcm Nat | Source

Move somewhere else!

clause :: QName -> (Nat, Bool, Clause) -> TCM HsDecl | Source

argpatts :: [Arg Pattern] -> [HsPat] -> TCM [HsPat] | Source

clausebody :: ClauseBody -> TCM HsExp | Source

term :: Term -> ReaderT Nat TCM HsExp | Source

literal :: Literal -> TCM HsExp | Source

hslit :: Literal -> HsLiteral | Source

condecl :: QName -> TCM (Nat, HsConDecl) | Source

cdecl :: QName -> Nat -> HsConDecl | Source

tvaldecl | Source

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

infodecl :: QName -> HsDecl | Source

hsCast :: HsExp -> HsExp | Source

writeModule :: HsModule -> TCM () | Source

malonzoDir :: TCM FilePath | Source

outFile :: TCM FilePath | Source

callGHC :: Interface -> TCM () | Source

Produced by Haddock version 2.4.2