Safe Haskell	None
Language	Haskell98

Agda.Compiler.MAlonzo.Compiler

Synopsis

Documentation

compilerMain :: Bool -> Interface -> TCM () Source

compile :: Interface -> TCM () Source

imports :: TCM [ImportDecl] Source

definitions :: Definitions -> TCM [Decl] Source

definition :: Maybe CoinductionKit -> Definition -> TCM [Decl] Source

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] Source

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

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

Move somewhere else!

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

argpatts :: [NamedArg Pattern] -> [Pat] -> TCM [Pat] Source

clausebody :: ClauseBody -> TCM Exp Source

term :: Term -> ReaderT Nat TCM Exp Source

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 Source

Irrelevant arguments are replaced by Haskells' ().

literal :: Literal -> TCM Exp Source

hslit :: Literal -> Literal Source

litqname :: QName -> TCM Exp Source

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

cdecl :: QName -> Nat -> ConDecl Source

tvaldecl Source

Arguments

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

infodecl :: QName -> Decl Source

hsCast :: Exp -> Exp Source

hsCast' :: Exp -> Exp Source

hsCoerce :: Exp -> Exp Source

writeModule :: Module -> TCM () Source

rteModule :: Module Source

explicitForAll :: Extension Source

compileDir :: TCM FilePath Source

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

outFile :: ModuleName -> TCM FilePath Source

outFile_ :: TCM FilePath Source

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