Safe Haskell | None |
---|---|
Language | Haskell98 |
- compilerMain :: Bool -> 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 -> Maybe String -> (Nat, Bool, Clause) -> TCM Decl
- argpatts :: [NamedArg 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
- explicitForAll :: Extension
- 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 ()
Documentation
compilerMain :: Bool -> 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
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
.
writeModule :: Module -> TCM () Source
outFile' :: (Pretty a, TransformBi ModuleName (Wrap a)) => a -> TCM (FilePath, FilePath) Source
outFile :: ModuleName -> TCM FilePath Source