Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Rules.Def

Contents

Definitions by pattern matching

Synopsis

Definitions by pattern matching

checkFunDef :: Delayed -> DefInfo -> QName -> [Clause] -> TCM () Source #

isAlias :: [Clause] -> Type -> Maybe (Expr, MetaId) Source #

A single clause without arguments and without type signature is an alias.

checkAlias :: Type -> ArgInfo -> Delayed -> DefInfo -> QName -> Expr -> TCM () Source #

Check a trivial definition of the form f = e

checkFunDef' Source #

Arguments

:: Type	the type we expect the function to have
-> ArgInfo	is it irrelevant (for instance)
-> Delayed	are the clauses delayed (not unfolded willy-nilly)
-> Maybe ExtLamInfo	does the definition come from an extended lambda (if so, we need to know some stuff about lambda-lifted args)
-> Maybe QName	is it a with function (if so, what's the name of the parent function)
-> DefInfo	range info
-> QName	the name of the function
-> [Clause]	the clauses to check
-> TCM ()

Type check a definition by pattern matching.

useTerPragma :: Definition -> TCM Definition Source #

Set funTerminates according to termination info in TCEnv, which comes from a possible termination pragma.

insertPatterns :: [Pattern] -> RHS -> RHS Source #

Insert some patterns in the in with-clauses LHS of the given RHS

data WithFunctionProblem Source #

Parameters for creating a with-function.

Constructors

NoWithFunction
WithFunction
Fields wfParentName :: QName Parent function name. wfName :: QName With function name. wfParentType :: Type Type of the parent function. wfBeforeTel :: Telescope Types of arguments to the with function before the with expressions (needed vars). wfAfterTel :: Telescope Types of arguments to the with function after the with expressions (unneeded vars). wfExprs :: [Term] With and rewrite expressions. wfExprTypes :: [EqualityView] Types of the with and rewrite expressions. wfRHSType :: Type Type of the right hand side. wfParentPats :: [NamedArg Pattern] Parent patterns. wfPermSplit :: Permutation Permutation resulting from splitting the telescope into needed and unneeded vars. wfPermParent :: Permutation Permutation reordering the variables in the parent pattern. wfPermFinal :: Permutation Final permutation (including permutation for the parent clause). wfClauses :: [Clause] The given clauses for the with function

mkBody :: Permutation -> Term -> ClauseBody Source #

Create a clause body from a term.

As we have type checked the term in the clause telescope, but the final body should have bindings in the order of the pattern variables, we need to apply the permutation to the checked term.

checkClause Source #

Arguments

:: Type	Type of function defined by this clause.
-> SpineClause	Clause.
-> TCM Clause	Type-checked clause.

Type check a function clause.

checkRHS Source #

Arguments

:: LHSInfo	Range of lhs.
-> QName	Name of function.
-> [NamedArg Pattern]	Patterns in lhs.
-> Type	Type of function.
-> LHSResult	Result of type-checking patterns
-> RHS	Rhs to check.
-> TCM (ClauseBody, WithFunctionProblem)

Type check the with and rewrite lhss and/or the rhs.

checkWithRHS Source #

Arguments

:: QName	Name of function.
-> QName	Name of the with-function.
-> Type	Type of function.
-> LHSResult	Result of type-checking patterns
-> [Term]	With-expressions.
-> [EqualityView]	Types of with-expressions.
-> [Clause]	With-clauses to check.
-> TCM (ClauseBody, WithFunctionProblem)

checkWithFunction :: WithFunctionProblem -> TCM () Source #

checkWhere Source #

Arguments

:: Type	Type of rhs.
-> [Declaration]	Where-declarations to check.
-> TCM a	Continuation.
-> TCM a

Type check a where clause.

containsAbsurdPattern :: Pattern -> Bool Source #

Check if a pattern contains an absurd pattern. For instance, suc ()