Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.MAlonzo.Compiler
Synopsis
compilerMain :: Interface -> TCM ()
compile :: Interface -> TCM ()
imports :: TCM [ImportDecl]
definitions :: Definitions -> TCM [Decl]
definition :: Maybe CoinductionKit -> Definition -> TCM [Decl]
checkConstructorType :: QName -> TCM [Decl]
checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl]
constructorArity :: MonadTCM tcm => QName -> tcm Nat
clause :: QName -> (Nat, Bool, Clause) -> TCM Decl
argpatts :: [Arg Pattern] -> [Pat] -> TCM [Pat]
clausebody :: ClauseBody -> TCM Exp
term :: Term -> ReaderT Nat TCM Exp
term' :: Arg Term -> ReaderT Nat TCM Exp
literal :: Literal -> TCM Exp
hslit :: Literal -> Literal
condecl :: QName -> TCM (Nat, ConDecl)
cdecl :: QName -> Nat -> ConDecl
tvaldecl :: QName -> Induction -> Nat -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
infodecl :: QName -> Decl
hsCast :: Exp -> Exp
writeModule :: Module -> TCM ()
rteModule :: Module
compileDir :: TCM FilePath
outFile :: ModuleName -> TCM FilePath
outFile_ :: TCM FilePath
callGHC :: Interface -> TCM ()
Documentation
compilerMain :: Interface -> TCM ()Source
compile :: Interface -> TCM ()Source
imports :: TCM [ImportDecl]Source
definitions :: Definitions -> TCM [Decl]Source
definition :: Maybe CoinductionKit -> Definition -> TCM [Decl]Source

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

   type Infinity a b = b

sharp :: forall a. () -> forall b. () -> b -> b
   sharp _ _ x = x

flat :: forall a. () -> forall b. () -> b -> b
   flat _ _ x = x
checkConstructorType :: QName -> TCM [Decl]Source
checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl]Source
constructorArity :: MonadTCM tcm => QName -> tcm NatSource
Move somewhere else!
clause :: QName -> (Nat, Bool, Clause) -> TCM DeclSource
argpatts :: [Arg Pattern] -> [Pat] -> TCM [Pat]Source
clausebody :: ClauseBody -> TCM ExpSource
term :: Term -> ReaderT Nat TCM ExpSource
Extract Agda term to Haskell expression. Irrelevant arguments are extracted as (). Types are extracted as (). DontCare outside of irrelevant arguments is extracted as error.
term' :: Arg Term -> ReaderT Nat TCM ExpSource
Irrelevant arguments are replaced by Haskells' ().
literal :: Literal -> TCM ExpSource
hslit :: Literal -> LiteralSource
condecl :: QName -> TCM (Nat, ConDecl)Source
cdecl :: QName -> Nat -> ConDeclSource
tvaldeclSource
:: QName
-> InductionIs the type inductive or coinductive?
-> Nat
-> Nat
-> [ConDecl]
-> Maybe Clause
-> [Decl]
infodecl :: QName -> DeclSource
hsCast :: Exp -> ExpSource
writeModule :: Module -> TCM ()Source
rteModule :: ModuleSource
compileDir :: TCM FilePathSource
outFile :: ModuleName -> TCM FilePathSource
outFile_ :: TCM FilePathSource
callGHC :: Interface -> TCM ()Source
Produced by Haddock version 2.6.1