Safe Haskell | None |
---|---|
Language | Haskell2010 |
Primitive functions, such as addition on builtin integers.
Synopsis
- data SigmaKit = SigmaKit {}
- getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)
- 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)
- requireCubical :: TCM ()
- primINeg' :: TCM PrimitiveImpl
- primDepIMin' :: TCM PrimitiveImpl
- primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl
- primIMin' :: TCM PrimitiveImpl
- primIMax' :: TCM PrimitiveImpl
- imax :: HasBuiltins m => m Term -> m Term -> m Term
- imin :: HasBuiltins m => m Term -> m Term -> m Term
- primIdJ :: TCM PrimitiveImpl
- primIdElim' :: TCM PrimitiveImpl
- primPOr :: TCM PrimitiveImpl
- primPartial' :: TCM PrimitiveImpl
- primPartialP' :: TCM PrimitiveImpl
- primSubOut' :: TCM PrimitiveImpl
- primIdFace' :: TCM PrimitiveImpl
- primIdPath' :: TCM PrimitiveImpl
- primTrans' :: TCM PrimitiveImpl
- primHComp' :: TCM PrimitiveImpl
- data TranspOrHComp
- cmdToName :: TranspOrHComp -> String
- data FamilyOrNot a
- primTransHComp :: TranspOrHComp -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)
- primComp :: TCM PrimitiveImpl
- listS :: [(Int, Term)] -> Substitution
- primGlue' :: TCM PrimitiveImpl
- prim_glue' :: TCM PrimitiveImpl
- prim_unglue' :: TCM PrimitiveImpl
- primFaceForall' :: TCM PrimitiveImpl
- decomposeInterval :: HasBuiltins m => Term -> m [(Map Int Bool, [Term])]
- decomposeInterval' :: HasBuiltins m => Term -> m [(Map Int (Set Bool), [Term])]
- mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl
- primCharToNatInjective :: TCM PrimitiveImpl
- primStringToListInjective :: 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
- (-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type
- (.-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type
- (..-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type
- garr :: Monad tcm => (Relevance -> Relevance) -> tcm Type -> tcm Type -> tcm Type
- gpi :: (MonadTCM tcm, MonadDebug tcm) => ArgInfo -> String -> tcm Type -> tcm Type -> tcm Type
- hPi :: (MonadTCM tcm, MonadDebug tcm) => String -> tcm Type -> tcm Type -> tcm Type
- nPi :: (MonadTCM tcm, MonadDebug tcm) => String -> tcm Type -> tcm Type -> tcm Type
- hPi' :: (MonadTCM tcm, MonadDebug tcm) => String -> NamesT tcm Type -> (NamesT tcm Term -> NamesT tcm Type) -> NamesT tcm Type
- nPi' :: (MonadTCM tcm, MonadDebug tcm) => String -> NamesT tcm Type -> (NamesT tcm Term -> NamesT tcm Type) -> NamesT tcm Type
- pPi' :: (MonadTCM tcm, MonadDebug tcm) => String -> NamesT tcm Term -> (NamesT tcm Term -> NamesT tcm Type) -> NamesT tcm Type
- el' :: Monad m => m Term -> m Term -> m Type
- elInf :: Functor m => m Term -> m Type
- nolam :: Term -> Term
- varM :: Monad tcm => Int -> tcm Term
- gApply :: Monad tcm => Hiding -> tcm Term -> tcm Term -> tcm Term
- gApply' :: Monad tcm => ArgInfo -> tcm Term -> tcm Term -> tcm Term
- (<@>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term
- (<#>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term
- (<..>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term
- (<@@>) :: Monad tcm => tcm Term -> (tcm Term, tcm Term, tcm Term) -> tcm Term
- list :: TCM Term -> TCM Term
- io :: TCM Term -> TCM Term
- path :: TCM Term -> TCM Term
- el :: Functor tcm => tcm Term -> tcm Type
- tset :: Monad tcm => tcm Type
- sSizeUniv :: Sort
- tSizeUniv :: Monad tcm => 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
Builtin Sigma
getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit) Source #
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 #
requireCubical :: TCM () Source #
primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl Source #
data TranspOrHComp Source #
Instances
Eq TranspOrHComp Source # | |
Defined in Agda.TypeChecking.Primitive (==) :: TranspOrHComp -> TranspOrHComp -> Bool # (/=) :: TranspOrHComp -> TranspOrHComp -> Bool # | |
Show TranspOrHComp Source # | |
Defined in Agda.TypeChecking.Primitive showsPrec :: Int -> TranspOrHComp -> ShowS # show :: TranspOrHComp -> String # showList :: [TranspOrHComp] -> ShowS # |
cmdToName :: TranspOrHComp -> String Source #
data FamilyOrNot a Source #
Instances
primTransHComp :: TranspOrHComp -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term) Source #
decomposeInterval :: HasBuiltins m => Term -> m [(Map Int Bool, [Term])] Source #
decomposeInterval' :: HasBuiltins m => Term -> m [(Map Int (Set Bool), [Term])] 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 ≡ 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 #
gpi :: (MonadTCM tcm, MonadDebug tcm) => ArgInfo -> String -> tcm Type -> tcm Type -> tcm Type Source #
hPi' :: (MonadTCM tcm, MonadDebug tcm) => String -> NamesT tcm Type -> (NamesT tcm Term -> NamesT tcm Type) -> NamesT tcm Type Source #
nPi' :: (MonadTCM tcm, MonadDebug tcm) => String -> NamesT tcm Type -> (NamesT tcm Term -> NamesT tcm Type) -> NamesT tcm Type Source #
pPi' :: (MonadTCM tcm, MonadDebug tcm) => String -> NamesT tcm Term -> (NamesT tcm Term -> NamesT tcm Type) -> NamesT tcm Type Source #
The actual primitive functions
lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl) Source #