Agda.Compiler.MAlonzo.Compiler

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