Agda-2.6.20240714: 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 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

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 #

Null (Match a) Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Match

Methods

empty :: Match a Source #

null :: Match a -> Bool Source #

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

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

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

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

buildSubstitution :: DeBruijn a => Impossible -> Int -> IntMap (Arg a) -> Substitution' a Source #

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

data OnlyLazy Source #

Whether the inconclusive matches are only on lazy patterns.

Constructors

OnlyLazy 
NonLazy 

Instances

Instances details
Monoid OnlyLazy Source # 
Instance details

Defined in Agda.TypeChecking.Patterns.Match

Semigroup OnlyLazy Source # 
Instance details

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]) Source #

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

type MonadMatch (m :: Type -> Type) = PureTCM m Source #

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.

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

Match a single pattern.