Agda.Compiler.MAlonzo.Compiler

Documentation

compilerMain :: Bool -> 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 -> Maybe String -> (Nat, Bool, Clause) -> TCM Decl

argpatts :: [NamedArg 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 -> Exp

litqnamepat :: QName -> Pat

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

compileDir :: TCM FilePath

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

outFile :: ModuleName -> TCM FilePath

outFile_ :: TCM FilePath

callGHC :: Bool -> Interface -> TCM ()