- isType :: Expr -> Sort -> TCM Type
- isType_ :: Expr -> TCM Type
- forcePi :: MonadTCM tcm => Hiding -> String -> Type -> tcm (Type, Constraints)
- checkTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a
- checkTypedBindings :: TypedBindings -> (Telescope -> TCM a) -> TCM a
- checkTypedBinding :: Hiding -> TypedBinding -> ([(String, Type)] -> TCM a) -> TCM a
- checkLiteral :: Literal -> Type -> TCM Term
- litType :: Literal -> TCM Type
- reduceCon :: MonadTCM tcm => QName -> tcm QName
- checkExpr :: Expr -> Type -> TCM Term
- inferHead :: Head -> TCM (Args -> Term, Type)
- inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)
- checkHeadApplication :: Expr -> Type -> Head -> [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, Constraints)
- checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM (Args, Constraints)
- inferExpr :: Expr -> TCM (Term, Type)
- checkLetBindings :: [LetBinding] -> TCM a -> TCM a
- checkLetBinding :: LetBinding -> TCM a -> TCM a
Types
forcePi :: MonadTCM tcm => Hiding -> String -> Type -> tcm (Type, Constraints)Source
Force a type to be a Pi. Instantiates if necessary. The Hiding
is only
used when instantiating a meta variable.
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.
checkTypedBinding :: Hiding -> TypedBinding -> ([(String, Type)] -> TCM a) -> TCM aSource
Literal
Terms
inferHead :: Head -> TCM (Args -> Term, Type)Source
Infer the type of a head thing (variable, function symbol, or constructor)
checkHeadApplication :: Expr -> Type -> Head -> [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, Constraints)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 t0'
and any constraints that have to be
solve for everything to be well-formed.
TODO: doesn't do proper blocking of terms
checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM (Args, Constraints)Source
Check that a list of arguments fits a telescope.
inferExpr :: Expr -> TCM (Term, Type)Source
Infer the type of an expression. Implemented by checking agains a meta variable.
Let bindings
checkLetBindings :: [LetBinding] -> TCM a -> TCM aSource
checkLetBinding :: LetBinding -> TCM a -> TCM aSource