| Safe Haskell | None |
|---|
Agda.TypeChecking.Rules.Term
Contents
- 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
- reduceCon :: QName -> TCM QName
- checkArguments' :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> Expr -> (Args -> Type -> TCM Term) -> TCM Term
- unScope :: Expr -> Expr
- checkExpr :: Expr -> Type -> TCM Term
- domainFree :: Hiding -> Relevance -> Name -> LamBinding
- 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
- traceCallE :: Error e => (Maybe r -> Call) -> ErrorT e TCM r -> ErrorT e TCM r
- checkArguments :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> ErrorT Type TCM (Args, Type)
- checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM Args
- inferExpr :: Expr -> TCM (Term, Type)
- defOrVar :: Expr -> Bool
- inferOrCheck :: Expr -> Maybe Type -> TCM (Term, Type)
- inferExprForWith :: 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 -> ExpandInstances -> 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.
domainFree :: Hiding -> Relevance -> Name -> LamBindingSource
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 -> ExpandInstances -> 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. Except for neutrals, for them a polymorphic type is inferred.
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