Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Rules.Term

Contents

- Types
- Telescopes
- Literal
- Terms
- Let bindings

Synopsis

- isType :: Expr -> Sort -> TCM Type
- isType_ :: Expr -> TCM Type
- forcePi :: MonadTCM tcm => Hiding -> String -> Type -> tcm (Type, Constraints)
- checkTelescope :: Telescope -> Sort -> (Telescope -> TCM a) -> TCM a
- checkTypedBindings :: TypedBindings -> Sort -> (Telescope -> TCM a) -> TCM a
- checkTypedBinding :: Hiding -> Sort -> TypedBinding -> ([(String, Type)] -> TCM a) -> TCM a
- 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
- checkArguments' :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> Expr -> (Args -> Type -> Constraints -> TCM Term) -> TCM Term
- checkExpr :: Expr -> Type -> TCM Term
- inferHead :: Head -> TCM (Args -> Term, Type)
- inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)
- checkConstructorApplication :: Expr -> Type -> QName -> [NamedArg Expr] -> TCM Term
- checkHeadApplication :: Expr -> Type -> Head -> [NamedArg Expr] -> TCM Term
- data ExpandHidden
  - = ExpandLast
  - | DontExpandLast
- 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

isType :: Expr -> Sort -> TCM Type

Check that an expression is a type.

isType_ :: Expr -> TCM Type

Check that an expression is a type without knowing the sort.

forcePi :: MonadTCM tcm => Hiding -> String -> Type -> tcm (Type, Constraints)

Force a type to be a Pi. Instantiates if necessary. The `Hiding` is only used when instantiating a meta variable.

# Telescopes

checkTelescope :: Telescope -> Sort -> (Telescope -> TCM a) -> TCM a

Type check a telescope. Binds the variables defined by the telescope.

checkTypedBindings :: TypedBindings -> Sort -> (Telescope -> TCM a) -> TCM a

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 -> Sort -> TypedBinding -> ([(String, Type)] -> TCM a) -> TCM a

checkTelescope_ :: Telescope -> (Telescope -> TCM a) -> TCM a

Type check a telescope. Binds the variables defined by the telescope.

checkTypedBindings_ :: TypedBindings -> (Telescope -> TCM a) -> TCM a

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 a

# Literal

checkLiteral :: Literal -> Type -> TCM Term

litType :: Literal -> TCM Type

# Terms

reduceCon :: MonadTCM tcm => QName -> tcm QName

checkArguments' :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> Expr -> (Args -> Type -> Constraints -> TCM Term) -> TCM Term

`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.

checkExpr :: Expr -> Type -> TCM Term

Type check an expression.

inferHead :: Head -> TCM (Args -> Term, Type)

Infer the type of a head thing (variable, function symbol, or constructor)

inferDef :: (QName -> Args -> Term) -> QName -> TCM (Term, Type)

checkConstructorApplication :: Expr -> Type -> QName -> [NamedArg Expr] -> TCM Term

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 -> Head -> [NamedArg Expr] -> TCM Term

`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.

data ExpandHidden

Constructors

ExpandLast |
DontExpandLast |

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)

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)

Check that a list of arguments fits a telescope.

inferExpr :: Expr -> TCM (Term, Type)

Infer the type of an expression. Implemented by checking agains a meta variable.

# Let bindings

checkLetBindings :: [LetBinding] -> TCM a -> TCM a

checkLetBinding :: LetBinding -> TCM a -> TCM a