Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Rules.LHS

Synopsis

checkLeftHandSide :: forall a. Call -> Maybe QName -> [NamedArg Pattern] -> Type -> Maybe Substitution -> [ProblemEq] -> (LHSResult -> TCM a) -> TCM a
data LHSResult = LHSResult {
- lhsParameters :: Nat
- lhsVarTele :: Telescope
- lhsPatterns :: [NamedArg DeBruijnPattern]
- lhsHasAbsurd :: Bool
- lhsBodyType :: Arg Type
- lhsPatSubst :: Substitution
- lhsAsBindings :: [AsBinding]
}
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
class IsFlexiblePattern a where
checkSortOfSplitVar :: (MonadTCM tcm, MonadError TCErr tcm, LensSort a) => a -> tcm ()

Documentation

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`.
-> 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).

Instances

InstantiateFull LHSResult #
Instance details 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 #
Instance details 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`.
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: [a] -> MaybeT TCM FlexibleVarKind # isFlexiblePattern :: [a] -> TCM Bool #
IsFlexiblePattern a => IsFlexiblePattern (Arg a) #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Arg a -> MaybeT TCM FlexibleVarKind # isFlexiblePattern :: Arg a -> TCM Bool #
IsFlexiblePattern (Pattern' a) #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Pattern' a -> MaybeT TCM FlexibleVarKind # isFlexiblePattern :: Pattern' a -> TCM Bool #
IsFlexiblePattern a => IsFlexiblePattern (Named name a) #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Named name a -> MaybeT TCM FlexibleVarKind # isFlexiblePattern :: Named name a -> TCM Bool #

checkSortOfSplitVar :: (MonadTCM tcm, MonadError TCErr tcm, LensSort a) => a -> tcm () #