Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Rules.Term

Synopsis

Types

isType :: Expr -> Sort -> TCM Type Source #

Check that an expression is a type.

isType' :: Comparison -> Expr -> Sort -> TCM Type Source #

Check that an expression is a type. * If c == CmpEq, the given sort must be the minimal sort. * If c == CmpLeq, the given sort may be any bigger sort.

isType_ :: Expr -> TCM Type Source #

Check that an expression is a type and infer its (minimal) sort.

isTypeEqualTo :: Expr -> Type -> TCM Type 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.

Currently UNUSED since SizeUniv is turned off (as of 2016).

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

Telescopes

checkGeneralizeTelescope Source #

Arguments

:: Maybe ModuleName

The module the telescope belongs to (if any).

-> GeneralizeTelescope

Telescope to check and add to the context for the continuation.

-> ([Maybe Name] -> Telescope -> TCM a)

Continuation living in the extended context.

-> TCM a 

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

Instances details
Show LamOrPi Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Term

Methods

showsPrec :: Int -> LamOrPi -> ShowS

show :: LamOrPi -> String

showList :: [LamOrPi] -> ShowS

Eq LamOrPi Source # 
Instance details

Defined in Agda.TypeChecking.Rules.Term

Methods

(==) :: LamOrPi -> LamOrPi -> Bool

(/=) :: LamOrPi -> LamOrPi -> Bool

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

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

checkDomain :: (LensLock a, LensModality a) => LamOrPi -> List1 a -> Expr -> TCM Type Source #

Check the domain of a function type. Used in checkTypedBindings and to typecheck A.Fun cases.

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 whether we check a typed lambda or a Pi. This flag is needed for irrelevance.

addTypedPatterns :: List1 (NamedArg Binder) -> TCM a -> TCM a Source #

After a typed binding has been checked, add the patterns it binds

checkTacticAttribute :: LamOrPi -> Ranged Expr -> TCM Term Source #

Check a tactic attribute. Should have type Term → TC ⊤.

Lambda abstractions

checkLambda :: Comparison -> TypedBinding -> Expr -> Type -> TCM Term Source #

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

checkLambda' Source #

Arguments

:: Comparison
cmp
-> Range

Range r of the typed binding

-> TypedBindingInfo

tac tactic/finiteness attribute of the typed binding

-> List1 (NamedArg Binder)

xps variables/patterns of the typed binding

-> Type

typ Type of the typed binding

-> Expr
body
-> Type
target
-> TCM Term 

lambdaModalityCheck :: (LensAnnotation dom, 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.

lambdaCohesionCheck :: LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo Source #

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

checkPostponedLambda :: Comparison -> Arg (List1 (WithHiding Name), Maybe Type) -> Expr -> Type -> TCM Term Source #

Checking a lambda whose domain type has already been checked.

insertHiddenLambdas Source #

Arguments

:: Hiding

Expected hiding.

-> Type

Expected to be a function type.

-> (Blocker -> 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 :: Comparison -> ExprInfo -> Hiding -> Expr -> Type -> TCM Term Source #

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

checkExtendedLambda :: Comparison -> ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr -> Type -> TCM Term Source #

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

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

Run a computation.

  • If successful, that's it, we are done.
  • If 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

expandModuleAssigns Source #

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.

checkRecordExpression Source #

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

Arguments

:: Comparison
cmp
-> ExprInfo
ei
-> Expr
recexpr
-> Assigns
fs
-> Expr
e = RecUpdate ei recexpr fs
-> Type

Need not be reduced.

-> TCM Term 
checkRecordUpdate cmp ei recexpr fs e t

Preconditions: e = RecUpdate ei recexpr fs and t is reduced.

Literal

Terms

scopedExpr :: Expr -> TCM Expr Source #

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

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

Type check an expression.

checkExpr' Source #

Arguments

:: Comparison 
-> Expr 
-> Type

Unreduced!

-> TCM Term 

Reflection

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

Arguments

:: (Comparison -> Type -> TCM (MetaId, Term)) 
-> Comparison 
-> Type

Not reduced!

-> MetaInfo 
-> InteractionId 
-> TCM Term 

Check an interaction point without arguments.

checkUnderscore :: MetaInfo -> Comparison -> Type -> TCM Term Source #

Check an underscore without arguments.

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

Type check a meta variable.

inferMeta :: MetaInfo -> (Comparison -> Type -> TCM (MetaId, Term)) -> 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 :: MetaInfo -> (Comparison -> Type -> TCM (MetaId, Term)) -> Maybe (Comparison, Type) -> 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.

domainFree :: ArgInfo -> Binder' Name -> LamBinding Source #

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

checkKnownArguments Source #

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.

checkKnownArgument Source #

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.

checkNamedArg :: NamedArg Expr -> Type -> TCM Term Source #

Check a single argument.

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.

defOrVar :: Expr -> Bool Source #

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

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

isModuleFreeVar :: Int -> TCM Bool Source #

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

inferExprForWith :: Arg 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

checkLetBindings :: Foldable t => t LetBinding -> TCM a -> TCM a Source #