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

Safe Haskell | None

Agda.TypeChecking.Rules.Term

Contents

- Types
- Telescopes
- Literal
- Terms
- Let bindings

Synopsis

- 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
  - = LamNotPi
  - | PiNotLam
- 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

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.

isTypeEqualTo :: Expr -> Type -> TCM Type

Check that an expression is a type which is equal to a given type.

leqType_ :: Type -> Type -> TCM ()

# Telescopes

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.

data LamOrPi

Constructors

LamNotPi |
PiNotLam |

Instances

Eq LamOrPi |
Show LamOrPi |

checkTypedBindings :: LamOrPi -> 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.

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 a

checkLambda :: Arg TypedBinding -> Expr -> Type -> TCM Term

Type check a lambda expression.

# Literal

checkLiteral :: Literal -> Type -> TCM Term

# Terms

reduceCon :: QName -> TCM QName

checkArguments' :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg Expr] -> Type -> Type -> Expr -> (Args -> Type -> 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.

Checks `e := ((_ : t0) args) : t`.

unScope :: Expr -> Expr

checkExpr :: Expr -> Type -> TCM Term

Type check an expression.

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)

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 -> Expr -> [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.

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)

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 Args

Check that a list of arguments fits a telescope.

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

Infer the type of an expression. Implemented by checking against a meta variable. Except for neutrals, for them a polymorphic type is inferred.

defOrVar :: Expr -> Bool

inferOrCheck :: Expr -> Maybe Type -> TCM (Term, Type)

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

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.

checkTerm :: Term -> Type -> TCM Term

# Let bindings

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

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