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

Safe Haskell | None

Agda.TypeChecking.Primitive

Contents

- Primitive functions
- The actual primitive functions

Description

Primitive functions, such as addition on builtin integers.

Synopsis

- constructorForm :: 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 :: a -> TCM Type
- class PrimTerm a where
  - primTerm :: a -> TCM Term
- class ToTerm a where
  - toTerm :: TCM (a -> Term)
- buildList :: TCM ([Term] -> Term)
- type FromTermFunction a = Arg Term -> TCM (Reduced (MaybeReduced (Arg Term)) a)
- class FromTerm a where
  - fromTerm :: TCM (FromTermFunction a)
- redBind :: TCM (Reduced a a') -> (a -> b) -> (a' -> TCM (Reduced b b')) -> TCM (Reduced b b')
- redReturn :: a -> TCM (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 -> TCM 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 :: Hiding -> Relevance -> 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 e
- domN :: e -> Dom e
- argH :: e -> Arg e
- domH :: e -> Dom e
- 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)

# Documentation

constructorForm :: 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 :: 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 -> TCM (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 :: 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 :: a -> TCM (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 -> TCM 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 :: Hiding -> Relevance -> 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 e

Abbreviation: `argN = `Arg` `NotHidden` `Relevant``.

domN :: e -> Dom e

argH :: e -> Arg e

Abbreviation: `argH = `Arg` `Hidden` `Relevant``.

domH :: e -> Dom 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)