| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Primitive
Description
Primitive functions, such as addition on builtin integers.
Synopsis
- data PrimitiveImpl = PrimImpl Type PrimFun
- newtype Nat = Nat {}
- newtype Lvl = Lvl {}
- class PrimType a where
- class PrimTerm a where
- class ToTerm a where
- buildList :: TCM ([Term] -> Term)
- type FromTermFunction a = Arg Term -> ReduceM (Reduced (MaybeReduced (Arg Term)) a)
- class FromTerm a where
- redBind :: ReduceM (Reduced a a') -> (a -> b) -> (a' -> ReduceM (Reduced b b')) -> ReduceM (Reduced b b')
- redReturn :: a -> ReduceM (Reduced a' a)
- fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a)
- fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a)
- primTrustMe :: TCM PrimitiveImpl
- getReflArgInfo :: ConHead -> TCM (Maybe ArgInfo)
- genPrimForce :: TCM Type -> (Term -> Arg Term -> Term) -> TCM PrimitiveImpl
- primForce :: TCM PrimitiveImpl
- primForceLemma :: TCM PrimitiveImpl
- mkPrimLevelZero :: TCM PrimitiveImpl
- mkPrimLevelSuc :: TCM PrimitiveImpl
- mkPrimLevelMax :: 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
- (-->) :: TCM Type -> TCM Type -> TCM Type
- (.-->) :: TCM Type -> TCM Type -> TCM Type
- (..-->) :: TCM Type -> TCM Type -> TCM Type
- garr :: (Relevance -> Relevance) -> TCM Type -> TCM Type -> TCM Type
- gpi :: ArgInfo -> String -> TCM Type -> TCM Type -> TCM Type
- hPi :: String -> TCM Type -> TCM Type -> TCM Type
- nPi :: String -> TCM Type -> TCM Type -> TCM Type
- varM :: Int -> TCM Term
- gApply :: Hiding -> TCM Term -> TCM Term -> TCM Term
- (<@>) :: TCM Term -> TCM Term -> TCM Term
- (<#>) :: TCM Term -> TCM Term -> TCM Term
- list :: TCM Term -> TCM Term
- io :: TCM Term -> TCM Term
- el :: TCM Term -> TCM Type
- tset :: TCM Type
- sSizeUniv :: Sort
- tSizeUniv :: TCM Type
- argN :: e -> Arg e
- domN :: e -> Dom e
- argH :: e -> Arg e
- domH :: e -> Dom e
- 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
Primitive functions
data PrimitiveImpl #
Instances
| Enum Nat # | |
| Eq Nat # | |
| Integral Nat # | |
| Num Nat # | |
| Ord Nat # | |
| Real Nat # | |
Defined in Agda.TypeChecking.Primitive Methods toRational :: Nat -> Rational # | |
| Show Nat # | |
| TermLike Nat # | |
| FromTerm Nat # | |
Defined in Agda.TypeChecking.Primitive Methods fromTerm :: TCM (FromTermFunction Nat) # | |
| ToTerm Nat # | |
| PrimTerm Nat # | |
Minimal complete definition
Minimal complete definition
Instances
| PrimTerm Bool # | |
| PrimTerm Char # | |
| PrimTerm Double # | |
| PrimTerm Integer # | |
| PrimTerm Word64 # | |
| PrimTerm Str # | |
| PrimTerm Fixity' # | |
| PrimTerm MetaId # | |
| PrimTerm QName # | |
| PrimTerm Type # | |
| PrimTerm Lvl # | |
| PrimTerm Nat # | |
| PrimTerm a => PrimTerm [a] # | |
Defined in Agda.TypeChecking.Primitive | |
| PrimTerm a => PrimTerm (IO a) # | |
| (PrimType a, PrimType b) => PrimTerm (a -> b) # | |
Defined in Agda.TypeChecking.Primitive | |
Minimal complete definition
Instances
| ToTerm Bool # | |
| ToTerm Char # | |
| ToTerm Double # | |
| ToTerm Integer # | |
| ToTerm Word64 # | |
| ToTerm Str # | |
| ToTerm Fixity' # | |
| ToTerm MetaId # | |
| ToTerm ArgInfo # | |
| ToTerm QName # | |
| ToTerm Fixity # | |
| ToTerm Associativity # | |
Defined in Agda.TypeChecking.Primitive | |
| ToTerm PrecedenceLevel # | |
Defined in Agda.TypeChecking.Primitive | |
| ToTerm Type # | |
| ToTerm Term # | |
| ToTerm Lvl # | |
| ToTerm Nat # | |
| ToTerm a => ToTerm [a] # | |
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) #
Minimal complete definition
Methods
fromTerm :: TCM (FromTermFunction a) #
Instances
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
fromReducedTerm :: (Term -> Maybe a) -> TCM (FromTermFunction a) #
fromLiteral :: (Literal -> Maybe a) -> TCM (FromTermFunction a) #
primTrustMe :: TCM PrimitiveImpl #
trustMe : {a : Level} {A : Set a} {x y : A} -> x ≡ ygetReflArgInfo :: 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.
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 #
Abbreviation: argN = .Arg defaultArgInfo
The actual primitive functions
lookupPrimitiveFunctionQ :: QName -> TCM (String, PrimitiveImpl) #