{-# LANGUAGE NondecreasingIndentation #-}

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

module Agda.TypeChecking.Patterns.Match where

import Prelude hiding (null)

import Control.Monad
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap

import Agda.Syntax.Common
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern

import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (getName', builtinHComp)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records

import Agda.Utils.Empty
import Agda.Utils.Functor (for, ($>), (<&>))
import Agda.Utils.Maybe
import Agda.Utils.Monad ( anyM, or2M)
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Size
import Agda.Utils.Tuple

import Agda.Utils.Impossible

-- | Result of matching a pattern against a term.
data Match a
  = Yes Simplification (IntMap (Arg a))
      -- ^ Matches with the given substitution for the pattern variables.
  | No MatchPrio
      -- ^ Mismatch where the constructor/literal pattern has the given priority.
  | DontKnow MatchPrio OnlyLazy (Blocked ())
      -- ^ Stuck where the constructor/literal pattern has the given priority.
      -- If matching is inconclusive we also want to know whether it is on a
      -- lazy pattern and whether it is due to a particular meta variable.
  deriving (Int -> Match a -> ShowS
[Match a] -> ShowS
Match a -> String
(Int -> Match a -> ShowS)
-> (Match a -> String) -> ([Match a] -> ShowS) -> Show (Match a)
forall a. Show a => Int -> Match a -> ShowS
forall a. Show a => [Match a] -> ShowS
forall a. Show a => Match a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Match a -> ShowS
showsPrec :: Int -> Match a -> ShowS
$cshow :: forall a. Show a => Match a -> String
show :: Match a -> String
$cshowList :: forall a. Show a => [Match a] -> ShowS
showList :: [Match a] -> ShowS
Show, (forall a b. (a -> b) -> Match a -> Match b)
-> (forall a b. a -> Match b -> Match a) -> Functor Match
forall a b. a -> Match b -> Match a
forall a b. (a -> b) -> Match a -> Match b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Match a -> Match b
fmap :: forall a b. (a -> b) -> Match a -> Match b
$c<$ :: forall a b. a -> Match b -> Match a
<$ :: forall a b. a -> Match b -> Match a
Functor)

instance Null (Match a) where
  empty :: Match a
empty = Simplification -> IntMap (Arg a) -> Match a
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
forall a. Null a => a
empty IntMap (Arg a)
forall a. Null a => a
empty
  null :: Match a -> Bool
null (Yes Simplification
simpl IntMap (Arg a)
as) = Simplification -> Bool
forall a. Null a => a -> Bool
null Simplification
simpl Bool -> Bool -> Bool
&& IntMap (Arg a) -> Bool
forall a. Null a => a -> Bool
null IntMap (Arg a)
as
  null Match a
_              = Bool
False

instance P.Pretty a => P.Pretty (Match a) where
  pretty :: Match a -> Doc
pretty (Yes Simplification
simp IntMap (Arg a)
xs) = Doc
"Yes" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> [(Int, Arg a)] -> Doc
forall a. Pretty a => a -> Doc
P.pretty (IntMap (Arg a) -> [(Int, Arg a)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Arg a)
xs)
  pretty (No MatchPrio
_) = Doc
"No"
  pretty (DontKnow MatchPrio
_ OnlyLazy
_ Blocked' Term ()
b) = Doc
"DontKnow" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
P.<+> Blocked' Term () -> Doc
forall a. Pretty a => a -> Doc
P.pretty Blocked' Term ()
b

matchedArgs :: Empty -> Int -> IntMap (Arg a) -> [Arg a]
matchedArgs :: forall a. Empty -> Int -> IntMap (Arg a) -> [Arg a]
matchedArgs Empty
err Int
n IntMap (Arg a)
vs = (Maybe (Arg a) -> Arg a) -> [Maybe (Arg a)] -> [Arg a]
forall a b. (a -> b) -> [a] -> [b]
map (Arg a -> Maybe (Arg a) -> Arg a
forall a. a -> Maybe a -> a
fromMaybe (Empty -> Arg a
forall a. Empty -> a
absurd Empty
err)) ([Maybe (Arg a)] -> [Arg a]) -> [Maybe (Arg a)] -> [Arg a]
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (Arg a) -> [Maybe (Arg a)]
forall a. Int -> IntMap (Arg a) -> [Maybe (Arg a)]
matchedArgs' Int
n IntMap (Arg a)
vs

matchedArgs' :: Int -> IntMap (Arg a) -> [Maybe (Arg a)]
matchedArgs' :: forall a. Int -> IntMap (Arg a) -> [Maybe (Arg a)]
matchedArgs' Int
n IntMap (Arg a)
vs = (Int -> Maybe (Arg a)) -> [Int] -> [Maybe (Arg a)]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe (Arg a)
get [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
  where
    get :: Int -> Maybe (Arg a)
get Int
k = Int -> IntMap (Arg a) -> Maybe (Arg a)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
k IntMap (Arg a)
vs

-- | Builds a proper substitution from an IntMap produced by match(Co)patterns
buildSubstitution :: (DeBruijn a)
                  => Impossible -> Int -> IntMap (Arg a) -> Substitution' a
buildSubstitution :: forall a.
DeBruijn a =>
Impossible -> Int -> IntMap (Arg a) -> Substitution' a
buildSubstitution Impossible
err Int
n IntMap (Arg a)
vs = (Maybe (Arg a) -> Substitution' a -> Substitution' a)
-> Substitution' a -> [Maybe (Arg a)] -> Substitution' a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Maybe (Arg a) -> Substitution' a -> Substitution' a
cons Substitution' a
forall a. Substitution' a
idS ([Maybe (Arg a)] -> Substitution' a)
-> [Maybe (Arg a)] -> Substitution' a
forall a b. (a -> b) -> a -> b
$ Int -> IntMap (Arg a) -> [Maybe (Arg a)]
forall a. Int -> IntMap (Arg a) -> [Maybe (Arg a)]
matchedArgs' Int
n IntMap (Arg a)
vs
  where cons :: Maybe (Arg a) -> Substitution' a -> Substitution' a
cons Maybe (Arg a)
Nothing  = Impossible -> Int -> Substitution' a -> Substitution' a
forall a. Impossible -> Int -> Substitution' a -> Substitution' a
strengthenS' Impossible
err Int
1
        cons (Just Arg a
v) = a -> Substitution' a -> Substitution' a
forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS (Arg a -> a
forall e. Arg e -> e
unArg Arg a
v)

-- | Combining match results.
-- When combining 'No' and 'DontKnow', the lower priority wins!
-- See issue #3054 / #8559.
instance Semigroup (Match a) where
  Match a
m <> :: Match a -> Match a -> Match a
<> Match a
m' = case (Match a
m, Match a
m') of
    -- @NotBlocked (StuckOn e)@ means blocked by a variable.
    -- In this case, no instantiation of meta-variables will make progress.
    (DontKnow MatchPrio
p OnlyLazy
l Blocked' Term ()
b , DontKnow MatchPrio
p' OnlyLazy
l' Blocked' Term ()
b' ) -> MatchPrio -> OnlyLazy -> Blocked' Term () -> Match a
forall a. MatchPrio -> OnlyLazy -> Blocked' Term () -> Match a
DontKnow (MatchPrio
p MatchPrio -> MatchPrio -> MatchPrio
forall a. Semigroup a => a -> a -> a
<> MatchPrio
p') (OnlyLazy
l OnlyLazy -> OnlyLazy -> OnlyLazy
forall a. Semigroup a => a -> a -> a
<> OnlyLazy
l') (Blocked' Term ()
b Blocked' Term () -> Blocked' Term () -> Blocked' Term ()
forall a. Semigroup a => a -> a -> a
<> Blocked' Term ()
b')
    (DontKnow{}     , Yes{}             ) -> Match a
m
    (DontKnow MatchPrio
p OnlyLazy
_ Blocked' Term ()
_ , No MatchPrio
p'             ) -> if MatchPrio
p MatchPrio -> MatchPrio -> Bool
forall a. Ord a => a -> a -> Bool
< MatchPrio
p' then Match a
m else Match a
m'
    (Yes{}          , DontKnow{}        ) -> Match a
m'
    (No MatchPrio
p           , DontKnow MatchPrio
p' OnlyLazy
_ Blocked' Term ()
_   ) -> if MatchPrio
p' MatchPrio -> MatchPrio -> Bool
forall a. Ord a => a -> a -> Bool
< MatchPrio
p then Match a
m' else Match a
m
    (No MatchPrio
p           , No MatchPrio
p'             ) -> MatchPrio -> Match a
forall a. MatchPrio -> Match a
No (MatchPrio
p MatchPrio -> MatchPrio -> MatchPrio
forall a. Semigroup a => a -> a -> a
<> MatchPrio
p')
    (No{}           , Yes{}             ) -> Match a
m
    (Yes{}          , No{}              ) -> Match a
m'
    (Yes Simplification
s IntMap (Arg a)
us       , Yes Simplification
s' IntMap (Arg a)
vs         ) -> Simplification -> IntMap (Arg a) -> Match a
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes (Simplification
s Simplification -> Simplification -> Simplification
forall a. Semigroup a => a -> a -> a
<> Simplification
s') (IntMap (Arg a)
us IntMap (Arg a) -> IntMap (Arg a) -> IntMap (Arg a)
forall a. Semigroup a => a -> a -> a
<> IntMap (Arg a)
vs)

instance Monoid (Match a) where
    mempty :: Match a
mempty = Match a
forall a. Null a => a
empty
    mappend :: Match a -> Match a -> Match a
mappend = Match a -> Match a -> Match a
forall a. Semigroup a => a -> a -> a
(<>)

-- | Whether the inconclusive matches are only on lazy patterns.
data OnlyLazy = OnlyLazy | NonLazy
  deriving (Int -> OnlyLazy -> ShowS
[OnlyLazy] -> ShowS
OnlyLazy -> String
(Int -> OnlyLazy -> ShowS)
-> (OnlyLazy -> String) -> ([OnlyLazy] -> ShowS) -> Show OnlyLazy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OnlyLazy -> ShowS
showsPrec :: Int -> OnlyLazy -> ShowS
$cshow :: OnlyLazy -> String
show :: OnlyLazy -> String
$cshowList :: [OnlyLazy] -> ShowS
showList :: [OnlyLazy] -> ShowS
Show)

instance Semigroup OnlyLazy where
  OnlyLazy
NonLazy  <> :: OnlyLazy -> OnlyLazy -> OnlyLazy
<> OnlyLazy
_        = OnlyLazy
NonLazy
  OnlyLazy
_        <> OnlyLazy
NonLazy  = OnlyLazy
NonLazy
  OnlyLazy
OnlyLazy <> OnlyLazy
OnlyLazy = OnlyLazy
OnlyLazy

instance Monoid OnlyLazy where
  mempty :: OnlyLazy
mempty = OnlyLazy
OnlyLazy
  mappend :: OnlyLazy -> OnlyLazy -> OnlyLazy
mappend = OnlyLazy -> OnlyLazy -> OnlyLazy
forall a. Semigroup a => a -> a -> a
(<>)

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

-- Andreas, 2014-05-08, see Issue 1124:
--
-- Due to a bug in TypeChecking.Patterns.Match
-- a failed match of (C n b) against (C O unit)
-- turned into (C n unit).
-- This was because all patterns were matched in
-- parallel, and evaluations of successfull matches
-- (and a record constructor like unit can always
-- be successfully matched) were returned, leading
-- to a reassembly of (C n b) as (C n unit) which is
-- illtyped.

-- Now patterns are matched left to right and
-- upon failure, no further matching is performed.

foldMatch
  :: forall m p v . (IsProjP p, MonadMatch m)
  => (p -> v -> m (Match Term, v))
  -> [p] -> [v] -> m (Match Term, [v])
foldMatch :: forall (m :: * -> *) p v.
(IsProjP p, MonadMatch m) =>
(p -> v -> m (Match Term, v)) -> [p] -> [v] -> m (Match Term, [v])
foldMatch p -> v -> m (Match Term, v)
match = [p] -> [v] -> m (Match Term, [v])
loop where
  loop :: [p] -> [v] -> m (Match Term, [v])
  loop :: [p] -> [v] -> m (Match Term, [v])
loop [p]
ps0 [v]
vs0 = do
    case ([p]
ps0, [v]
vs0) of
      ([], []) -> (Match Term, [v]) -> m (Match Term, [v])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
forall a. Null a => a
empty, [])
      (p
p : [p]
ps, v
v : [v]
vs) -> do
        (r, v') <- p -> v -> m (Match Term, v)
match p
p v
v
        case r of
          No MatchPrio
prio | Just{} <- p -> Maybe (ProjOrigin, AmbiguousQName)
forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP p
p -> (Match Term, [v]) -> m (Match Term, [v])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> Match Term
forall a. MatchPrio -> Match a
No MatchPrio
prio, v
v' v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
vs)
          No MatchPrio
_ -> do
            -- Issue 2964: Even when the first pattern doesn't match we should
            -- continue to the next patterns (and potentially block on them)
            -- because the splitting order in the case tree may not be
            -- left-to-right.
            (r', _vs') <- [p] -> [v] -> m (Match Term, [v])
loop [p]
ps [v]
vs
            -- Issue 2968: do not use vs' here, because it might
            -- contain ill-typed terms due to eta-expansion at wrong
            -- type.
            return (r <> r', v' : vs)
          DontKnow MatchPrio
_ OnlyLazy
OnlyLazy Blocked' Term ()
_ -> do
            (r', _vs') <- [p] -> [v] -> m (Match Term, [v])
loop [p]
ps [v]
vs
            return (r <> r', v' : vs)
          DontKnow MatchPrio
prio OnlyLazy
NonLazy Blocked' Term ()
m -> (Match Term, [v]) -> m (Match Term, [v])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> OnlyLazy -> Blocked' Term () -> Match Term
forall a. MatchPrio -> OnlyLazy -> Blocked' Term () -> Match a
DontKnow MatchPrio
prio OnlyLazy
NonLazy Blocked' Term ()
m, v
v' v -> [v] -> [v]
forall a. a -> [a] -> [a]
: [v]
vs)
          Yes{} -> do
            (r', vs') <- [p] -> [v] -> m (Match Term, [v])
loop [p]
ps [v]
vs
            return (r <> r', v' : vs')
      ([p], [v])
_ -> m (Match Term, [v])
forall a. HasCallStack => a
__IMPOSSIBLE__


-- TODO refactor matchPattern* to work with Elim instead.
mergeElim :: Elim -> Arg Term -> Elim
mergeElim :: Elim -> Arg Term -> Elim
mergeElim Apply{} Arg Term
arg = Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
arg
mergeElim (IApply Term
x Term
y Term
_) Arg Term
arg = Term -> Term -> Term -> Elim
forall a. a -> a -> a -> Elim' a
IApply Term
x Term
y (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg)
mergeElim Proj{} Arg Term
_ = Elim
forall a. HasCallStack => a
__IMPOSSIBLE__

mergeElims :: [Elim] -> [Arg Term] -> [Elim]
mergeElims :: [Elim] -> [Arg Term] -> [Elim]
mergeElims = (Elim -> Arg Term -> Elim) -> [Elim] -> [Arg Term] -> [Elim]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Elim -> Arg Term -> Elim
mergeElim

type MonadMatch m = PureTCM m

-- | @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).
matchCopatterns :: MonadMatch m
                => [NamedArg DeBruijnPattern]
                -> [Elim]
                -> m (Match Term, [Elim])
matchCopatterns :: forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern] -> [Elim] -> m (Match Term, [Elim])
matchCopatterns [NamedArg DeBruijnPattern]
ps [Elim]
vs = do
  String
-> Int
-> TCMT IO Doc
-> m (Match Term, [Elim])
-> m (Match Term, [Elim])
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"tc.match" Int
50
    ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"matchCopatterns"
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCMT IO Doc)
-> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map (DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM (DeBruijnPattern -> TCMT IO Doc)
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
ps)
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (Elim -> TCMT IO Doc) -> [Elim] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Elim -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Elim -> m Doc
prettyTCM [Elim]
vs)
          ]) (m (Match Term, [Elim]) -> m (Match Term, [Elim]))
-> m (Match Term, [Elim]) -> m (Match Term, [Elim])
forall a b. (a -> b) -> a -> b
$ do
  -- Buggy, see issue 1124:
  -- first mconcat . unzip <$> zipWithM' (matchCopattern . namedArg) ps vs
  (NamedArg DeBruijnPattern -> Elim -> m (Match Term, Elim))
-> [NamedArg DeBruijnPattern] -> [Elim] -> m (Match Term, [Elim])
forall (m :: * -> *) p v.
(IsProjP p, MonadMatch m) =>
(p -> v -> m (Match Term, v)) -> [p] -> [v] -> m (Match Term, [v])
foldMatch (DeBruijnPattern -> Elim -> m (Match Term, Elim)
forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Elim -> m (Match Term, Elim)
matchCopattern (DeBruijnPattern -> Elim -> m (Match Term, Elim))
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Elim
-> m (Match Term, Elim)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
ps [Elim]
vs

-- | Match a single copattern.
matchCopattern :: MonadMatch m
               => DeBruijnPattern
               -> Elim
               -> m (Match Term, Elim)
matchCopattern :: forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Elim -> m (Match Term, Elim)
matchCopattern pat :: DeBruijnPattern
pat@ProjP{} elim :: Elim
elim@(Proj ProjOrigin
_ QName
q) = do
  p <- DeBruijnPattern -> m DeBruijnPattern
forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
forall (m :: * -> *).
HasConstInfo m =>
DeBruijnPattern -> m DeBruijnPattern
normaliseProjP DeBruijnPattern
pat m DeBruijnPattern -> (DeBruijnPattern -> QName) -> m QName
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
         ProjP ProjOrigin
_ QName
p -> QName
p
         DeBruijnPattern
_         -> QName
forall a. HasCallStack => a
__IMPOSSIBLE__
  q       <- getOriginalProjection q
  return $ if p == q then (Yes YesSimplification empty, elim)
                     else (No empty,                    elim)
-- The following two cases are not impossible, see #2964
matchCopattern ProjP{} elim :: Elim
elim@Apply{}   = (Match Term, Elim) -> m (Match Term, Elim)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> Match Term
forall a. MatchPrio -> Match a
No MatchPrio
forall a. Null a => a
empty, Elim
elim)
matchCopattern DeBruijnPattern
_       elim :: Elim
elim@Proj{}    = (Match Term, Elim) -> m (Match Term, Elim)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> Match Term
forall a. MatchPrio -> Match a
No MatchPrio
forall a. Null a => a
empty, Elim
elim)
matchCopattern DeBruijnPattern
p       (Apply Arg Term
v) = (Arg Term -> Elim) -> (Match Term, Arg Term) -> (Match Term, Elim)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply ((Match Term, Arg Term) -> (Match Term, Elim))
-> m (Match Term, Arg Term) -> m (Match Term, Elim)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
matchPattern DeBruijnPattern
p Arg Term
v
matchCopattern DeBruijnPattern
p       e :: Elim
e@(IApply Term
x Term
y Term
r) = (Arg Term -> Elim) -> (Match Term, Arg Term) -> (Match Term, Elim)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (Elim -> Arg Term -> Elim
mergeElim Elim
e) ((Match Term, Arg Term) -> (Match Term, Elim))
-> m (Match Term, Arg Term) -> m (Match Term, Elim)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
matchPattern DeBruijnPattern
p (Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
r)

{-# SPECIALIZE matchPatterns :: [NamedArg DeBruijnPattern] -> [Arg Term] -> TCM (Match Term, [Arg Term]) #-}
matchPatterns :: MonadMatch m
              => [NamedArg DeBruijnPattern]
              -> [Arg Term]
              -> m (Match Term, [Arg Term])
matchPatterns :: forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern]
-> [Arg Term] -> m (Match Term, [Arg Term])
matchPatterns [NamedArg DeBruijnPattern]
ps [Arg Term]
vs = do
  String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.match" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
     [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"matchPatterns"
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg DeBruijnPattern] -> TCMT IO Doc
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList [NamedArg DeBruijnPattern]
ps
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM [Arg Term]
vs)
          ]

  String
