{-# 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 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 hiding (constructorForm)
import Agda.TypeChecking.Monad.Builtin (getName',builtinHComp, builtinConId)
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records

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

import Agda.Utils.Impossible

-- | If matching is inconclusive (@DontKnow@) we want to know whether
--   it is due to a particular meta variable.
data Match a = Yes Simplification (IntMap (Arg a))
             | No
             | DontKnow (Blocked ())
  deriving 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
<$ :: forall a b. a -> Match b -> Match a
$c<$ :: forall a b. a -> Match b -> Match a
fmap :: forall a b. (a -> b) -> Match a -> Match b
$cfmap :: forall a b. (a -> b) -> Match a -> Match b
Functor

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

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 = forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> Maybe a -> a
fromMaybe (forall a. Empty -> a
absurd Empty
err)) forall a b. (a -> b) -> a -> b
$ 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 = forall a b. (a -> b) -> [a] -> [b]
map Int -> Maybe (Arg a)
get [Int
0 .. Int
n forall a. Num a => a -> a -> a
- Int
1]
  where
    get :: Int -> Maybe (Arg a)
get Int
k = 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Maybe (Arg a) -> Substitution' a -> Substitution' a
cons forall a. Substitution' a
idS forall a b. (a -> b) -> a -> b
$ 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  = forall a. Impossible -> Int -> Substitution' a -> Substitution' a
strengthenS' Impossible
err Int
1
        cons (Just Arg a
v) = forall a. DeBruijn a => a -> Substitution' a -> Substitution' a
consS (forall e. Arg e -> e
unArg Arg a
v)


instance Semigroup (Match a) where
    -- @NotBlocked (StuckOn e)@ means blocked by a variable.
    -- In this case, no instantiation of meta-variables will make progress.
    DontKnow Blocked ()
b <> :: Match a -> Match a -> Match a
<> DontKnow Blocked ()
b'      = forall a. Blocked () -> Match a
DontKnow forall a b. (a -> b) -> a -> b
$ Blocked ()
b forall a. Semigroup a => a -> a -> a
<> Blocked ()
b'
    DontKnow Blocked ()
m <> Match a
_                = forall a. Blocked () -> Match a
DontKnow Blocked ()
m
    Match a
_          <> DontKnow Blocked ()
m       = forall a. Blocked () -> Match a
DontKnow Blocked ()
m
    -- One could imagine DontKnow _ <> No = No, but would break the
    -- equivalence to case-trees (Issue 2964).
    Match a
No         <> Match a
_                = forall a. Match a
No
    Match a
_          <> Match a
No               = forall a. Match a
No
    Yes Simplification
s IntMap (Arg a)
us   <> Yes Simplification
s' IntMap (Arg a)
vs        = forall a. Simplification -> IntMap (Arg a) -> Match a
Yes (Simplification
s forall a. Semigroup a => a -> a -> a
<> Simplification
s') (IntMap (Arg a)
us forall a. Semigroup a => a -> a -> a
<> IntMap (Arg a)
vs)

instance Monoid (Match a) where
    mempty :: Match a
mempty = forall a. Null a => a
empty
    mappend :: Match a -> Match a -> Match a
mappend = 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
      ([], []) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Null a => a
empty, [])
      (p
p : [p]
ps, v
v : [v]
vs) -> do
        (Match Term
r, v
v') <- p -> v -> m (Match Term, v)
match p
p v
v
        case Match Term
r of
          Match Term
No | Just{} <- forall a. IsProjP a => a -> Maybe (ProjOrigin, AmbiguousQName)
isProjP p
p -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Match a
No, v
v' forall a. a -> [a] -> [a]
: [v]
vs)
          Match Term
No -> 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.
            (Match Term
r', [v]
_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.
            forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
r forall a. Semigroup a => a -> a -> a
<> Match Term
r', v
v' forall a. a -> [a] -> [a]
: [v]
vs)
          DontKnow Blocked ()
