Agda.TypeChecking.Primitive

Primitive functions, such as addition on builtin integers.

Builtin Sigma

data SigmaKit

Constructors

SigmaKit

Fields

• sigmaName :: QName
• sigmaCon :: ConHead
• sigmaFst :: QName
• sigmaSnd :: QName

Instances

Eq SigmaKit

Defined in Agda.TypeChecking.Primitive

Methods

(==) :: SigmaKit -> SigmaKit -> Bool

(/=) :: SigmaKit -> SigmaKit -> Bool

Show SigmaKit

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> SigmaKit -> ShowS

show :: SigmaKit -> String

showList :: [SigmaKit] -> ShowS

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

Primitive functions

data PrimitiveImpl

Constructors

PrimImpl Type PrimFun

newtype Nat

Constructors

Nat

Fields

• unNat :: Integer

Instances

Enum Nat

Defined in Agda.TypeChecking.Primitive

Methods

succ :: Nat -> Nat

pred :: Nat -> Nat

toEnum :: Int -> Nat

fromEnum :: Nat -> Int

enumFrom :: Nat -> [Nat]

enumFromThen :: Nat -> Nat -> [Nat]

enumFromTo :: Nat -> Nat -> [Nat]

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]

Eq Nat

Defined in Agda.TypeChecking.Primitive

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Integral Nat

Defined in Agda.TypeChecking.Primitive

Methods

quot :: Nat -> Nat -> Nat

rem :: Nat -> Nat -> Nat

div :: Nat -> Nat -> Nat

mod :: Nat -> Nat -> Nat

quotRem :: Nat -> Nat -> (Nat, Nat)

divMod :: Nat -> Nat -> (Nat, Nat)

toInteger :: Nat -> Integer

Num Nat

Defined in Agda.TypeChecking.Primitive

Methods

(+) :: Nat -> Nat -> Nat

(-) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

Defined in Agda.TypeChecking.Primitive

Methods

compare :: Nat -> Nat -> Ordering

(<) :: Nat -> Nat -> Bool

(<=) :: Nat -> Nat -> Bool

(>) :: Nat -> Nat -> Bool

(>=) :: Nat -> Nat -> Bool

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Real Nat

Defined in Agda.TypeChecking.Primitive

Methods

toRational :: Nat -> Rational

Show Nat

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

TermLike Nat

Defined in Agda.TypeChecking.Primitive

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Nat -> m Nat

foldTerm :: Monoid m => (Term -> m) -> Nat -> m

FromTerm Nat

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Nat)

ToTerm Nat

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Nat -> Term)

toTermR :: TCM (Nat -> ReduceM Term)

PrimTerm Nat

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Nat -> TCM Term

newtype Lvl

Constructors

Lvl

Fields

• unLvl :: Integer

Instances

Eq Lvl

Defined in Agda.TypeChecking.Primitive

Methods

(==) :: Lvl -> Lvl -> Bool

(/=) :: Lvl -> Lvl -> Bool

Ord Lvl

Defined in Agda.TypeChecking.Primitive

Methods

compare :: Lvl -> Lvl -> Ordering

(<) :: Lvl -> Lvl -> Bool

(<=) :: Lvl -> Lvl -> Bool

(>) :: Lvl -> Lvl -> Bool

(>=) :: Lvl -> Lvl -> Bool

max :: Lvl -> Lvl -> Lvl

min :: Lvl -> Lvl -> Lvl

Show Lvl

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> Lvl -> ShowS

show :: Lvl -> String

showList :: [Lvl] -> ShowS

FromTerm Lvl

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Lvl)

ToTerm Lvl

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Lvl -> Term)

toTermR :: TCM (Lvl -> ReduceM Term)

PrimTerm Lvl

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Lvl -> TCM Term

class PrimType a where

Methods

primType :: a -> TCM Type

Instances

PrimTerm a => PrimType a

Defined in Agda.TypeChecking.Primitive

Methods

primType :: a -> TCM Type

class PrimTerm a where

Methods

primTerm :: a -> TCM Term

Instances

PrimTerm Bool

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Bool -> TCM Term

PrimTerm Char

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Char -> TCM Term

PrimTerm Double

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Double -> TCM Term

PrimTerm Integer

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Integer -> TCM Term

PrimTerm Word64

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Word64 -> TCM Term

PrimTerm Str

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Str -> TCM Term

PrimTerm Fixity'

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Fixity' -> TCM Term

PrimTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: MetaId -> TCM Term

PrimTerm QName

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: QName -> TCM Term

PrimTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Type -> TCM Term

PrimTerm Lvl

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Lvl -> TCM Term

PrimTerm Nat

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Nat -> TCM Term

PrimTerm a => PrimTerm [a]

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: [a] -> TCM Term

PrimTerm a => PrimTerm (IO a)

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: IO a -> TCM Term

(PrimType a, PrimType b) => PrimTerm (a -> b)

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: (a -> b) -> TCM Term

class ToTerm a where

Minimal complete definition

toTerm

Methods

toTerm :: TCM (a -> Term)

toTermR :: TCM (a -> ReduceM Term)

Instances

ToTerm Bool

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Bool -> Term)

toTermR :: TCM (Bool -> ReduceM Term)

ToTerm Char

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Char -> Term)

toTermR :: TCM (Char -> ReduceM Term)

ToTerm Double

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Double -> Term)

toTermR :: TCM (Double -> ReduceM Term)

ToTerm Integer

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Integer -> Term)