-> Int
-> TCMT IO Doc
-> m (Match Term, [Arg Term])
-> m (Match Term, [Arg Term])
forall (m :: * -> *) a.
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc String
"tc.match" Int
50
    ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"matchPatterns"
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> TCMT IO Doc)
-> [NamedArg DeBruijnPattern] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [NamedArg DeBruijnPattern]
ps)
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (TCMT IO Doc -> [TCMT IO Doc] -> [TCMT IO Doc]
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc
comma ([TCMT IO Doc] -> [TCMT IO Doc]) -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> TCMT IO Doc) -> [Arg Term] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty [Arg Term]
vs)
          ]) (m (Match Term, [Arg Term]) -> m (Match Term, [Arg Term]))
-> m (Match Term, [Arg Term]) -> m (Match Term, [Arg Term])
forall a b. (a -> b) -> a -> b
$ do
  -- Buggy, see issue 1124:
  -- (ms,vs) <- unzip <$> zipWithM' (matchPattern . namedArg) ps vs
  -- return (mconcat ms, vs)
  (NamedArg DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term))
-> [NamedArg DeBruijnPattern]
-> [Arg Term]
-> m (Match Term, [Arg Term])
forall (m :: * -> *) p v.
(IsProjP p, MonadMatch m) =>
(p -> v -> m (Match Term, v)) -> [p] -> [v] -> m (Match Term, [v])
foldMatch (DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
matchPattern (DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term))
-> (NamedArg DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> Arg Term
-> m (Match Term, Arg Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
ps [Arg Term]
vs

-- | Match a single pattern.
matchPattern :: MonadMatch m
             => DeBruijnPattern
             -> Arg Term
             -> m (Match Term, Arg Term)
matchPattern :: forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
matchPattern DeBruijnPattern
p Arg Term
u = m (Match Term, Arg Term) -> m (Match Term, Arg Term)
debugMatchPattern (m (Match Term, Arg Term) -> m (Match Term, Arg Term))
-> m (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a b. (a -> b) -> a -> b
$ case (DeBruijnPattern
p, Arg Term
u) of
  (ProjP{}, Arg Term
_            ) -> m (Match Term, Arg Term)
forall a. HasCallStack => a
__IMPOSSIBLE__
  (IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x , Arg Term
arg ) -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Simplification -> IntMap (Arg Term) -> Match Term
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification IntMap (Arg Term)
entry, Arg Term
arg)
    where entry :: IntMap (Arg Term)
entry = (Int, Arg Term) -> IntMap (Arg Term)
forall el coll. Singleton el coll => el -> coll
singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
x, Arg Term
arg)
  (VarP PatternInfo
_ DBPatVar
x , Arg Term
arg          ) -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Simplification -> IntMap (Arg Term) -> Match Term
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification IntMap (Arg Term)
entry, Arg Term
arg)
    where entry :: IntMap (Arg Term)
