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

Agda.TypeChecking.Rules.Term

Synopsis

# Types

Check that an expression is a type.

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

ptsRule :: (LensSort a, LensSort b) => a -> b -> TCM Sort Source #

Ensure that a (freshly created) function type does not inhabit SizeUniv. Precondition: When noFunctionsIntoSize t tBlame is called, we are in the context of tBlame in order to print it correctly. Not being in context of t should not matter, as we are only checking whether its sort reduces to SizeUniv.

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

# Telescopes

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

Type check a (module) telescope. Binds the variables defined by the telescope.

checkPiTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a Source #

Type check the telescope of a dependent function type. Binds the resurrected variables defined by the telescope. The returned telescope is unmodified (not resurrected).

data LamOrPi Source #

Flag to control resurrection on domains.

Constructors

 LamNotPi We are checking a module telescope. We pass into the type world to check the domain type. This resurrects the whole context. PiNotLam We are checking a telescope in a Pi-type. We stay in the term world, but add resurrected domains to the context to check the remaining domains and codomain of the Pi-type.

Instances

 Source # Methods(==) :: LamOrPi -> LamOrPi -> Bool #(/=) :: LamOrPi -> LamOrPi -> Bool # Source # MethodsshowList :: [LamOrPi] -> ShowS #

checkTelescope' :: LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a Source #

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

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

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

# Lambda abstractions

Type check a lambda expression.

Checking a lambda whose domain type has already been checked.

Arguments

 :: Hiding Expected hiding. -> Type Expected to be a function type. -> (MetaId -> Type -> TCM Term) Continuation on blocked type. -> (Type -> TCM Term) Continuation when expected hiding found. The continuation may assume that the Type is of the form (El _ (Pi _ _)). -> TCM Term Term with hidden lambda inserted.

Insert hidden lambda until the hiding info of the domain type matches the expected hiding info. Throws WrongHidingInLambda

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

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

Run a computation.

• If successful, return Nothing.
• If IlltypedPattern p a is thrown and type a is blocked on some meta x return Just x. Note that the returned meta might only exists in the state where the error was thrown, thus, be an invalid MetaId in the current state.
• If another error was thrown or the type a is not blocked, reraise the error.

# Records

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

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

# Terms

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

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.

Type check an expression.

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.

Unquote a TCM computation in a given hole.

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

# Meta variables

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

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

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.

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

checkArguments :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> ExceptT (Args, [NamedArg Expr], Type) TCM (Args, Type) 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 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.

Arguments

 :: ExpandHidden Eagerly insert trailing hidden arguments? -> Range Range of application. -> [NamedArg Expr] Arguments to check. -> Telescope Telescope to check arguments against. -> TCM (Args, Telescope) Checked arguments and remaining telescope if successful.

Check that a list of arguments fits a telescope. Inserts hidden arguments as necessary. Returns the type-checked arguments and the remaining telescope.

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

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

Check whether a de Bruijn index is bound by a module telescope.

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.