Safe Haskell | None |
---|
Primitive functions, such as addition on builtin integers.
- constructorForm :: Term -> TCM Term
- data PrimitiveImpl = PrimImpl Type PrimFun
- newtype Str = Str {}
- newtype Nat = Nat {}
- newtype Lvl = Lvl {}
- class PrimType a where
- class PrimTerm a where
- class ToTerm a where
- buildList :: TCM ([Term] -> Term)
- type FromTermFunction a = Arg Term -> TCM (Reduced (MaybeReduced (Arg Term)) a)
- class FromTerm a where
- fromTerm :: TCM (FromTermFunction a)
- redBind :: TCM (Reduced a a') -> (a -> b) -> (a' -> TCM (Reduced b b')) -> TCM (Reduced b b')
- redReturn :: a -> TCM (Reduced a' a)
- fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)
- fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)
- primTrustMe :: TCM PrimitiveImpl
- primQNameType :: TCM PrimitiveImpl
- primQNameDefinition :: TCM PrimitiveImpl
- primDataConstructors :: TCM PrimitiveImpl
- mkPrimLevelZero :: TCM PrimitiveImpl
- mkPrimLevelSuc :: TCM PrimitiveImpl
- mkPrimLevelMax :: TCM PrimitiveImpl
- mkPrimFun1TCM :: (FromTerm a, ToTerm b) => TCM Type -> (a -> TCM b) -> TCM PrimitiveImpl
- mkPrimFun1 :: (PrimType a, PrimType b, FromTerm a, ToTerm b) => (a -> b) -> TCM PrimitiveImpl
- mkPrimFun2 :: (PrimType a, PrimType b, PrimType c, FromTerm a, ToTerm a, FromTerm b, ToTerm c) => (a -> b -> c) -> TCM PrimitiveImpl
- mkPrimFun4 :: (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b, ToTerm b, PrimType c, FromTerm c, ToTerm c, PrimType d, FromTerm d, PrimType e, ToTerm e) => (a -> b -> c -> d -> e) -> TCM PrimitiveImpl
- (-->) :: TCM Type -> TCM Type -> TCM Type
- gpi :: Hiding -> Relevance -> String -> TCM Type -> TCM Type -> TCM Type
- hPi, nPi :: String -> TCM Type -> TCM Type -> TCM Type
- var :: Integer -> TCM Term
- gApply :: Hiding -> TCM Term -> TCM Term -> TCM Term
- (<@>), (<#>) :: TCM Term -> TCM Term -> TCM Term
- list :: TCM Term -> TCM Term
- io :: TCM Term -> TCM Term
- el :: TCM Term -> TCM Type
- tset :: TCM Type
- argN :: e -> Arg e
- argH :: e -> Arg e
- type Op a = a -> a -> a
- type Fun a = a -> a
- type Rel a = a -> a -> Bool
- type Pred a = a -> Bool
- primitiveFunctions :: Map String (TCM PrimitiveImpl)
- lookupPrimitiveFunction :: String -> TCM PrimitiveImpl
- rebindPrimitive :: String -> TCM PrimFun
Documentation
constructorForm :: Term -> TCM TermSource
Rewrite a literal to constructor form if possible.
Primitive functions
buildList :: TCM ([Term] -> Term)Source
buildList A ts
builds a list of type List A
. Assumes that the terms
ts
all have type A
.
type FromTermFunction a = Arg Term -> TCM (Reduced (MaybeReduced (Arg Term)) a)Source
fromTerm :: TCM (FromTermFunction a)Source
redBind :: TCM (Reduced a a') -> (a -> b) -> (a' -> TCM (Reduced b b')) -> TCM (Reduced b b')Source
Conceptually: redBind m f k = either (return . Left . f) k =<< m
fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)Source
fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)Source
mkPrimFun1TCM :: (FromTerm a, ToTerm b) => TCM Type -> (a -> TCM b) -> TCM PrimitiveImplSource
mkPrimFun1 :: (PrimType a, PrimType b, FromTerm a, ToTerm b) => (a -> b) -> TCM PrimitiveImplSource
mkPrimFun2 :: (PrimType a, PrimType b, PrimType c, FromTerm a, ToTerm a, FromTerm b, ToTerm c) => (a -> b -> c) -> TCM PrimitiveImplSource
mkPrimFun4 :: (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b, ToTerm b, PrimType c, FromTerm c, ToTerm c, PrimType d, FromTerm d, PrimType e, ToTerm e) => (a -> b -> c -> d -> e) -> TCM PrimitiveImplSource
The actual primitive functions
rebindPrimitive :: String -> TCM PrimFunSource
Rebind a primitive. Assumes everything is type correct. Used when importing a module with primitives.