Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Rules.Def

Synopsis

Definitions by pattern matching

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

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

checkAlias :: Type -> ArgInfo -> DefInfo -> QName -> Expr -> Maybe 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)

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

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, Map Name LetBinding)

substitution (from with abstraction) that needs to be applied to module parameters, and let-bindings inherited from parent clause

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

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

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

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

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

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

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

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

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

data WithFunctionProblem Source #

Parameters for creating a with-function.

Constructors

NoWithFunction 
WithFunction 

Fields

Info that is needed after all clauses have been processed.

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

The LHS part of checkClause.

checkClause Source #

Arguments

:: Type

Type of function defined by this clause.

-> Maybe (Substitution, Map Name LetBinding)

Module parameter substitution arising from with-abstraction, and inherited let-bindings.

-> SpineClause

Clause.

-> TCM (Clause, ClausesPostChecks)

Type-checked clause

Type check a function clause.

getReflPattern :: TCM Pattern Source #

Generate the abstract pattern corresponding to Refl

checkRHS Source #

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

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) Source #

Invoked in empty context.

checkWhere Source #

Arguments

:: WhereDeclarations

Where-declarations to check.

-> TCM a

Continuation.

-> TCM a 

Type check a where clause.

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

Enter a new section during type-checking.

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

Set the current clause number.