entry = (Int, Arg Term) -> IntMap (Arg Term)
forall el coll. Singleton el coll => el -> coll
singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
x, Arg Term
arg)
  (DotP PatternInfo
_ Term
_ , arg :: Arg Term
arg@(Arg ArgInfo
_ Term
v)) -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Simplification -> IntMap (Arg Term) -> Match Term
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification IntMap (Arg Term)
forall a. Null a => a
empty, Arg Term
arg)
  (LitP LitPatternInfo{ litPPrio :: LitPatternInfo -> MatchPrio
litPPrio = MatchPrio
prio } Literal
l , arg :: Arg Term
arg@(Arg ArgInfo
_ Term
v)) -> do
    w <- Term -> m (Blocked Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
v
    let arg' = Arg Term
arg Arg Term -> Term -> Arg Term
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
w
    case w of
      NotBlocked NotBlocked' Term
_ (Lit Literal
l')
          | Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'   -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Simplification -> IntMap (Arg Term) -> Match Term
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
YesSimplification IntMap (Arg Term)
forall a. Null a => a
empty , Arg Term
arg')
          | Bool
otherwise -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> Match Term
forall a. MatchPrio -> Match a
No MatchPrio
prio                     , Arg Term
arg')
      Blocked Blocker
b Term
_     -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> OnlyLazy -> Blocked' Term () -> Match Term
forall a. MatchPrio -> OnlyLazy -> Blocked' Term () -> Match a
DontKnow MatchPrio
prio OnlyLazy
NonLazy (Blocked' Term () -> Match Term) -> Blocked' Term () -> Match Term
forall a b. (a -> b) -> a -> b
$ Blocker -> () -> Blocked' Term ()
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b ()     , Arg Term
arg')
      NotBlocked NotBlocked' Term
r Term
t  -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> OnlyLazy -> Blocked' Term () -> Match Term
forall a. MatchPrio -> OnlyLazy -> Blocked' Term () -> Match a
DontKnow MatchPrio
prio OnlyLazy
NonLazy (Blocked' Term () -> Match Term) -> Blocked' Term () -> Match Term
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
r' () , Arg Term
arg')
        where r' :: NotBlocked' Term
r' = Elim -> NotBlocked' Term -> NotBlocked' Term
forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
stuckOn (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
arg') NotBlocked' Term
r

  -- Case constructor pattern.
  (ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps, Arg ArgInfo
info Term
v) -> do
    let prio :: MatchPrio
prio = ConPatternInfo -> MatchPrio
conPPrio ConPatternInfo
cpi
    let lazy :: OnlyLazy
lazy = if ConPatternInfo -> Bool
conPLazy ConPatternInfo
cpi then OnlyLazy
OnlyLazy else OnlyLazy
NonLazy
    if Bool -> Bool
not (ConPatternInfo -> Bool
conPRecord ConPatternInfo
cpi) then ConHead
-> MatchPrio
-> OnlyLazy
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
forall (m :: * -> *).
MonadMatch m =>
ConHead
-> MatchPrio
-> OnlyLazy
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback ConHead
c MatchPrio
prio OnlyLazy
lazy [NamedArg DeBruijnPattern]
ps (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v) else do
    QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe (QName, RecordData))
isEtaRecordConstructor (ConHead -> QName
conName ConHead
c) m (Maybe (QName, RecordData))
-> (Maybe (QName, RecordData) -> m (Match Term, Arg Term))
-> m (Match Term, Arg Term)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe (QName, RecordData)
Nothing -> ConHead
-> MatchPrio
-> OnlyLazy
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
forall (m :: * -> *).
MonadMatch m =>
ConHead
-> MatchPrio
-> OnlyLazy
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback ConHead
c MatchPrio
prio OnlyLazy
lazy [NamedArg DeBruijnPattern]
ps (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v)
      -- Case: Eta record constructor.
      -- This case is necessary if we want to use the clauses before
      -- record pattern translation (e.g., in type-checking definitions by copatterns).
      Just (QName
_r, RecordData
def) -> do
        String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.match" Int
50 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
          [ TCMT IO Doc
"matchPattern: eta record"
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"c  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ConHead -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ConHead -> m Doc
prettyTCM ConHead
c
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> [NamedArg DeBruijnPattern] -> TCMT IO Doc
forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList [NamedArg DeBruijnPattern]
ps
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"v  = " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
v
          ]
        -- Issue #7266: in case we are brazenly matching potentially ill-typed arguments,
        -- `v` might be an application of a *different* constructor.
        -- In that case we certainly have no match.
        case Term
v of
          Con ConHead
c' ConInfo
_ [Elim]
_ | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
/= ConHead
c' -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> Match Term
forall a. MatchPrio -> Match a
No MatchPrio
prio, Arg Term
u)
          Term
_ -> do
            let fs :: [Arg QName]
fs = (Dom QName -> Arg QName) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> Arg QName
forall t a. Dom' t a -> Arg a
argFromDom ([Dom QName] -> [Arg QName]) -> [Dom QName] -> [Arg QName]
forall a b. (a -> b) -> a -> b
$ RecordData -> [Dom QName]
_recFields RecordData
def
            Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Arg QName] -> Int
forall a. Sized a => a -> Int
size [Arg QName]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [NamedArg DeBruijnPattern] -> Int
forall a. Sized a => a -> Int
size [NamedArg DeBruijnPattern]
ps) m ()
forall a. HasCallStack => a
__IMPOSSIBLE__
            ([Arg Term] -> Arg Term)
-> (Match Term, [Arg Term]) -> (Match Term, Arg Term)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info (Term -> Arg Term)
-> ([Arg Term] -> Term) -> [Arg Term] -> Arg Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c (ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
cpi) ([Elim] -> Term) -> ([Arg Term] -> [Elim]) -> [Arg Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Arg Term -> Elim) -> [Arg Term] -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply) ((Match Term, [Arg Term]) -> (Match Term, Arg Term))
-> m (Match Term, [Arg Term]) -> m (Match Term, Arg Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
              [NamedArg DeBruijnPattern]
-> [Arg Term] -> m (Match Term, [Arg Term])
forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern]
-> [Arg Term] -> m (Match Term, [Arg Term])
matchPatterns [NamedArg DeBruijnPattern]
ps ([Arg Term] -> m (Match Term, [Arg Term]))
-> [Arg Term] -> m (Match Term, [Arg Term])
forall a b. (a -> b) -> a -> b
$ [Arg QName] -> (Arg QName -> Arg Term) -> [Arg Term]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
for [Arg QName]
fs ((Arg QName -> Arg Term) -> [Arg Term])
-> (Arg QName -> Arg Term) -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
ai QName
f) -> ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai (Term -> Arg Term) -> Term -> Arg Term
forall a b. (a -> b) -> a -> b
$ Term
v Term -> [Elim] -> Term
forall t. Apply t => t -> [Elim] -> t
`applyE` [ProjOrigin -> QName -> Elim
forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
  (DefP PatternInfo
o QName
q [NamedArg DeBruijnPattern]
ps, Arg Term
v) -> do
    let f :: Term -> Maybe ([Elim] -> Term, [Elim])
f (Def QName
q' [Elim]
vs) | QName
q QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
q' = ([Elim] -> Term, [Elim]) -> Maybe ([Elim] -> Term, [Elim])
forall a. a -> Maybe a
Just (QName -> [Elim] -> Term
Def QName
q, [Elim]
vs)
        f Term
_                     = Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
    (Term -> Maybe ([Elim] -> Term, [Elim]))
-> MatchPrio
-> OnlyLazy
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
forall (m :: * -> *).
MonadMatch m =>
(Term -> Maybe ([Elim] -> Term, [Elim]))
-> MatchPrio
-> OnlyLazy
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback' Term -> Maybe ([Elim] -> Term, [Elim])
f MatchPrio
forall a. Null a => a
empty OnlyLazy
NonLazy [NamedArg DeBruijnPattern]
ps Arg Term
v
 where
  debugMatchPattern :: m (Match Term, Arg Term) -> m (Match Term, Arg Term)
debugMatchPattern m (Match Term, Arg Term)
go = do
    String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.match" Int
20 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
       [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"matchPattern"
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"p =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DeBruijnPattern -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => DeBruijnPattern -> m Doc
prettyTCM DeBruijnPattern
p
            , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"u =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Arg Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Arg Term -> m Doc
prettyTCM Arg Term
u
            ]
    String -> Int -> TCMT IO Doc -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"tc.match" Int
60 (TCMT IO Doc -> m ()) -> TCMT IO Doc -> m ()
forall a b. (a -> b) -> a -> b
$
       [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"p (raw) =" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> DeBruijnPattern -> TCMT IO Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty DeBruijnPattern
p
            ]
    (m, t) <- m (Match Term, Arg Term)
go
    reportSDoc "tc.match" 60 $
      vcat [ nest 2 $ "result = " <+> pretty m ]
    -- reportSDoc "tc.match" 20 $
    --   vcat [ nest 2 $ "result = " <+> prettyTCM m ]
    return (m, t)

    -- Default: not an eta record constructor.
  fallback :: MonadMatch m
           => ConHead -> MatchPrio -> OnlyLazy -> [NamedArg DeBruijnPattern] -> Arg Term -> m (Match Term, Arg Term)
  fallback :: forall (m :: * -> *).
MonadMatch m =>
ConHead
-> MatchPrio
-> OnlyLazy
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback ConHead
c MatchPrio
prio OnlyLazy
lazy [NamedArg DeBruijnPattern]
ps Arg Term
v = do
    let f :: Term -> Maybe ([Elim] -> Term, [Elim])
f (Con ConHead
c' ConInfo
ci' [Elim]
vs) | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c' = ([Elim] -> Term, [Elim]) -> Maybe ([Elim] -> Term, [Elim])
forall a. a -> Maybe a
Just (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c' ConInfo
ci',[Elim]
vs)
        f Term
_                         = Maybe ([Elim] -> Term, [Elim])
forall a. Maybe a
Nothing
    (Term -> Maybe ([Elim] -> Term, [Elim]))
-> MatchPrio
-> OnlyLazy
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
forall (m :: * -> *).
MonadMatch m =>
(Term -> Maybe ([Elim] -> Term, [Elim]))
-> MatchPrio
-> OnlyLazy
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback' Term -> Maybe ([Elim] -> Term, [Elim])
f MatchPrio
prio OnlyLazy
lazy [NamedArg DeBruijnPattern]
ps Arg Term
v

  -- Regardless of blocking, constructors can be matched on.
  -- Since hcomp clauses are only computed during coverage checking
  -- and clause-based reduction is only used *before* coverage checking,
  -- we do not consider hcomp patterns here (see issue #8700).
  isMatchable :: Blocked Term -> Maybe Term
  isMatchable :: Blocked Term -> Maybe Term
isMatchable Blocked Term
r =
      case Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
r of
        t :: Term
t@Con{} -> Term -> Maybe Term
forall a. a -> Maybe a
Just Term
t
        Term
_       -> Maybe Term
forall a. Maybe a
Nothing

  -- DefP hcomp and ConP matching.
  fallback' :: MonadMatch m
            => (Term -> Maybe (Elims -> Term , Elims))
            -> MatchPrio
            -> OnlyLazy
            -> [NamedArg DeBruijnPattern]
            -> Arg Term
            -> m (Match Term, Arg Term)
  fallback' :: forall (m :: * -> *).
MonadMatch m =>
(Term -> Maybe ([Elim] -> Term, [Elim]))
-> MatchPrio
-> OnlyLazy
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback' Term -> Maybe ([Elim] -> Term, [Elim])
mtc MatchPrio
prio OnlyLazy
lazy [NamedArg DeBruijnPattern]
ps (Arg ArgInfo
info Term
v) = do

        w <- Term -> m (Blocked Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
v
        -- Unfold delayed (corecursive) definitions one step. This is
        -- only necessary if c is a coinductive constructor, but
        -- it does not hurt to do it all the time.
{-
        w <- case w of
               NotBlocked r (Def f es) ->   -- Andreas, 2014-06-12 TODO: r == ReallyNotBlocked sufficient?
                 unfoldDefinitionE True reduceB' (Def f []) f es
                   -- reduceB is used here because some constructors
                   -- are actually definitions which need to be
                   -- unfolded (due to open public).
               _ -> return w
-}
        -- Jesper, 23-06-2016: Note that unfoldCorecursion may destroy
        -- constructor forms, so we only call constructorForm after.
        w <- traverse constructorForm =<< case w of
               NotBlocked NotBlocked' Term
r Term
u -> ReduceM (Blocked Term) -> m (Blocked Term)
forall a. ReduceM a -> m a
forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce (ReduceM (Blocked Term) -> m (Blocked Term))
-> ReduceM (Blocked Term) -> m (Blocked Term)
forall a b. (a -> b) -> a -> b
$ Term -> ReduceM (Blocked Term)
unfoldCorecursion Term
u  -- Andreas, 2014-06-12 TODO: r == ReallyNotBlocked sufficient?
               Blocked Term
_ -> Blocked Term -> m (Blocked Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Blocked Term
w
        let v = Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
w
            arg = ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v  -- the reduced argument

        reportSDoc "tc.match" 40 $ vcat
          [ "  v = " <+> prettyTCM v <?> pretty (void w)
          ]

        case w of
          Blocked Term
b | Just Term
t <- Blocked Term -> Maybe Term
isMatchable Blocked Term
b ->
            case Term -> Maybe ([Elim] -> Term, [Elim])
mtc Term
t of
              Just ([Elim] -> Term
bld, [Elim]
vs) -> do
                (m, vs1) <- [NamedArg DeBruijnPattern]
-> [Arg Term] -> m (Match Term, [Arg Term])
forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern]
-> [Arg Term] -> m (Match Term, [Arg Term])
matchPatterns [NamedArg DeBruijnPattern]
ps ([Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ [Elim] -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
vs)
                return (yesSimplification m, Arg info $ bld (mergeElims vs vs1))
              Maybe ([Elim] -> Term, [Elim])
Nothing
                                    -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> Match Term
forall a. MatchPrio -> Match a
No MatchPrio
prio                               , Arg Term
arg)
          Blocked Blocker
b Term
_               -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> OnlyLazy -> Blocked' Term () -> Match Term
forall a. MatchPrio -> OnlyLazy -> Blocked' Term () -> Match a
DontKnow MatchPrio
prio OnlyLazy
lazy (Blocked' Term () -> Match Term) -> Blocked' Term () -> Match Term
forall a b. (a -> b) -> a -> b
$ Blocker -> () -> Blocked' Term ()
forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b ()     , Arg Term
arg)
          NotBlocked NotBlocked' Term
r Term
_            -> (Match Term, Arg Term) -> m (Match Term, Arg Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (MatchPrio -> OnlyLazy -> Blocked' Term () -> Match Term
forall a. MatchPrio -> OnlyLazy -> Blocked' Term () -> Match a
DontKnow MatchPrio
prio OnlyLazy
lazy (Blocked' Term () -> Match Term) -> Blocked' Term () -> Match Term
forall a b. (a -> b) -> a -> b
$ NotBlocked' Term -> () -> Blocked' Term ()
forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
r' () , Arg Term
arg)
            where r' :: NotBlocked' Term
r' = Elim -> NotBlocked' Term -> NotBlocked' Term
forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
stuckOn (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply Arg Term
arg) NotBlocked' Term
r

yesSimplification :: Match a -> Match a
yesSimplification :: forall a. Match a -> Match a
yesSimplification = \case
  Yes Simplification
_ IntMap (Arg a)
vs -> Simplification -> IntMap (Arg a) -> Match a
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
YesSimplification IntMap (Arg a)
vs
  Match a
m -> Match a
m

-- Matching patterns against patterns -------------------------------------

-- | Match a single pattern.
matchPatternP :: MonadMatch m
              => DeBruijnPattern
              -> Arg DeBruijnPattern
              -> m (Match DeBruijnPattern)
matchPatternP :: forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg DeBruijnPattern -> m (Match DeBruijnPattern)
matchPatternP DeBruijnPattern
p (Arg ArgInfo
info (DotP PatternInfo
_ Term
v)) = do
  (m, arg) <- DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
matchPattern DeBruijnPattern
p (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v)
  return $ fmap (DotP defaultPatternInfo) m
matchPatternP DeBruijnPattern
p arg :: Arg DeBruijnPattern
arg@(Arg ArgInfo
info DeBruijnPattern
q) = do
  let varMatch :: DBPatVar -> m (Match DeBruijnPattern)
varMatch DBPatVar
x = Match DeBruijnPattern -> m (Match DeBruijnPattern)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match DeBruijnPattern -> m (Match DeBruijnPattern))
-> Match DeBruijnPattern -> m (Match DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ Simplification
-> IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification (IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern)
-> IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ (Int, Arg DeBruijnPattern) -> IntMap (Arg DeBruijnPattern)
forall el coll. Singleton el coll => el -> coll
singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
x, Arg DeBruijnPattern
arg)
      termMatch :: m (Match DeBruijnPattern)
termMatch  = do
        (m, arg) <- DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
matchPattern DeBruijnPattern
p ((DeBruijnPattern -> Term) -> Arg DeBruijnPattern -> Arg Term
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Term
patternToTerm Arg DeBruijnPattern
arg)
        return $ fmap (DotP defaultPatternInfo) m
  case DeBruijnPattern
p of
    ProjP{}         -> m (Match DeBruijnPattern)
forall a. HasCallStack => a
__IMPOSSIBLE__
    IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x -> DBPatVar -> m (Match DeBruijnPattern)
varMatch DBPatVar
x
    VarP PatternInfo
_ DBPatVar
x        -> DBPatVar -> m (Match DeBruijnPattern)
varMatch DBPatVar
x
    DotP PatternInfo
_ Term
_        -> Match DeBruijnPattern -> m (Match DeBruijnPattern)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match DeBruijnPattern -> m (Match DeBruijnPattern))
-> Match DeBruijnPattern -> m (Match DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ Simplification
-> IntMap (Arg DeBruijnPattern) -> Match DeBruijnPattern
forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification IntMap (Arg DeBruijnPattern)
forall a. Null a => a
empty
    LitP{}          -> m (Match DeBruijnPattern)
termMatch -- Literal patterns bind no variables so we can fall back to the Term version.
    DefP{}          -> m (Match DeBruijnPattern)
termMatch

    ConP ConHead
c ConPatternInfo
cpi [NamedArg DeBruijnPattern]
ps ->
      case DeBruijnPattern
q of
        ConP ConHead
c' ConPatternInfo
_ [NamedArg DeBruijnPattern]
qs | ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
c'   -> [NamedArg DeBruijnPattern]
-> [Arg DeBruijnPattern] -> m (Match DeBruijnPattern)
forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern]
-> [Arg DeBruijnPattern] -> m (Match DeBruijnPattern)
matchPatternsP [NamedArg DeBruijnPattern]
ps (((NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map ((NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
 -> [NamedArg DeBruijnPattern] -> [Arg DeBruijnPattern])
-> ((Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern]
-> [Arg DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing [NamedArg DeBruijnPattern]
qs)
                     | Bool
otherwise -> Match DeBruijnPattern -> m (Match DeBruijnPattern)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Match DeBruijnPattern -> m (Match DeBruijnPattern))
-> Match DeBruijnPattern -> m (Match DeBruijnPattern)
forall a b. (a -> b) -> a -> b
$ MatchPrio -> Match DeBruijnPattern
forall a. MatchPrio -> Match a
No (ConPatternInfo -> MatchPrio
conPPrio ConPatternInfo
cpi)
        LitP{} -> (DeBruijnPattern -> DeBruijnPattern)
-> Match DeBruijnPattern -> Match DeBruijnPattern
forall a b. (a -> b) -> Match a -> Match b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> DeBruijnPattern
forall {x} {a}. Pattern' x -> Pattern' a
toLitP (Match DeBruijnPattern -> Match DeBruijnPattern)
-> m (Match DeBruijnPattern) -> m (Match DeBruijnPattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Match DeBruijnPattern)
termMatch
          where toLitP :: Pattern' x -> Pattern' a
toLitP (DotP PatternInfo
_ (Lit Literal
l)) = Literal -> Pattern' a
forall a. Literal -> Pattern' a
litP Literal
l   -- All bindings should be to literals
                toLitP Pattern' x
_                = Pattern' a
forall a. HasCallStack => a
__IMPOSSIBLE__
        DeBruijnPattern
_      -> m (Match DeBruijnPattern)
termMatch

matchPatternsP :: MonadMatch m
               => [NamedArg DeBruijnPattern]
               -> [Arg DeBruijnPattern]
               -> m (Match DeBruijnPattern)
matchPatternsP :: forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern]
-> [Arg DeBruijnPattern] -> m (Match DeBruijnPattern)
matchPatternsP [NamedArg DeBruijnPattern]
ps [Arg DeBruijnPattern]
qs = do
  [Match DeBruijnPattern] -> Match DeBruijnPattern
forall a. Monoid a => [a] -> a
mconcat ([Match DeBruijnPattern] -> Match DeBruijnPattern)
-> m [Match DeBruijnPattern] -> m (Match DeBruijnPattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DeBruijnPattern
 -> Arg DeBruijnPattern -> m (Match DeBruijnPattern))
-> [DeBruijnPattern]
-> [Arg DeBruijnPattern]
-> m [Match DeBruijnPattern]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM DeBruijnPattern -> Arg DeBruijnPattern -> m (Match DeBruijnPattern)
forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg DeBruijnPattern -> m (Match DeBruijnPattern)
matchPatternP ((NamedArg DeBruijnPattern -> DeBruijnPattern)
-> [NamedArg DeBruijnPattern] -> [DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg DeBruijnPattern -> DeBruijnPattern
forall a. NamedArg a -> a
namedArg [NamedArg DeBruijnPattern]
ps) [Arg DeBruijnPattern]
qs

{-# SPECIALIZE properlyMatching :: Pattern' a -> TCM Bool #-}
-- | Does the pattern perform a match that could fail?
properlyMatching :: HasConstInfo m => Pattern' a -> m Bool
properlyMatching :: forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
properlyMatching = Bool -> Bool -> Pattern' a -> m Bool
forall (m :: * -> *) a.
HasConstInfo m =>
Bool -> Bool -> Pattern' a -> m Bool
properlyMatching' Bool
True Bool
True

properlyMatching' :: HasConstInfo m
  => Bool       -- ^ Should absurd patterns count as proper match?
  -> Bool       -- ^ Should projection patterns count as proper match?
  -> Pattern' a -- ^ The pattern.
  -> m Bool
properlyMatching' :: forall (m :: * -> *) a.
HasConstInfo m =>
Bool -> Bool -> Pattern' a -> m Bool
properlyMatching' Bool
absP Bool
projP = \case
  Pattern' a
p | Bool
absP Bool -> Bool -> Bool
&& Pattern' a -> Maybe PatOrigin
forall x. Pattern' x -> Maybe PatOrigin
patternOrigin Pattern' a
p Maybe PatOrigin -> Maybe PatOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== PatOrigin -> Maybe PatOrigin
forall a. a -> Maybe a
Just PatOrigin
PatOAbsurd -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  ConP ConHead
con ConPatternInfo
ci [NamedArg (Pattern' a)]
ps    -- eta record constructors do not count as proper matches themselves
    | ConPatternInfo -> Bool
conPRecord ConPatternInfo
ci -> (Maybe (QName, RecordData) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (QName, RecordData) -> Bool)
-> m (Maybe (QName, RecordData)) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m (Maybe (QName, RecordData))
forall (m :: * -> *).
(HasCallStack, HasConstInfo m) =>
QName -> m (Maybe (QName, RecordData))
isEtaRecordConstructor (ConHead -> QName
conName ConHead
con)) m Bool -> m Bool -> m Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
`or2M` (NamedArg (Pattern' a) -> m Bool)
-> [NamedArg (Pattern' a)] -> m Bool
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
(a -> m Bool) -> f a -> m Bool
anyM (Pattern' a -> m Bool
forall (m :: * -> *) a. HasConstInfo m => Pattern' a -> m Bool
properlyMatching (Pattern' a -> m Bool)
-> (NamedArg (Pattern' a) -> Pattern' a)
-> NamedArg (Pattern' a)
-> m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg (Pattern' a) -> Pattern' a
forall a. NamedArg a -> a
namedArg) [NamedArg (Pattern' a)]
ps
    | Bool
otherwise     -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  LitP{}    -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  DefP{}    -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  ProjP{}   -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
projP
  VarP{}    -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  DotP{}    -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  IApplyP{} -> Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False