← 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/RecordPatterns.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/RecordPatterns.hs
1
 
{-# LANGUAGE CPP, PatternGuards, TupleSections, FlexibleInstances, GeneralizedNewtypeDeriving #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE FlexibleInstances #-}
 
3
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
4
{-# LANGUAGE PatternGuards #-}
 
5
{-# LANGUAGE TupleSections #-}
2
6
 
3
7
-- | Code which replaces pattern matching on record constructors with
4
8
-- uses of projection functions.
17
21
import Control.Monad.State
18
22
 
19
23
import Data.List
20
 
import Data.Map (Map)
21
24
import qualified Data.Map as Map
22
25
import qualified Data.Traversable as Trav
23
26
 
24
27
import Agda.Syntax.Common
25
 
import Agda.Syntax.Internal
26
 
 
 
28
import Agda.Syntax.Internal as I
27
29
import Agda.TypeChecking.CompiledClause
28
30
import Agda.TypeChecking.Coverage.SplitTree
29
31
import Agda.TypeChecking.Datatypes
39
41
import Agda.Utils.List
40
42
import qualified Agda.Utils.Map as Map
41
43
import Agda.Utils.Maybe
42
 
import Agda.Utils.Permutation
 
44
import Agda.Utils.Permutation hiding (dropFrom)
43
45
import Agda.Utils.Size
44
46
 
45
47
#include "../undefined.h"
62
64
    LitP{}             -> typeError $ ShouldBeRecordPattern p
63
65
    DotP{}             -> typeError $ ShouldBeRecordPattern p
64
66
    ConP c Nothing  ps -> typeError $ ShouldBeRecordPattern p
65
 
    ConP c (Just t) ps -> do
 
67
    ConP c (Just (_, t)) ps -> do
66
68
      t <- reduce t
67
69
      fields <- getRecordTypeFields (unArg t)
68
 
      concat <$> zipWithM comb (map proj fields) (map unArg ps)
 
70
      concat <$> zipWithM comb (map proj fields) (map namedArg ps)
 
71
    ProjP{}            -> __IMPOSSIBLE__ -- copattern cannot appear here
69
72
  where
70
 
    proj p = \ x -> Def (unArg p) [defaultArg x]
 
73
    proj p = (`applyE` [Proj $ unArg p])
 
74
--    proj p = \ x -> Def (unArg p) [defaultArg x]
71
75
    comb :: (Term -> Term) -> Pattern -> TCM [Term -> Term]
72
 
    comb prj p = map (prj .) <$> recordPatternToProjections p
 
76
    comb prj p = map (\ f -> f . prj) <$> recordPatternToProjections p
73
77
 
74
78
 
75
79
---------------------------------------------------------------------------
137
141
      (ccs, xssc, conMap)    <- Map.unzip3 <$> do
138
142
        Trav.forM (Map.mapWithKey (,) conMap) $ \ (c, WithArity ar cc) -> do
139
143
          (xs, cc)     <- loop cc
140
 
          dataOrRecCon <- getConstructorArity c
 
144
--          dataOrRecCon <- getConstructorArity c  -- TODO: c could be a projection
 
145
          dataOrRecCon <- do
 
146
            isProj <- isProjection c
 
147
            case isProj of
 
148
               Nothing -> getConstructorArity c
 
149
               Just{}  -> return $ Left 0
141
150
          let (isRC, n)   = either (False,) ((True,) . size) dataOrRecCon
142
151
              (xs0, rest) = genericSplitAt i xs
143
152
              (xs1, xs2 ) = genericSplitAt n rest
144
 
              -- if all dropped variables are virgins and we are record cons.
 
153
              -- if all dropped variables (xs1) are virgins and we are record cons.
145
154
              -- then new variable x is also virgin
146
155
              -- and we can translate away the split
147
156
              x           = isRC && and xs1
165
174
                  , catchAllBranch = catchAll })
166
175
 
167
176
        -- case: translated away one record pattern
168
 
        [cc] -> return (xs, cc)
 
177
        [cc] -> do
 
178
                -- Andreas, 2013-03-22
 
179
                -- Due to catch-all-expansion this is actually possible:
 
180
                -- -- we cannot have a catch-all if we had a record pattern
 
181
                -- whenJust catchAll __IMPOSSIBLE__
 
182
                -- We just drop the catch-all clause.  This is safe because
 
183
                -- for record patterns we have expanded all the catch-alls.
 
184
                return (xs, cc) -- mergeCatchAll cc catchAll)
