Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Primitive
Contents
Primitive functions
The actual primitive functions
Description
Primitive functions, such as addition on builtin integers.
Synopsis
constructorForm :: MonadTCM tcm => Term -> tcm Term
data PrimitiveImpl = PrimImpl Type PrimFun
newtype Str = Str {
unStr :: String
}
newtype Nat = Nat {
unNat :: Integer
}
newtype Lvl = Lvl {
unLvl :: Integer
}
class PrimType a where
primType :: MonadTCM tcm => a -> tcm Type
class PrimTerm a where
primTerm :: MonadTCM tcm => a -> tcm Term
class ToTerm a where
toTerm :: MonadTCM tcm => tcm (a -> Term)
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
data PrimitiveImpl Source
Constructors
PrimImpl Type PrimFun
newtype Str Source
Constructors
Str
unStr :: String
show/hide Instances
newtype Nat Source
Constructors
Nat
unNat :: Integer
show/hide Instances
newtype Lvl Source
Constructors
Lvl
unLvl :: Integer
show/hide Instances
class PrimType a whereSource
Methods
primType :: MonadTCM tcm => a -> tcm TypeSource
class PrimTerm a whereSource
Methods
primTerm :: MonadTCM tcm => a -> tcm TermSource
show/hide Instances
class ToTerm a whereSource
Methods
toTerm :: MonadTCM tcm => tcm (a -> Term)Source
show/hide Instances
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.
type FromTermFunction a = Arg Term -> TCM (Reduced (Arg Term) a)Source
class FromTerm a whereSource
Methods
fromTerm :: MonadTCM tcm => tcm (FromTermFunction a)Source
show/hide Instances
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
redReturn :: MonadTCM tcm => a -> tcm (Reduced a' a)Source
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
(-->) :: MonadTCM tcm => tcm Type -> tcm Type -> tcm TypeSource
gpi :: MonadTCM tcm => Hiding -> String -> tcm Type -> tcm Type -> tcm TypeSource
nPi :: MonadTCM tcm => String -> tcm Type -> tcm Type -> tcm TypeSource
hPi :: MonadTCM tcm => String -> tcm Type -> tcm Type -> tcm TypeSource
var :: MonadTCM tcm => Integer -> tcm TermSource
gApply :: MonadTCM tcm => Hiding -> tcm Term -> tcm Term -> tcm TermSource
(<#>) :: MonadTCM tcm => tcm Term -> tcm Term -> tcm TermSource
(<@>) :: MonadTCM tcm => tcm Term -> tcm Term -> tcm TermSource
list :: MonadTCM tcm => tcm Term -> tcm TermSource
io :: MonadTCM tcm => tcm Term -> tcm TermSource
el :: MonadTCM tcm => tcm Term -> tcm TypeSource
tset :: MonadTCM tcm => tcm TypeSource
The actual primitive functions
type Op a = a -> a -> aSource
type Fun a = a -> aSource
type Rel a = a -> a -> BoolSource
type Pred a = a -> BoolSource
primitiveFunctions :: Map String (TCM PrimitiveImpl)Source
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.
Produced by Haddock version 2.4.2