3
module Agda.TypeChecking.Patterns.Match where
7
import Data.Traversable
9
import Agda.Syntax.Common
10
import Agda.Syntax.Internal
11
import Agda.Syntax.Literal
13
import Agda.TypeChecking.Reduce
14
import Agda.TypeChecking.Monad
15
import Agda.TypeChecking.Monad.Builtin
16
import Agda.TypeChecking.Primitive
18
import Agda.Utils.Monad
20
#include "../../undefined.h"
21
import Agda.Utils.Impossible
23
-- | If matching is inconclusive (@DontKnow@) we want to know whether
24
-- it is due to a particular meta variable.
25
data Match = Yes [Term] | No | DontKnow (Maybe MetaId)
27
instance Monoid Match where
30
Yes us `mappend` Yes vs = Yes (us ++ vs)
31
Yes _ `mappend` No = No
32
Yes _ `mappend` DontKnow m = DontKnow m
35
-- Nothing means blocked by a variable. In this case no instantiation of
36
-- meta-variables will make progress.
37
DontKnow _ `mappend` DontKnow Nothing = DontKnow Nothing
39
-- One could imagine DontKnow _ `mappend` No = No, but would break the
40
-- equivalence to case-trees.
41
DontKnow m `mappend` _ = DontKnow m
43
matchPatterns :: MonadTCM tcm => [Arg Pattern] -> [Arg Term] -> tcm (Match, [Arg Term])
45
do (ms,vs) <- unzip <$> zipWithM' matchPattern ps vs
46
return (mconcat ms, vs)
48
matchPattern :: MonadTCM tcm => Arg Pattern -> Arg Term -> tcm (Match, Arg Term)
49
matchPattern (Arg h' (VarP _)) arg@(Arg _ v) = return (Yes [v], arg)
50
matchPattern (Arg _ (DotP _)) arg@(Arg _ v) = return (Yes [v], arg)
51
matchPattern (Arg h' (LitP l)) arg@(Arg h v) = do
53
let v = ignoreBlocking w
56
| l == l' -> return (Yes [], Arg h v)
57
| otherwise -> return (No, Arg h v)
58
NotBlocked (MetaV x _) -> return (DontKnow $ Just x, Arg h v)
59
Blocked x _ -> return (DontKnow $ Just x, Arg h v)
60
_ -> return (DontKnow Nothing, Arg h v)
61
matchPattern (Arg h' (ConP c ps)) (Arg h v) =
62
do w <- traverse constructorForm =<< reduceB v
63
-- Unfold delayed (corecursive) definitions one step. This is
64
-- only necessary if c is a coinductive constructor, but
65
-- 1) it does not hurt to do it all the time, and
66
-- 2) whatInduction c sometimes crashes because c may point to
67
-- an axiom at this stage (if we are checking the
68
-- projection functions for a record type).
70
NotBlocked (Def f args) ->
71
unfoldDefinition True reduceB (Def f []) f args
72
-- reduceB is used here because some constructors
73
-- are actually definitions which need to be
74
-- unfolded (due to open public).
76
let v = ignoreBlocking w
78
NotBlocked (Con c' vs)
80
(m, vs) <- matchPatterns ps vs
81
return (m, Arg h $ Con c' vs)
82
| otherwise -> return (No, Arg h v)
83
NotBlocked (MetaV x vs) -> return (DontKnow $ Just x, Arg h v)
84
Blocked x _ -> return (DontKnow $ Just x, Arg h v)
85
_ -> return (DontKnow Nothing, Arg h v)
added
removed
src/full/Agda/TypeChecking/Patterns/Match.hs
