Agda-2.5.2: 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

Primitive functions

data PrimitiveImpl #

Constructors

PrimImpl Type PrimFun 

newtype Nat #

Constructors

Nat 

Fields

Instances

Enum Nat # 

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 # 

Methods

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

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

Integral Nat # 

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 # 

Methods

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

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

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

negate :: Nat -> Nat #

abs :: Nat -> Nat #

signum :: Nat -> Nat #

fromInteger :: Integer -> Nat #

Ord Nat # 

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 # 

Methods

toRational :: Nat -> Rational #

Show Nat # 

Methods

showsPrec :: Int -> Nat -> ShowS #

show :: Nat -> String #

showList :: [Nat] -> ShowS #

TermLike Nat # 

Methods

traverseTerm :: (Term -> Term) -> Nat -> Nat #

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

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

FromTerm Nat # 
ToTerm Nat # 

Methods

toTerm :: TCM (Nat -> Term) #

toTermR :: TCM (Nat -> ReduceM Term) #

PrimTerm Nat # 

Methods

primTerm :: Nat -> TCM Term #

newtype Lvl #

Constructors

Lvl 

Fields

Instances

Eq Lvl # 

Methods

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

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

Ord Lvl # 

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 # 

Methods

showsPrec :: Int -> Lvl -> ShowS #

show :: Lvl -> String #

showList :: [Lvl] -> ShowS #

FromTerm Lvl # 
ToTerm Lvl # 

Methods

toTerm :: TCM (Lvl -> Term) #

toTermR :: TCM (Lvl -> ReduceM Term) #

PrimTerm Lvl # 

Methods

primTerm :: Lvl -> TCM Term #

class PrimType a where #

Minimal complete definition

primType

Methods

primType :: a -> TCM Type #

Instances

PrimTerm a => PrimType a # 

Methods

primType :: a -> TCM Type #

class PrimTerm a where #

Minimal complete definition

primTerm

Methods

primTerm :: a -> TCM Term #

Instances

PrimTerm Bool # 

Methods

primTerm :: Bool -> TCM Term #

PrimTerm Char # 

Methods

primTerm :: Char -> TCM Term #

PrimTerm Double # 

Methods

primTerm :: Double -> TCM Term #

PrimTerm Integer # 

Methods

primTerm :: Integer -> TCM Term #

PrimTerm Str # 

Methods

primTerm :: Str -> TCM Term #

PrimTerm Fixity' # 

Methods

primTerm :: Fixity' -> TCM Term #

PrimTerm MetaId # 

Methods

primTerm :: MetaId -> TCM Term #

PrimTerm QName # 

Methods

primTerm :: QName -> TCM Term #

PrimTerm Type # 

Methods

primTerm :: Type -> TCM Term #

PrimTerm Lvl # 

Methods

primTerm :: Lvl -> TCM Term #

PrimTerm Nat # 

Methods

primTerm :: Nat -> TCM Term #

PrimTerm a => PrimTerm [a] # 

Methods

primTerm :: [a] -> TCM Term #

PrimTerm a => PrimTerm (IO a) # 

Methods

primTerm :: IO a -> TCM Term #

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

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 # 

Methods

toTerm :: TCM (Bool -> Term) #

toTermR :: TCM (Bool -> ReduceM Term) #

ToTerm Char # 

Methods

toTerm :: TCM (Char -> Term) #

toTermR :: TCM (Char -> ReduceM Term) #

ToTerm Double # 

Methods

toTerm :: TCM (Double -> Term) #

toTermR :: TCM (Double -> ReduceM Term) #

ToTerm Integer # 
ToTerm Str # 

Methods

toTerm :: TCM (Str -> Term) #

toTermR :: TCM (Str -> ReduceM Term) #

ToTerm Fixity' # 
ToTerm MetaId # 

Methods

toTerm :: TCM (MetaId -> Term) #

toTermR :: TCM (MetaId -> ReduceM Term) #

ToTerm ArgInfo # 
ToTerm QName # 

Methods

toTerm :: TCM (QName -> Term) #

toTermR :: TCM (QName -> ReduceM Term) #

ToTerm Fixity # 

Methods

toTerm :: TCM (Fixity -> Term) #

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

ToTerm Associativity # 
ToTerm PrecedenceLevel # 
ToTerm Type # 

Methods

toTerm :: TCM (Type -> Term) #

toTermR :: TCM (Type -> ReduceM Term) #

ToTerm Term # 

Methods

toTerm :: TCM (Term -> Term) #

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

ToTerm Lvl # 

Methods

toTerm :: TCM (Lvl -> Term) #

toTermR :: TCM (Lvl -> ReduceM Term) #

ToTerm Nat # 

Methods

toTerm :: TCM (Nat -> Term) #

toTermR :: TCM (Nat -> ReduceM Term) #

ToTerm a => ToTerm [a] # 

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.

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) #

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

(.-->) :: TCM Type -> TCM Type -> TCM Type infixr 4 #

(..-->) :: TCM Type -> TCM Type -> TCM Type infixr 4 #

varM :: Int -> TCM Term #

(<@>) :: TCM Term -> TCM Term -> TCM Term infixl 9 #

(<#>) :: TCM Term -> TCM Term -> TCM Term infixl 9 #

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 #