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

Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Primitive

Contents

Description

Primitive functions, such as addition on builtin integers.

Synopsis

Builtin Sigma

data SigmaKit Source #

Constructors

SigmaKit 
Instances
Eq SigmaKit Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

Show SigmaKit Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> SigmaKit -> ShowS

show :: SigmaKit -> String

showList :: [SigmaKit] -> ShowS

Primitive functions

newtype Nat Source #

Constructors

Nat 

Fields

Instances
Enum Nat Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

Integral Nat Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

toRational :: Nat -> Rational

Show Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

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

ToTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

PrimTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

primTerm :: Nat -> TCM Term Source #

newtype Lvl Source #

Constructors

Lvl 

Fields

Instances
Eq Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

Ord Lvl Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> Lvl -> ShowS

show :: Lvl -> String

showList :: [Lvl] -> ShowS

FromTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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

PrimTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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

ToTerm Fixity' Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm ArgInfo Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Fixity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Associativity Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm PrecedenceLevel Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Type Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Term Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

ToTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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.

class FromTerm a where Source #

Instances
FromTerm Bool Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Char Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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

FromTerm MetaId Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm QName Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Lvl Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

FromTerm Nat Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

(ToTerm a, FromTerm a) => FromTerm [a] Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

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

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

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

data TranspOrHComp Source #

Constructors

DoTransp 
DoHComp 
Instances
Eq TranspOrHComp Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Show TranspOrHComp Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> TranspOrHComp -> ShowS

show :: TranspOrHComp -> String

showList :: [TranspOrHComp] -> ShowS

data FamilyOrNot a Source #

Constructors

IsFam 

Fields

IsNot 

Fields

Instances
Functor FamilyOrNot Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

Foldable FamilyOrNot Source # 
Instance details

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 Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

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

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

Show a => Show (FamilyOrNot a) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

Methods

showsPrec :: Int -> FamilyOrNot a -> ShowS

show :: FamilyOrNot a -> String

showList :: [FamilyOrNot a] -> ShowS

Reduce a => Reduce (FamilyOrNot a) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive

listS :: [(Int, Term)] -> Substitution 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.

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 #

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 #

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

tset :: Monad tcm => tcm Type 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 #

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

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