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

Agda.TypeChecking.Rules.LHS

Synopsis

Documentation

checkLeftHandSide Source #

Arguments

:: Call

Trace, e.g. CheckLHS or CheckPattern.

-> Range

Range of the entire left hand side, for error reporting.

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

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

Instances details
InstantiateFull LHSResult Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

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

Bind as patterns

class IsFlexiblePattern a where Source #

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

Minimal complete definition

maybeFlexiblePattern

Methods

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

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

Instances

Instances details
IsFlexiblePattern Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

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

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

IsFlexiblePattern a => IsFlexiblePattern (Arg a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

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

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

IsFlexiblePattern (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

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

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

IsFlexiblePattern a => IsFlexiblePattern [a] Source #

Lists of flexible patterns are RecordFlex.

Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

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

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

IsFlexiblePattern a => IsFlexiblePattern (Named name a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS

Methods

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

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

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