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]
- lhsPartialSplit :: IntSet
}
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
class IsFlexiblePattern a where
- maybeFlexiblePattern :: (HasConstInfo m, MonadDebug m) => a -> MaybeT m FlexibleVarKind
- isFlexiblePattern :: (HasConstInfo m, MonadDebug m) => a -> m Bool
data DataOrRecord
- = IsData
- | IsRecord {
  - recordInduction :: Maybe Induction
  - recordEtaEquality :: EtaEquality
  }
checkSortOfSplitVar :: (MonadTCM m, PureTCM m, MonadError TCErr m, LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty) => DataOrRecord -> a -> Telescope -> Maybe ty -> m ()

Documentation

checkLeftHandSide Source #

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

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 :: (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 [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 (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 (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 #

data DataOrRecord Source #

Constructors

IsData
IsRecord
Fields recordInduction :: Maybe Induction recordEtaEquality :: EtaEquality

Instances

Instances details

Show DataOrRecord Source #
Instance details 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 () Source #