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

Safe Haskell | None
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
- type Pred a = a -> Bool
- newtype Nat = Nat {
  - unNat :: Integer
  }
- type Fun a = a -> a
- type Op a = a -> a -> a
- 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
- 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 -> ReduceM Term)
- toTermTCM :: ToTerm a => TCM (a -> TCM Term)
- buildList :: TCM ([Term] -> Term)
- type FromTermFunction a = Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
- class FromTerm a where
  - fromTerm :: TCM (FromTermFunction a)
- 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
- type Rel a = a -> a -> Bool

# Documentation

module Agda.TypeChecking.Primitive.Base

module Agda.TypeChecking.Primitive.Cubical

type Pred a = a -> Bool Source #

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 -> ReduceM Term) Source #
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 #
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 #
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 #
Real Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods toRational :: Nat -> Rational Source #
Eq Nat Source # |
Instance details Defined in Agda.TypeChecking.Primitive Methods (==) :: Nat -> Nat -> Bool Source # (/=) :: Nat -> Nat -> Bool 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 #

type Fun a = a -> a Source #

type Op a = a -> a -> a 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 #

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 -> ReduceM Term) Source #
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 #

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 #

Methods

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

#### Instances

Instances details

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

toTermTCM :: ToTerm a => TCM (a -> TCM 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

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 #

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 `MetaId`s 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 #

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