Agda.TypeChecking.Rules.LHS

Documentation

checkLeftHandSide

Arguments

:: Call

Trace, e.g. CheckLHS or CheckPattern.

-> Maybe QName

The name of the definition we are checking.

-> [NamedArg Pattern]

The patterns.

-> Type

The expected type a = Γ → b.

-> Maybe Substitution

Module parameter substitution from with-abstraction.

-> [ProblemEq]

Patterns that have been stripped away by with-desugaring. ^ These should not contain any proper matches.

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

data LHSResult

Result of checking the LHS of a clause.

Constructors

LHSResult

Fields

• lhsParameters :: Nat

  The number of original module parameters. These are present in the the patterns.

• lhsVarTele :: Telescope

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

• lhsPatterns :: [NamedArg DeBruijnPattern]

  The patterns in internal syntax.

• lhsHasAbsurd :: Bool

  Whether the LHS has at least one absurd pattern.

• lhsBodyType :: Arg Type

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

• lhsPatSubst :: Substitution

  Substitution version of lhsPatterns, only up to the first projection pattern. Δ |- lhsPatSubst : Γ. Where Γ is the argument telescope of the function. This is used to update inherited dot patterns in with-function clauses.

• lhsAsBindings :: [AsBinding]

  As-bindings from the left-hand side. Return instead of bound since we want them in where's and right-hand sides, but not in with-clauses (Issue 2303).

• lhsPartialSplit :: IntSet

  have we done a partial split?

Instances

InstantiateFull LHSResult

Defined in Agda.TypeChecking.Rules.LHS

Methods

instantiateFull' :: LHSResult -> ReduceM LHSResult

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

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

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: Pattern -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Pattern -> TCM Bool

IsFlexiblePattern a => IsFlexiblePattern [a]

Lists of flexible patterns are RecordFlex.

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: [a] -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: [a] -> TCM Bool

IsFlexiblePattern a => IsFlexiblePattern (Arg a)

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: Arg a -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Arg a -> TCM Bool

IsFlexiblePattern (Pattern' a)

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: Pattern' a -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Pattern' a -> TCM Bool

IsFlexiblePattern a => IsFlexiblePattern (Named name a)

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: Named name a -> MaybeT TCM FlexibleVarKind

isFlexiblePattern :: Named name a -> TCM Bool

checkSortOfSplitVar :: (MonadTCM m, MonadReduce m, MonadError TCErr m, ReadTCState m, MonadDebug m, LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty) => DataOrRecord -> a -> Maybe ty -> m ()