Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.Rules.Term
Contents
Types
Telescopes
Literal
Terms
Let bindings
Synopsis
isType :: Expr -> Sort -> TCM Type
isType_ :: Expr -> TCM Type
forcePi :: MonadTCM tcm => Hiding -> String -> Type -> tcm (Type, Constraints)
checkTelescope :: Telescope -> Sort -> (Telescope -> TCM a) -> TCM a
checkTypedBindings :: TypedBindings -> Sort -> (Telescope -> TCM a) -> TCM a
checkTypedBinding :: Hiding -> Sort -> TypedBinding -> ([(String, Type)] -> TCM a) -> TCM a
checkTelescope_ :: Telescope -> (Telescope -> TCM a) -> TCM a
checkTypedBindings_ :: TypedBindings -> (Telescope -> TCM a) -> TCM a
checkTypedBinding_ :: Hiding -> TypedBinding -> ([(String, Type)] -> TCM a) -> TCM a
checkLiteral :: Literal -> Type -> TCM Term
litType :: Literal -> TCM Type
reduceCon :: MonadTCM tcm => QName -> tcm QName
checkArguments' :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> Expr -> (Args -> Type -> Constraints -> TCM Term) -> TCM Term
checkExpr :: Expr -> Type -> TCM Term
inferHead :: Head -> TCM (Args -> Term, Type)
inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)
checkConstructorApplication :: Expr -> Type -> QName -> [NamedArg Expr] -> TCM Term
checkHeadApplication :: Expr -> Type -> Head -> [NamedArg Expr] -> TCM Term
data ExpandHidden
= ExpandLast
| DontExpandLast
traceCallE :: Error e => (Maybe r -> Call) -> ErrorT e TCM r -> ErrorT e TCM r
checkArguments :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> ErrorT Type TCM (Args, Type, Constraints)
checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM (Args, Constraints)
inferExpr :: Expr -> TCM (Term, Type)
checkLetBindings :: [LetBinding] -> TCM a -> TCM a
checkLetBinding :: LetBinding -> TCM a -> TCM a
Types
isType :: Expr -> Sort -> TCM TypeSource
Check that an expression is a type.
isType_ :: Expr -> TCM TypeSource
Check that an expression is a type without knowing the sort.
forcePi :: MonadTCM tcm => Hiding -> String -> Type -> tcm (Type, Constraints)Source
Force a type to be a Pi. Instantiates if necessary. The Hiding is only used when instantiating a meta variable.
Telescopes
checkTelescope :: Telescope -> Sort -> (Telescope -> TCM a) -> TCM aSource
Type check a telescope. Binds the variables defined by the telescope.
checkTypedBindings :: TypedBindings -> Sort -> (Telescope -> TCM a) -> TCM aSource
Check a typed binding and extends the context with the bound variables. The telescope passed to the continuation is valid in the original context.
checkTypedBinding :: Hiding -> Sort -> TypedBinding -> ([(String, Type)] -> TCM a) -> TCM aSource
checkTelescope_ :: Telescope -> (Telescope -> TCM a) -> TCM aSource
Type check a telescope. Binds the variables defined by the telescope.
checkTypedBindings_ :: TypedBindings -> (Telescope -> TCM a) -> TCM aSource
Check a typed binding and extends the context with the bound variables. The telescope passed to the continuation is valid in the original context.
checkTypedBinding_ :: Hiding -> TypedBinding -> ([(String, Type)] -> TCM a) -> TCM aSource
Literal
checkLiteral :: Literal -> Type -> TCM TermSource
litType :: Literal -> TCM TypeSource
Terms
reduceCon :: MonadTCM tcm => QName -> tcm QNameSource
checkArguments' :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> Expr -> (Args -> Type -> Constraints -> TCM Term) -> TCM TermSource
checkArguments' exph r args t0 t e k tries checkArguments exph args t0 t. If it succeeds, it continues k with the returned results. If it fails, it registers a postponed typechecking problem and returns the resulting new meta variable.
checkExpr :: Expr -> Type -> TCM TermSource
Type check an expression.
inferHead :: Head -> TCM (Args -> Term, Type)Source
Infer the type of a head thing (variable, function symbol, or constructor)
inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)Source
checkConstructorApplication :: Expr -> Type -> QName -> [NamedArg Expr] -> TCM TermSource
Check the type of a constructor application. This is easier than a general application since the implicit arguments can be inserted without looking at the arguments to the constructor.
checkHeadApplication :: Expr -> Type -> Head -> [NamedArg Expr] -> TCM TermSource

checkHeadApplication e t hd args checks that e has type t, assuming that e has the form hd args. The corresponding type-checked term is returned.

If the head term hd is a coinductive constructor, then a top-level definition fresh tel = hd args (where the clause is delayed) is added, where tel corresponds to the current telescope. The returned term is fresh tel.

Precondition: The head hd has to be unambiguous, and there should not be any need to insert hidden lambdas.

data ExpandHidden Source
Constructors
ExpandLast
DontExpandLast
traceCallE :: Error e => (Maybe r -> Call) -> ErrorT e TCM r -> ErrorT e TCM rSource
checkArguments :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> ErrorT Type TCM (Args, Type, Constraints)Source
Check a list of arguments: checkArgs args t0 t1 checks that t0 = Delta -> t0' and args : Delta. Inserts hidden arguments to make this happen. Returns t0' and any constraints that have to be solve for everything to be well-formed. TODO: doesn't do proper blocking of terms
checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM (Args, Constraints)Source
Check that a list of arguments fits a telescope.
inferExpr :: Expr -> TCM (Term, Type)Source
Infer the type of an expression. Implemented by checking agains a meta variable.
Let bindings
checkLetBindings :: [LetBinding] -> TCM a -> TCM aSource
checkLetBinding :: LetBinding -> TCM a -> TCM aSource
Produced by Haddock version 2.6.1