Agda.TypeChecking.Primitive

Primitive functions, such as addition on builtin integers.

Primitive functions

data PrimitiveImpl

Constructors

PrimImpl Type PrimFun

newtype Str

Constructors

Str

Fields

unStr :: String

Instances

Eq Str

Ord Str

FromTerm Str

ToTerm Str

PrimTerm Str

newtype Nat

Constructors

Nat

Fields

unNat :: Integer

Instances

Enum Nat

Eq Nat

Integral Nat

Num Nat

Ord Nat

Real Nat

Show Nat

FromTerm Nat

ToTerm Nat

PrimTerm Nat

newtype Lvl

Constructors

Lvl

Fields

unLvl :: Integer

Instances

Eq Lvl

Ord Lvl

Show Lvl

FromTerm Lvl

ToTerm Lvl

PrimTerm Lvl

class PrimType a where

Methods

primType :: a -> TCM Type

Instances

PrimTerm a => PrimType a

class PrimTerm a where

Methods

primTerm :: a -> TCM Term

Instances

PrimTerm Bool

PrimTerm Char

PrimTerm Double

PrimTerm Integer

PrimTerm QName

PrimTerm Type

PrimTerm Lvl

PrimTerm Nat

PrimTerm Str

PrimTerm a => PrimTerm [a]

PrimTerm a => PrimTerm (IO a)

(PrimType a, PrimType b) => PrimTerm (a -> b)

class ToTerm a where

Methods

toTerm :: TCM (a -> Term)

Instances

ToTerm Bool

ToTerm Char

ToTerm Double

ToTerm Integer

ToTerm QName

ToTerm Type

ToTerm Lvl

ToTerm Nat

ToTerm Str

(PrimTerm a, ToTerm a) => ToTerm [a]

buildList :: TCM ([Term] -> Term)

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

type FromTermFunction a = Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)

class FromTerm a where

Methods

fromTerm :: TCM (FromTermFunction a)

Instances

FromTerm Bool

FromTerm Char

FromTerm Double

FromTerm Integer

FromTerm QName

FromTerm Lvl

FromTerm Nat

FromTerm Str

(ToTerm a, FromTerm a) => FromTerm [a]

redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b')

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

redReturn :: a -> ReduceM (Reduced a' a)

fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)

fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)

primTrustMe :: TCM PrimitiveImpl

primQNameType :: TCM PrimitiveImpl

primQNameDefinition :: TCM PrimitiveImpl

primDataConstructors :: TCM PrimitiveImpl

mkPrimLevelZero :: TCM PrimitiveImpl

mkPrimLevelSuc :: TCM PrimitiveImpl

mkPrimLevelMax :: TCM PrimitiveImpl

mkPrimFun1TCM :: (FromTerm a, ToTerm b) => TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl

mkPrimFun1 :: (PrimType a, PrimType b, FromTerm a, ToTerm b) => (a -> b) -> TCM PrimitiveImpl

mkPrimFun2 :: (PrimType a, PrimType b, PrimType c, FromTerm a, ToTerm a, FromTerm b, ToTerm c) => (a -> b -> c) -> TCM PrimitiveImpl

mkPrimFun4 :: (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

(-->) :: TCM Type -> TCM Type -> TCM Type

(.-->) :: TCM Type -> TCM Type -> TCM Type

gpi :: ArgInfo -> String -> TCM Type -> TCM Type -> TCM Type

hPi :: String -> TCM Type -> TCM Type -> TCM Type

nPi :: String -> TCM Type -> TCM Type -> TCM Type

varM :: Int -> TCM Term

gApply :: Hiding -> TCM Term -> TCM Term -> TCM Term

(<@>) :: TCM Term -> TCM Term -> TCM Term

(<#>) :: TCM Term -> TCM Term -> TCM Term

list :: TCM Term -> TCM Term

io :: TCM Term -> TCM Term

el :: TCM Term -> TCM Type

tset :: TCM Type

argN :: e -> Arg c e

Abbreviation: argN = Arg defaultArgInfo.

domN :: e -> Dom c e

argH :: e -> Arg c e

Abbreviation: argH = hide Arg defaultArgInfo.

domH :: e -> Dom c e

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

primitiveFunctions :: Map String (TCM PrimitiveImpl)

lookupPrimitiveFunction :: String -> TCM PrimitiveImpl

lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl)