| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Compiler.MAlonzo.Primitives
Synopsis
- newtype MainFunctionDef = MainFunctionDef Definition
- data CheckedMainFunctionDef = CheckedMainFunctionDef {}
- asMainFunctionDef :: Definition -> Maybe MainFunctionDef
- mainFunctionDefs :: Interface -> [MainFunctionDef]
- checkTypeOfMain :: Definition -> HsCompileM (Maybe CheckedMainFunctionDef)
- checkTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef
- charBuiltins :: [SomeBuiltin]
- floatBuiltins :: [SomeBuiltin]
- usedBuiltins :: BuiltinThings -> [Definition] -> Set SomeBuiltin
- treelessPrimName :: TPrim -> String
- primBody :: MonadTCError m => PrimitiveId -> m Exp
- noCheckCover :: (HasBuiltins m, MonadReduce m) => QName -> m Bool
Entrypoint (main)
newtype MainFunctionDef Source #
Constructors
| MainFunctionDef Definition |
data CheckedMainFunctionDef Source #
Constructors
| CheckedMainFunctionDef | |
Fields | |
mainFunctionDefs :: Interface -> [MainFunctionDef] Source #
checkTypeOfMain :: Definition -> HsCompileM (Maybe CheckedMainFunctionDef) Source #
Check that the main function has type IO a, for some a.
Primitives and builtins
charBuiltins :: [SomeBuiltin] Source #
These builtins need a qualified import of Data.Char.
floatBuiltins :: [SomeBuiltin] Source #
These builtins need a qualified import of MAlonzo.RTE.Float.
usedBuiltins :: BuiltinThings -> [Definition] -> Set SomeBuiltin Source #
Which builtins are actually used in the definitions?
Translating primitives
treelessPrimName :: TPrim -> String Source #
primBody :: MonadTCError m => PrimitiveId -> m Exp Source #
Definition bodies for primitive functions
noCheckCover :: (HasBuiltins m, MonadReduce m) => QName -> m Bool Source #