Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Patterns.Match

Description

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

Synopsis

Documentation

data Match a Source #

If matching is inconclusive (DontKnow) we want to know whether it is due to a particular meta variable.

Constructors

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

Instances

Instances details
Functor Match Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Match

Methods

fmap :: (a -> b) -> Match a -> Match b #

(<$) :: a -> Match b -> Match a #

Semigroup (Match a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Match

Methods

(<>) :: Match a -> Match a -> Match a #

sconcat :: NonEmpty (Match a) -> Match a #

stimes :: Integral b => b -> Match a -> Match a #

Monoid (Match a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Match

Methods

mempty :: Match a #

mappend :: Match a -> Match a -> Match a #

mconcat :: [Match a] -> Match a #

Null (Match a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Match

Methods

empty :: Match a Source #

null :: Match a -> Bool Source #

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

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.

matchPattern :: DeBruijnPattern -> Arg Term -> ReduceM (Match Term, Arg Term) Source #

Match a single pattern.

yesSimplification :: (Match a, b) -> (Match a, b) Source #