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

Instances

Eq Str
Ord Str
FromTerm Str
ToTerm Str
PrimTerm Str

newtype Nat | Source

Constructors

Nat |

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 |

unLvl :: Integer |

Instances

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

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

Instances

PrimTerm Bool
PrimTerm Char
PrimTerm Double
PrimTerm Integer
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 :: MonadTCM tcm => tcm (a -> Term) | Source

Instances

ToTerm Bool
ToTerm Char
ToTerm Double
ToTerm Integer
ToTerm Lvl
ToTerm Nat
ToTerm Str
(PrimTerm a, ToTerm a) => ToTerm ([] a)

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

Instances

FromTerm Bool
FromTerm Char
FromTerm Double
FromTerm Integer
FromTerm Lvl
FromTerm Nat
FromTerm Str
(ToTerm a, FromTerm a) => FromTerm ([] a)

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.4.2