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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Primitive

Contents

- Builtin Sigma
- Primitive functions
- The actual primitive functions

Description

Primitive functions, such as addition on builtin integers.

Synopsis

- data SigmaKit = SigmaKit {
  - sigmaName :: QName
  - sigmaCon :: ConHead
  - sigmaFst :: QName
  - sigmaSnd :: QName
  }
- getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit)
- data PrimitiveImpl = PrimImpl Type PrimFun
- 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)
  - toTermR :: TCM (a -> ReduceM Term)
- 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
  - = DoTransp
  - | DoHComp
- cmdToName :: TranspOrHComp -> String
- data FamilyOrNot a
  - = IsFam {
    - famThing :: a
    }
  - | IsNot {
    - famThing :: 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
- primWord64ToNatInjective :: 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

data SigmaKit Source #

Constructors

SigmaKit |

Fields

- sigmaName :: QName
- sigmaCon :: ConHead
- sigmaFst :: QName
- sigmaSnd :: QName

Instances

Eq SigmaKit Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods (==) :: SigmaKit -> SigmaKit -> Bool Source # (/=) :: SigmaKit -> SigmaKit -> Bool Source #
Show SigmaKit Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods showsPrec :: Int -> SigmaKit -> ShowS Source # show :: SigmaKit -> String Source # showList :: [SigmaKit] -> ShowS Source #

getSigmaKit :: (HasBuiltins m, HasConstInfo m) => m (Maybe SigmaKit) Source #

# Primitive functions

data PrimitiveImpl Source #

Constructors

PrimImpl Type PrimFun |

newtype Nat Source #

Constructors

Nat |

Fields

- unNat :: Integer

Instances

Enum Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods succ :: Nat -> Nat Source # pred :: Nat -> Nat Source # toEnum :: Int -> Nat Source # fromEnum :: Nat -> Int Source # enumFrom :: Nat -> [Nat] Source # enumFromThen :: Nat -> Nat -> [Nat] Source # enumFromTo :: Nat -> Nat -> [Nat] Source # enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] Source #
Eq Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods (==) :: Nat -> Nat -> Bool Source # (/=) :: Nat -> Nat -> Bool Source #
Integral Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods quot :: Nat -> Nat -> Nat Source # rem :: Nat -> Nat -> Nat Source # div :: Nat -> Nat -> Nat Source # mod :: Nat -> Nat -> Nat Source # quotRem :: Nat -> Nat -> (Nat, Nat) Source # divMod :: Nat -> Nat -> (Nat, Nat) Source # toInteger :: Nat -> Integer Source #
Num Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods (+) :: Nat -> Nat -> Nat Source # (-) :: Nat -> Nat -> Nat Source # (*) :: Nat -> Nat -> Nat Source # negate :: Nat -> Nat Source # abs :: Nat -> Nat Source # signum :: Nat -> Nat Source # fromInteger :: Integer -> Nat Source #
Ord Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods compare :: Nat -> Nat -> Ordering Source # (<) :: Nat -> Nat -> Bool Source # (<=) :: Nat -> Nat -> Bool Source # (>) :: Nat -> Nat -> Bool Source # (>=) :: Nat -> Nat -> Bool Source # max :: Nat -> Nat -> Nat Source # min :: Nat -> Nat -> Nat Source #
Real Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toRational :: Nat -> Rational Source #
Show Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods showsPrec :: Int -> Nat -> ShowS Source # show :: Nat -> String Source # showList :: [Nat] -> ShowS Source #
TermLike Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods traverseTermM :: Monad m => (Term -> m Term) -> Nat -> m Nat Source # foldTerm :: Monoid m => (Term -> m) -> Nat -> m Source #
FromTerm Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Nat) Source #
ToTerm Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Nat -> Term) Source # toTermR :: TCM (Nat -> ReduceM Term) Source #
PrimTerm Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Nat -> TCM Term Source #

newtype Lvl Source #

Constructors

Lvl |

Fields

- unLvl :: Integer

Instances

