← 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/List.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/List.hs
1
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE PatternGuards #-}
 
3
{-# LANGUAGE TemplateHaskell #-}
2
4
 
3
5
{-| Utitlity functions on lists.
4
6
-}
5
7
module Agda.Utils.List where
6
8
 
7
 
import Agda.Utils.TestHelpers
8
 
import Agda.Utils.QuickCheck
9
 
import Agda.Utils.Tuple
10
 
 
11
 
import Text.Show.Functions
 
9
import Data.Functor ((<$>))
12
10
import Data.Function
13
11
import Data.List
14
12
import Data.Maybe
15
13
import qualified Data.Set as Set
16
14
 
 
15
import Text.Show.Functions ()
 
16
import Test.QuickCheck
 
17
import Test.QuickCheck.All
 
18
 
 
19
import Agda.Utils.TestHelpers
 
20
-- import Agda.Utils.QuickCheck -- Andreas, 2014-04-27 Inconvenient
 
21
-- because cabal-only CPP directive
 
22
import Agda.Utils.Tuple
 
23
 
17
24
#include "../undefined.h"
18
25
import Agda.Utils.Impossible
19
26
 
27
34
uncons []     = Nothing
28
35
uncons (x:xs) = Just (x,xs)
29
36
 
 
37
-- | Maybe cons.   @mcons ma as = maybeToList ma ++ as@
 
38
mcons :: Maybe a -> [a] -> [a]
 
39
mcons ma as = maybe as (:as) ma
 
40
 
 
41
-- | 'init' and 'last' in one go, safe.
 
42
initLast :: [a] -> Maybe ([a],a)
 
43
initLast [] = Nothing
 
44
initLast as = Just $ loop as where
 
45
  loop []       = __IMPOSSIBLE__
 
46
  loop [a]      = ([], a)
 
47
  loop (a : as) = mapFst (a:) $ loop as
 
48
 
 
49
-- | Lookup function (partially safe).
 
50
(!!!) :: [a] -> Int -> Maybe a
 
51
_        !!! n | n < 0 = __IMPOSSIBLE__
 
52
[]       !!! _         = Nothing
 
53
(x : _)  !!! 0         = Just x
 
54
(_ : xs) !!! n         = xs !!! (n - 1)
 
55
 
30
56
-- | downFrom n = [n-1,..1,0]
31
57
downFrom :: Integral a => a -> [a]
32
58
downFrom n | n <= 0     = []
49
75
  Left  b -> (b:bs, cs)
50
76
  Right c -> (bs, c:cs)
51
77
 
 
78
-- | A generalized version of @takeWhile@.
 
79
--   (Cf. @mapMaybe@ vs. @filter@).
 
80
takeWhileJust :: (a -> Maybe b) -> [a] -> [b]
 
81
takeWhileJust p = loop
 
82
  where
 
83
    loop (a : as) | Just b <- p a = b : loop as
 
84
    loop _ = []
 
85
 
 
86
-- | A generalized version of @span@.
 
87
spanJust :: (a -> Maybe b) -> [a] -> ([b], [a])
 
88
spanJust p = loop
 
89
  where
 
90
    loop (a : as) | Just b <- p a = mapFst (b :) $ loop as
 
91
    loop as                       = ([], as)
 
92
 
 
93
-- | Partition a list into 'Nothing's and 'Just's.
 
94
--   @'mapMaybe' f = snd . partitionMaybe f@.
 
95
partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])
 
96
partitionMaybe f = loop
 
97
  where
 
98
    loop []       = ([], [])
 
99
    loop (a : as) = case f a of
 
100
      Nothing -> mapFst (a :) $ loop as
 
101
      Just b  -> mapSnd (b :) $ loop as
 
102
 
52
103
-- | Sublist relation.
53
104
isSublistOf :: Eq a => [a] -> [a] -> Bool
54
105
isSublistOf []       ys = True
69
120
  | p == r    = maybePrefixMatch pat rest
70
121
  | otherwise = Nothing
71
122
 
 
123
-- | Result of 'preOrSuffix'.
 
124
data PreOrSuffix a
 
125
  = IsPrefix a [a] -- ^ First list is prefix of second.
 
126
  | IsSuffix a [a] -- ^ First list is suffix of second.
 
127
  | IsBothfix      -- ^ The lists are equal.
 
