Safe Haskell | Safe-Infered |
---|
- 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]
- conArityAndPars :: QName -> TCM (Nat, 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
- litqname :: QName -> TCM Exp
- condecl :: QName -> TCM (Nat, ConDecl)
- cdecl :: QName -> Nat -> ConDecl
- tvaldecl :: QName -> Induction -> 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' :: (Data a, Pretty a) => a -> TCMT IO (FilePath, FilePath)
- outFile :: ModuleName -> TCM FilePath
- outFile_ :: TCM FilePath
- callGHC :: Interface -> TCM ()
Documentation
compilerMain :: 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 :: forall a. () -> forall b. () -> b -> b flat _ _ x = x
checkConstructorType :: QName -> TCM [Decl]Source
checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl]Source
clausebody :: ClauseBody -> TCM ExpSource
term :: Term -> ReaderT Nat TCM ExpSource
Extract Agda term to Haskell expression.
Irrelevant arguments are extracted as ()
.
Types are extracted as ()
.
DontCare
outside of irrelevant arguments is extracted as error
.
writeModule :: Module -> TCM ()Source
outFile :: ModuleName -> TCM FilePathSource