← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Patterns/Match.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/TypeChecking/Patterns/Match.hs
1
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE DeriveFunctor #-}
 
3
{-# LANGUAGE ScopedTypeVariables #-}
2
4
 
3
5
module Agda.TypeChecking.Patterns.Match where
4
6
 
5
 
import Control.Monad
6
7
import Data.Monoid
7
 
import Data.Traversable
 
8
import Data.Traversable (traverse)
8
9
 
9
10
import Agda.Syntax.Common
10
 
import Agda.Syntax.Internal
11
 
import Agda.Syntax.Literal
 
11
import Agda.Syntax.Internal as I
12
12
 
13
13
import Agda.TypeChecking.Reduce
14
 
import Agda.TypeChecking.Monad
15
 
import Agda.TypeChecking.Monad.Builtin
16
 
import Agda.TypeChecking.Primitive
 
14
import Agda.TypeChecking.Reduce.Monad
 
15
import Agda.TypeChecking.Substitute
 
16
import Agda.TypeChecking.Monad hiding (reportSDoc)
17
17
import Agda.TypeChecking.Pretty
18
18
 
 
19
import Agda.Utils.Functor (for, ($>))
19
20
import Agda.Utils.Monad
 
21
import Agda.Utils.Size
 
22
import Agda.Utils.Tuple
20
23
 
21
24
#include "../../undefined.h"
22
25
import Agda.Utils.Impossible
23
26
 
24
27
-- | If matching is inconclusive (@DontKnow@) we want to know whether
25
28
--   it is due to a particular meta variable.
26
 
data Match = Yes [Term] | No | DontKnow (Maybe MetaId)
27
 
 
28
 
instance Monoid Match where
29
 
    mempty = Yes []
30
 
 
31
 
    Yes us     `mappend` Yes vs           = Yes (us ++ vs)
32
 
    Yes _      `mappend` No               = No
33
 
    Yes _      `mappend` DontKnow m       = DontKnow m
34
 
    No         `mappend` _                = No
 
29
data Match a = Yes Simplification [a] | No | DontKnow (Maybe MetaId)
 
30
  deriving (Functor)
 
31
 
 
32
instance Monoid (Match a) where
 
33
    mempty = Yes mempty []
 
34
 
 
35
    Yes s us   `mappend` Yes s' vs        = Yes (s `mappend` s') (us ++ vs)
 
36
    Yes _ _    `mappend` No               = No
 
37
    Yes _ _    `mappend` DontKnow m       = DontKnow m
 
38
    No         `mappend` _                = No
35
39
 
36
40
    -- Nothing means blocked by a variable.  In this case no instantiation of
37
41
    -- meta-variables will make progress.
41
45
    -- equivalence to case-trees.
42
46
    DontKnow m `mappend` _                = DontKnow m
43
47
 
44
 
matchPatterns :: [Arg Pattern] -> [Arg Term] -> TCM (Match, [Arg Term])
 
48
-- | Instead of 'zipWithM', we need to use this lazy version
 
49
--   of combining pattern matching computations.
 
50
 
 
51
-- Andreas, 2014-05-08, see Issue 1124:
 
52
--
 
53
-- Due to a bug in TypeChecking.Patterns.Match
 
54
-- a failed match of (C n b) against (C O unit)
 
55
-- turned into (C n unit).
 
56
-- This was because all patterns were matched in
 
57
-- parallel, and evaluations of successfull matches
 
58
-- (and a record constructor like unit can always
 
59
-- be successfully matched) were returned, leading
 
60
-- to a reassembly of (C n b) as (C n unit) which is
 
61
-- illtyped.
 
62
 
 
63
-- Now patterns are matched left to right and
 
64
-- upon failure, no further matching is performed.
 
65
 
 
66
foldMatch
 
67
  :: forall a b . (a -> b -> ReduceM (Match Term, b))
 
68
  -> [a] -> [b] -> ReduceM (Match Term, [b])
 
69
foldMatch match = loop where
 
70
  loop :: [a] -> [b] -> ReduceM (Match Term, [b])
 
71
  loop ps0 vs0 = do
 
72
  case (ps0, vs0) of
 
73
    ([], []) -> return (mempty, [])
 
74
    (p : ps, v : vs) -> do
 
