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.
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Patterns.Match
Pattern matcher used in the reducer for clauses that have not been compiled to case trees yet.
- 3 types
- 15 values
- PackageAgda-2.8.0.2
- Exports18
- LanguageHaskell2010
- LicenceMIT
- SourceMatch.hs
Builds a proper substitution from an IntMap produced by match(Co)patterns
Instead of zipWithM, we need to use this lazy version of combining pattern matching computations.
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).
Match a single copattern.
Match a single pattern.
Match a single pattern.
Does the pattern perform a match that could fail?
value
properlyMatching' :: HasConstInfo m=> BoolShould absurd patterns count as proper match?
-> BoolShould projection patterns count as proper match?
-> Pattern' aThe pattern.
-> m Bool