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

Safe Haskell | None

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]
- conArityAndPars :: QName -> TCM (Nat, 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
- litqname :: QName -> TCM Exp
- condecl :: QName -> TCM (Nat, ConDecl)
- cdecl :: QName -> Nat -> ConDecl
- tvaldecl :: QName -> Induction -> Nat -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
- infodecl :: QName -> Decl
- hsCast :: Exp -> Exp
- hsCast' :: Exp -> Exp
- hsCoerce :: Exp -> Exp
- writeModule :: Module -> TCM ()
- rteModule :: Module
- explicitForAll :: Extension
- compileDir :: TCM FilePath
- outFile' :: (TransformBi ModuleName (Wrap a), Pretty a) => a -> TCMT IO (FilePath, FilePath)
- outFile :: ModuleName -> TCM FilePath
- outFile_ :: TCM FilePath
- callGHC :: Interface -> TCM ()

# Documentation

compilerMain :: Interface -> TCM ()

compile :: Interface -> TCM ()

imports :: TCM [ImportDecl]

definitions :: Definitions -> TCM [Decl]

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

checkConstructorType :: QName -> TCM [Decl]

checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl]

conArityAndPars :: QName -> TCM (Nat, Nat)

Move somewhere else!

clause :: QName -> (Nat, Bool, Clause) -> TCM Decl

argpatts :: [Arg Pattern] -> [Pat] -> TCM [Pat]

clausebody :: ClauseBody -> TCM Exp

term :: Term -> ReaderT Nat TCM Exp

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 Exp

Irrelevant arguments are replaced by Haskells' ().

literal :: Literal -> TCM Exp

hslit :: Literal -> Literal

litqname :: QName -> TCM Exp

condecl :: QName -> TCM (Nat, ConDecl)

cdecl :: QName -> Nat -> ConDecl

tvaldecl

Arguments

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

infodecl :: QName -> Decl

hsCast :: Exp -> Exp

hsCast' :: Exp -> Exp

hsCoerce :: Exp -> Exp

writeModule :: Module -> TCM ()

rteModule :: Module

explicitForAll :: Extension

compileDir :: TCM FilePath

outFile' :: (TransformBi ModuleName (Wrap a), Pretty a) => a -> TCMT IO (FilePath, FilePath)

outFile :: ModuleName -> TCM FilePath

outFile_ :: TCM FilePath

callGHC :: Interface -> TCM ()