- isType :: Expr -> Sort -> TCM Type
- isType_ :: Expr -> TCM Type
- isTypeEqualTo :: Expr -> Type -> TCM Type
- leqType_ :: Type -> Type -> TCM ()
- checkTelescope_ :: Telescope -> (Telescope -> TCM a) -> TCM a
- checkTypedBindings_ :: TypedBindings -> (Telescope -> TCM a) -> TCM a
- data LamOrPi
- checkTypedBindings :: LamOrPi -> TypedBindings -> (Telescope -> TCM a) -> TCM a
- checkTypedBinding :: LamOrPi -> Hiding -> Relevance -> TypedBinding -> ([(String, Type)] -> TCM a) -> TCM a
- checkLambda :: Arg TypedBinding -> Expr -> Type -> TCM Term
- checkLiteral :: Literal -> Type -> TCM Term
- litType :: Literal -> TCM Type
- reduceCon :: QName -> TCM QName
- checkArguments' :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> Expr -> (Args -> Type -> TCM Term) -> TCM Term
- checkExpr :: Expr -> Type -> TCM Term
- checkMeta :: (Type -> TCM Term) -> Type -> MetaInfo -> TCM Term
- inferMeta :: (Type -> TCM Term) -> MetaInfo -> TCM (Args -> Term, Type)
- inferHead :: Expr -> TCM (Args -> Term, Type)
- inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)
- checkConstructorApplication :: Expr -> Type -> QName -> [NamedArg Expr] -> TCM Term
- checkHeadApplication :: Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
- data ExpandHidden
- traceCallE :: Error e => (Maybe r -> Call) -> ErrorT e TCM r -> ErrorT e TCM r
- checkArguments :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> ErrorT Type TCM (Args, Type)
- checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM Args
- inferExpr :: Expr -> TCM (Term, Type)
- checkTerm :: Term -> Type -> TCM Term
- checkLetBindings :: [LetBinding] -> TCM a -> TCM a
- checkLetBinding :: LetBinding -> TCM a -> TCM a
Types
isTypeEqualTo :: Expr -> Type -> TCM TypeSource
Check that an expression is a type which is equal to a given type.
Telescopes
checkTelescope_ :: Telescope -> (Telescope -> TCM a) -> TCM aSource
Type check a telescope. Binds the variables defined by the telescope.
checkTypedBindings_ :: TypedBindings -> (Telescope -> TCM a) -> TCM aSource
Check a typed binding and extends the context with the bound variables. The telescope passed to the continuation is valid in the original context.
checkTypedBindings :: LamOrPi -> TypedBindings -> (Telescope -> TCM a) -> TCM aSource
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 -> Hiding -> Relevance -> TypedBinding -> ([(String, Type)] -> TCM a) -> TCM aSource
checkLambda :: Arg TypedBinding -> Expr -> Type -> TCM TermSource
Type check a lambda expression.
Literal
Terms
checkArguments' :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> Expr -> (Args -> Type -> TCM Term) -> TCM TermSource
checkArguments' exph r args t0 t e 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
.
inferHead :: Expr -> TCM (Args -> Term, Type)Source
Infer the type of a head thing (variable, function symbol, or constructor)
checkConstructorApplication :: Expr -> Type -> QName -> [NamedArg Expr] -> TCM TermSource
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 TermSource
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 -> Range -> [NamedArg Expr] -> Type -> Type -> ErrorT 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.
TODO: doesn't do proper blocking of terms
checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM ArgsSource
Check that a list of arguments fits a telescope.
inferExpr :: Expr -> TCM (Term, Type)Source
Infer the type of an expression. Implemented by checking against a meta variable.
Let bindings
checkLetBindings :: [LetBinding] -> TCM a -> TCM aSource
checkLetBinding :: LetBinding -> TCM a -> TCM aSource