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 :: forall a. () -> forall b. () -> b -> b
   sharp _ _ x = x

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

checkConstructorType :: QName -> TCM [Decl]

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

constructorArity :: MonadTCM tcm => QName -> tcm 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

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

writeModule :: Module -> TCM ()

rteModule :: Module

compileDir :: TCM FilePath

outFile :: ModuleName -> TCM FilePath

outFile_ :: TCM FilePath

callGHC :: Interface -> TCM ()