Eq Lvl Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods (==) :: Lvl -> Lvl -> Bool Source # (/=) :: Lvl -> Lvl -> Bool Source #
Ord Lvl Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods compare :: Lvl -> Lvl -> Ordering Source # (<) :: Lvl -> Lvl -> Bool Source # (<=) :: Lvl -> Lvl -> Bool Source # (>) :: Lvl -> Lvl -> Bool Source # (>=) :: Lvl -> Lvl -> Bool Source # max :: Lvl -> Lvl -> Lvl Source # min :: Lvl -> Lvl -> Lvl Source #
Show Lvl Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods showsPrec :: Int -> Lvl -> ShowS Source # show :: Lvl -> String Source # showList :: [Lvl] -> ShowS Source #
FromTerm Lvl Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Lvl) Source #
ToTerm Lvl Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Lvl -> Term) Source # toTermR :: TCM (Lvl -> ReduceM Term) Source #
PrimTerm Lvl Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Lvl -> TCM Term Source #

class PrimType a where Source #

Methods

primType :: a -> TCM Type Source #

Instances

PrimTerm a => PrimType a Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primType :: a -> TCM Type Source #

class PrimTerm a where Source #

Methods

primTerm :: a -> TCM Term Source #

Instances

PrimTerm Bool Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Bool -> TCM Term Source #
PrimTerm Char Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Char -> TCM Term Source #
PrimTerm Double Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Double -> TCM Term Source #
PrimTerm Integer Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Integer -> TCM Term Source #
PrimTerm Word64 Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Word64 -> TCM Term Source #
PrimTerm Str Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Str -> TCM Term Source #
PrimTerm Fixity' Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Fixity' -> TCM Term Source #
PrimTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: MetaId -> TCM Term Source #
PrimTerm QName Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: QName -> TCM Term Source #
PrimTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Type -> TCM Term Source #
PrimTerm Lvl Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Lvl -> TCM Term Source #
PrimTerm Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Nat -> TCM Term Source #
PrimTerm a => PrimTerm [a] Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: [a] -> TCM Term Source #
PrimTerm a => PrimTerm (IO a) Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: IO a -> TCM Term Source #
(PrimType a, PrimType b) => PrimTerm (a -> b) Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: (a -> b) -> TCM Term Source #

class ToTerm a where Source #

Minimal complete definition

toTerm

Methods

toTerm :: TCM (a -> Term) Source #

toTermR :: TCM (a -> ReduceM Term) Source #

Instances

ToTerm Bool Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Bool -> Term) Source # toTermR :: TCM (Bool -> ReduceM Term) Source #
ToTerm Char Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Char -> Term) Source # toTermR :: TCM (Char -> ReduceM Term) Source #
ToTerm Double Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Double -> Term) Source # toTermR :: TCM (Double -> ReduceM Term) Source #
ToTerm Integer Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Integer -> Term) Source # toTermR :: TCM (Integer -> ReduceM Term) Source #
ToTerm Word64 Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Word64 -> Term) Source # toTermR :: TCM (Word64 -> ReduceM Term) Source #
ToTerm Str Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Str -> Term) Source # toTermR :: TCM (Str -> ReduceM Term) Source #
ToTerm Fixity' Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity' -> Term) Source # toTermR :: TCM (Fixity' -> ReduceM Term) Source #
ToTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (MetaId -> Term) Source # toTermR :: TCM (MetaId -> ReduceM Term) Source #
ToTerm ArgInfo Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (ArgInfo -> Term) Source # toTermR :: TCM (ArgInfo -> ReduceM Term) Source #
ToTerm QName Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (QName -> Term) Source # toTermR :: TCM (QName -> ReduceM Term) Source #
ToTerm Fixity Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity -> Term) Source # toTermR :: TCM (Fixity -> ReduceM Term) Source #
ToTerm Associativity Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Associativity -> Term) Source # toTermR :: TCM (Associativity -> ReduceM Term) Source #
ToTerm PrecedenceLevel Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (PrecedenceLevel -> Term) Source # toTermR :: TCM (PrecedenceLevel -> ReduceM Term) Source #
ToTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Type -> Term) Source # toTermR :: TCM (Type -> ReduceM Term) Source #
ToTerm Term Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Term -> Term) Source # toTermR :: TCM (Term -> ReduceM Term) Source #
ToTerm Lvl Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Lvl -> Term) Source # toTermR :: TCM (Lvl -> ReduceM Term) Source #
ToTerm Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Nat -> Term) Source # toTermR :: TCM (Nat -> ReduceM Term) Source #
ToTerm a => ToTerm [a] Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM ([a] -> Term) Source # toTermR :: TCM ([a] -> ReduceM Term) 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

