ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Rules.LHS

2 types
1 class
3 values

PackageAgda-2.7.0.1
Exports6
LanguageHaskell2010
LicenceMIT
SourceLHS.hs

valuecheckLeftHandSide

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

datadata LHSResult

Result of checking the LHS of a clause.

Constructors

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

Instances1InstantiateFull

InstantiateFull LHSResultDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS

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

Bind as patterns

classclass IsFlexiblePattern a where

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

Methods

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

Instances5IsFlexiblePattern

IsFlexiblePattern PatternDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS
IsFlexiblePattern (Pattern' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS
IsFlexiblePattern a => IsFlexiblePattern (Arg a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS
IsFlexiblePattern a => IsFlexiblePattern [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS
Lists of flexible patterns are RecordFlex.
IsFlexiblePattern a => IsFlexiblePattern (Named name a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS

typetype DataOrRecord = DataOrRecord' InductionAndEta

valuecheckSortOfSplitVar

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