Agda.TypeChecking.Rules.Term

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

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

| 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

isType :: Expr -> Sort -> TCM Type

Check that an expression is a type.

isType_ :: Expr -> TCM Type

Check that an expression is a type without knowing the sort.

forcePi :: MonadTCM tcm => Hiding -> String -> Type -> tcm (Type, Constraints)

Force a type to be a Pi. Instantiates if necessary. The Hiding is only used when instantiating a meta variable.

checkTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a

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

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

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

checkLiteral :: Literal -> Type -> TCM Term

litType :: Literal -> TCM Type

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

checkExpr :: Expr -> Type -> TCM Term

Type check an expression.

inferHead :: Head -> TCM (Args -> Term, Type)

Infer the type of a head thing (variable, function symbol, or constructor)

inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)

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

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

Constructors

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)

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)

Check that a list of arguments fits a telescope.

inferExpr :: Expr -> TCM (Term, Type)

Infer the type of an expression. Implemented by checking agains a meta variable.

checkLetBindings :: [LetBinding] -> TCM a -> TCM a

checkLetBinding :: LetBinding -> TCM a -> TCM a

Produced by Haddock version 2.6.0