| 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
- 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
- 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)
Documentation
If matching is inconclusive (DontKnow) we want to know whether
it is due to a particular meta variable.
buildSubstitution :: DeBruijn a => Impossible -> Int -> IntMap (Arg a) -> Substitution' a Source #
Builds a proper substitution from an IntMap produced by match(Co)patterns
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.
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 #