Agda.TypeChecking.Rules.LHS

Documentation

checkLeftHandSide

Arguments

:: forall a. 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?

• lhsIndexedSplit :: Bool

  have we split on an indexed type?

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 :: (HasConstInfo m, MonadDebug m) => a -> MaybeT m FlexibleVarKind

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => a -> m Bool

Instances

IsFlexiblePattern Pattern

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern -> MaybeT m FlexibleVarKind

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern -> m Bool

IsFlexiblePattern a => IsFlexiblePattern (Arg a)

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Arg a -> MaybeT m FlexibleVarKind

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Arg a -> m Bool

IsFlexiblePattern (Pattern' a)

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Pattern' a -> MaybeT m FlexibleVarKind

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Pattern' a -> m Bool

IsFlexiblePattern a => IsFlexiblePattern [a]

Lists of flexible patterns are RecordFlex.

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => [a] -> MaybeT m FlexibleVarKind

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => [a] -> m Bool

IsFlexiblePattern a => IsFlexiblePattern (Named name a)

Defined in Agda.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => Named name a -> MaybeT m FlexibleVarKind

isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => Named name a -> m Bool

data DataOrRecord

Constructors

IsData

IsRecord

Fields

• recordInduction :: Maybe Induction
• recordEtaEquality :: EtaEquality

Instances

Show DataOrRecord

Defined in Agda.TypeChecking.Rules.LHS

Methods

showsPrec :: Int -> DataOrRecord -> ShowS

show :: DataOrRecord -> String

showList :: [DataOrRecord] -> ShowS

checkSortOfSplitVar :: (MonadTCM m, PureTCM m, MonadError TCErr m, LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty) => DataOrRecord -> a -> Telescope -> Maybe ty -> m ()