m -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Blocked () -> Match a
DontKnow Blocked ()
m, v
v' forall a. a -> [a] -> [a]
: [v]
vs)
          Yes{} -> do
            (Match Term
r', [v]
vs') <- [p] -> [v] -> m (Match Term, [v])
loop [p]
ps [v]
vs
            forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
r forall a. Semigroup a => a -> a -> a
<> Match Term
r', v
v' forall a. a -> [a] -> [a]
: [v]
vs')
      ([p], [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 = forall a. Arg a -> Elim' a
Apply Arg Term
arg
mergeElim (IApply Term
x Term
y Term
_) Arg Term
arg = forall a. a -> a -> a -> Elim' a
IApply Term
x Term
y (forall e. Arg e -> e
unArg Arg Term
arg)
mergeElim Proj{} Arg Term
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

mergeElims :: [Elim] -> [Arg Term] -> [Elim]
mergeElims :: [Elim] -> [Arg Term] -> [Elim]
mergeElims = 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
  forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc VerboseKey
"tc.match" Int
50
    (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"matchCopatterns"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NamedArg a -> a
namedArg) [NamedArg DeBruijnPattern]
ps)
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Elim]
vs)
          ]) forall a b. (a -> b) -> a -> b
$ do
  -- Buggy, see issue 1124:
  -- mapFst mconcat . unzip <$> zipWithM' (matchCopattern . namedArg) ps vs
  forall (m :: * -> *) p v.
(IsProjP p, MonadMatch m) =>
(p -> v -> m (Match Term, v)) -> [p] -> [v] -> m (Match Term, [v])
foldMatch (forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Elim -> m (Match Term, Elim)
matchCopattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
  QName
p <- forall a (m :: * -> *).
(NormaliseProjP a, HasConstInfo m) =>
a -> m a
normaliseProjP DeBruijnPattern
pat forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
         ProjP ProjOrigin
_ QName
p -> QName
p
         DeBruijnPattern
_         -> forall a. HasCallStack => a
__IMPOSSIBLE__
  QName
q       <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
getOriginalProjection QName
q
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if QName
p forall a. Eq a => a -> a -> Bool
== QName
q then (forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
YesSimplification forall a. Null a => a
empty, Elim
elim)
                     else (forall a. Match a
No,                          Elim
elim)
-- The following two cases are not impossible, see #2964
matchCopattern ProjP{} elim :: Elim
elim@Apply{}   = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Match a
No , Elim
elim)
matchCopattern DeBruijnPattern
_       elim :: Elim
elim@Proj{}    = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Match a
No , Elim
elim)
matchCopattern DeBruijnPattern
p       (Apply Arg Term
v) = forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd forall a. Arg a -> Elim' a
Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) = forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (Elim -> Arg Term -> Elim
mergeElim Elim
e) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
matchPattern DeBruijnPattern
p (forall a. a -> Arg a
defaultArg Term
r)

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
  forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m ()
reportSDoc VerboseKey
"tc.match" Int
20 forall a b. (a -> b) -> a -> b
$
     forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"matchPatterns"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *).
MonadPretty m =>
[NamedArg DeBruijnPattern] -> m Doc
prettyTCMPatternList [NamedArg DeBruijnPattern]
ps
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs)
          ]

  forall (m :: * -> *) a.
MonadDebug m =>
VerboseKey -> Int -> TCMT IO Doc -> m a -> m a
traceSDoc VerboseKey
"tc.match" Int
50
    (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat [ TCMT IO Doc
"matchPatterns"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"ps =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (m :: * -> *). Applicative m => VerboseKey -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> VerboseKey
show) [NamedArg DeBruijnPattern]
ps)
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"vs =" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
fsep (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Semigroup (m Doc), Foldable t) =>
m Doc -> t (m Doc) -> [m Doc]
punctuate forall (m :: * -> *). Applicative m => m Doc
comma forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [Arg Term]
vs)
          ]) forall a b. (a -> b) -> a -> b
$ do
  -- Buggy, see issue 1124:
  -- (ms,vs) <- unzip <$> zipWithM' (matchPattern . namedArg) ps vs
  -- return (mconcat ms, vs)
  forall (m :: * -> *) p v.
