Agda.TypeChecking.Rules.Term

Types

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.

isTypeEqualTo :: Expr -> Type -> TCM Type

Check that an expression is a type which is equal to a given type.

leqType_ :: Type -> Type -> TCM ()

Telescopes

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.

data LamOrPi

Constructors

LamNotPi

PiNotLam

Instances

Eq LamOrPi

Show LamOrPi

checkTypedBindings :: LamOrPi -> 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.

Parametrized by a flag wether we check a typed lambda or a Pi. This flag is needed for irrelevance.

checkTypedBinding :: LamOrPi -> ArgInfo -> TypedBinding -> (ListTel -> TCM a) -> TCM a

Lambda abstractions

checkLambda :: Arg TypedBinding -> Expr -> Type -> TCM Term

Type check a lambda expression.

checkAbsurdLambda :: ExprInfo -> Hiding -> Expr -> Type -> TCM Term

checkAbsurdLambda i h e t checks absurd lambda against type t. Precondition: e = AbsurdLam i h

checkExtendedLambda :: ExprInfo -> DefInfo -> QName -> [Clause] -> Expr -> Type -> TCM Term

checkExtendedLambda i di qname cs e t check pattern matching lambda. Precondition: e = ExtendedLam i di qname cs

Records

checkRecordExpression :: Assigns -> Expr -> Type -> TCM Term

checkRecordExpression fs e t checks record construction against type t. Precondition e = Rec _ fs.

checkRecordUpdate :: ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term

checkRecordUpdate ei recexpr fs e t Precondition e = RecUpdate ei recexpr fs.

Literal

checkLiteral :: Literal -> Type -> TCM Term

Terms

checkArguments' :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> (Args -> Type -> TCM Term) -> TCM Term

checkArguments' exph r args t0 t 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.

Checks e := ((_ : t0) args) : t.

checkExpr :: Expr -> Type -> TCM Term

Type check an expression.

checkApplication :: Expr -> Args -> Expr -> Type -> TCM Term

checkApplication hd args e t checks an application. Precondition: Application hs args = appView e

checkApplication disambiguates constructors (and continues to checkConstructorApplication) and resolves pattern synonyms.

domainFree :: ArgInfo -> Name -> LamBinding

Turn a domain-free binding (e.g. lambda) into a domain-full one, by inserting an underscore for the missing type.

Meta variables

checkMeta :: (Type -> TCM Term) -> Type -> MetaInfo -> TCM Term

inferMeta :: (Type -> TCM Term) -> MetaInfo -> TCM (Args -> Term, Type)

checkOrInferMeta :: (Type -> TCM Term) -> Maybe Type -> MetaInfo -> TCM (Term, Type)

Type check a meta variable. If its type is not given, we return its type, or a fresh one, if it is a new meta. If its type is given, we check that the meta has this type, and we return the same type.

Applications

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

Infer the type of a head thing (variable, function symbol, or constructor). We return a function that applies the head to arguments. This is because in case of a constructor we want to drop the parameters.

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

checkConstructorApplication :: Expr -> Type -> ConHead -> [NamedArg Expr] -> TCM Term

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 -> Expr -> [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.

traceCallE :: Error e => (Maybe r -> Call) -> ErrorT e TCM r -> ErrorT e TCM r

checkArguments :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> ErrorT (Args, [NamedArg Expr], Type) TCM (Args, Type)

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 the evaluated arguments vs, the remaining type t0' (which should be a subtype of t1) and any constraints cs that have to be solved for everything to be well-formed.

checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM Args

Check that a list of arguments fits a telescope.

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

Infer the type of an expression. Implemented by checking against a meta variable. Except for neutrals, for them a polymorphic type is inferred.

defOrVar :: Expr -> Bool

checkDontExpandLast :: Expr -> Type -> TCM Term

Used to check aliases f = e. Switches off ExpandLast for the checking of top-level application.

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

Infer the type of an expression, and if it is of the form {tel} -> D vs for some datatype D then insert the hidden arguments. Otherwise, leave the type polymorphic.

Let bindings

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

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

class ConvColor a i where

Methods

convColor :: a -> i

Instances

ConvColor ArgInfo ArgInfo

ConvColor a i => ConvColor [a] [i]

ConvColor (Dom e) (Dom e)

ConvColor (Arg e) (Arg e)