169
185
 
170
186
        -- case: more than one record patterns (impossible)
171
187
        _    -> __IMPOSSIBLE__
172
188
 
 
189
{- UNUSED
 
190
instance Monoid CompiledClauses where
 
191
  mempty = __IMPOSSIBLE__
 
192
  mappend (Case n c) (Case n' c') | n == n' = Case n $ mappend c c'
 
193
  mappend _ _ = __IMPOSSIBLE__
 
194
 
 
195
mergeCatchAll :: CompiledClauses -> Maybe CompiledClauses -> CompiledClauses
 
196
mergeCatchAll cc ca = maybe cc (mappend cc) ca
 
197
{-
 
198
  case (cc, ca) of
 
199
    (_       , Nothing) -> cc
 
200
    (Case n c, Just (Case n' c')) | n == n' -> Case n $ mappend c c'
 
201
    _                   -> __IMPOSSIBLE__ -- this would mean non-determinism
 
202
-}
 
203
-}
 
204
 
173
205
-- | @replaceByProjections i projs cc@ replaces variables @i..i+n-1@
174
206
--   (counted from left) by projections @projs_1 i .. projs_n i@.
175
207
--
199
231
          let (xs0,xs1,xs2)     = cutSublist i n xs
200
232
              names | null xs1  = ["r"]
201
233
                    | otherwise = map unArg xs1
202
 
              x                 = defaultArg $ foldr1 (++) names
 
234
              x                 = defaultArg $ foldr1 appendArgNames names
203
235
              xs'               = xs0 ++ x : xs2
204
 
              us                = map (\ p -> Def p [defaultArg $ var 0]) (reverse projs)
 
236
              us                = map (\ p -> Var 0 [Proj p]) (reverse projs)
 
237
--              us                = map (\ p -> Def p [defaultArg $ var 0]) (reverse projs)
205
238
              -- go from level (i + n - 1) to index (subtract from |xs|-1)
206
239
              index             = length xs - (i + n)
207
240
          in  Done xs' $ applySubst (liftS (length xs2) $ us ++# raiseS 1) v
399
432
  -- cs: List of changes, with types in the context of the old
400
433
  -- telescope.
401
434
 
402
 
  (ps, s, cs) <- runRecPatM $ translatePatterns $ clausePats clause
 
435
  (ps, s, cs) <- runRecPatM $ translatePatterns $ namedClausePats clause
403
436
 
404
437
  let -- Number of variables + dot patterns in new clause.
405
438
      noNewPatternVars = size cs
470
503
 
471
504
      -- New clause.
472
505
      c = clause
