Agda.TypeChecking.Rules.LHS

Documentation

flexiblePatterns :: [NamedArg Pattern] -> TCM FlexibleVars

Compute the set of flexible patterns in a list of patterns. The result is the deBruijn indices of the flexible patterns.

class IsFlexiblePattern a where

A pattern is flexible if it is dotted or implicit, or a record pattern with only flexible subpatterns.

Minimal complete definition

maybeFlexiblePattern

Methods

maybeFlexiblePattern :: a -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: a -> TCM Bool

Instances

IsFlexiblePattern Pattern

IsFlexiblePattern a => IsFlexiblePattern [a]

Lists of flexible patterns are RecordFlex.

IsFlexiblePattern (Pattern' a)

IsFlexiblePattern a => IsFlexiblePattern (Named name a)

IsFlexiblePattern a => IsFlexiblePattern (Arg c a)

dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Dom Type] -> TCM [DotPatternInst]

Compute the dot pattern instantiations.

instantiatePattern

Arguments

:: Substitution

Partial substitution for the pattern variables, given in order of the clause telescope, (not in the order of occurrence in the patterns).

-> Permutation

Map from the pattern variables to the telescope variables.

-> [NamedArg Pattern]

Input patterns.

-> [NamedArg Pattern]

Output patterns, with some VarP replaced by DotP according to the Substitution.

In an internal pattern, replace some pattern variables by dot patterns, according to the given substitution.

instantiatePattern'

Arguments

:: Substitution

Partial substitution for the pattern variables, given in order of the clause telescope, (not in the order of occurrence in the patterns).

-> Permutation

Map from the pattern variables to the telescope variables.

-> [NamedArg Pattern]

Input patterns.

-> [NamedArg Pattern]

Output patterns, with some VarP replaced by DotP according to the Substitution.

In an internal pattern, replace some pattern variables by dot patterns, according to the given substitution.

isSolvedProblem :: Problem -> Bool

Check if a problem is solved. That is, if the patterns are all variables.

noShadowingOfConstructors

Arguments

:: Call

Trace, e.g., CheckPatternShadowing clause

-> Problem

-> TCM ()

For each user-defined pattern variable in the Problem, check that the corresponding data type (if any) does not contain a constructor of the same name (which is not in scope); this "shadowing" could indicate an error, and is not allowed.

Precondition: The problem has to be solved.

checkDotPattern :: DotPatternInst -> TCM ()

Check that a dot pattern matches it's instantiation.

bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a

Bind the variables in a left hand side and check that Hiding of the patterns matches the hiding info in the type.

Precondition: the patterns should all be VarP, WildP, or AbsurdP and the telescope should have the same size as the pattern list. There could also be ConPs resulting from eta expanded implicit record patterns.

bindAsPatterns :: [AsBinding] -> TCM a -> TCM a

Bind as patterns

data LHSResult

Result of checking the LHS of a clause.

Constructors

LHSResult

Fields

lhsVarTele :: Telescope

Δ : The types of the pattern variables, in internal dependency order. Corresponds to clauseTel.

lhsPatterns :: [NamedArg Pattern]

The patterns in internal syntax.

lhsBodyType :: Arg Type

The type of the body. Is bσ if Γ is defined. Irrelevant to indicate the rhs must be checked in irrelevant mode.

lhsPermutation :: Permutation

The permutation from pattern vars to Δ. Corresponds to clausePerm.

Instances

InstantiateFull LHSResult

checkLeftHandSide

Arguments

:: Call

Trace, e.g. CheckPatternShadowing clause

-> Maybe QName

The name of the definition we are checking.

-> [NamedArg Pattern]

The patterns.

-> Type

The expected type a = Γ → b.

-> (LHSResult -> TCM a)

Continuation.

-> TCM a

Check a LHS. Main function.

checkLeftHandSide a ps a ret checks that user patterns ps eliminate the type a of the defined function, and calls continuation ret if successful.

checkLHS

Arguments

:: Maybe QName

The name of the definition we are checking.

-> LHSState

The current state.

-> TCM LHSState

The final state after all splitting is completed

The loop (tail-recursive): split at a variable in the problem until problem is solved

noPatternMatchingOnCodata :: [NamedArg Pattern] -> TCM ()

Ensures that we are not performing pattern matching on codata.