Agda.TypeChecking.Monad.Builtin

Documentation

data CoinductionKit

The coinductive primitives.

Constructors

CoinductionKit

Fields

• nameOfInf :: QName
• nameOfSharp :: QName
• nameOfFlat :: QName

class (Functor m, Applicative m, MonadFail m) => HasBuiltins m where

Methods

getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))

Instances

HasBuiltins ReduceM

Defined in Agda.TypeChecking.Reduce.Monad

Methods

getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun))

HasBuiltins m => HasBuiltins (MaybeT m)

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> MaybeT m (Maybe (Builtin PrimFun))

MonadIO m => HasBuiltins (TCMT m)

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun))

HasBuiltins m => HasBuiltins (NamesT m)

Defined in Agda.TypeChecking.Names

Methods

getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun))

HasBuiltins m => HasBuiltins (ExceptT e m)

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> ExceptT e m (Maybe (Builtin PrimFun))

HasBuiltins m => HasBuiltins (StateT s m)

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> StateT s m (Maybe (Builtin PrimFun))

litType :: Literal -> TCM Type

setBuiltinThings :: BuiltinThings PrimFun -> TCM ()

bindBuiltinName :: String -> Term -> TCM ()

bindPrimitive :: String -> PrimFun -> TCM ()

getBuiltin :: String -> TCM Term

getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)

getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)

getPrimitive :: String -> TCM PrimFun

getPrimitiveTerm :: String -> TCM Term

getPrimitiveTerm' :: HasBuiltins m => String -> m (Maybe Term)

getTerm' :: HasBuiltins m => String -> m (Maybe Term)

getName' :: HasBuiltins m => String -> m (Maybe QName)

getTerm :: HasBuiltins m => String -> String -> m Term

getTerm use name looks up name as a primitive or builtin, and throws an error otherwise. The use argument describes how the name is used for the sake of the error message.

constructorForm :: Term -> TCM Term

Rewrite a literal to constructor form if possible.

constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term

primInteger :: TCM Term

primIntegerPos :: TCM Term

primIntegerNegSuc :: TCM Term

primFloat :: TCM Term

primChar :: TCM Term

primString :: TCM Term

primBool :: TCM Term

primSigma :: TCM Term

primUnit :: TCM Term

primUnitUnit :: TCM Term

primTrue :: TCM Term

primFalse :: TCM Term

primList :: TCM Term

primNil :: TCM Term

primCons :: TCM Term

primIO :: TCM Term

primId :: TCM Term

primConId :: TCM Term

primIdElim :: TCM Term

primPath :: TCM Term

primPathP :: TCM Term

primInterval :: TCM Term

primIZero :: TCM Term

primIOne :: TCM Term

primIMin :: TCM Term

primIMax :: TCM Term

primINeg :: TCM Term

primPartial :: TCM Term

primPartialP :: TCM Term

primIsOne :: TCM Term

primItIsOne :: TCM Term

primTrans :: TCM Term

primHComp :: TCM Term

primEquiv :: TCM Term

primEquivFun :: TCM Term

primEquivProof :: TCM Term

primPathToEquiv :: TCM Term

primGlue :: TCM Term

prim_glue :: TCM Term

prim_unglue :: TCM Term

primFaceForall :: TCM Term

primIsOne1 :: TCM Term

primIsOne2 :: TCM Term

primIsOneEmpty :: TCM Term

primSub :: TCM Term

primSubIn :: TCM Term

primSubOut :: TCM Term

primNat :: TCM Term

primSuc :: TCM Term

primZero :: TCM Term

primNatPlus :: TCM Term

primNatMinus :: TCM Term

primNatTimes :: TCM Term

primNatDivSucAux :: TCM Term

primNatModSucAux :: TCM Term

primNatEquality :: TCM Term

primNatLess :: TCM Term

primWord64 :: TCM Term

primSizeUniv :: TCM Term

primSize :: TCM Term

primSizeLt :: TCM Term

primSizeSuc :: TCM Term

primSizeInf :: TCM Term

primSizeMax :: TCM Term

primInf :: TCM Term

primSharp :: TCM Term

primFlat :: TCM Term

primEquality :: TCM Term

primRefl :: TCM Term

primRewrite :: TCM Term

primLevel :: TCM Term

primLevelZero :: TCM Term

primLevelSuc :: TCM Term

primLevelMax :: TCM Term

primSetOmega :: TCM Term

primFromNat :: TCM Term

primFromNeg :: TCM Term

primFromString :: TCM Term

primQName :: TCM Term

primArg :: TCM Term

primArgArg :: TCM Term

primAbs :: TCM Term

primAbsAbs :: TCM Term

primAgdaSort :: TCM Term

primHiding :: TCM Term

primHidden :: TCM Term

primInstance :: TCM Term

primVisible :: TCM Term

primRelevance :: TCM Term

primRelevant :: TCM Term

primIrrelevant :: TCM Term

primAssoc :: TCM Term

primAssocLeft :: TCM Term

primAssocRight :: TCM Term

primAssocNon :: TCM Term

primPrecedence :: TCM Term

primPrecRelated :: TCM Term