FromTerm Bool Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Bool) Source #
FromTerm Char Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Char) Source #
FromTerm Double Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Double) Source #
FromTerm Integer Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Integer) Source #
FromTerm Word64 Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Word64) Source #
FromTerm Str Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Str) Source #
FromTerm MetaId Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction MetaId) Source #
FromTerm QName Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction QName) Source #
FromTerm Lvl Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Lvl) Source #
FromTerm Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Nat) Source #
(ToTerm a, FromTerm a) => FromTerm [a] Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods 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`

redReturn :: a -> ReduceM (Reduced a' a) Source #

fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a) Source #

fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a) Source #

requireCubical :: TCM () Source #

primINeg' :: TCM PrimitiveImpl Source #

primDepIMin' :: TCM PrimitiveImpl Source #

primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl Source #

primIMin' :: TCM PrimitiveImpl Source #

primIMax' :: TCM PrimitiveImpl Source #

imax :: HasBuiltins m => m Term -> m Term -> m Term Source #

imin :: HasBuiltins m => m Term -> m Term -> m Term Source #

primIdJ :: TCM PrimitiveImpl Source #

primIdElim' :: TCM PrimitiveImpl Source #

primPOr :: TCM PrimitiveImpl Source #

primPartial' :: TCM PrimitiveImpl Source #

primPartialP' :: TCM PrimitiveImpl Source #

primSubOut' :: TCM PrimitiveImpl Source #

primIdFace' :: TCM PrimitiveImpl Source #

primIdPath' :: TCM PrimitiveImpl Source #

primTrans' :: TCM PrimitiveImpl Source #

primHComp' :: TCM PrimitiveImpl Source #

data TranspOrHComp Source #

Constructors

DoTransp |
DoHComp |

Instances

Eq TranspOrHComp Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods (==) :: TranspOrHComp -> TranspOrHComp -> Bool Source # (/=) :: TranspOrHComp -> TranspOrHComp -> Bool Source #
Show TranspOrHComp Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods showsPrec :: Int -> TranspOrHComp -> ShowS Source # show :: TranspOrHComp -> String Source # showList :: [TranspOrHComp] -> ShowS Source #

cmdToName :: TranspOrHComp -> String Source #

data FamilyOrNot a Source #

Constructors

IsFam |

Fields

- famThing :: a

IsNot |

Fields

- famThing :: a

Instances

Functor FamilyOrNot Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods fmap :: (a -> b) -> FamilyOrNot a -> FamilyOrNot b Source # (<$) :: a -> FamilyOrNot b -> FamilyOrNot a Source #
Foldable FamilyOrNot Source # |

Instance details

Defined in Agda.TypeChecking.Primitive

Methods

fold :: Monoid m => FamilyOrNot m -> m Source #

foldMap :: Monoid m => (a -> m) -> FamilyOrNot a -> m Source #

foldr :: (a -> b -> b) -> b -> FamilyOrNot a -> b Source #

foldr' :: (a -> b -> b) -> b -> FamilyOrNot a -> b Source #

foldl :: (b -> a -> b) -> b -> FamilyOrNot a -> b Source #

foldl' :: (b -> a -> b) -> b -> FamilyOrNot a -> b Source #

foldr1 :: (a -> a -> a) -> FamilyOrNot a -> a Source #

foldl1 :: (a -> a -> a) -> FamilyOrNot a -> a Source #

toList :: FamilyOrNot a -> [a] Source #

null :: FamilyOrNot a -> Bool Source #

length :: FamilyOrNot a -> Int Source #

elem :: Eq a => a -> FamilyOrNot a -> Bool Source #

maximum :: Ord a => FamilyOrNot a -> a Source #

minimum :: Ord a => FamilyOrNot a -> a Source #

sum :: Num a => FamilyOrNot a -> a Source #

product :: Num a => FamilyOrNot a -> a Source #

Traversable FamilyOrNot Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods traverse :: Applicative f => (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b) Source # sequenceA :: Applicative f => FamilyOrNot (f a) -> f (FamilyOrNot a) Source # mapM :: Monad m => (a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b) Source # sequence :: Monad m => FamilyOrNot (m a) -> m (FamilyOrNot a) Source #
Eq a => Eq (FamilyOrNot a) Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods (==) :: FamilyOrNot a -> FamilyOrNot a -> Bool Source # (/=) :: FamilyOrNot a -> FamilyOrNot a -> Bool Source #
Show a => Show (FamilyOrNot a) Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods showsPrec :: Int -> FamilyOrNot a -> ShowS Source # show :: FamilyOrNot a -> String Source # showList :: [FamilyOrNot a] -> ShowS Source #
Reduce a => Reduce (FamilyOrNot a) Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a) Source # reduceB' :: FamilyOrNot a -> ReduceM (Blocked (FamilyOrNot a)) Source #

primTransHComp :: TranspOrHComp -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term) Source #

primComp :: TCM PrimitiveImpl Source #

listS :: [(Int, Term)] -> Substitution Source #

primGlue' :: TCM PrimitiveImpl Source #

prim_glue' :: TCM PrimitiveImpl Source #

prim_unglue' :: TCM PrimitiveImpl Source #

primFaceForall' :: TCM PrimitiveImpl 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.

primCharToNatInjective :: TCM PrimitiveImpl Source #

primStringToListInjective :: TCM PrimitiveImpl Source #

primWord64ToNatInjective :: TCM PrimitiveImpl Source #

getRefl :: TCM (Arg Term -> Term) Source #

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`.