128
  | IsNofix        -- ^ The lists are incomparable.
 
129
 
 
130
-- | Compare lists with respect to prefix partial order.
 
131
preOrSuffix :: Eq a => [a] -> [a] -> PreOrSuffix a
 
132
preOrSuffix []     []     = IsBothfix
 
133
preOrSuffix []     (b:bs) = IsPrefix b bs
 
134
preOrSuffix (a:as) []     = IsSuffix a as
 
135
preOrSuffix (a:as) (b:bs)
 
136
  | a == b    = preOrSuffix as bs
 
137
  | otherwise = IsNofix
 
138
 
72
139
-- | Split a list into sublists. Generalisation of the prelude function
73
140
--   @words@.
74
141
--
156
223
groupOn :: Ord b => (a -> b) -> [a] -> [[a]]
157
224
groupOn f = groupBy ((==) `on` f) . sortBy (compare `on` f)
158
225
 
 
226
-- | @splitExactlyAt n xs = Just (ys, zs)@ iff @xs = ys ++ zs@
 
227
--   and @genericLength ys = n@.
 
228
splitExactlyAt :: Integral n => n -> [a] -> Maybe ([a], [a])
 
229
splitExactlyAt 0 xs       = return ([], xs)
 
230
splitExactlyAt n []       = Nothing
 
231
splitExactlyAt n (x : xs) = mapFst (x :) <$> splitExactlyAt (n-1) xs
 
232
 
159
233
-- | @'extractNthElement' n xs@ gives the @n@-th element in @xs@
160
234
-- (counting from 0), plus the remaining elements (preserving order).
161
235
 
175
249
    genericTake n rest ++ [elem] ++ genericDrop n rest == xs
176
250
  where (elem, rest) = extractNthElement n xs
177
251
 
 
252
-- | A generalised variant of 'elemIndex'.
178
253
 
179
254
genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe i
180
255
genericElemIndex x xs =
204
278
    forAll (two $ vector n) $ \(xs, ys) ->
205
279
      zipWith' f xs ys == zipWith f xs ys
206
280
 
 
281
{- UNUSED; a better type would be
 
282
   zipWithTails :: (a -> b -> c) -> [a] -> [b] -> ([c], Either [a] [b])
 
283
 
207
284
-- | Like zipWith, but returns the leftover elements of the input lists.
208
285
zipWithTails :: (a -> b -> c) -> [a] -> [b] -> ([c], [a] , [b])
209
286
zipWithTails f xs       []       = ([], xs, [])
210
287
zipWithTails f []       ys       = ([], [] , ys)
211
288
zipWithTails f (x : xs) (y : ys) = (f x y : zs , as , bs)
212
289
  where (zs , as , bs) = zipWithTails f xs ys
 
290
-}
213
291
 
214
292
-- | Efficient version of nub that sorts the list first. The tag function is
215
293
--   assumed to be cheap. If it isn't pair up the elements with their tags and
223
301
prop_uniqBy :: [Integer] -> Bool
224
302
prop_uniqBy xs = sort (nub xs) == uniqBy id xs
225
303
 
 
304
-- Hack to make $quickCheckAll work under ghc-7.8
 
305
return []
 
306
 
226
307
------------------------------------------------------------------------
227
308
-- All tests
228
309
 
229
310
tests :: IO Bool
230
 
tests = runTests "Agda.Utils.List"
231
 
  [ quickCheck' prop_distinct_fastDistinct
232
 
  , quickCheck' prop_groupBy'
233
 
  , quickCheck' prop_extractNthElement
234
 
  , quickCheck' prop_genericElemIndex
235
 
  , quickCheck' prop_zipWith'
236
 
  , quickCheck' prop_uniqBy
237
 
  ]
 
311
tests = do
 
312
  putStrLn "Agda.Utils.List"
 
313
  $quickCheckAll
 
314
 
 
315
-- tests = runTests "Agda.Utils.List"
 
316
--   [ quickCheck' prop_distinct_fastDistinct
 
317
--   , quickCheck' prop_groupBy'
 
318
--   , quickCheck' prop_extractNthElement
 
319
--   , quickCheck' prop_genericElemIndex
 
320
--   , quickCheck' prop_zipWith'
 
321
--   , quickCheck' prop_uniqBy
 
322
--   ]