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

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 => tcm ([Term] -> Term)
- type FromTermFunction a = Arg Term -> TCM (Reduced (MaybeReduced (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
- (-->) :: 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
- 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

Rewrite a literal to constructor form if possible.

# 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 :: MonadTCM tcm => a -> tcm Type

Instances

PrimTerm a => PrimType a |

class PrimTerm a where

Methods

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

Instances

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

Instances

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

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

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

class FromTerm a where

Methods

fromTerm :: MonadTCM tcm => 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 :: 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)

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

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

primitiveFunctions :: Map String (TCM PrimitiveImpl)

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

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

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