Agda-2.6.0.1: 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.

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 # Instance detailsDefined in Agda.TypeChecking.Rules.Term Methods(==) :: LamOrPi -> LamOrPi -> Bool #(/=) :: LamOrPi -> LamOrPi -> Bool # Source # Instance detailsDefined in Agda.TypeChecking.Rules.Term 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 -> TypedBinding -> (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.

ifPath :: Type -> TCM a -> TCM a -> TCM a Source #

# Lambda abstractions

Type check a lambda expression. "checkLambda bs e ty" means ( bs -> e) : ty

lambdaModalityCheck :: LensModality dom => dom -> ArgInfo -> TCM ArgInfo Source #

Check that modality info in lambda is compatible with modality coming from the function type. If lambda has no user-given modality, copy that of function type.

lambdaIrrelevanceCheck :: LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo Source #

Check that irrelevance info in lambda is compatible with irrelevance coming from the function type. If lambda has no user-given relevance, copy that of function type.

lambdaQuantityCheck :: LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo Source #

Check that quantity info in lambda is compatible with quantity coming from the function type. If lambda has no user-given quantity, copy that of function type.

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 :: Comparison -> 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

catchIlltypedPatternBlockedOnMeta :: TCM a -> ((TCErr, MetaId) -> TCM a) -> TCM a Source #

Run a computation.

• If successful, that's it, we are done.
• If IlltypedPattern p a, NotADatatype a or CannotEliminateWithPattern p a is thrown and type a is blocked on some meta x, reset any changes to the state and pass (the error and) x to the handler.
• If SplitError (UnificationStuck c tel us vs _) is thrown and the unification problem us =?= vs : tel is blocked on some meta x pass x to the handler.
• If another error was thrown or the type a is not blocked, reraise the error.

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.

# Records

Arguments

 :: [Either Assign ModuleName] Modules and field assignments. -> [Name] Names of fields of the record type. -> TCM Assigns Completed field assignments from modules.

Picks up record field assignments from modules that export a definition that has the same name as the missing field.

Arguments

 :: Comparison How do we related the inferred type of the record expression to the expected type? Subtype or equal type? -> RecordAssigns mfs: modules and field assignments. -> Expr Must be A.Rec _ mfs. -> Type Expected type of record expression. -> TCM Term Record value in internal syntax.

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

Remove top layers of scope info of expression and set the scope accordingly in the TCState.

Type check an expression.

# Reflection

Checking quoteGoal (deprecated)

Checking quoteContext (deprecated)

unquoteM :: Expr -> Term -> Type -> TCM () Source #

Unquote a TCM computation in a given hole.

unquoteTactic :: Term -> Term -> Type -> TCM () Source #

Run a tactic tac : Term → TC ⊤ in a hole (second argument) of the type given by the third argument. Runs the continuation if successful.

# Meta variables

checkQuestionMark :: (Type -> TCM (MetaId, Term)) -> Type -> MetaInfo -> InteractionId -> TCM Term Source #

Check an interaction point without arguments.

Check an underscore without arguments.

checkMeta :: (Type -> TCM (MetaId, Term)) -> Type -> MetaInfo -> TCM Term Source #

Type check a meta variable.

inferMeta :: (Type -> TCM (MetaId, Term)) -> MetaInfo -> TCM (Elims -> Term, Type) Source #

Infer the type of a meta variable. If it is a new one, we create a new meta for its type.

checkOrInferMeta :: (Type -> TCM (MetaId, 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.

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

Arguments

 :: [NamedArg Expr] User-supplied arguments (hidden ones may be missing). -> Args Inferred arguments (including hidden ones). -> Type Type of the head (must be Pi-type with enough domains). -> TCM (Args, Type) Remaining inferred arguments, remaining type.

Check arguments whose value we already know.

This function can be used to check user-supplied parameters we have already computed by inference.

Precondition: The type t of the head has enough domains.

Arguments

 :: NamedArg Expr User-supplied argument. -> Args Inferred arguments (including hidden ones). -> Type Type of the head (must be Pi-type with enough domains). -> TCM (Args, Type) Remaining inferred arguments, remaining type.

Check an argument whose value we already know.

Check a single argument.

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.