75
      (r, v') <- match p v
 
76
      case r of
 
77
        No         -> return (No        , v' : vs)
 
78
        DontKnow m -> return (DontKnow m, v' : vs)
 
79
        Yes s us   -> do
 
80
          (r', vs') <- loop ps vs
 
81
          let vs1 = v' : vs'
 
82
          case r' of
 
83
            Yes s' us' -> return (Yes (s `mappend` s') (us ++ us'), vs1)
 
84
            No         -> return (No                              , vs1)
 
85
            DontKnow m -> return (DontKnow m                      , vs1)
 
86
    _ -> __IMPOSSIBLE__
 
87
 
 
88
-- | @matchCopatterns ps es@ matches spine @es@ against copattern spine @ps@.
 
89
--
 
90
--   Returns 'Yes' and a substitution for the pattern variables
 
91
--   (in form of [Term]) if matching was successful.
 
92
--
 
93
--   Returns 'No' if there was a constructor or projection mismatch.
 
94
--
 
95
--   Returns 'DontKnow' if an argument could not be evaluated to
 
96
--   constructor form because of a blocking meta variable.
 
97
--
 
98
--   In any case, also returns spine @es@ in reduced form
 
99
--   (with all the weak head reductions performed that were necessary
 
100
--   to come to a decision).
 
101
matchCopatterns :: [I.NamedArg Pattern] -> [Elim] -> ReduceM (Match Term, [Elim])
 
102
matchCopatterns ps vs = do
 
103
    traceSDoc "tc.match" 50
 
104
     (vcat [ text "matchCopatterns"
 
105
           , nest 2 $ text "ps =" <+> fsep (punctuate comma $ map (prettyTCM . namedArg) ps)
 
106
           , nest 2 $ text "vs =" <+> fsep (punctuate comma $ map prettyTCM vs)
 
107
           ]) $ do
 
108
    -- Buggy, see issue 1124:
 
109
    -- mapFst mconcat . unzip <$> zipWithM' (matchCopattern . namedArg) ps vs
 
110
    foldMatch (matchCopattern . namedArg) ps vs
 
111
 
 
112
-- | Match a single copattern.
 
113
matchCopattern :: Pattern -> Elim -> ReduceM (Match Term, Elim)
 
114
matchCopattern (ProjP p) elim@(Proj q)
 
115
  | p == q    = return (Yes YesSimplification [], elim)
 
116
  | otherwise = return (No                      , elim)
 
117
matchCopattern (ProjP p) elim@Apply{}
 
118
              = return (DontKnow Nothing, elim)
 
119
matchCopattern _ elim@Proj{} = return (DontKnow Nothing, elim)
 
120
matchCopattern p (Apply v)   = mapSnd Apply <$> matchPattern p v
 
121
 
 
122
matchPatterns :: [I.NamedArg Pattern] -> [I.Arg Term] -> ReduceM (Match Term, [I.Arg Term])
45
123
matchPatterns ps vs = do
46
 
    reportSDoc "tc.match" 50 $
47
 
      vcat [ text "matchPatterns"
 
124
    traceSDoc "tc.match" 50
 
125
     (vcat [ text "matchPatterns"
48
126
           , nest 2 $ text "ps =" <+> fsep (punctuate comma $ map (text . show) ps)
49
127
           , nest 2 $ text "vs =" <+> fsep (punctuate comma $ map prettyTCM vs)
50
 
           ]
51
 
 
52
 
    (ms,vs) <- unzip <$> zipWithM' matchPattern ps vs
53
 
    return (mconcat ms, vs)
54
 
 
55
 
matchPattern :: Arg Pattern -> Arg Term -> TCM (Match, Arg Term)
56
 
matchPattern (Arg h' _  (VarP _)) arg@(Arg _ _ v) = return (Yes [v], arg)
57
 
matchPattern (Arg _  _  (DotP _)) arg@(Arg _ _ v) = return (Yes [v], arg)
58
 
matchPattern (Arg h' r' (LitP l)) arg@(Arg h r v) = do
59
 
    w <- reduceB v
60
 
    let v = ignoreBlocking w
 
128
           ]) $ do
 
129
    -- Buggy, see issue 1124:
 
130
    -- (ms,vs) <- unzip <$> zipWithM' (matchPattern . namedArg) ps vs
 
131
    -- return (mconcat ms, vs)
 
132
    foldMatch (matchPattern . namedArg) ps vs
 
133
 
 
134
-- | Match a single pattern.
 
135
matchPattern :: Pattern -> I.Arg Term -> ReduceM (Match Term, I.Arg Term)
 
136
matchPattern p u = case (p, u) of
 
137
  (ProjP{}, _            ) -> __IMPOSSIBLE__
 
138
  (VarP _ , arg@(Arg _ v)) -> return (Yes NoSimplification [v], arg)
 
139
  (DotP _ , arg@(Arg _ v)) -> return (Yes NoSimplification [v], arg)
 
140
  (LitP l , arg@(Arg _ v)) -> do
 
141
    w <- reduceB' v
 
142
    let arg' = arg $> ignoreBlocking w
61
143
    case ignoreSharing <$> w of
62
144
        NotBlocked (Lit l')
63
 
            | l == l'          -> return (Yes [], Arg h r v)
64
 
            | otherwise        -> return (No, Arg h r v)
65
 
        NotBlocked (MetaV x _) -> return (DontKnow $ Just x, Arg h r v)
66
 
        Blocked x _            -> return (DontKnow $ Just x, Arg h r v)
67
 
        _                      -> return (DontKnow Nothing, Arg h r v)
 
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')
68
150
 
69
151
{- Andreas, 2012-04-02 NO LONGER UP-TO-DATE
70
152
matchPattern (Arg h' r' (ConP c _ ps))     (Arg h Irrelevant v) = do
76
158
                return (m, Arg h Irrelevant $ Con c vs)
77
159
-}
78
160
 
79
 
matchPattern (Arg h' r' (ConP c _ ps))     (Arg h r v) =
80
 
    do  w <- traverse constructorForm =<< reduceB v
 
161
  -- Case record pattern: always succeed!
 
162
  -- This case is necessary if we want to use the clauses before
 
163
  -- record pattern translation (e.g., in type-checking definitions by copatterns).
 
164
  (ConP con@(ConHead c ds) Just{} ps, arg@(Arg info v))
 
165
     -- precondition: con actually comes with the record fields
 
166
     | size ds == size ps -> mapSnd (Arg info . Con con) <$> do
 
167
         matchPatterns ps $ for ds $ \ d -> Arg info $ v `applyE` [Proj d]
 
168
           -- TODO: correct info for projected terms
 
169
     | otherwise -> __IMPOSSIBLE__
 
170
 
 
171
  -- Case data constructor pattern.
 
172
  (ConP c _ ps, Arg info v) ->
 
173
    do  w <- traverse constructorForm =<< reduceB' v
81
174
        -- Unfold delayed (corecursive) definitions one step. This is
82
175
        -- only necessary if c is a coinductive constructor, but
83
176
        -- 1) it does not hurt to do it all the time, and
85
178
        --    an axiom at this stage (if we are checking the
86
179
        --    projection functions for a record type).
87
180
        w <- case ignoreSharing <$> w of
88
 
               NotBlocked (Def f args) ->
89
 
                 unfoldDefinition True reduceB (Def f []) f args
 
181
               NotBlocked (Def f es) ->
 
182
                 unfoldDefinitionE True reduceB' (Def f []) f es
90
183
                   -- reduceB is used here because some constructors
91
184
                   -- are actually definitions which need to be
92
185
                   -- unfolded (due to open public).
93
186
               _ -> return w
94
187
        let v = ignoreBlocking w
95
188
        case ignoreSharing <$> w of
 
189
 
 
190
{- Andreas, 2013-10-27 the following considered HARMFUL:
96
191
          -- Andreas, 2010-09-07 matching a record constructor against
97
192
          -- something irrelevant will just continue matching against
98
193
          -- irrelevant stuff
99
194
          -- NotBlocked (Sort Prop)
100
 
          _  | r == Irrelevant -> do
 
195
          _  | isIrrelevant info -> do
101
196
                (m, vs) <- matchPatterns ps $
102
 
                  repeat $ Arg NotHidden Irrelevant $ Sort Prop
103
 
                return (m, Arg h r $ Con c vs)
 
197
                  repeat $ setRelevance Irrelevant $ defaultArg $ Sort Prop
 
198
                    -- repeat looks very bad here (non-termination!)
 
199
                return (m, Arg info $ Con c vs)
 
200
-}
104
201
          NotBlocked (Con c' vs)
105
 
            | c == c'             -> do
106
 
                (m, vs) <- matchPatterns ps vs
107
 
                return (m, Arg h r $ Con c' vs)
108
 
            | otherwise           -> return (No, Arg h r v)
109
 
          NotBlocked (MetaV x vs) -> return (DontKnow $ Just x, Arg h r v)
110
 
          Blocked x _             -> return (DontKnow $ Just x, Arg h r v)
111
 
          _                       -> return (DontKnow Nothing, Arg h r v)
 
202
            | c == c'            -> do
 
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)
 
208
          _                       -> return (DontKnow Nothing, Arg info v)
 
209
 
 
210
yesSimplification (Yes _ vs, us) = (Yes YesSimplification vs, us)
 
211
yesSimplification r              = r