Safe Haskell | None |
---|---|
Language | Haskell98 |
- isType :: Expr -> Sort -> TCM Type
- isType_ :: Expr -> TCM Type
- ptsRule :: (LensSort a, LensSort b) => a -> b -> TCM Sort
- 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
- 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
- checkRecordExpression :: Assigns -> Expr -> Type -> TCM Term
- checkRecordUpdate :: ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term
- checkLiteral :: Literal -> Type -> TCM Term
- checkArguments' :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> (Args -> Type -> TCM Term) -> TCM Term
- checkExpr :: Expr -> Type -> TCM Term
- checkApplication :: Expr -> Args -> Expr -> Type -> TCM Term
- domainFree :: ArgInfo -> Name -> LamBinding
- checkMeta :: (Type -> TCM Term) -> Type -> MetaInfo -> TCM Term
- inferMeta :: (Type -> TCM Term) -> MetaInfo -> TCM (Args -> Term, Type)
- checkOrInferMeta :: (Type -> TCM Term) -> Maybe Type -> MetaInfo -> TCM (Term, Type)
- inferHeadDef :: QName -> TCM (Args -> Term, Type)
- inferHead :: Expr -> TCM (Args -> Term, Type)
- inferDef :: (QName -> Args -> TCM Term) -> QName -> TCM (Term, Type)
- checkConstructorApplication :: Expr -> Type -> ConHead -> [NamedArg Expr] -> TCM Term
- checkHeadApplication :: Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
- traceCallE :: Error e => Call -> ExceptT e TCM r -> ExceptT e TCM r
- checkArguments :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> ExceptT (Args, [NamedArg Expr], Type) TCM (Args, Type)
- checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM (Args, Telescope)
- 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
- class ConvColor a i where
- convColor :: a -> i
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.
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
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
.
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.
checkArguments :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> ExceptT (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.
:: ExpandHidden | Eagerly insert trailing hidden arguments? |
-> Range | Range of application. |
-> [NamedArg Expr] | Arguments to check. |
-> Telescope | Telescope to check arguments against. |
-> TCM (Args, Telescope) | Checked arguments and remaining telescope if successful. |
Check that a list of arguments fits a telescope. Inserts hidden arguments as necessary. Returns the type-checked arguments and the remaining 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.
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