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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Rules.Term

Contents

Synopsis

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.

isTypeEqualTo :: Expr -> Type -> TCM Type Source

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

data LamOrPi Source

Constructors

LamNotPi 
PiNotLam 

Instances

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

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

Type check a lambda expression.

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

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

Records

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

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

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

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

Literal

Terms

checkArguments' :: ExpandHidden -> ExpandInstances -> 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.

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

Type check an expression.

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

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 Source

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.

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

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

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

checkArguments :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> ErrorT (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.

checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM Args 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 against a meta variable. Except for neutrals, for them a polymorphic type is inferred.

checkDontExpandLast :: Expr -> Type -> TCM Term Source

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

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

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

class ConvColor a i where Source

Methods

convColor :: a -> i Source

Instances