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

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 :: [Int]
  }
- bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
- class IsFlexiblePattern a where
  - maybeFlexiblePattern :: a -> MaybeT TCM FlexibleVarKind
  - isFlexiblePattern :: a -> TCM Bool
- checkSortOfSplitVar :: (MonadTCM tcm, MonadReduce tcm, MonadError TCErr tcm, LensSort a) => DataOrRecord -> a -> Maybe (Arg Type) -> tcm ()

# Documentation

checkLeftHandSide Source #

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 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 :: [Int]

  have we done a partial split?

Instances

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 :: a -> MaybeT TCM FlexibleVarKind Source #

isFlexiblePattern :: a -> TCM Bool Source #

Instances

IsFlexiblePattern Pattern Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Pattern -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Pattern -> TCM Bool Source #
IsFlexiblePattern a => IsFlexiblePattern [a] Source # | Lists of flexible patterns are `RecordFlex`.
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: [a] -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: [a] -> TCM Bool Source #
IsFlexiblePattern a => IsFlexiblePattern (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Arg a -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Arg a -> TCM Bool Source #
IsFlexiblePattern (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Pattern' a -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Pattern' a -> TCM Bool Source #
IsFlexiblePattern a => IsFlexiblePattern (Named name a) Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: Named name a -> MaybeT TCM FlexibleVarKind Source # isFlexiblePattern :: Named name a -> TCM Bool Source #

checkSortOfSplitVar :: (MonadTCM tcm, MonadReduce tcm, MonadError TCErr tcm, LensSort a) => DataOrRecord -> a -> Maybe (Arg Type) -> tcm () Source #