Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Primitive

Description

Primitive functions, such as addition on builtin integers.

Synopsis

module Agda.TypeChecking.Primitive.Base
module Agda.TypeChecking.Primitive.Cubical
newtype Nat = Nat {
- unNat :: Integer
}
type Pred a = a -> Bool
type Fun a = a -> a
newtype Lvl = Lvl {
- unLvl :: Integer
}
class PrimType a where
- primType :: a -> TCM Type
class PrimType a => PrimTerm a where
- primTerm :: a -> TCM Term
class ToTerm a where
- toTerm :: TCM (a -> Term)
- toTermR :: TCM (a -> ReduceM Term)
type FromTermFunction a = Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
class FromTerm a where
- fromTerm :: TCM (FromTermFunction a)
type Op a = a -> a -> a
type Rel a = a -> a -> Bool
getRefl :: TCM (Arg Term -> Term)
primitiveFunctions :: Map PrimitiveId (TCM PrimitiveImpl)
primWord64ToNatInjective :: TCM PrimitiveImpl
primFloatToWord64Injective :: TCM PrimitiveImpl
primCharToNatInjective :: TCM PrimitiveImpl
primStringToListInjective :: TCM PrimitiveImpl
primStringFromListInjective :: TCM PrimitiveImpl
primEraseEquality :: TCM PrimitiveImpl
primForce :: TCM PrimitiveImpl
primForceLemma :: TCM PrimitiveImpl
primQNameToWord64sInjective :: TCM PrimitiveImpl
primMetaToNatInjective :: TCM PrimitiveImpl
buildList :: TCM ([Term] -> Term)
fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)
fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)
mkPrimInjective :: Type -> Type -> QName -> TCM PrimitiveImpl
metaToNat :: MetaId -> Nat
getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo)
genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
mkPrimLevelZero :: TCM PrimitiveImpl
mkPrimLevelSuc :: TCM PrimitiveImpl
mkPrimLevelMax :: TCM PrimitiveImpl
primLockUniv' :: TCM PrimitiveImpl
mkPrimFun1TCM :: (FromTerm a, ToTerm 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
mkPrimFun3 :: (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b, ToTerm b, PrimType c, FromTerm c, PrimType d, ToTerm d) => (a -> b -> c -> d) -> 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

Documentation

module Agda.TypeChecking.Primitive.Base

module Agda.TypeChecking.Primitive.Cubical

newtype Nat Source #

Constructors

Nat
Fields unNat :: Integer

Instances

Instances details

Pretty Nat Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods pretty :: Nat -> Doc Source # prettyPrec :: Int -> Nat -> Doc Source # prettyList :: [Nat] -> Doc 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 #
PrimTerm Nat Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Nat -> TCM Term Source #
PrimType Nat Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primType :: Nat -> TCM Type Source #
ToTerm Nat Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Nat -> Term) Source # toTermR :: TCM (Nat -> ReduceM Term) Source #
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]
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
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
Real Nat Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toRational :: Nat -> Rational
Eq Nat Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods (==) :: Nat -> Nat -> Bool (/=) :: Nat -> Nat -> Bool
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

type Pred a = a -> Bool Source #

type Fun a = a -> a Source #

newtype Lvl Source #

Constructors

Lvl
Fields unLvl :: Integer

Instances

Instances details

Pretty Lvl Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods pretty :: Lvl -> Doc Source # prettyPrec :: Int -> Lvl -> Doc Source # prettyList :: [Lvl] -> Doc Source #
FromTerm Lvl Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Lvl) Source #
PrimTerm Lvl Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Lvl -> TCM Term Source #
PrimType Lvl Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primType :: Lvl -> TCM Type Source #
ToTerm Lvl Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Lvl -> Term) Source # toTermR :: TCM (Lvl -> ReduceM Term) Source #
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

class PrimType a where Source #

Minimal complete definition

Nothing

Methods

primType :: a -> TCM Type Source #

default primType :: PrimTerm a => a -> TCM Type Source #

Instances

Instances details

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

class PrimType a => PrimTerm a where Source #

Methods

primTerm :: a -> TCM Term Source #

Instances

Instances details

PrimTerm QName Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: QName -> 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 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 Word64 Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Word64 -> TCM Term Source #
PrimTerm Text Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Text -> TCM Term Source #
PrimTerm Integer Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Integer -> TCM Term Source #
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 a => PrimTerm (IO a) Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: IO a -> TCM Term Source #
PrimTerm a => PrimTerm (Maybe a) Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: Maybe a -> TCM Term Source #
PrimTerm a => PrimTerm [a] Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods primTerm :: [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 #
(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

Instances details

ToTerm QName Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (QName -> Term) Source # toTermR :: TCM (QName -> 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 Associativity Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Associativity -> Term) Source # toTermR :: TCM (Associativity -> 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 Fixity' Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Fixity' -> Term) Source # toTermR :: TCM (Fixity' -> ReduceM Term) Source #
ToTerm FixityLevel Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (FixityLevel -> Term) Source # toTermR :: TCM (FixityLevel -> 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 Term Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Term -> Term) Source # toTermR :: TCM (Term -> 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 Blocker Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Blocker -> Term) Source # toTermR :: TCM (Blocker -> 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 Word64 Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Word64 -> Term) Source # toTermR :: TCM (Word64 -> ReduceM Term) Source #
ToTerm Text Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Text -> Term) Source # toTermR :: TCM (Text -> 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 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 (Dom Type) Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Dom Type -> Term) Source # toTermR :: TCM (Dom Type -> ReduceM Term) Source #
ToTerm a => ToTerm (Maybe a) Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM (Maybe a -> Term) Source # toTermR :: TCM (Maybe a -> 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 #
(ToTerm a, ToTerm b) => ToTerm (a, b) Source #
Instance details Defined in Agda.TypeChecking.Primitive Methods toTerm :: TCM ((a, b) -> Term) Source # toTermR :: TCM ((a, b) -> ReduceM Term) Source #

type FromTermFunction a = Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a) Source #

class FromTerm a where Source #

Methods

fromTerm :: TCM (FromTermFunction a) Source #

Instances

Instances details

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

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

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

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

primitiveFunctions :: Map PrimitiveId (TCM PrimitiveImpl) Source #

primWord64ToNatInjective :: TCM PrimitiveImpl Source #

primFloatToWord64Injective :: TCM PrimitiveImpl Source #

primCharToNatInjective :: TCM PrimitiveImpl Source #

primStringToListInjective :: TCM PrimitiveImpl Source #

primStringFromListInjective :: TCM PrimitiveImpl Source #

primEraseEquality :: TCM PrimitiveImpl Source #

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

primForce :: TCM PrimitiveImpl Source #

primForceLemma :: TCM PrimitiveImpl Source #

primQNameToWord64sInjective :: TCM PrimitiveImpl Source #

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

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

fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a) 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.

metaToNat :: MetaId -> Nat Source #

Converts MetaIds to natural numbers.

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.

mkPrimLevelZero :: TCM PrimitiveImpl Source #

mkPrimLevelSuc :: TCM PrimitiveImpl Source #

mkPrimLevelMax :: TCM PrimitiveImpl Source #

primLockUniv' :: TCM PrimitiveImpl Source #

mkPrimFun1TCM :: (FromTerm a, ToTerm 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 #

mkPrimFun3 :: (PrimType a, FromTerm a, ToTerm a, PrimType b, FromTerm b, ToTerm b, PrimType c, FromTerm c, PrimType d, ToTerm d) => (a -> b -> c -> d) -> 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 #