Safe Haskell | None |
---|---|
Language | Haskell2010 |
Primitive functions, such as addition on builtin integers.
Synopsis
- data PrimitiveImpl = PrimImpl Type PrimFun
- newtype Nat = Nat {}
- newtype Lvl = Lvl {}
- class PrimType a where
- class 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)
- redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b')
- redReturn :: a -> ReduceM (Reduced a' a)
- fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)
- fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)
- primTrustMe :: 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
- 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
- (-->) :: TCM Type -> TCM Type -> TCM Type
- (.-->) :: TCM Type -> TCM Type -> TCM Type
- (..-->) :: TCM Type -> TCM Type -> TCM Type
- garr :: (Relevance -> Relevance) -> TCM Type -> TCM Type -> TCM Type
- gpi :: ArgInfo -> 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
- sSizeUniv :: Sort
- tSizeUniv :: 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)
- getBuiltinName :: String -> TCM (Maybe QName)
- isBuiltin :: QName -> String -> TCM Bool
Primitive functions
Instances
Enum Nat Source # | |
Eq Nat Source # | |
Integral Nat Source # | |
Num Nat Source # | |
Ord Nat Source # | |
Real Nat Source # | |
Defined in Agda.TypeChecking.Primitive toRational :: Nat -> Rational # | |
Show Nat Source # | |
TermLike Nat Source # | |
FromTerm Nat Source # | |
Defined in Agda.TypeChecking.Primitive | |
ToTerm Nat Source # | |
PrimTerm Nat 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 # | |
Instances
ToTerm Bool Source # | |
ToTerm Char Source # | |
ToTerm Double Source # | |
ToTerm Integer Source # | |
ToTerm Word64 Source # | |
ToTerm Str Source # | |
ToTerm Fixity' Source # | |
ToTerm MetaId Source # | |
ToTerm ArgInfo Source # | |
ToTerm QName Source # | |
ToTerm Fixity Source # | |
ToTerm Associativity Source # | |
Defined in Agda.TypeChecking.Primitive | |
ToTerm PrecedenceLevel Source # | |
Defined in Agda.TypeChecking.Primitive | |
ToTerm Type Source # | |
ToTerm Term Source # | |
ToTerm Lvl Source # | |
ToTerm Nat Source # | |
ToTerm a => ToTerm [a] 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 #
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 fromTerm :: TCM (FromTermFunction [a]) Source # |
redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b') Source #
Conceptually: redBind m f k = either (return . Left . f) k =<< m
fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a) Source #
fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a) Source #
primTrustMe :: TCM PrimitiveImpl Source #
trustMe : {a : Level} {A : Set a} {x y : A} -> x ≡ y
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, TermLike 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 #
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 Source #
The actual primitive functions
lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl) Source #