 | Agda-2.2.10: A dependently typed functional programming language and proof assistant | Source code | Contents | Index |
| Agda.Compiler.MAlonzo.Compiler |
| compilerMain :: Interface -> TCM () |
| compile :: Interface -> TCM () |
| imports :: TCM [ImportDecl] |
| definitions :: Definitions -> TCM [Decl] |
| definition :: Maybe CoinductionKit -> Definition -> TCM [Decl] |
| checkConstructorType :: QName -> TCM [Decl] |
| checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl] |
| constructorArity :: MonadTCM tcm => QName -> tcm Nat |
| clause :: QName -> (Nat, Bool, Clause) -> TCM Decl |
| argpatts :: [Arg Pattern] -> [Pat] -> TCM [Pat] |
| clausebody :: ClauseBody -> TCM Exp |
| term :: Term -> ReaderT Nat TCM Exp |
| term' :: Arg Term -> ReaderT Nat TCM Exp |
| literal :: Literal -> TCM Exp |
| hslit :: Literal -> Literal |
| condecl :: QName -> TCM (Nat, ConDecl) |
| cdecl :: QName -> Nat -> ConDecl |
| tvaldecl :: QName -> Induction -> 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 () |
| compilerMain :: 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 :: forall a. () -> forall b. () -> b -> b sharp _ _ x = x flat :: forall a. () -> forall b. () -> b -> b flat _ _ x = x
| checkConstructorType :: QName -> TCM [Decl] | Source |
| checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl] | Source |
| constructorArity :: MonadTCM tcm => QName -> tcm Nat | Source |
| clause :: QName -> (Nat, Bool, Clause) -> TCM Decl | Source |
| argpatts :: [Arg Pattern] -> [Pat] -> TCM [Pat] | Source |
| clausebody :: ClauseBody -> TCM Exp | Source |
| term :: Term -> ReaderT Nat TCM Exp | Source |
| term' :: Arg Term -> ReaderT Nat TCM Exp | Source |
| literal :: Literal -> TCM Exp | Source |
| hslit :: Literal -> Literal | Source |
| condecl :: QName -> TCM (Nat, ConDecl) | Source |
| cdecl :: QName -> Nat -> ConDecl | Source |
| tvaldecl | Source |
| :: QName | |
| -> Induction | Is the type inductive or coinductive? |
| -> Nat | |
| -> Nat | |
| -> [ConDecl] | |
| -> Maybe Clause | |
| -> [Decl] |
| infodecl :: QName -> Decl | Source |
| hsCast :: Exp -> Exp | Source |
| writeModule :: Module -> TCM () | Source |
| rteModule :: Module | Source |
| compileDir :: TCM FilePath | Source |
| outFile :: ModuleName -> TCM FilePath | Source |
| outFile_ :: TCM FilePath | Source |
| callGHC :: Interface -> TCM () | Source |