toTermR :: TCM (Integer -> ReduceM Term)

ToTerm Word64

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Word64 -> Term)

toTermR :: TCM (Word64 -> ReduceM Term)

ToTerm Str

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Str -> Term)

toTermR :: TCM (Str -> ReduceM Term)

ToTerm Fixity'

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Fixity' -> Term)

toTermR :: TCM (Fixity' -> ReduceM Term)

ToTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (MetaId -> Term)

toTermR :: TCM (MetaId -> ReduceM Term)

ToTerm ArgInfo

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (ArgInfo -> Term)

toTermR :: TCM (ArgInfo -> ReduceM Term)

ToTerm QName

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (QName -> Term)

toTermR :: TCM (QName -> ReduceM Term)

ToTerm Fixity

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Fixity -> Term)

toTermR :: TCM (Fixity -> ReduceM Term)

ToTerm Associativity

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Associativity -> Term)

toTermR :: TCM (Associativity -> ReduceM Term)

ToTerm PrecedenceLevel

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (PrecedenceLevel -> Term)

toTermR :: TCM (PrecedenceLevel -> ReduceM Term)

ToTerm Type

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Type -> Term)

toTermR :: TCM (Type -> ReduceM Term)

ToTerm Term

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Term -> Term)

toTermR :: TCM (Term -> ReduceM Term)

ToTerm Lvl

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Lvl -> Term)

toTermR :: TCM (Lvl -> ReduceM Term)

ToTerm Nat

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM (Nat -> Term)

toTermR :: TCM (Nat -> ReduceM Term)

ToTerm a => ToTerm [a]

Defined in Agda.TypeChecking.Primitive

Methods

toTerm :: TCM ([a] -> Term)

toTermR :: TCM ([a] -> ReduceM Term)

buildList :: TCM ([Term] -> Term)

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)

class FromTerm a where

Methods

fromTerm :: TCM (FromTermFunction a)

Instances

FromTerm Bool

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Bool)

FromTerm Char

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Char)

FromTerm Double

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Double)

FromTerm Integer

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Integer)

FromTerm Word64

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Word64)

FromTerm Str

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Str)

FromTerm MetaId

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction MetaId)

FromTerm QName

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction QName)

FromTerm Lvl

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Lvl)

FromTerm Nat

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction Nat)

(ToTerm a, FromTerm a) => FromTerm [a]

Defined in Agda.TypeChecking.Primitive

Methods

fromTerm :: TCM (FromTermFunction [a])

redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b')

Conceptually: redBind m f k = either (return . Left . f) k =<< m

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

Constructors

DoTransp

DoHComp

Instances

Eq TranspOrHComp

Defined in Agda.TypeChecking.Primitive

Methods

(==) :: TranspOrHComp -> TranspOrHComp -> Bool

(/=) :: TranspOrHComp -> TranspOrHComp -> Bool

Show TranspOrHComp

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> TranspOrHComp -> ShowS

show :: TranspOrHComp -> String

showList :: [TranspOrHComp] -> ShowS

cmdToName :: TranspOrHComp -> String

data FamilyOrNot a

Constructors

IsFam

Fields

• famThing :: a

IsNot

Fields

• famThing :: a

Instances

Functor FamilyOrNot

Defined in Agda.TypeChecking.Primitive

Methods

fmap :: (a -> b) -> FamilyOrNot a -> FamilyOrNot b

(<$) :: a -> FamilyOrNot b -> FamilyOrNot a

Foldable FamilyOrNot

Defined in Agda.TypeChecking.Primitive

Methods

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

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

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

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

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

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

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

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

toList :: FamilyOrNot a -> [a]

null :: FamilyOrNot a -> Bool

length :: FamilyOrNot a -> Int

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

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

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

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

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

Traversable FamilyOrNot

Defined in Agda.TypeChecking.Primitive

Methods

traverse :: Applicative f => (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)

sequenceA :: Applicative f => FamilyOrNot (f a) -> f (FamilyOrNot a)

mapM :: Monad m => (a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)

sequence :: Monad m => FamilyOrNot (m a) -> m (FamilyOrNot a)

Eq a => Eq (FamilyOrNot a)

Defined in Agda.TypeChecking.Primitive

Methods

(==) :: FamilyOrNot a -> FamilyOrNot a -> Bool

(/=) :: FamilyOrNot a -> FamilyOrNot a -> Bool

Show a => Show (FamilyOrNot a)

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> FamilyOrNot a -> ShowS

show :: FamilyOrNot a -> String

showList :: [FamilyOrNot a] -> ShowS

Reduce a => Reduce (FamilyOrNot a)

Defined in Agda.TypeChecking.Primitive

Methods

reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a)

reduceB' :: FamilyOrNot a -> ReduceM (Blocked (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

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

primStringToListInjective :: TCM PrimitiveImpl

primWord64ToNatInjective :: TCM PrimitiveImpl

getRefl :: TCM (Arg Term -> Term)

primEraseEquality :: TCM PrimitiveImpl

primEraseEquality : {a : Level} {A : Set a} {x y : A} -> x ≡ y -> x ≡ y

getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo)

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

Used for both primForce and primForceLemma.

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 infixr 4

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

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

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 infixl 9

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

(<..>) :: 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

Abbreviation: argN = Arg defaultArgInfo.

domN :: e -> Dom e

argH :: e -> Arg e

Abbreviation: argH = hide Arg defaultArgInfo.

domH :: e -> Dom e

The actual primitive functions

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