| 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]
- buildSubstitution :: DeBruijn a => Empty -> Int -> IntMap (Arg a) -> Substitution' a
- foldMatch :: forall p v. IsProjP p => (p -> v -> ReduceM (Match Term, v)) -> [p] -> [v] -> ReduceM (Match Term, [v])
- mergeElim :: Elim -> Arg Term -> Elim
- mergeElims :: [Elim] -> [Arg Term] -> [Elim]
- matchCopatterns :: [NamedArg DeBruijnPattern] -> [Elim] -> ReduceM (Match Term, [Elim])
- matchCopattern :: DeBruijnPattern -> Elim -> ReduceM (Match Term, Elim)
- matchPatterns :: [NamedArg DeBruijnPattern] -> [Arg Term] -> ReduceM (Match Term, [Arg Term])
- matchPattern :: DeBruijnPattern -> Arg Term -> ReduceM (Match Term, Arg Term)
- yesSimplification :: (Match a, b) -> (Match a, b)
- matchPatternP :: DeBruijnPattern -> Arg DeBruijnPattern -> ReduceM (Match DeBruijnPattern)
- matchPatternsP :: [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern] -> ReduceM (Match DeBruijnPattern)
Documentation
If matching is inconclusive (DontKnow) we want to know whether
it is due to a particular meta variable.
buildSubstitution :: DeBruijn a => Empty -> Int -> IntMap (Arg a) -> Substitution' a Source #
Builds a proper substitution from an IntMap produced by match(Co)patterns
foldMatch :: forall p v. IsProjP p => (p -> v -> ReduceM (Match Term, v)) -> [p] -> [v] -> ReduceM (Match Term, [v]) Source #
Instead of zipWithM, we need to use this lazy version
of combining pattern matching computations.
matchCopatterns :: [NamedArg DeBruijnPattern] -> [Elim] -> ReduceM (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 :: DeBruijnPattern -> Elim -> ReduceM (Match Term, Elim) Source #
Match a single copattern.
matchPatterns :: [NamedArg DeBruijnPattern] -> [Arg Term] -> ReduceM (Match Term, [Arg Term]) Source #
matchPattern :: DeBruijnPattern -> Arg Term -> ReduceM (Match Term, Arg Term) Source #
Match a single pattern.
yesSimplification :: (Match a, b) -> (Match a, b) Source #
matchPatternP :: DeBruijnPattern -> Arg DeBruijnPattern -> ReduceM (Match DeBruijnPattern) Source #
Match a single pattern.
matchPatternsP :: [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern] -> ReduceM (Match DeBruijnPattern) Source #