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

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Rules.Def

Contents

Synopsis

Definitions by pattern matching

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

wfExprTypes :: [Type]

Types of the with 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.

checkWhere Source

Arguments

:: Type

Type of rhs.

-> [Declaration]

Where-declarations to check.

-> TCM a

Continutation.

-> TCM a 

Type check a where clause.

containsAbsurdPattern :: Pattern -> Bool Source

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