Safe Haskell | None |
---|---|
Language | Haskell2010 |
- compilerMain :: IsMain -> Interface -> TCM ()
- compile :: Interface -> TCM ()
- imports :: TCM [ImportDecl]
- definitions :: Definitions -> TCM [Decl]
- definition :: Maybe CoinductionKit -> Definition -> TCM [Decl]
- data CCEnv = CCEnv {}
- type NameSupply = [Name]
- type CCContext = [Name]
- mapNameSupply :: (NameSupply -> NameSupply) -> CCEnv -> CCEnv
- mapContext :: (CCContext -> CCContext) -> CCEnv -> CCEnv
- initCCEnv :: CCEnv
- lookupIndex :: Int -> CCContext -> Name
- type CC = ReaderT CCEnv TCM
- freshNames :: Int -> ([Name] -> CC a) -> CC a
- intros :: Int -> ([Name] -> CC a) -> CC a
- checkConstructorType :: QName -> TCM [Decl]
- checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl]
- closedTerm :: TTerm -> TCM Exp
- term :: TTerm -> CC Exp
- compilePrim :: TPrim -> Exp
- alt :: Int -> TAlt -> CC Alt
- literal :: Literal -> Exp
- hslit :: Literal -> Literal
- litString :: String -> Exp
- litqname :: QName -> Exp
- litqnamepat :: QName -> Pat
- erasedArity :: QName -> TCM Nat
- condecl :: QName -> TCM (Nat, ConDecl)
- cdecl :: QName -> Nat -> ConDecl
- tvaldecl :: QName -> Induction -> Nat -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
- infodecl :: QName -> [Decl] -> [Decl]
- hsCast :: Exp -> Exp
- hsCast' :: Exp -> Exp
- hsCastApp :: Exp -> Exp
- hsCoerce :: Exp -> Exp
- copyRTEModules :: TCM ()
- writeModule :: Module -> TCM ()
- outFile' :: Pretty a => a -> TCM (FilePath, FilePath)
- outFile :: ModuleName -> TCM FilePath
- outFile_ :: TCM FilePath
- callGHC :: IsMain -> Interface -> TCM ()
Documentation
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
Environment for naming of local variables.
Invariant: reverse ccCxt ++ ccNameSupply
CCEnv | |
|
type NameSupply = [Name] Source #
mapNameSupply :: (NameSupply -> NameSupply) -> CCEnv -> CCEnv Source #
checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl] Source #
term :: TTerm -> CC Exp Source #
Extract Agda term to Haskell expression.
Erased arguments are extracted as ()
.
Types are extracted as ()
.
compilePrim :: TPrim -> Exp Source #
litqnamepat :: QName -> Pat Source #
copyRTEModules :: TCM () Source #
writeModule :: Module -> TCM () Source #