Agda-2.8.0: 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 -> [Definition] -> [ModuleName]
- xForPrim :: Map SomeBuiltin a -> BuiltinThings -> [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 -> [Definition] -> [ModuleName] Source #

Haskell modules to be imported for BUILT-INs

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

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

Definition bodies for primitive functions

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