Agda.TypeChecking.Rules.Def

Definitions by pattern matching

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

checkMacroType :: Type -> TCM ()

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

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

checkAlias :: Type -> ArgInfo -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM ()

Check a trivial definition of the form f = e

checkFunDef'

Arguments

:: Type

the type we expect the function to have

-> ArgInfo

is it irrelevant (for instance)

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

checkFunDefS

Arguments

:: Type

the type we expect the function to have

-> ArgInfo

is it irrelevant (for instance)

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

-> Maybe Substitution

substitution (from with abstraction) that needs to be applied to module parameters

-> [Clause]

the clauses to check

-> TCM ()

Type check a definition by pattern matching.

useTerPragma :: Definition -> TCM Definition

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

mapLHSCores :: (LHSCore -> LHSCore) -> RHS -> RHS

Modify all the LHSCore of the given RHS. (Used to insert patterns for rewrite or the inspect idiom)

insertNames :: [Arg (Maybe BindName)] -> RHS -> RHS

Insert some names into the with-clauses LHS of the given RHS. (Used for the inspect idiom)

insertInspects :: [Arg (Maybe BindName)] -> LHSCore -> LHSCore

insertPatterns :: [Arg Pattern] -> RHS -> RHS

Insert some with-patterns into the with-clauses LHS of the given RHS. (Used for rewrite)

insertPatternsLHSCore :: [Arg Pattern] -> LHSCore -> LHSCore

Insert with-patterns before the trailing with patterns. If there are none, append the with-patterns.

data WithFunctionProblem

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.

• wfParentTel :: Telescope

  Context of the parent patterns.

• 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 :: [Arg (Term, EqualityView)]

  With and rewrite expressions and their types.

• wfRHSType :: Type

  Type of the right hand side.

• wfParentPats :: [NamedArg DeBruijnPattern]

  Parent patterns.

• wfParentParams :: Nat

  Number of module parameters in 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 :: List1 Clause

  The given clauses for the with function

• wfCallSubst :: Substitution

  Subtsitution to generate call for the parent.

checkSystemCoverage :: QName -> [Int] -> Type -> [Clause] -> TCM System

Info that is needed after all clauses have been processed.

data ClausesPostChecks

Constructors

CPC

Fields

• cpcPartialSplits :: IntSet

  Which argument indexes have a partial split.

Instances

Monoid ClausesPostChecks

Defined in Agda.TypeChecking.Rules.Def

Methods

mempty :: ClausesPostChecks

mappend :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks

mconcat :: [ClausesPostChecks] -> ClausesPostChecks

Semigroup ClausesPostChecks

Defined in Agda.TypeChecking.Rules.Def

Methods

(<>) :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks

sconcat :: NonEmpty ClausesPostChecks -> ClausesPostChecks

stimes :: Integral b => b -> ClausesPostChecks -> ClausesPostChecks

checkClauseLHS :: Type -> Maybe Substitution -> SpineClause -> (LHSResult -> TCM a) -> TCM a

The LHS part of checkClause.

checkClause

Arguments

:: Type

Type of function defined by this clause.

-> Maybe Substitution

Module parameter substitution arising from with-abstraction.

-> SpineClause

Clause.

-> TCM (Clause, ClausesPostChecks)

Type-checked clause

Type check a function clause.

getReflPattern :: TCM Pattern

Generate the abstract pattern corresponding to Refl

checkRHS

Arguments

:: LHSInfo

Range of lhs.

-> QName

Name of function.

-> [NamedArg Pattern]

Patterns in lhs.

-> Type

Top-level type of function.

-> LHSResult

Result of type-checking patterns

-> RHS

Rhs to check.

-> TCM (Maybe Term, WithFunctionProblem)

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

checkWithRHS

Arguments

:: QName

Name of function.

-> QName

Name of the with-function.

-> Type

Type of function.

-> LHSResult

Result of type-checking patterns

-> [Arg (Term, EqualityView)]

Expressions and types of with-expressions.

-> List1 Clause

With-clauses to check.

-> TCM (Maybe Term, WithFunctionProblem)

checkWithFunction :: [Name] -> WithFunctionProblem -> TCM (Maybe Term)

Invoked in empty context.

checkWhere

Arguments

:: WhereDeclarations

Where-declarations to check.

-> TCM a

Continuation.

-> TCM a

Type check a where clause.

newSection :: Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a

Enter a new section during type-checking.

atClause :: QName -> Int -> Type -> Maybe Substitution -> SpineClause -> TCM a -> TCM a

Set the current clause number.