Primitive functions, such as addition on builtin integers.
- constructorForm :: MonadTCM tcm => 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 :: MonadTCM tcm => Term -> tcm ([Term] -> Term)
- type FromTermFunction a = Arg Term -> TCM (Reduced (Arg Term) a)
- class FromTerm a where
- fromTerm :: MonadTCM tcm => tcm (FromTermFunction a)
- redBind :: MonadTCM tcm => tcm (Reduced a a') -> (a -> b) -> (a' -> tcm (Reduced b b')) -> tcm (Reduced b b')
- redReturn :: MonadTCM tcm => a -> tcm (Reduced a' a)
- fromReducedTerm :: MonadTCM tcm => (Term -> Maybe a) -> tcm (FromTermFunction a)
- fromLiteral :: MonadTCM tcm => (Literal -> Maybe a) -> tcm (FromTermFunction a)
- primTrustMe :: MonadTCM tcm => tcm PrimitiveImpl
- mkPrimFun1 :: (MonadTCM tcm, PrimType a, PrimType b, FromTerm a, ToTerm b) => (a -> b) -> tcm PrimitiveImpl
- mkPrimFun2 :: (MonadTCM tcm, PrimType a, PrimType b, PrimType c, FromTerm a, ToTerm a, FromTerm b, ToTerm c) => (a -> b -> c) -> tcm PrimitiveImpl
- mkPrimFun4 :: (MonadTCM tcm, 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
- abstractPrim :: (MonadTCM tcm, PrimType a) => a -> tcm PrimitiveImpl
- abstractFromType :: MonadTCM tcm => tcm Type -> tcm PrimitiveImpl
- (-->) :: MonadTCM tcm => tcm Type -> tcm Type -> tcm Type
- gpi :: MonadTCM tcm => Hiding -> String -> tcm Type -> tcm Type -> tcm Type
- nPi :: MonadTCM tcm => String -> tcm Type -> tcm Type -> tcm Type
- hPi :: MonadTCM tcm => String -> tcm Type -> tcm Type -> tcm Type
- var :: MonadTCM tcm => Integer -> tcm Term
- gApply :: MonadTCM tcm => Hiding -> tcm Term -> tcm Term -> tcm Term
- (<#>) :: MonadTCM tcm => tcm Term -> tcm Term -> tcm Term
- (<@>) :: MonadTCM tcm => tcm Term -> tcm Term -> tcm Term
- list :: MonadTCM tcm => tcm Term -> tcm Term
- io :: MonadTCM tcm => tcm Term -> tcm Term
- el :: MonadTCM tcm => tcm Term -> tcm Type
- tset :: MonadTCM tcm => tcm Type
- 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 :: MonadTCM tcm => String -> tcm PrimitiveImpl
- rebindPrimitive :: MonadTCM tcm => String -> tcm PrimFun
Documentation
constructorForm :: MonadTCM tcm => Term -> tcm TermSource
Rewrite a literal to constructor form if possible.
Primitive functions
buildList :: MonadTCM tcm => Term -> tcm ([Term] -> Term)Source
buildList A ts
builds a list of type List A
. Assumes that the terms
ts
all have type A
.
fromTerm :: MonadTCM tcm => tcm (FromTermFunction a)Source
redBind :: MonadTCM tcm => 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 :: MonadTCM tcm => (Term -> Maybe a) -> tcm (FromTermFunction a)Source
fromLiteral :: MonadTCM tcm => (Literal -> Maybe a) -> tcm (FromTermFunction a)Source
primTrustMe :: MonadTCM tcm => tcm PrimitiveImplSource
mkPrimFun1 :: (MonadTCM tcm, PrimType a, PrimType b, FromTerm a, ToTerm b) => (a -> b) -> tcm PrimitiveImplSource
mkPrimFun2 :: (MonadTCM tcm, PrimType a, PrimType b, PrimType c, FromTerm a, ToTerm a, FromTerm b, ToTerm c) => (a -> b -> c) -> tcm PrimitiveImplSource
mkPrimFun4 :: (MonadTCM tcm, 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
abstractPrim :: (MonadTCM tcm, PrimType a) => a -> tcm PrimitiveImplSource
abstractFromType :: MonadTCM tcm => tcm Type -> tcm PrimitiveImplSource
The actual primitive functions
lookupPrimitiveFunction :: MonadTCM tcm => String -> tcm PrimitiveImplSource
rebindPrimitive :: MonadTCM tcm => String -> tcm PrimFunSource
Rebind a primitive. Assumes everything is type correct. Used when importing a module with primitives.