|
Agda.TypeChecking.Primitive |
|
|
|
|
Description |
Primitive functions, such as addition on builtin integers.
|
|
Synopsis |
|
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 | | | 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 |
|
|
Rewrite a literal to constructor form if possible.
|
|
Primitive functions
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
buildList A ts builds a list of type List A. Assumes that the terms
ts all have type A.
|
|
|
|
|
|
|
|
Conceptually: redBind m f k = either (return . Left . f) k =<< m
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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 | Source |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The actual primitive functions
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Rebind a primitive. Assumes everything is type correct. Used when
importing a module with primitives.
|
|
Produced by Haddock version 2.6.0 |