← 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/CompiledClause/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/CompiledClause/Match.hs
1
 
{-# LANGUAGE CPP, PatternGuards #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE PatternGuards #-}
 
3
{-# LANGUAGE ScopedTypeVariables #-}
 
4
 
2
5
module Agda.TypeChecking.CompiledClause.Match where
3
6
 
4
7
import Control.Applicative
 
8
import Control.Monad.Reader (asks)
5
9
import qualified Data.Map as Map
6
 
import Data.Traversable
7
10
import Data.List
 
11
import Debug.Trace (trace)
8
12
 
9
13
import Agda.Syntax.Internal
10
14
import Agda.Syntax.Common
11
15
import Agda.TypeChecking.CompiledClause
12
 
import Agda.TypeChecking.Monad
 
16
import Agda.TypeChecking.Monad hiding (reportSDoc, reportSLn)
 
17
import Agda.TypeChecking.Pretty
 
18
import Agda.TypeChecking.Reduce
 
19
import Agda.TypeChecking.Reduce.Monad as RedM
13
20
import Agda.TypeChecking.Substitute
14
 
import Agda.TypeChecking.Reduce
15
 
import Agda.TypeChecking.Primitive
16
 
 
17
 
import Agda.Utils.List
18
 
 
 
21
 
 
22
import Agda.Utils.Maybe
 
23
 
 
24
#include "../../undefined.h"
19
25
import Agda.Utils.Impossible
20
 
#include "../../undefined.h"
21
 
 
22
 
matchCompiled :: CompiledClauses -> MaybeReducedArgs -> TCM (Reduced (Blocked Args) Term)
23
 
matchCompiled c args = match c args id []
24
 
 
25
 
type Stack = [(CompiledClauses, MaybeReducedArgs, Args -> Args)]
 
26
 
 
27
matchCompiled :: CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Args) Term)
 
28
matchCompiled c args = do
 
29
  r <- matchCompiledE c $ map (fmap Apply) args
 
30
  case r of
 
31
    YesReduction simpl v -> return $ YesReduction simpl v
 
32
    NoReduction bes      -> return $ NoReduction $ fmap (map fromElim) bes
 
33
  where fromElim (Apply v) = v
 
34
        fromElim (Proj f ) = __IMPOSSIBLE__
 
35
 
 
36
-- | @matchCompiledE c es@ takes a function given by case tree @c@ and
 
37
--   and a spine @es@ and tries to apply the function to @es@.
 
38
matchCompiledE :: CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Elims) Term)
 
39
matchCompiledE c args = match' [(c, args, id)]
 
40
 
 
41
-- | A stack entry is a triple consisting of
 
42
--   1. the part of the case tree to continue matching,
 
43
--   2. the current argument vector, and
 
44
--   3. a patch function taking the current argument vector back
 
45
--      to the original argument vector.
 
46
type Frame = (CompiledClauses, MaybeReducedElims, Elims -> Elims)
 
47
type Stack = [Frame]
 
48
 
 
49
 
 
50
-- | @match'@ tries to solve the matching problems on the @Stack@.
 
51
--   In each iteration, the top problem is removed and handled.
 
52
--
 
53
--   If the top problem was a @Done@, we succeed.
 
54
--
 
55
--   If the top problem was a @Case n@ and the @n@th argument of the problem
 
56
--   is not a constructor or literal, we are stuck, thus, fail.
 
57
--
 
58
--   If we have a branch for the constructor/literal, we put it on the stack
 
59
--   to continue.
 
60
--   If we do not have a branch, we fall through to the next problem, which
 
61
--   should be the corresponding catch-all branch.
 
62
--
 
63
--   An empty stack is an exception that can come only from an incomplete
 
64
--   function definition.
26
65
 
27
66
-- TODO: literal/constructor pattern conflict (for Nat)
28
67
 
29
 
match :: CompiledClauses -> MaybeReducedArgs -> (Args -> Args) -> Stack -> TCM (Reduced (Blocked Args) Term)
30
 