primForce :: TCM PrimitiveImpl Source #

primForceLemma :: TCM PrimitiveImpl Source #

mkPrimLevelZero :: TCM PrimitiveImpl Source #

mkPrimLevelSuc :: TCM PrimitiveImpl Source #

mkPrimLevelMax :: TCM PrimitiveImpl Source #

mkPrimSetOmega :: TCM PrimitiveImpl Source #

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 #

(-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type infixr 4 Source #

(.-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type infixr 4 Source #

(..-->) :: Monad tcm => tcm Type -> tcm Type -> tcm Type infixr 4 Source #

garr :: Monad tcm => (Relevance -> Relevance) -> tcm Type -> tcm Type -> tcm Type Source #

gpi :: (MonadTCM tcm, MonadDebug tcm) => ArgInfo -> String -> tcm Type -> tcm Type -> tcm Type Source #

hPi :: (MonadTCM tcm, MonadDebug tcm) => String -> tcm Type -> tcm Type -> tcm Type Source #

nPi :: (MonadTCM tcm, MonadDebug tcm) => 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 #

el' :: Monad m => m Term -> m Term -> m Type Source #

elInf :: Functor m => m Term -> m Type Source #

nolam :: Term -> Term Source #

varM :: Monad tcm => Int -> tcm Term Source #

gApply :: Monad tcm => Hiding -> tcm Term -> tcm Term -> tcm Term Source #

gApply' :: Monad tcm => ArgInfo -> tcm Term -> tcm Term -> tcm Term Source #

(<@>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term infixl 9 Source #

(<#>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term infixl 9 Source #

(<..>) :: Monad tcm => tcm Term -> tcm Term -> tcm Term Source #

(<@@>) :: Monad tcm => tcm Term -> (tcm Term, tcm Term, tcm Term) -> tcm Term Source #

list :: TCM Term -> TCM Term Source #

io :: TCM Term -> TCM Term Source #

path :: TCM Term -> TCM Term Source #

el :: Functor tcm => tcm Term -> tcm Type Source #

tset :: Monad tcm => tcm Type Source #

sSizeUniv :: Sort Source #

tSizeUniv :: Monad tcm => tcm Type Source #

argN :: e -> Arg e Source #

Abbreviation: `argN = `Arg` `defaultArgInfo``.

domN :: e -> Dom e Source #

argH :: e -> Arg e Source #

Abbreviation: `argH = `hide` `Arg` `defaultArgInfo``.

domH :: e -> Dom e Source #

# The actual primitive functions

type Op a = a -> a -> a Source #

type Fun a = a -> a Source #

type Rel a = a -> a -> Bool Source #

type Pred a = a -> Bool Source #

primitiveFunctions :: Map String (TCM PrimitiveImpl) Source #

lookupPrimitiveFunction :: String -> TCM PrimitiveImpl Source #

lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl) Source #

getBuiltinName :: String -> TCM (Maybe QName) Source #

isBuiltin :: QName -> String -> TCM Bool Source #