Agda.Compiler.MAlonzo.Compiler

Documentation

compilerMain :: Interface -> TCM ()

compile :: Interface -> TCM ()

imports :: TCM [HsImportDecl]

definitions :: Definitions -> TCM [HsDecl]

definition :: Maybe CoinductionKit -> Definition -> TCM [HsDecl]

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 [HsDecl]

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

constructorArity :: MonadTCM tcm => QName -> tcm Nat

Move somewhere else!

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

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

clausebody :: ClauseBody -> TCM HsExp

term :: Term -> ReaderT Nat TCM HsExp

literal :: Literal -> TCM HsExp

hslit :: Literal -> HsLiteral

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

cdecl :: QName -> Nat -> HsConDecl

tvaldecl

Arguments

:: QName

-> Induction

Is the type inductive or coinductive?

-> Nat

-> Nat

-> [HsConDecl]

-> Maybe Clause

-> [HsDecl]

infodecl :: QName -> HsDecl

hsCast :: HsExp -> HsExp

writeModule :: HsModule -> TCM ()

compileDir :: TCM FilePath

outFile :: TCM FilePath

callGHC :: Interface -> TCM ()