| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 -> (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
checkExpr :: Expr -> Type -> TCM Term
inferHead :: Head -> TCM (Args -> Term, Type)
inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)
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 Type | Source

Check that an expression is a type.

isType_ :: Expr -> TCM Type | Source

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 -> (Telescope -> TCM a) -> TCM a | Source

Type check a telescope. Binds the variables defined by the telescope.

checkTypedBindings :: TypedBindings -> (Telescope -> TCM a) -> TCM a | Source

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 a | Source

Literal

checkLiteral :: Literal -> Type -> TCM Term | Source

litType :: Literal -> TCM Type | Source

Terms

reduceCon :: MonadTCM tcm => QName -> tcm QName | Source

checkExpr :: Expr -> Type -> TCM Term | Source

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

checkHeadApplication :: Expr -> Type -> Head -> [NamedArg Expr] -> TCM Term | Source

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

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 a | Source

checkLetBinding :: LetBinding -> TCM a -> TCM a | Source

Produced by Haddock version 2.4.2