Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Primitive

Contents

Description

Primitive functions, such as addition on builtin integers.

Synopsis

Documentation

constructorForm :: MonadTCM tcm => Term -> tcm Term

Rewrite a literal to constructor form if possible.

Primitive functions

data PrimitiveImpl

Constructors

PrimImpl Type PrimFun 

newtype Str

Constructors

Str 

Fields

unStr :: String
 

newtype Nat

Constructors

Nat 

Fields

unNat :: Integer
 

newtype Lvl

Constructors

Lvl 

Fields

unLvl :: Integer
 

class PrimType a where

Methods

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

Instances

class ToTerm a where

Methods

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

buildList :: MonadTCM tcm => tcm ([Term] -> Term)

buildList A ts builds a list of type List A. Assumes that the terms ts all have type A.

redBind :: MonadTCM tcm => tcm (Reduced a a') -> (a -> b) -> (a' -> tcm (Reduced b b')) -> tcm (Reduced b b')

Conceptually: redBind m f k = either (return . Left . f) k =<< m

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)

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

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

gpi :: MonadTCM tcm => Hiding -> Relevance -> 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

The actual primitive functions

type Op a = a -> a -> a

type Fun a = a -> a

type Rel a = a -> a -> Bool

type Pred a = a -> Bool

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

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