(IsProjP p, MonadMatch m) =>
(p -> v -> m (Match Term, v)) -> [p] -> [v] -> m (Match Term, [v])
foldMatch (forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
matchPattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = case (DeBruijnPattern
p, Arg Term
u) of
  (ProjP{}, Arg Term
_            ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
  (IApplyP PatternInfo
_ Term
_ Term
_ DBPatVar
x , Arg Term
arg ) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification IntMap (Arg Term)
entry, Arg Term
arg)
    where entry :: IntMap (Arg Term)
entry = forall el coll. Singleton el coll => el -> coll
singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
x, Arg Term
arg)
  (VarP PatternInfo
_ DBPatVar
x , Arg Term
arg          ) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification IntMap (Arg Term)
entry, Arg Term
arg)
    where entry :: IntMap (Arg Term)
entry = 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)) -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification forall a. Null a => a
empty, Arg Term
arg)
  (LitP PatternInfo
_ Literal
l , arg :: Arg Term
arg@(Arg ArgInfo
_ Term
v)) -> do
    Blocked Term
w <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
v
    let arg' :: Arg Term
arg' = Arg Term
arg forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
w
    case Blocked Term
w of
      NotBlocked NotBlocked' Term
_ (Lit Literal
l')
          | Literal
l forall a. Eq a => a -> a -> Bool
== Literal
l'            -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
YesSimplification forall a. Null a => a
empty , Arg Term
arg')
          | Bool
otherwise          -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Match a
No                          , Arg Term
arg')
      Blocked Blocker
b Term
_              -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Blocked () -> Match a
DontKnow forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b ()     , Arg Term
arg')
      NotBlocked NotBlocked' Term
r Term
t           -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Blocked () -> Match a
DontKnow forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
r' () , Arg Term
arg')
        where r' :: NotBlocked' Term
r' = forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
stuckOn (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
    if Bool -> Bool
not (ConPatternInfo -> Bool
conPRecord ConPatternInfo
cpi) then forall (m :: * -> *).
MonadMatch m =>
ConHead
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback ConHead
c [NamedArg DeBruijnPattern]
ps (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v) else do
    forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe [Arg QName])
isEtaRecordCon (ConHead -> QName
conName ConHead
c) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe [Arg QName]
Nothing -> forall (m :: * -> *).
MonadMatch m =>
ConHead
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback ConHead
c [NamedArg DeBruijnPattern]
ps (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v)
      Just [Arg QName]
fs -> do
        -- 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).
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Int
size [Arg QName]
fs forall a. Eq a => a -> a -> Bool
== forall a. Sized a => a -> Int
size [NamedArg DeBruijnPattern]
ps) forall a. HasCallStack => a
__IMPOSSIBLE__
        forall b d a. (b -> d) -> (a, b) -> (a, d)
mapSnd (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c (ConPatternInfo -> ConInfo
fromConPatternInfo ConPatternInfo
cpi) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
          forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern]
-> [Arg Term] -> m (Match Term, [Arg Term])
matchPatterns [NamedArg DeBruijnPattern]
ps forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
for [Arg QName]
fs forall a b. (a -> b) -> a -> b
$ \ (Arg ArgInfo
ai QName
f) -> forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
ai forall a b. (a -> b) -> a -> b
$ Term
v forall t. Apply t => t -> [Elim] -> t
`applyE` [forall a. ProjOrigin -> QName -> Elim' a
Proj ProjOrigin
ProjSystem QName
f]
    where
    isEtaRecordCon :: HasConstInfo m => QName -> m (Maybe [Arg QName])
    isEtaRecordCon :: forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe [Arg QName])
