Agda-2.6.20240714: A dependently typed functional programming language and proof assistant

Safe Haskell	None
Language	Haskell2010

Agda.Compiler.MAlonzo.Primitives

Synopsis

newtype MainFunctionDef = MainFunctionDef Definition
data CheckedMainFunctionDef = CheckedMainFunctionDef {
- checkedMainDef :: MainFunctionDef
- checkedMainDecl :: Decl
}
asMainFunctionDef :: Definition -> Maybe MainFunctionDef
mainFunctionDefs :: Interface -> [MainFunctionDef]
checkTypeOfMain :: Definition -> HsCompileM (Maybe CheckedMainFunctionDef)
checkTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef
treelessPrimName :: TPrim -> String
importsForPrim :: BuiltinThings PrimFun -> [Definition] -> [ModuleName]
xForPrim :: Map SomeBuiltin a -> BuiltinThings PrimFun -> [Definition] -> [a]
primBody :: MonadTCError m => PrimitiveId -> m Exp
noCheckCover :: (HasBuiltins m, MonadReduce m) => QName -> m Bool

Documentation

newtype MainFunctionDef Source #

Constructors

MainFunctionDef Definition

data CheckedMainFunctionDef Source #

Constructors

CheckedMainFunctionDef
Fields checkedMainDef :: MainFunctionDef checkedMainDecl :: Decl

asMainFunctionDef :: Definition -> Maybe MainFunctionDef Source #

mainFunctionDefs :: Interface -> [MainFunctionDef] Source #

checkTypeOfMain :: Definition -> HsCompileM (Maybe CheckedMainFunctionDef) Source #

Check that the main function has type IO a, for some a.

checkTypeOfMain' :: MainFunctionDef -> TCM CheckedMainFunctionDef Source #

treelessPrimName :: TPrim -> String Source #

importsForPrim :: BuiltinThings PrimFun -> [Definition] -> [ModuleName] Source #

Haskell modules to be imported for BUILT-INs

xForPrim :: Map SomeBuiltin a -> BuiltinThings PrimFun -> [Definition] -> [a] Source #

primBody :: MonadTCError m => PrimitiveId -> m Exp Source #

Definition bodies for primitive functions

noCheckCover :: (HasBuiltins m, MonadReduce m) => QName -> m Bool Source #