1{-# LANGUAGE NondecreasingIndentation #-}
2
3-- | Pattern matcher used in the reducer for clauses that
4--   have not been compiled to case trees yet.
5
6module Agda.TypeChecking.Patterns.Match where
7
8import Prelude hiding (null)
9
10import Control.Monad
11import Data.IntMap (IntMap)
12import qualified Data.IntMap as IntMap
13
14import Agda.Syntax.Common
15import Agda.Syntax.Internal
16import Agda.Syntax.Internal.Pattern
17
18import Agda.TypeChecking.Reduce
19import Agda.TypeChecking.Reduce.Monad
20import Agda.TypeChecking.Substitute
21import Agda.TypeChecking.Monad hiding (constructorForm)
22import Agda.TypeChecking.Pretty
23import Agda.TypeChecking.Records
24
25import Agda.Utils.Empty
26import Agda.Utils.Functor (for, ($>), (<&>))
27import Agda.Utils.Maybe
28import Agda.Utils.Null
29import Agda.Utils.Singleton
30import Agda.Utils.Size
31import Agda.Utils.Tuple
32
33import Agda.Utils.Impossible
34
35-- | If matching is inconclusive (@DontKnow@) we want to know whether
36--   it is due to a particular meta variable.
37data Match a = Yes Simplification (IntMap (Arg a))
38             | No
39             | DontKnow (Blocked ())
40  deriving Functor
41
42instance Null (Match a) where
43  empty = Yes empty empty
44  null (Yes simpl as) = null simpl && null as
45  null _              = False
46
47matchedArgs :: Empty -> Int -> IntMap (Arg a) -> [Arg a]
48matchedArgs err n vs = map (fromMaybe (absurd err)) $ matchedArgs' n vs
49
50matchedArgs' :: Int -> IntMap (Arg a) -> [Maybe (Arg a)]
51matchedArgs' n vs = map get [0 .. n - 1]
52  where
53    get k = IntMap.lookup k vs
54
55-- | Builds a proper substitution from an IntMap produced by match(Co)patterns
56buildSubstitution :: (DeBruijn a)
57                  => Impossible -> Int -> IntMap (Arg a) -> Substitution' a
58buildSubstitution err n vs = foldr cons idS $ matchedArgs' n vs
59  where cons Nothing  = Strengthen err
60        cons (Just v) = consS (unArg v)
61
62
63instance Semigroup (Match a) where
64    -- @NotBlocked (StuckOn e)@ means blocked by a variable.
65    -- In this case, no instantiation of meta-variables will make progress.
66    DontKnow b <> DontKnow b'      = DontKnow $ b <> b'
67    DontKnow m <> _                = DontKnow m
68    _          <> DontKnow m       = DontKnow m
69    -- One could imagine DontKnow _ <> No = No, but would break the
70    -- equivalence to case-trees (Issue 2964).
71    No         <> _                = No
72    _          <> No               = No
73    Yes s us   <> Yes s' vs        = Yes (s <> s') (us <> vs)
74
75instance Monoid (Match a) where
76    mempty = empty
77    mappend = (<>)
78
79-- | Instead of 'zipWithM', we need to use this lazy version
80--   of combining pattern matching computations.
81
82-- Andreas, 2014-05-08, see Issue 1124:
83--
84-- Due to a bug in TypeChecking.Patterns.Match
85-- a failed match of (C n b) against (C O unit)
86-- turned into (C n unit).
87-- This was because all patterns were matched in
88-- parallel, and evaluations of successfull matches
89-- (and a record constructor like unit can always
90-- be successfully matched) were returned, leading
91-- to a reassembly of (C n b) as (C n unit) which is
92-- illtyped.
93
94-- Now patterns are matched left to right and
95-- upon failure, no further matching is performed.
96
97foldMatch
98  :: forall m p v . (IsProjP p, MonadMatch m)
99  => (p -> v -> m (Match Term, v))
100  -> [p] -> [v] -> m (Match Term, [v])
101foldMatch match = loop where
102  loop :: [p] -> [v] -> m (Match Term, [v])
103  loop ps0 vs0 = do
104    case (ps0, vs0) of
105      ([], []) -> return (empty, [])
106      (p : ps, v : vs) -> do
107        (r, v') <- match p v
108        case r of
109          No | Just{} <- isProjP p -> return (No, v' : vs)
110          No -> do
111            -- Issue 2964: Even when the first pattern doesn't match we should
112            -- continue to the next patterns (and potentially block on them)
113            -- because the splitting order in the case tree may not be
114            -- left-to-right.
115            (r', _vs') <- loop ps vs
116            -- Issue 2968: do not use vs' here, because it might
117            -- contain ill-typed terms due to eta-expansion at wrong
118            -- type.
119            return (r <> r', v' : vs)
120          DontKnow m -> return (DontKnow m, v' : vs)
121          Yes{} -> do
122            (r', vs') <- loop ps vs
123            return (r <> r', v' : vs')
124      _ -> __IMPOSSIBLE__
125
126
127-- TODO refactor matchPattern* to work with Elim instead.
128mergeElim :: Elim -> Arg Term -> Elim
129mergeElim Apply{} arg = Apply arg
130mergeElim (IApply x y _) arg = IApply x y (unArg arg)
131mergeElim Proj{} _ = __IMPOSSIBLE__
132
133mergeElims :: [Elim] -> [Arg Term] -> [Elim]
134mergeElims = zipWith mergeElim
135
136type MonadMatch m = PureTCM m
137
138-- | @matchCopatterns ps es@ matches spine @es@ against copattern spine @ps@.
139--
140--   Returns 'Yes' and a substitution for the pattern variables
141--   (in form of IntMap Term) if matching was successful.
142--
143--   Returns 'No' if there was a constructor or projection mismatch.
144--
145--   Returns 'DontKnow' if an argument could not be evaluated to
146--   constructor form because of a blocking meta variable.
147--
148--   In any case, also returns spine @es@ in reduced form
149--   (with all the weak head reductions performed that were necessary
150--   to come to a decision).
151matchCopatterns :: MonadMatch m
152                => [NamedArg DeBruijnPattern]
153                -> [Elim]
154                -> m (Match Term, [Elim])
155matchCopatterns ps vs = do
156  traceSDoc "tc.match" 50
157    (vcat [ "matchCopatterns"
158          , nest 2 $ "ps =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) ps)
159          , nest 2 $ "vs =" <+> fsep (punctuate comma $ map prettyTCM vs)
160          ]) $ do
161  -- Buggy, see issue 1124:
162  -- mapFst mconcat . unzip <$> zipWithM' (matchCopattern . namedArg) ps vs
163  foldMatch (matchCopattern . namedArg) ps vs
164
165-- | Match a single copattern.
166matchCopattern :: MonadMatch m
167               => DeBruijnPattern
168               -> Elim
169               -> m (Match Term, Elim)
170matchCopattern pat@ProjP{} elim@(Proj _ q) = do
171  p <- normaliseProjP pat <&> \case
172         ProjP _ p -> p
173         _         -> __IMPOSSIBLE__
174  q       <- getOriginalProjection q
175  return $ if p == q then (Yes YesSimplification empty, elim)
176                     else (No,                          elim)
177-- The following two cases are not impossible, see #2964
178matchCopattern ProjP{} elim@Apply{}   = return (No , elim)
179matchCopattern _       elim@Proj{}    = return (No , elim)
180matchCopattern p       (Apply v) = mapSnd Apply <$> matchPattern p v
181matchCopattern p       e@(IApply x y r) = mapSnd (mergeElim e) <$> matchPattern p (defaultArg r)
182
183matchPatterns :: MonadMatch m
184              => [NamedArg DeBruijnPattern]
185              -> [Arg Term]
186              -> m (Match Term, [Arg Term])
187matchPatterns ps vs = do
188  reportSDoc "tc.match" 20 $
189     vcat [ "matchPatterns"
190          , nest 2 $ "ps =" <+> prettyTCMPatternList ps
191          , nest 2 $ "vs =" <+> fsep (punctuate comma $ map prettyTCM vs)
192          ]
193
194  traceSDoc "tc.match" 50
195    (vcat [ "matchPatterns"
196          , nest 2 $ "ps =" <+> fsep (punctuate comma $ map (text . show) ps)
197          , nest 2 $ "vs =" <+> fsep (punctuate comma $ map prettyTCM vs)
198          ]) $ do
199  -- Buggy, see issue 1124:
200  -- (ms,vs) <- unzip <$> zipWithM' (matchPattern . namedArg) ps vs
201  -- return (mconcat ms, vs)
202  foldMatch (matchPattern . namedArg) ps vs
203
204-- | Match a single pattern.
205matchPattern :: MonadMatch m
206             => DeBruijnPattern
207             -> Arg Term
208             -> m (Match Term, Arg Term)
209matchPattern p u = case (p, u) of
210  (ProjP{}, _            ) -> __IMPOSSIBLE__
211  (IApplyP _ _ _ x , arg ) -> return (Yes NoSimplification entry, arg)
212    where entry = singleton (dbPatVarIndex x, arg)
213  (VarP _ x , arg          ) -> return (Yes NoSimplification entry, arg)
214    where entry = singleton (dbPatVarIndex x, arg)
215  (DotP _ _ , arg@(Arg _ v)) -> return (Yes NoSimplification empty, arg)
216  (LitP _ l , arg@(Arg _ v)) -> do
217    w <- reduceB v
218    let arg' = arg $> ignoreBlocking w
219    case w of
220      NotBlocked _ (Lit l')
221          | l == l'            -> return (Yes YesSimplification empty , arg')
222          | otherwise          -> return (No                          , arg')
223      Blocked b _              -> return (DontKnow $ Blocked b ()     , arg')
224      NotBlocked r t           -> return (DontKnow $ NotBlocked r' () , arg')
225        where r' = stuckOn (Apply arg') r
226
227  -- Case constructor pattern.
228  (ConP c cpi ps, Arg info v) -> do
229    if not (conPRecord cpi) then fallback c ps (Arg info v) else do
230    isEtaRecordCon (conName c) >>= \case
231      Nothing -> fallback c ps (Arg info v)
232      Just fs -> do
233        -- Case: Eta record constructor.
234        -- This case is necessary if we want to use the clauses before
235        -- record pattern translation (e.g., in type-checking definitions by copatterns).
236        unless (size fs == size ps) __IMPOSSIBLE__
237        mapSnd (Arg info . Con c (fromConPatternInfo cpi) . map Apply) <$> do
238          matchPatterns ps $ for fs $ \ (Arg ai f) -> Arg ai $ v `applyE` [Proj ProjSystem f]
239    where
240    isEtaRecordCon :: HasConstInfo m => QName -> m (Maybe [Arg QName])
241    isEtaRecordCon c = do
242      (theDef <$> getConstInfo c) >>= \case
243        Constructor{ conData = d } -> do
244          (theDef <$> getConstInfo d) >>= \case
245            r@Record{ recFields = fs } | YesEta <- recEtaEquality r -> return $ Just $ map argFromDom fs
246            _ -> return Nothing
247        _ -> __IMPOSSIBLE__
248  (DefP o q ps, v) -> do
249    let f (Def q' vs) | q == q' = Just (Def q, vs)
250        f _                     = Nothing
251    fallback' f ps v
252 where
253    -- Default: not an eta record constructor.
254  fallback :: MonadMatch m
255           => ConHead -> [NamedArg DeBruijnPattern] -> Arg Term -> m (Match Term, Arg Term)
256  fallback c ps v = do
257    let f (Con c' ci' vs) | c == c' = Just (Con c' ci',vs)
258        f _                         = Nothing
259    fallback' f ps v
260
261  -- Regardless of blocking, constructors and a properly applied @hcomp@
262  -- can be matched on.
263  isMatchable' :: HasBuiltins m => m (Blocked Term -> Maybe Term)
264  isMatchable' = do
265    mhcomp <- getName' builtinHComp
266    return $ \ r ->
267      case ignoreBlocking r of
268        t@Con{} -> Just t
269        t@(Def q [l,a,phi,u,u0]) | Just q == mhcomp
270                -> Just t
271        _       -> Nothing
272
273  -- DefP hcomp and ConP matching.
274  fallback' :: MonadMatch m
275            => (Term -> Maybe (Elims -> Term , Elims))
276            -> [NamedArg DeBruijnPattern]
277            -> Arg Term
278            -> m (Match Term, Arg Term)
279  fallback' mtc ps (Arg info v) = do
280        isMatchable <- isMatchable'
281
282        w <- reduceB v
283        -- Unfold delayed (corecursive) definitions one step. This is
284        -- only necessary if c is a coinductive constructor, but
285        -- 1) it does not hurt to do it all the time, and
286        -- 2) whatInduction c sometimes crashes because c may point to
287        --    an axiom at this stage (if we are checking the
288        --    projection functions for a record type).
289{-
290        w <- case w of
291               NotBlocked r (Def f es) ->   -- Andreas, 2014-06-12 TODO: r == ReallyNotBlocked sufficient?
292                 unfoldDefinitionE True reduceB' (Def f []) f es
293                   -- reduceB is used here because some constructors
294                   -- are actually definitions which need to be
295                   -- unfolded (due to open public).
296               _ -> return w
297-}
298        -- Jesper, 23-06-2016: Note that unfoldCorecursion may destroy
299        -- constructor forms, so we only call constructorForm after.
300        w <- traverse constructorForm =<< case w of
301               NotBlocked r u -> liftReduce $ unfoldCorecursion u  -- Andreas, 2014-06-12 TODO: r == ReallyNotBlocked sufficient?
302               _ -> return w
303        let v = ignoreBlocking w
304            arg = Arg info v  -- the reduced argument
305
306        case w of
307          b | Just t <- isMatchable b ->
308            case mtc t of
309              Just (bld, vs) -> do
310                (m, vs1) <- yesSimplification <$> matchPatterns ps (fromMaybe __IMPOSSIBLE__ $ allApplyElims vs)
311                return (m, Arg info $ bld (mergeElims vs vs1))
312              Nothing
313                                    -> return (No                          , arg)
314          Blocked b _               -> return (DontKnow $ Blocked b ()     , arg)
315          NotBlocked r _            -> return (DontKnow $ NotBlocked r' () , arg)
316            where r' = stuckOn (Apply arg) r
317
318-- ASR (08 November 2014). The type of the function could be
319--
320-- @(Match Term, [Arg Term]) -> (Match Term, [Arg Term])@.
321yesSimplification :: (Match a, b) -> (Match a, b)
322yesSimplification (Yes _ vs, us) = (Yes YesSimplification vs, us)
323yesSimplification r              = r
324
325-- Matching patterns against patterns -------------------------------------
326
327-- | Match a single pattern.
328matchPatternP :: MonadMatch m
329              => DeBruijnPattern
330              -> Arg DeBruijnPattern
331              -> m (Match DeBruijnPattern)
332matchPatternP p (Arg info (DotP _ v)) = do
333  (m, arg) <- matchPattern p (Arg info v)
334  return $ fmap (DotP defaultPatternInfo) m
335matchPatternP p arg@(Arg info q) = do
336  let varMatch x = return $ Yes NoSimplification $ singleton (dbPatVarIndex x, arg)
337      termMatch  = do
338        (m, arg) <- matchPattern p (fmap patternToTerm arg)
339        return $ fmap (DotP defaultPatternInfo) m
340  case p of
341    ProjP{}         -> __IMPOSSIBLE__
342    IApplyP _ _ _ x -> varMatch x
343    VarP _ x        -> varMatch x
344    DotP _ _        -> return $ Yes NoSimplification empty
345    LitP{}          -> termMatch -- Literal patterns bind no variables so we can fall back to the Term version.
346    DefP{}          -> termMatch
347
348    ConP c cpi ps ->
349      case q of
350        ConP c' _ qs | c == c'   -> matchPatternsP ps ((map . fmap) namedThing qs)
351                     | otherwise -> return No
352        LitP{} -> fmap toLitP <$> termMatch
353          where toLitP (DotP _ (Lit l)) = litP l   -- All bindings should be to literals
354                toLitP _                = __IMPOSSIBLE__
355        _      -> termMatch
356
357matchPatternsP :: MonadMatch m
358               => [NamedArg DeBruijnPattern]
359               -> [Arg DeBruijnPattern]
360               -> m (Match DeBruijnPattern)
361matchPatternsP ps qs = do
362  mconcat <$> zipWithM matchPatternP (map namedArg ps) qs
363