match Fail args patch stack = return $ NoReduction $ NotBlocked (patch $ map ignoreReduced args)
31
 
match (Done xs t) args _ _
32
 
  | m < n     = return $ YesReduction $ applySubst (parallelS $ reverse $ toTm args)
33
 
                                      $ foldr lam t (drop m xs)
34
 
  | otherwise = return $ YesReduction $
35
 
                  applySubst (parallelS $ reverse $ toTm args0) t `apply` map ignoreReduced args1
36
 
  where
37
 
    n              = length xs
38
 
    m              = length args
39
 
    toTm           = map (unArg . ignoreReduced)
40
 
    (args0, args1) = splitAt n $ map (fmap $ fmap shared) args
41
 
    lam x t        = Lam (argHiding x) (Abs (unArg x) t)
42
 
match (Case n bs) args patch stack =
43
 
  case genericSplitAt n args of
44
 
    (_, []) -> return $ NoReduction $ NotBlocked $ patch $ map ignoreReduced args
45
 
    (args0, MaybeRed red (Arg h r v0) : args1) -> do
46
 
      w  <- case red of
47
 
              Reduced b  -> return $ fmap (const v0) b
48
 
              NotReduced ->
49
 
                unfoldCorecursion =<< instantiate v0
50
 
      cv <- constructorForm $ ignoreBlocking w
51
 
      let v      = ignoreBlocking w
52
 
          args'  = args0 ++ [MaybeRed red $ Arg h r v] ++ args1
53
 
          stack' = maybe [] (\c -> [(c, args', patch)]) (catchAllBranch bs)
54
 
                   ++ stack
55
 
          patchLit args = patch (args0 ++ [Arg h r v] ++ args1)
56
 
            where (args0, args1) = splitAt n args
57
 
          patchCon c m args = patch (args0 ++ [Arg h r $ Con c vs] ++ args1)
