Safe Haskell | None |
---|
- 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 -> ArgInfo -> TypedBinding -> (ListTel -> TCM a) -> TCM a
- checkLambda :: Arg TypedBinding -> Expr -> Type -> 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)
- 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 => (Maybe r -> Call) -> ErrorT e TCM r -> ErrorT e TCM r
- checkArguments :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> ErrorT (Args, [NamedArg Expr], Type) TCM (Args, Type)
- checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM Args
- inferExpr :: Expr -> TCM (Term, Type)
- defOrVar :: Expr -> Bool
- checkDontExpandLast :: Expr -> Type -> TCM Term
- inferExprForWith :: Expr -> TCM (Term, Type)
- checkTerm :: Term -> Type -> TCM Term
- checkLetBindings :: [LetBinding] -> TCM a -> TCM a
- checkLetBinding :: LetBinding -> TCM a -> TCM a
- class ConvColor a i where
- convColor :: a -> i
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 -> ArgInfo -> TypedBinding -> (ListTel -> TCM a) -> TCM aSource
Lambda abstractions
checkLambda :: Arg TypedBinding -> Expr -> Type -> TCM TermSource
Type check a lambda expression.
checkAbsurdLambda :: ExprInfo -> Hiding -> Expr -> Type -> TCM TermSource
checkAbsurdLambda i h e t
checks absurd lambda against type t
.
Precondition: e = AbsurdLam i h
checkExtendedLambda :: ExprInfo -> DefInfo -> QName -> [Clause] -> Expr -> Type -> TCM TermSource
checkExtendedLambda i di qname cs e t
check pattern matching lambda.
Precondition: e = ExtendedLam i di qname cs
Records
checkRecordExpression :: Assigns -> Expr -> Type -> TCM TermSource
checkRecordExpression fs e t
checks record construction against type t
.
Precondition e = Rec _ fs
.
checkRecordUpdate :: ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM TermSource
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 TermSource
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 TermSource
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 -> LamBindingSource
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 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 -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> ErrorT (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.
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. Except for neutrals, for them a polymorphic type is inferred.
checkDontExpandLast :: Expr -> Type -> TCM TermSource
Used to check aliases f = e
.
Switches off ExpandLast
for the checking of top-level application.
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 aSource
checkLetBinding :: LetBinding -> TCM a -> TCM aSource