isEtaRecordCon QName
c = do
      (Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Constructor{ conData :: Defn -> QName
conData = QName
d } -> do
          (Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
d) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            r :: Defn
r@Record{ recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs } | HasEta' PatternOrCopattern
YesEta <- Defn -> HasEta' PatternOrCopattern
recEtaEquality Defn
r -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall t a. Dom' t a -> Arg a
argFromDom [Dom QName]
fs
            Defn
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        Defn
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
  (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 forall a. Eq a => a -> a -> Bool
== QName
q' = forall a. a -> Maybe a
Just (QName -> [Elim] -> Term
Def QName
q, [Elim]
vs)
        f Term
_                     = forall a. Maybe a
Nothing
    forall (m :: * -> *).
MonadMatch m =>
(Term -> Maybe ([Elim] -> Term, [Elim]))
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback' Term -> Maybe ([Elim] -> Term, [Elim])
f [NamedArg DeBruijnPattern]
ps Arg Term
v
 where
    -- Default: not an eta record constructor.
  fallback :: MonadMatch m
           => ConHead -> [NamedArg DeBruijnPattern] -> Arg Term -> m (Match Term, Arg Term)
  fallback :: forall (m :: * -> *).
MonadMatch m =>
ConHead
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback ConHead
c [NamedArg DeBruijnPattern]
ps Arg Term
v = do
    let f :: Term -> Maybe ([Elim] -> Term, [Elim])
f (Con ConHead
c' ConInfo
ci' [Elim]
vs) | ConHead
c forall a. Eq a => a -> a -> Bool
== ConHead
c' = forall a. a -> Maybe a
Just (ConHead -> ConInfo -> [Elim] -> Term
Con ConHead
c' ConInfo
ci',[Elim]
vs)
        f Term
_                         = forall a. Maybe a
Nothing
    forall (m :: * -> *).
MonadMatch m =>
(Term -> Maybe ([Elim] -> Term, [Elim]))
-> [NamedArg DeBruijnPattern]
-> Arg Term
-> m (Match Term, Arg Term)
fallback' Term -> Maybe ([Elim] -> Term, [Elim])
f [NamedArg DeBruijnPattern]
ps Arg Term
v

  -- Regardless of blocking, constructors and a properly applied @hcomp@
  -- can be matched on.
  isMatchable' :: HasBuiltins m => m (Blocked Term -> Maybe Term)
  isMatchable' :: forall (m :: * -> *).
HasBuiltins m =>
m (Blocked Term -> Maybe Term)
isMatchable' = do
    [Maybe QName
mhcomp,Maybe QName
mconid] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *).
HasBuiltins m =>
VerboseKey -> m (Maybe QName)
getName' [VerboseKey
builtinHComp, VerboseKey
builtinConId]
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ Blocked Term
r ->
      case forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
r of
        t :: Term
t@Con{} -> forall a. a -> Maybe a
Just Term
t
        t :: Term
t@(Def QName
q [Elim
l,Elim
a,Elim
phi,Elim
u,Elim
u0]) | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mhcomp
                -> forall a. a -> Maybe a
Just Term
t
        t :: Term
t@(Def QName
q [Elim
l,Elim
a,Elim
x,Elim
y,Elim
phi,Elim
p]) | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mconid
                -> forall a. a -> Maybe a
Just Term
t
        -- TODO this covers the transpIx functions, but it's a hack.
        t :: Term
t@(Def QName
q [Elim]
_) | NotBlocked{blockingStatus :: forall t a. Blocked' t a -> NotBlocked' t
blockingStatus = MissingClauses QName
_} <- Blocked Term
r -> forall a. a -> Maybe a
Just Term
t
        Term
_       -> forall a. Maybe a
Nothing

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

        Blocked Term
w <- 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
        -- 1) it does not hurt to do it all the time, and
        -- 2) whatInduction c sometimes crashes because c may point to
        --    an axiom at this stage (if we are checking the
        --    projection functions for a record type).
{-
        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.
        Blocked Term
w <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< case Blocked Term
w of
               NotBlocked NotBlocked' Term
r Term
u -> forall (m :: * -> *) a. MonadReduce m => ReduceM a -> m a
liftReduce forall a b. (a -> b) -> a -> b
$ Term -> ReduceM (Blocked Term)
unfoldCorecursion Term
u  -- Andreas, 2014-06-12 TODO: r == ReallyNotBlocked sufficient?
               Blocked Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Blocked Term
w
        let v :: Term
v = forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
w
            arg :: Arg Term
arg = forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v  -- the reduced argument

        case Blocked Term
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
                (Match Term
m, [Arg Term]
vs1) <- forall a b. (Match a, b) -> (Match a, b)
yesSimplification forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern]
-> [Arg Term] -> m (Match Term, [Arg Term])
matchPatterns [NamedArg DeBruijnPattern]
ps (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims [Elim]
vs)
                forall (m :: * -> *) a. Monad m => a -> m a
