Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Primitive

Contents

Primitive functions
The actual primitive functions

Description

Primitive functions, such as addition on builtin integers.

Synopsis

Primitive functions

data PrimitiveImpl Source

Constructors

PrimImpl Type PrimFun

newtype Str Source

Constructors

Str
Fields unStr :: String

Instances

Eq Str
Ord Str
FromTerm Str
ToTerm Str
PrimTerm Str

newtype Nat Source

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 Source

Constructors

Lvl
Fields unLvl :: Integer

Instances

Eq Lvl
Ord Lvl
Show Lvl
FromTerm Lvl
ToTerm Lvl
PrimTerm Lvl

class PrimType a where Source

Methods

primType :: a -> TCM Type Source

Instances

PrimTerm a => PrimType a

class PrimTerm a where Source

Methods

primTerm :: a -> TCM Term Source

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 Source

Methods

toTerm :: TCM (a -> Term) Source

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) 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 -> ReduceM (Reduced (MaybeReduced (Arg Term)) a) Source

class FromTerm a where Source

Methods

fromTerm :: TCM (FromTermFunction a) Source

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') Source

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

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

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

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

primTrustMe :: TCM PrimitiveImpl Source

primQNameType :: TCM PrimitiveImpl Source

primQNameDefinition :: TCM PrimitiveImpl Source

primDataConstructors :: TCM PrimitiveImpl Source

mkPrimLevelZero :: TCM PrimitiveImpl Source

mkPrimLevelSuc :: TCM PrimitiveImpl Source

mkPrimLevelMax :: TCM PrimitiveImpl Source

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

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

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

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 Source

(-->) :: TCM Type -> TCM Type -> TCM Type infixr 4 Source

(.-->) :: TCM Type -> TCM Type -> TCM Type infixr 4 Source

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

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

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

varM :: Int -> TCM Term Source

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

(<@>) :: TCM Term -> TCM Term -> TCM Term infixl 9 Source

(<#>) :: TCM Term -> TCM Term -> TCM Term infixl 9 Source

list :: TCM Term -> TCM Term Source

io :: TCM Term -> TCM Term Source

el :: TCM Term -> TCM Type Source

tset :: TCM Type Source

argN :: e -> Arg c e Source

Abbreviation: argN = Arg defaultArgInfo.

domN :: e -> Dom c e Source

argH :: e -> Arg c e Source

Abbreviation: argH = hide Arg defaultArgInfo.

domH :: e -> Dom c e 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 :: String -> TCM PrimitiveImpl Source

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