21
21
import Agda.Utils.Size
22
22
import Agda.Utils.Tuple
24
#include "../../undefined.h"
24
#include "undefined.h"
25
25
import Agda.Utils.Impossible
27
27
-- | If matching is inconclusive (@DontKnow@) we want to know whether
28
28
-- it is due to a particular meta variable.
29
data Match a = Yes Simplification [a] | No | DontKnow (Maybe MetaId)
29
data Match a = Yes Simplification [a]
31
| DontKnow (Maybe MetaId)
32
34
instance Monoid (Match a) where
33
35
mempty = Yes mempty []
35
37
Yes s us `mappend` Yes s' vs = Yes (s `mappend` s') (us ++ vs)
36
38
Yes _ _ `mappend` No = No
37
39
Yes _ _ `mappend` DontKnow m = DontKnow m
40
42
-- Nothing means blocked by a variable. In this case no instantiation of
41
43
-- meta-variables will make progress.
44
46
-- One could imagine DontKnow _ `mappend` No = No, but would break the
45
47
-- equivalence to case-trees.
46
DontKnow m `mappend` _ = DontKnow m
48
DontKnow m `mappend` _ = DontKnow m
48
50
-- | Instead of 'zipWithM', we need to use this lazy version
49
51
-- of combining pattern matching computations.
142
144
let arg' = arg $> ignoreBlocking w
143
145
case ignoreSharing <$> w of
145
| l == l' -> return (Yes YesSimplification [] , arg')
146
| otherwise -> return (No , arg')
147
NotBlocked (MetaV x _) -> return (DontKnow $ Just x , arg')
148
Blocked x _ -> return (DontKnow $ Just x , arg')
149
_ -> return (DontKnow Nothing , arg')
147
| l == l' -> return (Yes YesSimplification [] , arg')
148
| otherwise -> return (No , arg')
149
NotBlocked (MetaV x _) -> return (DontKnow $ Just x , arg')
150
Blocked x _ -> return (DontKnow $ Just x , arg')
151
_ -> return (DontKnow Nothing , arg')
151
153
{- Andreas, 2012-04-02 NO LONGER UP-TO-DATE
152
154
matchPattern (Arg h' r' (ConP c _ ps)) (Arg h Irrelevant v) = do
153
155
-- Andreas, 2010-09-07 matching a record constructor against
154
156
-- something irrelevant will just continue matching against
155
157
-- irrelevant stuff
156
(m, vs) <- matchPatterns ps $
158
(m, vs) <- matchPatterns ps $
157
159
repeat $ Arg NotHidden Irrelevant $ DontCare __IMPOSSIBLE__
158
return (m, Arg h Irrelevant $ Con c vs)
160
return (m, Arg h Irrelevant $ Con c vs)
161
163
-- Case record pattern: always succeed!
162
164
-- This case is necessary if we want to use the clauses before
163
165
-- record pattern translation (e.g., in type-checking definitions by copatterns).
164
(ConP con@(ConHead c ds) Just{} ps, arg@(Arg info v))
166
(ConP con@(ConHead c _ ds) Just{} ps, arg@(Arg info v))
165
167
-- precondition: con actually comes with the record fields
166
168
| size ds == size ps -> mapSnd (Arg info . Con con) <$> do
167
169
matchPatterns ps $ for ds $ \ d -> Arg info $ v `applyE` [Proj d]
171
173
-- Case data constructor pattern.
172
174
(ConP c _ ps, Arg info v) ->
173
do w <- traverse constructorForm =<< reduceB' v
175
do w <- traverse constructorForm =<< reduceB' v
174
176
-- Unfold delayed (corecursive) definitions one step. This is
175
177
-- only necessary if c is a coinductive constructor, but
176
178
-- 1) it does not hurt to do it all the time, and
185
187
-- unfolded (due to open public).
187
189
let v = ignoreBlocking w
188
case ignoreSharing <$> w of
190
case ignoreSharing <$> w of
190
192
{- Andreas, 2013-10-27 the following considered HARMFUL:
191
193
-- Andreas, 2010-09-07 matching a record constructor against
193
195
-- irrelevant stuff
194
196
-- NotBlocked (Sort Prop)
195
197
_ | isIrrelevant info -> do
196
(m, vs) <- matchPatterns ps $
198
(m, vs) <- matchPatterns ps $
197
199
repeat $ setRelevance Irrelevant $ defaultArg $ Sort Prop
198
200
-- repeat looks very bad here (non-termination!)
199
return (m, Arg info $ Con c vs)
201
return (m, Arg info $ Con c vs)
201
NotBlocked (Con c' vs)
203
(m, vs) <- yesSimplification <$> matchPatterns ps vs
204
return (m, Arg info $ Con c' vs)
205
| otherwise -> return (No, Arg info v) -- NOTE: v the reduced thing(shadowing!). Andreas, 2013-07-03
206
NotBlocked (MetaV x vs) -> return (DontKnow $ Just x, Arg info v)
207
Blocked x _ -> return (DontKnow $ Just x, Arg info v)
203
NotBlocked (Con c' vs)
205
(m, vs) <- yesSimplification <$> matchPatterns ps vs
206
return (m, Arg info $ Con c' vs)
207
| otherwise -> return (No, Arg info v) -- NOTE: v the reduced thing(shadowing!). Andreas, 2013-07-03
208
NotBlocked (MetaV x vs) -> return (DontKnow $ Just x, Arg info v)
209
Blocked x _ -> return (DontKnow $ Just x, Arg info v)
208
210
_ -> return (DontKnow Nothing, Arg info v)
212
-- ASR (08 November 2014). The type of the function could be
214
-- @(Match Term, [I.Arg Term]) -> (Match Term, [I.Arg Term])@.
215
yesSimplification :: (Match a, b) -> (Match a, b)
210
216
yesSimplification (Yes _ vs, us) = (Yes YesSimplification vs, us)
211
217
yesSimplification r = r
added
removed
src/full/Agda/TypeChecking/Patterns/Match.hs
