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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Builtin

Synopsis

- data CoinductionKit = CoinductionKit {
  - nameOfInf :: QName
  - nameOfSharp :: QName
  - nameOfFlat :: QName
  }
- class (Functor m, Applicative m, MonadFail m) => HasBuiltins m where
  - getBuiltinThing :: String -> 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
- constructorForm :: Term -> TCM Term
- 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
- 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
- pathView' :: HasBuiltins m => m (Type -> PathView)
- idViewAsPath :: HasBuiltins m => Type -> m PathView
- boldPathView :: Type -> PathView
- pathUnview :: PathView -> Type
- primEqualityName :: TCM QName
- equalityView :: Type -> TCM EqualityView
- equalityUnview :: EqualityView -> Type
- constrainedPrims :: [String]
- getNameOfConstrained :: HasBuiltins m => String -> m (Maybe QName)
- module Agda.Syntax.Builtin

# Documentation

data CoinductionKit Source #

The coinductive primitives.

Constructors

CoinductionKit |

Fields

- nameOfInf :: QName
- nameOfSharp :: QName
- nameOfFlat :: QName

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

Methods

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

Instances

HasBuiltins ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Reduce.Monad Methods getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> MaybeT m (Maybe (Builtin PrimFun)) Source #
MonadIO m => HasBuiltins (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names Methods getBuiltinThing :: String -> NamesT m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (ExceptT e m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> ExceptT e m (Maybe (Builtin PrimFun)) Source #
HasBuiltins m => HasBuiltins (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Builtin Methods getBuiltinThing :: String -> StateT s m (Maybe (Builtin PrimFun)) Source #

litType :: Literal -> TCM Type Source #

setBuiltinThings :: BuiltinThings PrimFun -> TCM () Source #

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

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

getBuiltin :: String -> TCM Term Source #

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

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

getPrimitive :: String -> TCM PrimFun Source #

getPrimitiveTerm :: String -> TCM Term Source #

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

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

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

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

`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 Source #

Rewrite a literal to constructor form if possible.

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

primInteger :: TCM Term Source #

primIntegerPos :: TCM Term Source #

primIntegerNegSuc :: TCM Term Source #

primFloat :: TCM Term Source #

primChar :: TCM Term Source #

primString :: TCM Term Source #

primBool :: TCM Term Source #

primSigma :: TCM Term Source #

primUnit :: TCM Term Source #

primUnitUnit :: TCM Term Source #

primTrue :: TCM Term Source #

primFalse :: TCM Term Source #

primList :: TCM Term Source #

primNil :: TCM Term Source #

primCons :: TCM Term Source #

primIO :: TCM Term Source #

primId :: TCM Term Source #

primConId :: TCM Term Source #

primIdElim :: TCM Term Source #

primPath :: TCM Term Source #

primPathP :: TCM Term Source #

primInterval :: TCM Term Source #

primIZero :: TCM Term Source #

primIOne :: TCM Term Source #

primIMin :: TCM Term Source #

primIMax :: TCM Term Source #

primINeg :: TCM Term Source #

primPartial :: TCM Term Source #

primPartialP :: TCM Term Source #

primIsOne :: TCM Term Source #

primItIsOne :: TCM Term Source #

primTrans :: TCM Term Source #

primHComp :: TCM Term Source #

primEquiv :: TCM Term Source #

primEquivFun :: TCM Term Source #

primEquivProof :: TCM Term Source #

primPathToEquiv :: TCM Term Source #

primGlue :: TCM Term Source #

prim_glue :: TCM Term Source #

prim_unglue :: TCM Term Source #

primFaceForall :: TCM Term Source #

primIsOne1 :: TCM Term Source #

primIsOne2 :: TCM Term Source #

primIsOneEmpty :: TCM Term Source #

primSub :: TCM Term Source #

primSubIn :: TCM Term Source #

primSubOut :: TCM Term Source #

primNat :: TCM Term Source #

primSuc :: TCM Term Source #

primZero :: TCM Term Source #

primNatPlus :: TCM Term Source #

primNatMinus :: TCM Term Source #

primNatTimes :: TCM Term Source #

primNatDivSucAux :: TCM Term Source #

primNatModSucAux :: TCM Term Source #

primNatEquality :: TCM Term Source #

primNatLess :: TCM Term Source #

primWord64 :: TCM Term Source #

primSizeUniv :: TCM Term Source #

primSize :: TCM Term Source #

primSizeLt :: TCM Term Source #

primSizeSuc :: TCM Term Source #

primSizeInf :: TCM Term Source #

primSizeMax :: TCM Term Source #

primInf :: TCM Term Source #

primSharp :: TCM Term Source #

primFlat :: TCM Term Source #

primEquality :: TCM Term Source #

primRefl :: TCM Term Source #

primRewrite :: TCM Term Source #

primLevel :: TCM Term Source #

primLevelZero :: TCM Term Source #

primLevelSuc :: TCM Term Source #

primLevelMax :: TCM Term Source #

primSetOmega :: TCM Term Source #

primFromNat :: TCM Term Source #

primFromNeg :: TCM Term Source #

primFromString :: TCM Term Source #

primQName :: TCM Term Source #

primArg :: TCM Term Source #

primArgArg :: TCM Term Source #

primAbs :: TCM Term Source #

primAbsAbs :: TCM Term Source #

primAgdaSort :: TCM Term Source #

primHiding :: TCM Term Source #

primHidden :: TCM Term Source #

primInstance :: TCM Term Source #

primVisible :: TCM Term Source #

primRelevance :: TCM Term Source #

primRelevant :: TCM Term Source #

primIrrelevant :: TCM Term Source #

primAssoc :: TCM Term Source #

primAssocLeft :: TCM Term Source #

primAssocRight :: TCM Term Source #

primAssocNon :: TCM Term Source #

primPrecedence :: TCM Term Source #

primPrecRelated :: TCM Term Source #

primPrecUnrelated :: TCM Term Source #

primFixity :: TCM Term Source #

primFixityFixity :: TCM Term Source #

primArgInfo :: TCM Term Source #

primArgArgInfo :: TCM Term Source #

primAgdaSortSet :: TCM Term Source #

primAgdaSortLit :: TCM Term Source #

primAgdaSortUnsupported :: TCM Term Source #

primAgdaTerm :: TCM Term Source #

primAgdaTermVar :: TCM Term Source #

primAgdaTermLam :: TCM Term Source #

primAgdaTermExtLam :: TCM Term Source #

primAgdaTermDef :: TCM Term Source #

primAgdaTermCon :: TCM Term Source #

primAgdaTermPi :: TCM Term Source #

primAgdaTermSort :: TCM Term Source #

primAgdaTermLit :: TCM Term Source #

primAgdaTermUnsupported :: TCM Term Source #

primAgdaTermMeta :: TCM Term Source #

primAgdaErrorPart :: TCM Term Source #

primAgdaErrorPartString :: TCM Term Source #

primAgdaErrorPartTerm :: TCM Term Source #

primAgdaErrorPartName :: TCM Term Source #

primAgdaLiteral :: TCM Term Source #

primAgdaLitNat :: TCM Term Source #

primAgdaLitWord64 :: TCM Term Source #

primAgdaLitFloat :: TCM Term Source #

primAgdaLitChar :: TCM Term Source #

primAgdaLitString :: TCM Term Source #

primAgdaLitQName :: TCM Term Source #

primAgdaLitMeta :: TCM Term Source #

primAgdaPattern :: TCM Term Source #

primAgdaPatCon :: TCM Term Source #

primAgdaPatVar :: TCM Term Source #

primAgdaPatDot :: TCM Term Source #

primAgdaPatLit :: TCM Term Source #

primAgdaPatProj :: TCM Term Source #

primAgdaPatAbsurd :: TCM Term Source #

primAgdaClause :: TCM Term Source #

primAgdaClauseClause :: TCM Term Source #

primAgdaClauseAbsurd :: TCM Term Source #

primAgdaDefinitionFunDef :: TCM Term Source #

primAgdaDefinitionDataDef :: TCM Term Source #

primAgdaDefinitionRecordDef :: TCM Term Source #

primAgdaDefinitionDataConstructor :: TCM Term Source #

primAgdaDefinitionPostulate :: TCM Term Source #

primAgdaDefinitionPrimitive :: TCM Term Source #

primAgdaDefinition :: TCM Term Source #

primAgdaMeta :: TCM Term Source #

primAgdaTCM :: TCM Term Source #

primAgdaTCMReturn :: TCM Term Source #

primAgdaTCMBind :: TCM Term Source #

primAgdaTCMUnify :: TCM Term Source #

primAgdaTCMTypeError :: TCM Term Source #

primAgdaTCMInferType :: TCM Term Source #

primAgdaTCMCheckType :: TCM Term Source #

primAgdaTCMNormalise :: TCM Term Source #

primAgdaTCMReduce :: TCM Term Source #

primAgdaTCMCatchError :: TCM Term Source #

primAgdaTCMGetContext :: TCM Term Source #

primAgdaTCMExtendContext :: TCM Term Source #

primAgdaTCMInContext :: TCM Term Source #

primAgdaTCMFreshName :: TCM Term Source #

primAgdaTCMDeclareDef :: TCM Term Source #

primAgdaTCMDeclarePostulate :: TCM Term Source #

primAgdaTCMDefineFun :: TCM Term Source #

primAgdaTCMGetType :: TCM Term Source #

primAgdaTCMGetDefinition :: TCM Term Source #

primAgdaTCMQuoteTerm :: TCM Term Source #

primAgdaTCMUnquoteTerm :: TCM Term Source #

primAgdaTCMBlockOnMeta :: TCM Term Source #

primAgdaTCMCommit :: TCM Term Source #

primAgdaTCMIsMacro :: TCM Term Source #

primAgdaTCMWithNormalisation :: TCM Term Source #

primAgdaTCMDebugPrint :: TCM Term Source #

primAgdaTCMNoConstraints :: TCM Term Source #

primAgdaTCMRunSpeculative :: TCM Term Source #

coinductionKit' :: TCM CoinductionKit Source #

Tries to build a `CoinductionKit`.

coinductionKit :: TCM (Maybe CoinductionKit) Source #

getPrimName :: Term -> QName Source #

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

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

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

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

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

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

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

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

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

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

Non dependent Path

boldPathView :: Type -> PathView Source #

pathUnview :: PathView -> Type Source #

Revert the `PathView`.

Postcondition: type is reduced.

primEqualityName :: TCM QName Source #

Get the name of the equality type.

equalityView :: Type -> TCM EqualityView Source #

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

Precondition: type is reduced.

equalityUnview :: EqualityView -> Type Source #

Revert the `EqualityView`.

Postcondition: type is reduced.

constrainedPrims :: [String] Source #

Primitives with typechecking constrants.

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

module Agda.Syntax.Builtin