return (Match Term
m, forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info forall a b. (a -> b) -> a -> b
$ [Elim] -> Term
bld ([Elim] -> [Arg Term] -> [Elim]
mergeElims [Elim]
vs [Arg Term]
vs1))
              Maybe ([Elim] -> Term, [Elim])
Nothing
                                    -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Match a
No                          , Arg Term
arg)
          Blocked Blocker
b Term
_               -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Blocked () -> Match a
DontKnow forall a b. (a -> b) -> a -> b
$ forall t a. Blocker -> a -> Blocked' t a
Blocked Blocker
b ()     , Arg Term
arg)
          NotBlocked NotBlocked' Term
r Term
_            -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Blocked () -> Match a
DontKnow forall a b. (a -> b) -> a -> b
$ forall t a. NotBlocked' t -> a -> Blocked' t a
NotBlocked NotBlocked' Term
r' () , Arg Term
arg)
            where r' :: NotBlocked' Term
r' = forall t. Elim' t -> NotBlocked' t -> NotBlocked' t
stuckOn (forall a. Arg a -> Elim' a
Apply Arg Term
arg) NotBlocked' Term
r

-- ASR (08 November 2014). The type of the function could be
--
-- @(Match Term, [Arg Term]) -> (Match Term, [Arg Term])@.
yesSimplification :: (Match a, b) -> (Match a, b)
yesSimplification :: forall a b. (Match a, b) -> (Match a, b)
yesSimplification (Yes Simplification
_ IntMap (Arg a)
vs, b
us) = (forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
YesSimplification IntMap (Arg a)
vs, b
us)
yesSimplification (Match a, b)
r              = (Match a, b)
r

-- 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
  (Match Term
m, Arg Term
arg) <- forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
matchPattern DeBruijnPattern
p (forall e. ArgInfo -> e -> Arg e
Arg ArgInfo
info Term
v)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo) Match Term
m
matchPatternP DeBruijnPattern
p arg :: Arg DeBruijnPattern
arg@(Arg ArgInfo
info DeBruijnPattern
q) = do
  let varMatch :: DBPatVar -> m (Match DeBruijnPattern)
varMatch DBPatVar
x = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton (DBPatVar -> Int
dbPatVarIndex DBPatVar
x, Arg DeBruijnPattern
arg)
      termMatch :: m (Match DeBruijnPattern)
termMatch  = do
        (Match Term
m, Arg Term
arg) <- forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg Term -> m (Match Term, Arg Term)
matchPattern DeBruijnPattern
p (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DeBruijnPattern -> Term
patternToTerm Arg DeBruijnPattern
arg)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall x. PatternInfo -> Term -> Pattern' x
DotP PatternInfo
defaultPatternInfo) Match Term
m
  case DeBruijnPattern
p of
    ProjP{}         -> 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
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Simplification -> IntMap (Arg a) -> Match a
Yes Simplification
NoSimplification 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 forall a. Eq a => a -> a -> Bool
== ConHead
c'   -> forall (m :: * -> *).
MonadMatch m =>
[NamedArg DeBruijnPattern]
-> [Arg DeBruijnPattern] -> m (Match DeBruijnPattern)
matchPatternsP [NamedArg DeBruijnPattern]
ps ((forall a b. (a -> b) -> [a] -> [b]
map forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall name a. Named name a -> a
namedThing [NamedArg DeBruijnPattern]
qs)
                     | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Match a
No
        LitP{} -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {x} {a}. Pattern' x -> Pattern' a
toLitP 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)) = forall a. Literal -> Pattern' a
litP Literal
l   -- All bindings should be to literals
                toLitP Pattern' x
_                = 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
  forall a. Monoid a => [a] -> a
mconcat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM forall (m :: * -> *).
MonadMatch m =>
DeBruijnPattern -> Arg DeBruijnPattern -> m (Match DeBruijnPattern)
matchPatternP (forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg [NamedArg DeBruijnPattern]
ps) [Arg DeBruijnPattern]
qs