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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rules.Term

Contents

- Types
- Telescopes
- Lambda abstractions
- Records
- Literal
- Terms
- Reflection
- Meta variables
- Let bindings

Synopsis

- isType :: Expr -> Sort -> TCM Type
- isType' :: Comparison -> Expr -> Sort -> TCM Type
- isType_ :: Expr -> TCM Type
- checkLevel :: NamedArg Expr -> TCM Level
- isTypeEqualTo :: Expr -> Type -> TCM Type
- leqType_ :: Type -> Type -> TCM ()
- checkGeneralizeTelescope :: Maybe ModuleName -> GeneralizeTelescope -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a
- checkTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a
- checkPiTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a
- data LamOrPi
  - = LamNotPi
  - | PiNotLam
- checkTelescope' :: LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
- checkDomain :: (LensLock a, LensModality a) => LamOrPi -> List1 a -> Expr -> TCM Type
- checkPiDomain :: (LensLock a, LensModality a) => List1 a -> Expr -> TCM Type
- checkTypedBindings :: LamOrPi -> TypedBinding -> (Telescope -> TCM a) -> TCM a
- addTypedPatterns :: List1 (NamedArg Binder) -> TCM a -> TCM a
- checkTacticAttribute :: LamOrPi -> Ranged Expr -> TCM Term
- checkPath :: NamedArg Binder -> Type -> Expr -> Type -> TCM Term
- checkLambda :: Comparison -> TypedBinding -> Expr -> Type -> TCM Term
- checkLambda' :: Comparison -> Range -> TypedBindingInfo -> List1 (NamedArg Binder) -> Type -> Expr -> Type -> TCM Term
- lambdaModalityCheck :: (LensAnnotation dom, LensModality dom) => dom -> ArgInfo -> TCM ArgInfo
- lambdaIrrelevanceCheck :: LensRelevance dom => dom -> ArgInfo -> TCM ArgInfo
- lambdaQuantityCheck :: LensQuantity dom => dom -> ArgInfo -> TCM ArgInfo
- lambdaAnnotationCheck :: LensAnnotation dom => dom -> ArgInfo -> TCM ArgInfo
- lambdaCohesionCheck :: LensCohesion dom => dom -> ArgInfo -> TCM ArgInfo
- lambdaPolarityCheck :: LensModalPolarity dom => dom -> ArgInfo -> TCM ArgInfo
- lambdaAddContext :: MonadAddContext m => Name -> ArgName -> Dom Type -> m a -> m a
- checkPostponedLambda :: Comparison -> Arg (List1 (WithHiding Name), Maybe Type) -> Expr -> Type -> TCM Term
- checkPostponedLambda0 :: Comparison -> Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term
- insertHiddenLambdas :: Hiding -> Type -> (Blocker -> Type -> TCM Term) -> (Type -> TCM Term) -> TCM Term
- checkAbsurdLambda :: Comparison -> ExprInfo -> Hiding -> Expr -> Type -> TCM Term
- makeAbsurdLambda :: Range -> Dom Type -> Abs Type -> TCM QName
- checkExtendedLambda :: Comparison -> ExprInfo -> DefInfo -> Erased -> QName -> List1 Clause -> Expr -> Type -> TCM Term
- catchIlltypedPatternBlockedOnMeta :: TCM a -> ((TCErr, Blocker) -> TCM a) -> TCM a
- expandModuleAssigns :: [Either Assign ModuleName] -> [Name] -> TCM Assigns
- checkRecordExpression :: Comparison -> RecordAssigns -> Expr -> Type -> TCM Term
- checkRecordUpdate :: Comparison -> KwRange -> ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term
- checkLiteral :: Literal -> Type -> TCM Term
- scopedExpr :: Expr -> TCM Expr
- checkExpr :: Expr -> Type -> TCM Term
- checkExpr' :: Comparison -> Expr -> Type -> TCM Term
- doQuoteTerm :: Comparison -> Term -> Type -> TCM Term
- unquoteM :: Expr -> Term -> Type -> TCM ()
- unquoteTactic :: Term -> Term -> Type -> TCM ()
- checkQuestionMark :: (Comparison -> Type -> TCM (MetaId, Term)) -> Comparison -> Type -> MetaInfo -> InteractionId -> TCM Term
- checkUnderscore :: MetaInfo -> Comparison -> Type -> TCM Term
- checkMeta :: MetaInfo -> (Comparison -> Type -> TCM (MetaId, Term)) -> Comparison -> Type -> TCM Term
- inferMeta :: MetaInfo -> (Comparison -> Type -> TCM (MetaId, Term)) -> TCM (Elims -> Term, Type)
- checkOrInferMeta :: MetaInfo -> (Comparison -> Type -> TCM (MetaId, Term)) -> Maybe (Comparison, Type) -> TCM (Term, Type)
- domainFree :: ArgInfo -> Binder' Name -> LamBinding
- checkKnownArguments :: [NamedArg Expr] -> Args -> Type -> TCM (Args, Type)
- checkKnownArgument :: NamedArg Expr -> Args -> Type -> TCM (Args, Type)
- checkNamedArg :: NamedArg Expr -> Type -> TCM Term
- inferExpr :: Expr -> TCM (Term, Type)
- inferExpr' :: ExpandHidden -> Expr -> TCM (Term, Type)
- defOrVar :: Expr -> Bool
- checkDontExpandLast :: Comparison -> Expr -> Type -> TCM Term
- isModuleFreeVar :: Int -> TCM Bool
- inferExprForWith :: Arg Expr -> TCM (Term, Type)
- checkLetBindings' :: Foldable t => t LetBinding -> TCM a -> TCM a
- checkLetBinding' :: LetBinding -> TCM a -> TCM a
- checkLetBinding :: LetBinding -> TCM a -> TCM a
- checkLetBindings :: Foldable t => t LetBinding -> TCM a -> TCM a

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

checkLevel :: NamedArg Expr -> TCM Level Source #

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.

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

# 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 Source # show :: LamOrPi -> String Source # showList :: [LamOrPi] -> ShowS Source #
Eq LamOrPi Source # |
Instance details Defined in Agda.TypeChecking.Rules.Term Methods (==) :: LamOrPi -> LamOrPi -> Bool Source # (/=) :: LamOrPi -> LamOrPi -> Bool Source #

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.

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

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

checkPath :: NamedArg Binder -> Type -> Expr -> Type -> TCM Term Source #

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

lambdaAnnotationCheck :: LensAnnotation dom => dom -> ArgInfo -> TCM ArgInfo Source #

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.

lambdaPolarityCheck :: LensModalPolarity dom => dom -> ArgInfo -> TCM ArgInfo Source #

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

lambdaAddContext :: MonadAddContext m => Name -> ArgName -> Dom Type -> m a -> m a Source #

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

Checking a lambda whose domain type has already been checked.

checkPostponedLambda0 :: Comparison -> Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term Source #

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`

makeAbsurdLambda :: Range -> Dom Type -> Abs Type -> TCM QName Source #

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

-> KwRange | Range of the `record` keyword.

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

checkLiteral :: Literal -> Type -> TCM Term Source #

# 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

doQuoteTerm :: Comparison -> Term -> Type -> TCM Term Source #

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.

inferExpr' :: ExpandHidden -> Expr -> TCM (Term, Type) Source #

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 #

checkLetBinding' :: LetBinding -> TCM a -> TCM a Source #

checkLetBinding :: LetBinding -> TCM a -> TCM a Source #

Version of checkLetBinding which traces the fact that we're checking each binding in the Call.

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