473
 
            { clauseTel  = newTel
474
 
            , clausePerm = newPerm
475
 
            , clausePats = applySubst lhsSubst ps
476
 
            , clauseBody = translateBody cs rhsSubst $ clauseBody clause
 
506
            { clauseTel       = newTel
 
507
            , clausePerm      = newPerm
 
508
            , namedClausePats = applySubst lhsSubst ps
 
509
            , clauseBody      = translateBody cs rhsSubst $ clauseBody clause
477
510
            }
478
511
 
479
512
  reportSDoc "tc.lhs.recpat" 10 $
539
572
-- patterns, should be removed, and a new variable, with the name @x@,
540
573
-- inserted instead. The type of the new variable is @t@.
541
574
 
542
 
type Changes = [Either Pattern (Kind -> Nat, String, Dom Type)]
 
575
type Changes = [Either Pattern (Kind -> Nat, ArgName, I.Dom Type)]
543
576
 
544
577
-- | Record pattern trees.
545
578
 
547
580
  = Leaf Pattern
548
581
    -- ^ Corresponds to variable and dot patterns; contains the
549
582
    -- original pattern.
550
 
  | RecCon (Arg Type) [(Term -> Term, RecordTree)]
 
583
  | RecCon (I.Arg Type) [(Term -> Term, RecordTree)]
551
584
    -- ^ @RecCon t args@ stands for a record constructor application:
552
585
    -- @t@ is the type of the application, and the list contains a
553
586
    -- projection function and a tree for every argument.
624
657
translatePattern p@VarP{} = removeTree (Leaf p)
625
658
translatePattern p@DotP{} = removeTree (Leaf p)
626
659
translatePattern p@LitP{} = return (p, [], [])
627
 
 
628
 
 
629
 
translatePatterns ::
630
 
  [Arg Pattern] -> RecPatM ([Arg Pattern], [Term], Changes)
 
660
translatePattern p@ProjP{}= __IMPOSSIBLE__
 
661
 
 
662
translatePatterns :: [I.NamedArg Pattern] -> RecPatM ([I.NamedArg Pattern], [Term], Changes)
631
663
translatePatterns ps = do
632
 
  (ps', ss, cs) <- unzip3 <$> mapM (translatePattern . unArg) ps
633
 
  return (ps' `withArgsFrom` ps, concat ss, concat cs)
 
664
  (ps', ss, cs) <- unzip3 <$> mapM (translatePattern . namedArg) ps
 
665
  return (zipWith (\p -> fmap (p <$)) ps' ps, concat ss, concat cs)
634
666
 
635
667
-- | Traverses a pattern and returns one of two things:
636
668
--
651
682
  Pattern ->
652
683
  RecPatM (Either (RecPatM (Pattern, [Term], Changes)) RecordTree)
653
684
recordTree p@(ConP _ Nothing _) = return $ Left $ translatePattern p
654
 
recordTree (ConP c (Just t) ps) = do
655
 
  rs <- mapM (recordTree . unArg) ps
 
685
recordTree (ConP c ci@(Just (_, t)) ps) = do
 
686
  rs <- mapM (recordTree . namedArg) ps
656
687
  case allRight rs of
657
 
    Left rs ->
 
688
    Nothing ->
658
689
      return $ Left $ do
659
690
        (ps', ss, cs) <- unzip3 <$> mapM (either id removeTree) rs
660
 
        return (ConP c (Just t) (ps' `withArgsFrom` ps),
 
691
        return (ConP c ci (ps' `withNamedArgsFrom` ps),
661
692
                concat ss, concat cs)
662
 
    Right ts -> liftTCM $ do
 
693
    Just ts -> liftTCM $ do
663
694
      t <- reduce t
664
695
      fields <- getRecordTypeFields (unArg t)
665
 
      let proj p = \x -> Def (unArg p) [defaultArg x]
 
696
--      let proj p = \x -> Def (unArg p) [defaultArg x]
 
697
      let proj p = (`applyE` [Proj $ unArg p])
666
698
      return $ Right $ RecCon t $ zip (map proj fields) ts
667
699
recordTree p@VarP{} = return (Right (Leaf p))
668
700
recordTree p@DotP{} = return (Right (Leaf p))
669
701
recordTree p@LitP{} = return $ Left $ translatePattern p
 
702
recordTree p@ProjP{}= __IMPOSSIBLE__
670
703
 
671
704
------------------------------------------------------------------------
672
705
-- Translation of the clause telescope and body
677
710
  :: Changes
678
711
     -- ^ Explanation of how the telescope should be changed. Types
679
712
     -- should be in the context of the old telescope.
680
 
  -> [(String, Dom Type)]
 
713
  -> [(ArgName, I.Dom Type)]
681
714
     -- ^ Old telescope, flattened, in textual left-to-right
682
715
     -- order.
683
 
  -> [Maybe (String, Dom Type)]
 
716
  -> [Maybe (ArgName, I.Dom Type)]
684
717
     -- ^ New telescope, flattened, in textual left-to-right order.
685
718
     -- 'Nothing' is used to indicate the locations of dot patterns.
686
719
translateTel (Left (DotP{}) : rest)   tel = Nothing : translateTel rest tel