Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rules.LHS

Synopsis

- checkLeftHandSide :: Call -> Range -> 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
  - lhsIndexedSplit :: Bool
  }
- bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
- class IsFlexiblePattern a where
  - maybeFlexiblePattern :: forall (m :: Type -> Type). (HasConstInfo m, MonadDebug m) => a -> MaybeT m FlexibleVarKind
  - isFlexiblePattern :: (HasConstInfo m, MonadDebug 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 ()

# 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 `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, 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 #

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 #