Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- isType :: Expr -> Sort -> TCM Type
- isType_ :: Expr -> TCM Type
- noFunctionsIntoSize :: Type -> Type -> TCM ()
- isTypeEqualTo :: Expr -> Type -> TCM Type
- leqType_ :: Type -> Type -> TCM ()
- checkTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a
- checkPiTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a
- data LamOrPi
- checkTelescope' :: LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
- checkTypedBindings :: LamOrPi -> TypedBindings -> (Telescope -> TCM a) -> TCM a
- checkTypedBinding :: LamOrPi -> ArgInfo -> TypedBinding -> (ListTel -> TCM a) -> TCM a
- checkLambda :: Arg TypedBinding -> Expr -> Type -> TCM Term
- lambdaIrrelevanceCheck :: LensRelevance dom => ArgInfo -> dom -> TCM ArgInfo
- lambdaAddContext :: Name -> ArgName -> Dom Type -> TCM a -> TCM a
- checkPostponedLambda :: Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term
- insertHiddenLambdas :: Hiding -> Type -> (MetaId -> Type -> TCM Term) -> (Type -> TCM Term) -> TCM Term
- checkAbsurdLambda :: ExprInfo -> Hiding -> Expr -> Type -> TCM Term
- checkExtendedLambda :: ExprInfo -> DefInfo -> QName -> [Clause] -> Expr -> Type -> TCM Term
- catchIlltypedPatternBlockedOnMeta :: TCM a -> ((TCErr, MetaId) -> TCM a) -> TCM a
- expandModuleAssigns :: [Either Assign ModuleName] -> [Name] -> TCM Assigns
- checkRecordExpression :: RecordAssigns -> Expr -> Type -> TCM Term
- checkRecordUpdate :: ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term
- checkLiteral :: Literal -> Type -> TCM Term
- scopedExpr :: Expr -> TCM Expr
- checkExpr :: Expr -> Type -> TCM Term
- quoteGoal :: Type -> TCM (Either [MetaId] Term)
- quoteContext :: TCM (Either [MetaId] Term)
- unquoteM :: Expr -> Term -> Type -> TCM Term -> TCM Term
- unquoteTactic :: Term -> Term -> Type -> TCM Term -> TCM Term
- checkQuestionMark :: (Type -> TCM (MetaId, Term)) -> Type -> MetaInfo -> InteractionId -> TCM Term
- checkUnderscore :: Type -> MetaInfo -> TCM Term
- checkMeta :: (Type -> TCM (MetaId, Term)) -> Type -> MetaInfo -> TCM Term
- inferMeta :: (Type -> TCM (MetaId, Term)) -> MetaInfo -> TCM (Elims -> Term, Type)
- checkOrInferMeta :: (Type -> TCM (MetaId, Term)) -> Maybe Type -> MetaInfo -> TCM (Term, Type)
- domainFree :: ArgInfo -> 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 :: Expr -> Type -> TCM Term
- isModuleFreeVar :: Int -> TCM Bool
- inferExprForWith :: Expr -> TCM (Term, Type)
- checkLetBindings :: [LetBinding] -> TCM a -> TCM a
- checkLetBinding :: LetBinding -> TCM a -> TCM a
Types
noFunctionsIntoSize :: Type -> Type -> TCM () 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
.
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 (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).
Flag to control resurrection on domains.
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. |
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.
checkTypedBinding :: LamOrPi -> ArgInfo -> TypedBinding -> (ListTel -> TCM a) -> TCM a Source #
Lambda abstractions
checkLambda :: Arg TypedBinding -> Expr -> Type -> TCM Term Source #
Type check a lambda expression.
lambdaIrrelevanceCheck :: LensRelevance dom => ArgInfo -> dom -> 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.
checkPostponedLambda :: Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term Source #
Checking a lambda whose domain type has already been checked.
:: 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 |
-> 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 :: 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
catchIlltypedPatternBlockedOnMeta :: TCM a -> ((TCErr, MetaId) -> TCM a) -> TCM a Source #
Run a computation.
- If successful, return Nothing.
- If
IlltypedPattern p a
,NotADatatype a
orCannotEliminateWithPattern p a
is thrown and typea
is blocked on some metax
, reset any changes to the state and returnJust x
. - If
SplitError (UnificationStuck c tel us vs _)
is thrown and the unification problemus =?= vs : tel
is blocked on some metax
returnJust x
. - 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.
If --sharing is enabled, we will never catch errors since it's not safe to roll back the state.
Records
expandModuleAssigns :: [Either Assign ModuleName] -> [Name] -> TCM Assigns Source #
checkRecordExpression :: RecordAssigns -> 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
scopedExpr :: Expr -> TCM Expr Source #
Remove top layers of scope info of expression and set the scope accordingly
in the TCState
.
Reflection
unquoteM :: Expr -> Term -> Type -> TCM Term -> TCM Term Source #
Unquote a TCM computation in a given hole.
Meta variables
checkQuestionMark :: (Type -> TCM (MetaId, Term)) -> Type -> MetaInfo -> InteractionId -> TCM Term Source #
Check an interaction point 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.
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.
:: [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.
:: 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.
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 #
checkDontExpandLast :: 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 :: 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 :: [LetBinding] -> TCM a -> TCM a Source #
checkLetBinding :: LetBinding -> TCM a -> TCM a Source #