Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

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 Term Source

Rewrite a literal to constructor form if possible.

Primitive functions

data PrimitiveImpl Source

Constructors PrimImpl Type PrimFun

newtype Str Source

Constructors Str unStr :: String

newtype Nat Source

Constructors Nat unNat :: Integer

newtype Lvl Source

Constructors Lvl unLvl :: Integer

class PrimType a where Source

Methods primType :: MonadTCM tcm => a -> tcm Type Source

class PrimTerm a where Source

Methods primTerm :: MonadTCM tcm => a -> tcm Term Source

class ToTerm a where Source

Methods toTerm :: MonadTCM tcm => tcm (a -> Term) Source

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 where Source

Methods 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

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 PrimitiveImpl Source

mkPrimFun1 :: (MonadTCM tcm, PrimType a, PrimType b, FromTerm a, ToTerm b) => (a -> b) -> tcm PrimitiveImpl Source

mkPrimFun2 :: (MonadTCM tcm, PrimType a, PrimType b, PrimType c, FromTerm a, ToTerm a, FromTerm b, ToTerm c) => (a -> b -> c) -> tcm PrimitiveImpl Source

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

abstractPrim :: (MonadTCM tcm, PrimType a) => a -> tcm PrimitiveImpl Source

abstractFromType :: MonadTCM tcm => tcm Type -> tcm PrimitiveImpl Source

(-->) :: MonadTCM tcm => tcm Type -> tcm Type -> tcm Type Source

gpi :: MonadTCM tcm => Hiding -> String -> tcm Type -> tcm Type -> tcm Type Source

nPi :: MonadTCM tcm => String -> tcm Type -> tcm Type -> tcm Type Source

hPi :: MonadTCM tcm => String -> tcm Type -> tcm Type -> tcm Type Source

var :: MonadTCM tcm => Integer -> tcm Term Source

gApply :: MonadTCM tcm => Hiding -> tcm Term -> tcm Term -> tcm Term Source

(<#>) :: MonadTCM tcm => tcm Term -> tcm Term -> tcm Term Source

(<@>) :: MonadTCM tcm => tcm Term -> tcm Term -> tcm Term Source

list :: MonadTCM tcm => tcm Term -> tcm Term Source

io :: MonadTCM tcm => tcm Term -> tcm Term Source

el :: MonadTCM tcm => tcm Term -> tcm Type Source

tset :: MonadTCM tcm => tcm Type Source

The actual primitive functions

type Op a = a -> a -> a Source

type Fun a = a -> a Source

type Rel a = a -> a -> Bool Source

type Pred a = a -> Bool Source

primitiveFunctions :: Map String (TCM PrimitiveImpl) Source

lookupPrimitiveFunction :: MonadTCM tcm => String -> tcm PrimitiveImpl Source

rebindPrimitive :: MonadTCM tcm => String -> tcm PrimFun Source

Rebind a primitive. Assumes everything is type correct. Used when importing a module with primitives.

Produced by Haddock version 2.6.0