| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Primitive
Description
Primitive functions, such as addition on builtin integers.
Synopsis
- module Agda.TypeChecking.Primitive.Base
- module Agda.TypeChecking.Primitive.Cubical
- newtype Nat = Nat {
- unNat :: Integer
- getRefl :: TCM (Arg Term -> Term)
- primitiveFunctions :: Map PrimitiveId (TCM PrimitiveImpl)
- type Pred a = a -> Bool
- type Fun a = a -> a
- primWord64ToNatInjective :: TCM PrimitiveImpl
- primFloatToWord64Injective :: TCM PrimitiveImpl
- primCharToNatInjective :: TCM PrimitiveImpl
- primStringToListInjective :: TCM PrimitiveImpl
- primStringFromListInjective :: TCM PrimitiveImpl
- primEraseEquality :: TCM PrimitiveImpl
- primForce :: TCM PrimitiveImpl
- primForceLemma :: TCM PrimitiveImpl
- primQNameToWord64sInjective :: TCM PrimitiveImpl
- primMetaToNatInjective :: TCM PrimitiveImpl
- newtype Lvl = Lvl {
- unLvl :: Integer
- class PrimType a where
- class PrimType a => PrimTerm a where
- class ToTerm a where
- buildList :: TCM ([Term] -> Term)
- type FromTermFunction a = Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
- class FromTerm a where
- fromTerm :: TCM (FromTermFunction a)
- fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)
- fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)
- mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl
- metaToNat :: MetaId -> Nat
- getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo)
- genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
- mkPrimLevelZero :: TCM PrimitiveImpl
- mkPrimLevelSuc :: TCM PrimitiveImpl
- mkPrimLevelMax :: TCM PrimitiveImpl
- type Op a = a -> a -> a
- primLockUniv' :: TCM PrimitiveImpl
- mkPrimFun1TCM :: (FromTerm a, ToTerm b) => TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl
- mkPrimFun1 :: (PrimType a, FromTerm a, PrimType b, ToTerm b) => (a -> b) -> TCM PrimitiveImpl
- mkPrimFun2 :: (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b, PrimType c, ToTerm c) => (a -> b -> c) -> TCM PrimitiveImpl
- mkPrimFun3 :: (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b, ToTerm b, PrimType c, FromTerm c, PrimType d, ToTerm d) => (a -> b -> c -> d) -> 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
- type Rel a = a -> a -> Bool
Documentation
Instances
| Pretty Nat Source # | |
| TermLike Nat Source # | |
| FromTerm Nat Source # | |
Defined in Agda.TypeChecking.Primitive | |
| PrimTerm Nat Source # | |
| PrimType Nat Source # | |
| ToTerm Nat Source # | |
| Enum Nat Source # | |
| Num Nat Source # | |
| Integral Nat Source # | |
| Real Nat Source # | |
Defined in Agda.TypeChecking.Primitive Methods toRational :: Nat -> Rational | |
| Eq Nat Source # | |
| Ord Nat Source # | |
primitiveFunctions :: Map PrimitiveId (TCM PrimitiveImpl) Source #
primEraseEquality :: TCM PrimitiveImpl Source #
primEraseEquality : {a : Level} {A : Set a} {x y : A} -> x ≡ y -> x ≡ yclass PrimType a where Source #
Minimal complete definition
Nothing
Instances
| PrimType QName Source # | |
| PrimType Fixity' Source # | |
| PrimType MetaId Source # | |
| PrimType Type Source # | |
| PrimType Lvl Source # | |
| PrimType Nat Source # | |
| PrimType Word64 Source # | |
| PrimType Text Source # | |
| PrimType Integer Source # | |
| PrimType Bool Source # | |
| PrimType Char Source # | |
| PrimType Double Source # | |
| PrimTerm a => PrimType (IO a) Source # | |
| PrimTerm a => PrimType (Maybe a) Source # | |
| PrimTerm a => PrimType [a] Source # | |
| (PrimType a, PrimType b) => PrimType (a, b) Source # | |
| (PrimType a, PrimType b) => PrimType (a -> b) Source # | |
class PrimType a => PrimTerm a where Source #
Instances
| PrimTerm QName Source # | |
| PrimTerm Fixity' Source # | |
| PrimTerm MetaId Source # | |
| PrimTerm Type Source # | |
| PrimTerm Lvl Source # | |
| PrimTerm Nat Source # | |
| PrimTerm Word64 Source # | |
| PrimTerm Text Source # | |
| PrimTerm Integer Source # | |
| PrimTerm Bool Source # | |
| PrimTerm Char Source # | |
| PrimTerm Double Source # | |
| PrimTerm a => PrimTerm (IO a) Source # | |
| PrimTerm a => PrimTerm (Maybe a) Source # | |
| PrimTerm a => PrimTerm [a] Source # | |
| (PrimType a, PrimType b) => PrimTerm (a, b) Source # | |
| (PrimType a, PrimType b) => PrimTerm (a -> b) Source # | |
Minimal complete definition
Instances
| ToTerm QName Source # | |
| ToTerm ArgInfo Source # | |
| ToTerm Associativity Source # | |
Defined in Agda.TypeChecking.Primitive | |
| ToTerm Fixity Source # | |
| ToTerm Fixity' Source # | |
| ToTerm FixityLevel Source # | |
Defined in Agda.TypeChecking.Primitive | |
| ToTerm MetaId Source # | |
| ToTerm Term Source # | |
| ToTerm Type Source # | |
| ToTerm Blocker Source # | |
| ToTerm Lvl Source # | |
| ToTerm Nat Source # | |
| ToTerm Word64 Source # | |
| ToTerm Text Source # | |
| ToTerm Integer Source # | |
| ToTerm Bool Source # | |
| ToTerm Char Source # | |
| ToTerm Double Source # | |
| ToTerm (Dom Type) Source # | |
| ToTerm a => ToTerm (Maybe a) Source # | |
| ToTerm a => ToTerm [a] Source # | |
| (ToTerm a, ToTerm b) => ToTerm (a, b) Source # | |
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
fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a) Source #
fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a) Source #
mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl Source #
mkPrimInjective takes two Set0 a and b and a function f of type
a -> b and outputs a primitive internalizing the fact that f is injective.
getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo) Source #
Get the ArgInfo of the principal argument of BUILTIN REFL.
Returns Nothing for e.g.
data Eq {a} {A : Set a} (x : A) : A → Set a where
refl : Eq x x
Returns Just ... for e.g.
data Eq {a} {A : Set a} : (x y : A) → Set a where
refl : ∀ x → Eq x x
genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl Source #
Used for both primForce and primForceLemma.
mkPrimFun1TCM :: (FromTerm a, ToTerm b) => TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl Source #
mkPrimFun1 :: (PrimType a, FromTerm a, PrimType b, ToTerm b) => (a -> b) -> TCM PrimitiveImpl Source #
mkPrimFun2 :: (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b, PrimType c, ToTerm c) => (a -> b -> c) -> TCM PrimitiveImpl Source #
mkPrimFun3 :: (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b, ToTerm b, PrimType c, FromTerm c, PrimType d, ToTerm d) => (a -> b -> c -> d) -> TCM PrimitiveImpl Source #