Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Rules.LHS

Synopsis

checkLeftHandSide :: Call -> Range -> LetOrClause -> [NamedArg Pattern] -> Type -> IsWithFunction 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]
- lhsPartialSplit :: IntSet
- lhsIndexedSplit :: Bool
}
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
class IsFlexiblePattern a where
- maybeFlexiblePattern :: forall (m :: Type -> Type). HasConstInfo m => a -> MaybeT m FlexibleVarKind
- isFlexiblePattern :: HasConstInfo m => a -> m Bool
type DataOrRecord = DataOrRecord' InductionAndEta
checkSortOfSplitVar :: (MonadTCM m, PureTCM m, MonadError TCErr m, LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty) => DataOrRecord -> a -> Telescope -> Maybe ty -> m ()
data LetOrClause
- = LetLHS
- | ClauseLHS QName
buildLHSSubstitutions :: Context -> NAPs -> IsWithFunction (Arity, Substitution) -> (Substitution, Substitution)

Documentation

checkLeftHandSide Source #

Arguments

:: Call	Trace, e.g. `CheckLHS` or `CheckPattern`.
-> Range	`Range` of the entire left hand side, for error reporting.
-> LetOrClause	Are we checking a let-pattern or a function clause?
-> [NamedArg Pattern]	The patterns.
-> Type	The expected type `a = Γ → b`.
-> IsWithFunction 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, called in the context constructed from the `lhsVarTele` via `computeLHSContext`. All components of `LHSResult` live in this context, including `lhsVarTele`.
-> 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. Like the other components (e.g. lhsBodyType), this telescope lives in the ambient context. To print it, we need not drop Δ from the ambient context.
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

Instances details

InstantiateFull LHSResult Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods instantiateFull' :: LHSResult -> ReduceM LHSResult Source #

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 => a -> MaybeT m FlexibleVarKind Source #

isFlexiblePattern :: HasConstInfo 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 => Pattern -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo 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 => Arg a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo 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 => Pattern' a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo 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 => [a] -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo 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 => Named name a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo m => Named name a -> m Bool Source #

type DataOrRecord = DataOrRecord' InductionAndEta Source #

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

data LetOrClause Source #

Are we checking the LHS of a let-pattern binding or a function clause?

Constructors

LetLHS	Checking a pattern bound by a let.
ClauseLHS QName	Checking the LHS of a clause of the function with the given `QName`.

buildLHSSubstitutions :: Context -> NAPs -> IsWithFunction (Arity, Substitution) -> (Substitution, Substitution) Source #

Compute substitution from the out patterns ps