Agda.TypeChecking.Patterns.Match

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

Documentation

data Match a

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

Functor Match

Defined in Agda.TypeChecking.Patterns.Match

Methods

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

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

Null (Match a)

Defined in Agda.TypeChecking.Patterns.Match

Methods

empty :: Match a

null :: Match a -> Bool

Monoid (Match a)

Defined in Agda.TypeChecking.Patterns.Match

Methods

mempty :: Match a

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

mconcat :: [Match a] -> Match a

Semigroup (Match a)

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

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

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

data OnlyLazy

Whether the inconclusive matches are only on lazy patterns.

Constructors

OnlyLazy

NonLazy

Instances

Monoid OnlyLazy

Defined in Agda.TypeChecking.Patterns.Match

Methods

mempty :: OnlyLazy

mappend :: OnlyLazy -> OnlyLazy -> OnlyLazy

mconcat :: [OnlyLazy] -> OnlyLazy

Semigroup OnlyLazy

Defined in Agda.TypeChecking.Patterns.Match

Methods

(<>) :: OnlyLazy -> OnlyLazy -> OnlyLazy

sconcat :: NonEmpty OnlyLazy -> OnlyLazy

stimes :: Integral b => b -> OnlyLazy -> OnlyLazy

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

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

mergeElim :: Elim -> Arg Term -> Elim

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

type MonadMatch m = PureTCM m

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

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)

Match a single copattern.

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

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

Match a single pattern.

yesSimplification :: Match a -> Match a

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

Match a single pattern.

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