58
 
            where (args0, args1') = splitAt n args
59
 
                  (vs, args1)     = splitAt m args1'
60
 
      case ignoreSharing <$> w of
61
 
        Blocked x _            -> return $ NoReduction $ Blocked x (patch $ map ignoreReduced args')
62
 
        NotBlocked (MetaV x _) -> return $ NoReduction $ Blocked x (patch $ map ignoreReduced args')
63
 
        NotBlocked (Lit l) -> case Map.lookup l (litBranches bs) of
64
 
          Nothing -> match' stack''
65
 
          Just cc -> match cc (args0 ++ args1) patchLit stack''
66
 
          where
67
 
            stack'' = (++ stack') $ case ignoreSharing cv of
68
 
              Con c vs -> case Map.lookup c (conBranches bs) of
69
 
                Nothing -> []
70
 
                Just cc -> [(content cc, args0 ++ map (MaybeRed red) vs ++ args1, patchCon c (length vs))]
71
 
              _        -> []
72
 
        NotBlocked (Con c vs) -> case Map.lookup c (conBranches bs) of
73
 
          Nothing -> match' stack'
74
 
          Just cc -> match (content cc)
75
 
                           (args0 ++ map (MaybeRed red) vs ++ args1)
76
 
                           (patchCon c (length vs))
77
 
                           stack'
78
 
        NotBlocked _ -> return $ NoReduction $ NotBlocked (patch $ map ignoreReduced args')
79
 
 
80
 
match' :: Stack -> TCM (Reduced (Blocked Args) Term)
81
 
match' ((c, args, patch):stack) = match c args patch stack
82
 
match' [] = typeError $ GenericError "Incomplete pattern matching"
83
 
 
84
 
unfoldCorecursion v = case v of
85
 
  Def f args -> unfoldDefinition True unfoldCorecursion (Def f []) f args
86
 
  Shared{}   -> fmap shared <$> unfoldCorecursion (ignoreSharing v) -- don't update when unfolding corecursion!
87
 
  _          -> reduceB v
 
68
match' :: Stack -> ReduceM (Reduced (Blocked Elims) Term)
 
69
match' ((c, es, patch) : stack) = do
 
70
  let debug = do
 
71
       traceSDoc "reduce.compiled" 95 $ vcat $
 
72
         [ text "reducing case" <+> do
 
73
             caseMaybeM (asks envAppDef) __IMPOSSIBLE__ $ \ f -> do
 
74
               sep $ prettyTCM f : map prettyTCM es
 
75
         , text $ "trying clause " ++ show c
 
76
         ]
 
77
  let no          es = return $ NoReduction $ NotBlocked $ patch $ map ignoreReduced es
 
78
      noBlocked x es = return $ NoReduction $ Blocked x  $ patch $ map ignoreReduced es
 
79
      yes t            = flip YesReduction t <$> asks envSimplification
 
80
 
 
81
  -- traceSLn "reduce.compiled" 95 "CompiledClause.Match.match'" $ do
 
82
  debug $ do
 
83
 
 
84
  case c of
 
85
 
 
86
    -- impossible case
 
87
    Fail -> no es
 
88
 
 
89
    -- done matching
 
90
    Done xs t
 
91
      -- if the function was partially applied, return a lambda
 
92
      | m < n     -> yes $ applySubst (toSubst es) $ foldr lam t (drop m xs)
 
93
      -- otherwise, just apply instantiation to body
 
94
      -- apply the result to any extra arguments
 
95
      | otherwise -> yes $ applySubst (toSubst es0) t `applyE` map ignoreReduced es1
 
96
--      | otherwise -> yes $ applySubst (toSubst args0) t `apply` map ignoreReduced args1
 
97
      where
 
98
        n              = length xs
 
99
        m              = length es
 
100
        -- at least the first @n@ elims must be @Apply@s, so we can
 
101
        -- turn them into a subsitution
 
102
        toSubst        = parallelS . reverse . map (unArg . argFromElim . ignoreReduced)
 
103
--        (args0, args1) = splitAt n $ map (fmap $ fmap shared) args
 
104
--        (args0, es1)   = takeArgsFromElims n $ map (fmap $ fmap shared) args
 
105
        -- Andreas, 2013-05-21 why introduce sharing only here,
 
106
        -- and not in underapplied case also?
 
107
        (es0, es1)     = splitAt n $ map (fmap $ fmap shared) es
 
108
        lam x t        = Lam (argInfo x) (Abs (unArg x) t)
 
109
 
 
110
    -- splitting on the @n@th elimination
 
111
    Case n bs -> do
 
112
      case genericSplitAt n es of
 
113
        -- if the @n@th elimination is not supplied, no match
 
114
        (_, []) -> no es
 
115
        -- if the @n@th elimination is @e0@
 
116
--        (args0, MaybeRed red (Arg info v0) : args1) -> do
 
117
        (es0, MaybeRed red e0 : es1) -> do
 
118
          -- get the reduced form of @e0@
 
119
{-
 
120
          w  <- case red of
 
121
                  Reduced b  -> return $ v0 <$ b
 
122
                  NotReduced -> unfoldCorecursion v0
 
123
          let v = ignoreBlocking w
 
124
              args'  = args0 ++ [MaybeRed red $ Arg info v] ++ args1
 
125
-}
 
126
          eb :: Blocked Elim <- do
 
127
                case red of
 
128
                  Reduced b  -> return $ e0 <$ b
 
129
                  NotReduced -> unfoldCorecursionE e0
 
130
          let e = ignoreBlocking eb
 
131
              -- replace the @n@th argument by its reduced form
 
132
              es' = es0 ++ [MaybeRed red e] ++ es1
 
133
              -- if a catch-all clause exists, put it on the stack
 
134
              catchAllFrame stack = maybe stack (\c -> (c, es', patch) : stack) (catchAllBranch bs)
 
135
              -- If our argument is @Lit l@, we push @litFrame l@ onto the stack.
 
136
              litFrame l stack =
 
137
                case Map.lookup l (litBranches bs) of
 
138
                  Nothing -> stack
 
139
                  Just cc -> (cc, es0 ++ es1, patchLit) : stack
 
140
              -- If our argument (or its constructor form) is @Con c vs@
 
141
              -- we push @conFrame c vs@ onto the stack.
 
142
              conFrame c vs stack =
 
143
                case Map.lookup (conName c) (conBranches bs) of
 
144
                    Nothing -> stack
 
145
                    Just cc -> ( content cc
 
146
                               , es0 ++ map (MaybeRed red . Apply) vs ++ es1
 
147
                               , patchCon c (length vs)
 
148
                               ) : stack
 
149
              -- If our argument is @Proj p@, we push @projFrame p@ onto the stack.
 
150
              projFrame p stack =
 
151
                case Map.lookup p (conBranches bs) of
 
152
                  Nothing -> stack
 
153
                  Just cc -> (content cc, es0 ++ es1, patchLit) : stack
 
154
              -- The new patch function restores the @n@th argument to @v@:
 
155
              -- In case we matched a literal, just put @v@ back.
 
156
              patchLit es = patch (es0 ++ [e] ++ es1)
 
157
                where (es0, es1) = splitAt n es
 
158
              -- In case we matched constructor @c@ with @m@ arguments,
 
159
              -- contract these @m@ arguments @vs@ to @Con c vs@.
 
160
              patchCon c m es = patch (es0 ++ [Con c vs <$ e] ++ es2)
 
161
                where (es0, rest) = splitAt n es
 
162
                      (es1, es2)  = splitAt m rest
 
163
                      vs          = map argFromElim es1
 
164
 
 
165
          -- Now do the matching on the @n@ths argument:
 
166
          case fmap ignoreSharing <$> eb of
 
167
            Blocked x _            -> noBlocked x es'
 
168
            NotBlocked (Apply (Arg info (MetaV x _))) -> noBlocked x es'
 
169
 
 
170
            -- In case of a literal, try also its constructor form
 
171
            NotBlocked (Apply (Arg info v@(Lit l))) -> performedSimplification $ do
 
172
              cv <- constructorForm v
 
173
              let cFrame stack = case ignoreSharing cv of
 
174
                    Con c vs -> conFrame c vs stack
 
175
                    _        -> stack
 
176
              match' $ litFrame l $ cFrame $ catchAllFrame stack
 
177
 
 
178
            -- In case of a constructor, push the conFrame
 
179
            NotBlocked (Apply (Arg info (Con c vs))) -> performedSimplification $
 
180
              match' $ conFrame c vs $ catchAllFrame $ stack
 
181
 
 
182
            -- In case of a projection, push the litFrame
 
183
            NotBlocked (Proj p) -> performedSimplification $
 
184
              match' $ projFrame p $ stack
 
185
 
 
186
            NotBlocked _ -> no es'
 
187
 
 
188
-- If we reach the empty stack, then pattern matching was incomplete
 
189
match' [] = do  {- new line here since __IMPOSSIBLE__ does not like the ' in match' -}
 
190
  caseMaybeM (asks envAppDef) __IMPOSSIBLE__ $ \ f -> do
 
191
    error $ "Incomplete pattern matching when applying " ++ show f
 
192
 
 
193
 
 
194
-- Andreas, 2013-03-20 recursive invokations of unfoldCorecursion
 
195
-- need also to instantiate metas, see Issue 826.
 
196
unfoldCorecursionE :: Elim -> ReduceM (Blocked Elim)
 
197
unfoldCorecursionE e@(Proj f)           = return $ NotBlocked e
 
198
unfoldCorecursionE (Apply (Arg info v)) = fmap (Apply . Arg info) <$>
 
199
  unfoldCorecursion v
 
200
 
 
201
unfoldCorecursion :: Term -> ReduceM (Blocked Term)
 
202
unfoldCorecursion v = do
 
203
  v <- instantiate' v
 
204
  case v of
 
205
    Def f es -> unfoldDefinitionE True unfoldCorecursion (Def f []) f es
 
206
    Shared{} -> fmap shared <$> unfoldCorecursion (ignoreSharing v) -- don't update when unfolding corecursion!
 
207
    _          -> reduceB' v