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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Patterns.Match

Description

Pattern matcher used in the reducer for clauses that have not been compiled to case trees yet.

Synopsis

- data Match a
  - = Yes Simplification (IntMap (Arg a))
  - | No
  - | DontKnow OnlyLazy (Blocked ())
- matchedArgs :: Empty -> Int -> IntMap (Arg a) -> [Arg a]
- matchedArgs' :: Int -> IntMap (Arg a) -> [Maybe (Arg a)]
- buildSubstitution :: DeBruijn a => Impossible -> Int -> IntMap (Arg a) -> Substitution' a
- data OnlyLazy
  - = OnlyLazy
  - | NonLazy
- foldMatch :: forall m p v. (IsProjP p, MonadMatch m) => (p -> v -> m (Match Term, v)) -> [p] -> [v] -> m (Match Term, [v])
- mergeElim :: Elim -> Arg Term -> Elim
- mergeElims :: [Elim] -> [Arg Term] -> [Elim]
- type MonadMatch (m :: Type -> Type) = PureTCM m
- matchCopatterns :: MonadMatch m => [NamedArg DeBruijnPattern] -> [Elim] -> m (Match Term, [Elim])
- matchCopattern :: MonadMatch m => DeBruijnPattern -> Elim -> m (Match Term, Elim)
- matchPatterns :: MonadMatch m => [NamedArg DeBruijnPattern] -> [Arg Term] -> m (Match Term, [Arg Term])
- matchPattern :: MonadMatch m => DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
- yesSimplification :: Match a -> Match a
- matchPatternP :: MonadMatch m => DeBruijnPattern -> Arg DeBruijnPattern -> m (Match DeBruijnPattern)
- matchPatternsP :: MonadMatch m => [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern] -> m (Match DeBruijnPattern)
- properlyMatching :: HasConstInfo m => Pattern' a -> m Bool
- properlyMatching' :: HasConstInfo m => Bool -> Bool -> Pattern' a -> m Bool

# Documentation

data Match a Source #

If matching is inconclusive (`DontKnow`) we want to know whether it is on a lazy pattern and whether it is due to a particular meta variable.

Constructors

Yes Simplification (IntMap (Arg a)) |
No |
DontKnow OnlyLazy (Blocked ()) |

#### Instances

Instances details

Functor Match Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Match Methods fmap :: (a -> b) -> Match a -> Match b Source # (<$) :: a -> Match b -> Match a Source #
Null (Match a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Match Methods empty :: Match a Source # null :: Match a -> Bool Source #
Monoid (Match a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Match Methods mempty :: Match a Source # mappend :: Match a -> Match a -> Match a Source # mconcat :: [Match a] -> Match a Source #
Semigroup (Match a) Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Match Methods (<>) :: Match a -> Match a -> Match a Source # sconcat :: NonEmpty (Match a) -> Match a Source # stimes :: Integral b => b -> Match a -> Match a Source #

matchedArgs :: Empty -> Int -> IntMap (Arg a) -> [Arg a] Source #

matchedArgs' :: Int -> IntMap (Arg a) -> [Maybe (Arg a)] Source #

buildSubstitution :: DeBruijn a => Impossible -> Int -> IntMap (Arg a) -> Substitution' a Source #

Builds a proper substitution from an IntMap produced by match(Co)patterns

data OnlyLazy Source #

Whether the inconclusive matches are only on lazy patterns.

Constructors

OnlyLazy |
NonLazy |

#### Instances

Instances details

Monoid OnlyLazy Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Match Methods mempty :: OnlyLazy Source # mappend :: OnlyLazy -> OnlyLazy -> OnlyLazy Source # mconcat :: [OnlyLazy] -> OnlyLazy Source #
Semigroup OnlyLazy Source # |
Instance details Defined in Agda.TypeChecking.Patterns.Match Methods (<>) :: OnlyLazy -> OnlyLazy -> OnlyLazy Source # sconcat :: NonEmpty OnlyLazy -> OnlyLazy Source # stimes :: Integral b => b -> OnlyLazy -> OnlyLazy Source #

foldMatch :: forall m p v. (IsProjP p, MonadMatch m) => (p -> v -> m (Match Term, v)) -> [p] -> [v] -> m (Match Term, [v]) Source #

Instead of `zipWithM`, we need to use this lazy version of combining pattern matching computations.

mergeElim :: Elim -> Arg Term -> Elim Source #

mergeElims :: [Elim] -> [Arg Term] -> [Elim] Source #

type MonadMatch (m :: Type -> Type) = PureTCM m Source #

matchCopatterns :: MonadMatch m => [NamedArg DeBruijnPattern] -> [Elim] -> m (Match Term, [Elim]) Source #

`matchCopatterns ps es` matches spine `es` against copattern spine `ps`.

Returns `Yes` and a substitution for the pattern variables (in form of IntMap Term) if matching was successful.

Returns `No` if there was a constructor or projection mismatch.

Returns `DontKnow` if an argument could not be evaluated to constructor form because of a blocking meta variable.

In any case, also returns spine `es` in reduced form (with all the weak head reductions performed that were necessary to come to a decision).

matchCopattern :: MonadMatch m => DeBruijnPattern -> Elim -> m (Match Term, Elim) Source #

Match a single copattern.

matchPatterns :: MonadMatch m => [NamedArg DeBruijnPattern] -> [Arg Term] -> m (Match Term, [Arg Term]) Source #

matchPattern :: MonadMatch m => DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term) Source #

Match a single pattern.

yesSimplification :: Match a -> Match a Source #

matchPatternP :: MonadMatch m => DeBruijnPattern -> Arg DeBruijnPattern -> m (Match DeBruijnPattern) Source #

Match a single pattern.

matchPatternsP :: MonadMatch m => [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern] -> m (Match DeBruijnPattern) Source #

properlyMatching :: HasConstInfo m => Pattern' a -> m Bool Source #

Does the pattern perform a match that could fail?

properlyMatching' Source #

Arguments

:: HasConstInfo m |
=> Bool | Should absurd patterns count as proper match?
-> Bool | Should projection patterns count as proper match?
-> Pattern' a | The pattern.
-> m Bool |