← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/full/Agda/Utils/Permutation.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/Utils/Permutation.hs
1
 
{-# LANGUAGE DeriveDataTypeable, CPP #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE DeriveDataTypeable #-}
 
3
{-# LANGUAGE DeriveFoldable #-}
 
4
{-# LANGUAGE DeriveFunctor #-}
 
5
{-# LANGUAGE DeriveTraversable #-}
 
6
 
2
7
module Agda.Utils.Permutation where
3
8
 
 
9
import Prelude hiding (drop)
 
10
 
 
11
import Data.List hiding (drop)
 
12
import qualified Data.List as List
 
13
import Data.Maybe
 
14
 
 
15
import Data.Foldable (Foldable)
 
16
import Data.Traversable (Traversable)
4
17
import Data.Typeable (Typeable)
5
 
import Data.List
 
18
 
6
19
import Agda.Utils.Size
 
20
import Agda.Utils.List ((!!!))
 
21
 
 
22
#include "../undefined.h"
7
23
import Agda.Utils.Impossible
8
24
 
9
 
#include "../undefined.h"
10
 
 
 
25
-- | Partial permutations. Examples:
 
26
--
 
27
--   @permute [1,2,0]   [x0,x1,x2] = [x1,x2,x0]@     (proper permutation).
 
28
--
 
29
--   @permute [1,0]     [x0,x1,x2] = [x1,x0]@        (partial permuation).
 
30
--
 
31
--   @permute [1,0,1,2] [x0,x1,x2] = [x1,x0,x1,x2]@  (not a permutation because not invertible).
11
32
--
12
33
--   Agda typing would be:
13
34
--   @Perm : {m : Nat}(n : Nat) -> Vec (Fin n) m -> Permutation@
35
55
--   Agda typing:
36
56
--   @permute (Perm {m} n is) : Vec A m -> Vec A n@
37
57
permute :: Permutation -> [a] -> [a]
38
 
permute (Perm _ is) xs = map (xs !!!) is
 
58
permute (Perm _ is) xs = map (xs !!!!) is
39
59
  where
40
 
    []     !!! _ = __IMPOSSIBLE__
41
 
    (x:xs) !!! 0 = x
42
 
    (x:xs) !!! n = xs !!! (n - 1)
 
60
    xs !!!! n = fromMaybe __IMPOSSIBLE__ (xs !!! n)
43
61
 
 
62
-- | Identity permutation.
44
63
idP :: Int -> Permutation
45
64
idP n = Perm n [0..n - 1]
46
65
 
 
66
-- | Restrict a permutation to work on @n@ elements, discarding picks @>=n@.
47
67
takeP :: Int -> Permutation -> Permutation
48
68
takeP n (Perm m xs) = Perm n $ filter (< n) xs
49
69
 
 
70
-- | Pick the elements that are not picked by the permutation.
 
71
droppedP :: Permutation -> Permutation
 
72
droppedP (Perm n xs) = Perm n $ [0..n-1] \\ xs
 
73
 
50
74
-- | @liftP k@ takes a @Perm {m} n@ to a @Perm {m+k} (n+k)@.
51
75
--   Analogous to 'Agda.TypeChecking.Substitution.liftS',
52
76
--   but Permutations operate on de Bruijn LEVELS, not indices.
129
153
      where
130
154
        xs = [ x | (x, []) <- g ]
131
155
        remove x g = [ (y, filter (/= x) ys) | (y, ys) <- g, x /= y ]
 
156
 
 
157
-- * Drop (apply) and undrop (abstract)
 
158
 
 
159
-- | Delayed dropping which allows undropping.
 
160
data Drop a = Drop
 
161
  { dropN    :: Int  -- ^ Non-negative number of things to drop.
 
162
  , dropFrom :: a    -- ^ Where to drop from.
 
163
  }
 
164
  deriving (Eq, Ord, Show, Typeable, Functor, Foldable, Traversable)
 
165
 
 
166
-- | Things that support delayed dropping.
 
167
class DoDrop a where
 
168
 
 
169
  doDrop :: Drop a -> a              -- ^ Perform the dropping.
 
170
 
 
171
  dropMore :: Int -> Drop a -> Drop a  -- ^ Drop more.
 
172
  dropMore n (Drop m xs) = Drop (m + n) xs
 
173
 
 
174
  unDrop :: Int -> Drop a -> Drop a  -- ^ Pick up dropped stuff.
 
175
  unDrop n (Drop m xs)
 
176
    | n <= m    = Drop (m - n) xs
 
177
    | otherwise = __IMPOSSIBLE__
 
178
 
 
179
instance DoDrop [a] where
 
180
  doDrop   (Drop m xs) = List.drop m xs
 
181
 
 
182
instance DoDrop Permutation where
 
183
  doDrop (Drop k (Perm n xs)) =
 
184
    Perm (n + m) $ [0..m-1] ++ map (+ m) (List.drop k xs)
 
185
    where m = -k
 
186
  unDrop m = dropMore (-m) -- allow picking up more than dropped