| 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
- primitiveFunctions :: Map String (TCM PrimitiveImpl)
- type Pred a = a -> Bool
- type Rel a = a -> a -> Bool
- type Fun a = a -> a
- type Op a = a -> a -> a
- class FromTerm a where
- fromTerm :: TCM (FromTermFunction a)
- type FromTermFunction a = Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
- class ToTerm a where
- class PrimTerm a where
- class PrimType a where
- newtype Lvl = Lvl {}
- newtype Nat = Nat {}
- buildList :: TCM ([Term] -> Term)
- fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)
- fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)
- mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl
- primMetaToNatInjective :: TCM PrimitiveImpl
- primCharToNatInjective :: TCM PrimitiveImpl
- primStringToListInjective :: TCM PrimitiveImpl
- primWord64ToNatInjective :: TCM PrimitiveImpl
- primFloatToWord64Injective :: TCM PrimitiveImpl
- primQNameToWord64sInjective :: TCM PrimitiveImpl
- getRefl :: TCM (Arg Term -> Term)
- primEraseEquality :: TCM PrimitiveImpl
- getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo)
- genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
- primForce :: TCM PrimitiveImpl
- primForceLemma :: TCM PrimitiveImpl
- mkPrimLevelZero :: TCM PrimitiveImpl
- mkPrimLevelSuc :: TCM PrimitiveImpl
- mkPrimLevelMax :: TCM PrimitiveImpl
- mkPrimSetOmega :: TCM PrimitiveImpl
- mkPrimFun1TCM :: (FromTerm a, ToTerm b, TermLike 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
- 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
Documentation
class FromTerm a where Source #
Methods
fromTerm :: TCM (FromTermFunction a) Source #
Instances
| FromTerm Bool Source # | |
Defined in Agda.TypeChecking.Primitive | |
| FromTerm Char Source # | |
Defined in Agda.TypeChecking.Primitive | |
| FromTerm Double Source # | |
Defined in Agda.TypeChecking.Primitive | |
| FromTerm Integer Source # | |
Defined in Agda.TypeChecking.Primitive | |
| FromTerm Word64 Source # | |
Defined in Agda.TypeChecking.Primitive | |
| FromTerm Str Source # | |
Defined in Agda.TypeChecking.Primitive | |
| FromTerm MetaId Source # | |
Defined in Agda.TypeChecking.Primitive | |
| FromTerm QName Source # | |
Defined in Agda.TypeChecking.Primitive | |
| FromTerm Lvl Source # | |
Defined in Agda.TypeChecking.Primitive | |
| FromTerm Nat Source # | |
Defined in Agda.TypeChecking.Primitive | |
| (ToTerm a, FromTerm a) => FromTerm [a] Source # | |
Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction [a]) Source # | |
type FromTermFunction a = Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a) Source #
Minimal complete definition
Instances
| ToTerm Bool Source # | |
| ToTerm Char Source # | |
| ToTerm Double Source # | |
| ToTerm Integer Source # | |
| ToTerm Word64 Source # | |
| ToTerm Str Source # | |
| ToTerm Fixity' Source # | |
| ToTerm Fixity Source # | |
| ToTerm Associativity Source # | |
Defined in Agda.TypeChecking.Primitive | |
| ToTerm FixityLevel Source # | |
Defined in Agda.TypeChecking.Primitive | |
| ToTerm MetaId Source # | |
| ToTerm ArgInfo Source # | |
| ToTerm QName Source # | |
| ToTerm Type Source # | |
| ToTerm Term Source # | |
| ToTerm Lvl Source # | |
| ToTerm Nat Source # | |
| ToTerm a => ToTerm [a] Source # | |
| (ToTerm a, ToTerm b) => ToTerm (a, b) Source # | |
class PrimTerm a where Source #
Instances
| PrimTerm Bool Source # | |
| PrimTerm Char Source # | |
| PrimTerm Double Source # | |
| PrimTerm Integer Source # | |
| PrimTerm Word64 Source # | |
| PrimTerm Str Source # | |
| PrimTerm Fixity' Source # | |
| PrimTerm MetaId Source # | |
| PrimTerm QName Source # | |
| PrimTerm Type Source # | |
| PrimTerm Lvl Source # | |
| PrimTerm Nat Source # | |
| PrimTerm a => PrimTerm [a] Source # | |
| PrimTerm a => PrimTerm (IO a) Source # | |
| (PrimType a, PrimType b) => PrimTerm (a -> b) Source # | |
| (PrimType a, PrimType b) => PrimTerm (a, b) Source # | |
Instances
| Enum Nat Source # | |
| Eq Nat Source # | |
| Integral Nat Source # | |
| Num Nat Source # | |
| Ord Nat Source # | |
| Real Nat Source # | |
Defined in Agda.TypeChecking.Primitive Methods toRational :: Nat -> Rational # | |
| Show Nat Source # | |
| TermLike Nat Source # | |
| FromTerm Nat Source # | |
Defined in Agda.TypeChecking.Primitive | |
| ToTerm Nat Source # | |
| PrimTerm Nat 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.
fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a) Source #
fromLiteral :: (Literal -> 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.
primEraseEquality :: TCM PrimitiveImpl Source #
primEraseEquality : {a : Level} {A : Set a} {x y : A} -> x ≡ y -> x ≡ ygetReflArgInfo :: 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, TermLike b) => TCM Type -> (a -> ReduceM b) -> TCM PrimitiveImpl Source #
mkPrimFun1 :: (PrimType a, FromTerm a, PrimType b, ToTerm b) => (a -> b) -> TCM PrimitiveImpl Source #