primPrecUnrelated :: TCM Term

primFixity :: TCM Term

primFixityFixity :: TCM Term

primArgInfo :: TCM Term

primArgArgInfo :: TCM Term

primAgdaSortSet :: TCM Term

primAgdaSortLit :: TCM Term

primAgdaSortUnsupported :: TCM Term

primAgdaTerm :: TCM Term

primAgdaTermVar :: TCM Term

primAgdaTermLam :: TCM Term

primAgdaTermExtLam :: TCM Term

primAgdaTermDef :: TCM Term

primAgdaTermCon :: TCM Term

primAgdaTermPi :: TCM Term

primAgdaTermSort :: TCM Term

primAgdaTermLit :: TCM Term

primAgdaTermUnsupported :: TCM Term

primAgdaTermMeta :: TCM Term

primAgdaErrorPart :: TCM Term

primAgdaErrorPartString :: TCM Term

primAgdaErrorPartTerm :: TCM Term

primAgdaErrorPartName :: TCM Term

primAgdaLiteral :: TCM Term

primAgdaLitNat :: TCM Term

primAgdaLitWord64 :: TCM Term

primAgdaLitFloat :: TCM Term

primAgdaLitChar :: TCM Term

primAgdaLitString :: TCM Term

primAgdaLitQName :: TCM Term

primAgdaLitMeta :: TCM Term

primAgdaPattern :: TCM Term

primAgdaPatCon :: TCM Term

primAgdaPatVar :: TCM Term

primAgdaPatDot :: TCM Term

primAgdaPatLit :: TCM Term

primAgdaPatProj :: TCM Term

primAgdaPatAbsurd :: TCM Term

primAgdaClause :: TCM Term

primAgdaClauseClause :: TCM Term

primAgdaClauseAbsurd :: TCM Term

primAgdaDefinitionFunDef :: TCM Term

primAgdaDefinitionDataDef :: TCM Term

primAgdaDefinitionRecordDef :: TCM Term

primAgdaDefinitionDataConstructor :: TCM Term

primAgdaDefinitionPostulate :: TCM Term

primAgdaDefinitionPrimitive :: TCM Term

primAgdaDefinition :: TCM Term

primAgdaMeta :: TCM Term

primAgdaTCM :: TCM Term

primAgdaTCMReturn :: TCM Term

primAgdaTCMBind :: TCM Term

primAgdaTCMUnify :: TCM Term

primAgdaTCMTypeError :: TCM Term

primAgdaTCMInferType :: TCM Term

primAgdaTCMCheckType :: TCM Term

primAgdaTCMNormalise :: TCM Term

primAgdaTCMReduce :: TCM Term

primAgdaTCMCatchError :: TCM Term

primAgdaTCMGetContext :: TCM Term

primAgdaTCMExtendContext :: TCM Term

primAgdaTCMInContext :: TCM Term

primAgdaTCMFreshName :: TCM Term

primAgdaTCMDeclareDef :: TCM Term

primAgdaTCMDeclarePostulate :: TCM Term

primAgdaTCMDefineFun :: TCM Term

primAgdaTCMGetType :: TCM Term

primAgdaTCMGetDefinition :: TCM Term

primAgdaTCMQuoteTerm :: TCM Term

primAgdaTCMUnquoteTerm :: TCM Term

primAgdaTCMBlockOnMeta :: TCM Term

primAgdaTCMCommit :: TCM Term

primAgdaTCMIsMacro :: TCM Term

primAgdaTCMWithNormalisation :: TCM Term

primAgdaTCMDebugPrint :: TCM Term

primAgdaTCMNoConstraints :: TCM Term

primAgdaTCMRunSpeculative :: TCM Term

coinductionKit' :: TCM CoinductionKit

Tries to build a CoinductionKit.

coinductionKit :: TCM (Maybe CoinductionKit)

getPrimName :: Term -> QName

getBuiltinName' :: HasBuiltins m => String -> m (Maybe QName)

getPrimitiveName' :: HasBuiltins m => String -> m (Maybe QName)

isPrimitive :: HasBuiltins m => String -> QName -> m Bool

intervalView' :: HasBuiltins m => m (Term -> IntervalView)

intervalView :: HasBuiltins m => Term -> m IntervalView

intervalUnview :: HasBuiltins m => IntervalView -> m Term

intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)

pathView :: HasBuiltins m => Type -> m PathView

Check whether the type is actually an path (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

pathView' :: HasBuiltins m => m (Type -> PathView)

idViewAsPath :: HasBuiltins m => Type -> m PathView

Non dependent Path

boldPathView :: Type -> PathView

pathUnview :: PathView -> Type

Revert the PathView.

Postcondition: type is reduced.

primEqualityName :: TCM QName

Get the name of the equality type.

equalityView :: Type -> TCM EqualityView

Check whether the type is actually an equality (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

equalityUnview :: EqualityView -> Type

Revert the EqualityView.

Postcondition: type is reduced.

constrainedPrims :: [String]

Primitives with typechecking constrants.

getNameOfConstrained :: HasBuiltins m => String -> m (Maybe QName)

module Agda.Syntax.Builtin