summaryrefslogtreecommitdiff
path: root/src/full/Agda/Utils/List.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Utils/List.hs')
-rw-r--r--src/full/Agda/Utils/List.hs175
1 files changed, 31 insertions, 144 deletions
diff --git a/src/full/Agda/Utils/List.hs b/src/full/Agda/Utils/List.hs
index 27d3826..5ddfe9c 100644
--- a/src/full/Agda/Utils/List.hs
+++ b/src/full/Agda/Utils/List.hs
@@ -1,13 +1,11 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TemplateHaskell #-}
-
-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# LANGUAGE CPP #-}
{-| Utitlity functions on lists.
-}
module Agda.Utils.List where
+import Control.Arrow (first)
+
import Data.Functor ((<$>))
import Data.Function
import Data.List
@@ -16,12 +14,9 @@ import qualified Data.Map as Map
import qualified Data.Set as Set
import Text.Show.Functions ()
-import Test.QuickCheck
import qualified Agda.Utils.Bag as Bag
-import Agda.Utils.TestHelpers
--- import Agda.Utils.QuickCheck -- Andreas, 2014-04-27 Inconvenient
--- because cabal-only CPP directive
+
import Agda.Utils.Tuple
#include "undefined.h"
@@ -73,7 +68,6 @@ initLast as = Just $ loop as where
-- | Lookup function (partially safe).
(!!!) :: [a] -> Int -> Maybe a
-_ !!! n | n < 0 = __IMPOSSIBLE__
[] !!! _ = Nothing
(x : _) !!! 0 = Just x
(_ : xs) !!! n = xs !!! (n - 1)
@@ -88,18 +82,12 @@ updateHead :: (a -> a) -> [a] -> [a]
updateHead f [] = []
updateHead f (a : as) = f a : as
-spec_updateHead f as = let (bs, cs) = splitAt 1 as in map f bs ++ cs
-prop_updateHead f as = updateHead f as == spec_updateHead f as
-
-- | Update the last element of a list, if it exists.
updateLast :: (a -> a) -> [a] -> [a]
updateLast f [] = []
updateLast f [a] = [f a]
updateLast f (a : as@(_ : _)) = a : updateLast f as
-spec_updateLast f as = let (bs, cs) = splitAt (length as - 1) as in bs ++ map f cs
-prop_updateLast f as = updateLast f as == spec_updateLast f as
-
-- | Update nth element of a list, if it exists.
-- Precondition: the index is >= 0.
updateAt :: Int -> (a -> a) -> [a] -> [a]
@@ -107,9 +95,6 @@ updateAt _ f [] = []
updateAt 0 f (a : as) = f a : as
updateAt n f (a : as) = a : updateAt (n-1) f as
-spec_updateAt n f as = let (bs, cs) = splitAt n as in bs ++ updateHead f cs
-prop_updateAt (NonNegative n) f as = updateAt n f as == spec_updateAt n f as
-
-- | A generalized version of @partition@.
-- (Cf. @mapMaybe@ vs. @filter@).
mapEither :: (a -> Either b c) -> [a] -> ([b],[c])
@@ -146,6 +131,25 @@ partitionMaybe f = loop
Nothing -> mapFst (a :) $ loop as
Just b -> mapSnd (b :) $ loop as
+-- | Like 'filter', but additionally return the last partition
+-- of the list where the predicate is @False@ everywhere.
+filterAndRest :: (a -> Bool) -> [a] -> ([a],[a])
+filterAndRest p = mapMaybeAndRest $ \ a -> if p a then Just a else Nothing
+
+-- | Like 'mapMaybe', but additionally return the last partition
+-- of the list where the function always returns @Nothing@.
+mapMaybeAndRest :: (a -> Maybe b) -> [a] -> ([b],[a])
+mapMaybeAndRest f = loop [] where
+ loop acc = \case
+ [] -> ([], reverse acc)
+ x:xs | Just y <- f x -> first (y:) $ loop [] xs
+ | otherwise -> loop (x:acc) xs
+
+-- | Drops from both lists simultaneously until one list is empty.
+dropCommon :: [a] -> [b] -> ([a],[b])
+dropCommon (x : xs) (y : ys) = dropCommon xs ys
+dropCommon xs ys = (xs, ys)
+
-- | Sublist relation.
isSublistOf :: Eq a => [a] -> [a] -> Bool
isSublistOf [] ys = True
@@ -159,12 +163,14 @@ type Suffix a = [a]
-- | Check if a list has a given prefix. If so, return the list
-- minus the prefix.
-maybePrefixMatch :: Eq a => Prefix a -> [a] -> Maybe (Suffix a)
-maybePrefixMatch [] rest = Just rest
-maybePrefixMatch (_:_) [] = Nothing
-maybePrefixMatch (p:pat) (r:rest)
- | p == r = maybePrefixMatch pat rest
- | otherwise = Nothing
+stripPrefixBy :: (a -> a -> Bool) -> Prefix a -> [a] -> Maybe (Suffix a)
+stripPrefixBy eq = loop
+ where
+ loop [] rest = Just rest
+ loop (_:_) [] = Nothing
+ loop (p:pat) (r:rest)
+ | eq p r = loop pat rest
+ | otherwise = Nothing
-- | Result of 'preOrSuffix'.
data PreOrSuffix a
@@ -214,12 +220,6 @@ chopWhen p xs =
(w, [_]) -> [w, []]
(w, _ : ys) -> w : chopWhen p ys
-prop_chop_intercalate :: Property
-prop_chop_intercalate =
- forAllShrink (choose (0, 4 :: Int)) shrink $ \ d ->
- forAllShrink (listOf (choose (0, 4 :: Int))) shrink $ \ xs ->
- xs === intercalate [d] (chopWhen (== d) xs)
-
-- | All ways of removing one element from a list.
holes :: [a] -> [(a, [a])]
holes [] = []
@@ -247,9 +247,6 @@ distinct (x:xs) = x `notElem` xs && distinct xs
fastDistinct :: Ord a => [a] -> Bool
fastDistinct xs = Set.size (Set.fromList xs) == length xs
-prop_distinct_fastDistinct :: [Integer] -> Bool
-prop_distinct_fastDistinct xs = distinct xs == fastDistinct xs
-
-- | Checks if all the elements in the list are equal. Assumes that
-- the 'Eq' instance stands for an equivalence relation.
allEqual :: Eq a => [a] -> Bool
@@ -277,19 +274,6 @@ groupBy' p xxs@(x : xs) = grp x $ zipWith (\x y -> (p x y, y)) xxs xs
[] -> []
((_, z) : zs) -> grp z zs
-prop_groupBy' :: (Bool -> Bool -> Bool) -> [Bool] -> Property
-prop_groupBy' p xs =
- classify (length xs - length gs >= 3) "interesting" $
- concat gs == xs
- &&
- and [not (null zs) | zs <- gs]
- &&
- and [and (pairInitTail zs zs) | zs <- gs]
- &&
- (null gs || not (or (pairInitTail (map last gs) (map head gs))))
- where gs = groupBy' p xs
- pairInitTail xs ys = zipWith p (init xs) (tail ys)
-
-- | @'groupOn' f = 'groupBy' (('==') \`on\` f) '.' 'sortBy' ('compare' \`on\` f)@.
groupOn :: Ord b => (a -> b) -> [a] -> [[a]]
@@ -302,25 +286,6 @@ splitExactlyAt 0 xs = return ([], xs)
splitExactlyAt n [] = Nothing
splitExactlyAt n (x : xs) = mapFst (x :) <$> splitExactlyAt (n-1) xs
--- | @'extractNthElement' n xs@ gives the @n@-th element in @xs@
--- (counting from 0), plus the remaining elements (preserving order).
-
-extractNthElement' :: Integral i => i -> [a] -> ([a], a, [a])
-extractNthElement' n xs = (left, el, right)
- where
- (left, el : right) = genericSplitAt n xs
-
-extractNthElement :: Integral i => i -> [a] -> (a, [a])
-extractNthElement n xs = (el, left ++ right)
- where
- (left, el, right) = extractNthElement' n xs
-
-prop_extractNthElement :: Integer -> [Integer] -> Property
-prop_extractNthElement n xs =
- 0 <= n && n < genericLength xs ==>
- genericTake n rest ++ [elem] ++ genericDrop n rest == xs
- where (elem, rest) = extractNthElement n xs
-
-- | A generalised variant of 'elemIndex'.
genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe i
@@ -331,11 +296,6 @@ genericElemIndex x xs =
zip [0..] $
map (== x) xs
-prop_genericElemIndex :: Integer -> [Integer] -> Property
-prop_genericElemIndex x xs =
- classify (x `elem` xs) "members" $
- genericElemIndex x xs == elemIndex x xs
-
-- | Requires both lists to have the same length.
zipWith' :: (a -> b -> c) -> [a] -> [b] -> [c]
@@ -344,12 +304,6 @@ zipWith' f (x : xs) (y : ys) = f x y : zipWith' f xs ys
zipWith' f [] (_ : _) = {- ' -} __IMPOSSIBLE__
zipWith' f (_ : _) [] = {- ' -} __IMPOSSIBLE__
-prop_zipWith' :: (Integer -> Integer -> Integer) -> Property
-prop_zipWith' f =
- forAll natural $ \n ->
- forAll (two $ vector n) $ \(xs, ys) ->
- zipWith' f xs ys == zipWith f xs ys
-
{- UNUSED; a better type would be
zipWithTails :: (a -> b -> c) -> [a] -> [b] -> ([c], Either [a] [b])
@@ -376,9 +330,6 @@ nubOn tag =
. map (\p@(_, x) -> (tag x, p))
. zip [1..]
-prop_nubOn :: (Integer -> Integer) -> [Integer] -> Bool
-prop_nubOn f xs = nubOn f xs == nubBy ((==) `on` f) xs
-
-- | Efficient variant of 'nubBy' for finite lists.
--
-- Specification: For each list @xs@ there is a list @ys@ which is a
@@ -392,26 +343,6 @@ prop_nubOn f xs = nubOn f xs == nubBy ((==) `on` f) xs
uniqOn :: Ord b => (a -> b) -> [a] -> [a]
uniqOn key = Map.elems . Map.fromList . map (\ a -> (key a, a))
-prop_uniqOn1 :: (Integer -> Integer) -> [Integer] -> Bool
-prop_uniqOn1 f xs' =
- or [ uniqOn f xs == nubBy ((==) `on` f) ys
- | ys <- permutations xs
- ]
- where
- xs = take 5 xs'
-
- permutations [] = [[]]
- permutations (x : xs) =
- [ ys1 ++ x : ys2
- | ys <- permutations xs
- , n <- [0..length ys]
- , let (ys1, ys2) = splitAt n ys
- ]
-
-prop_uniqOn2 :: (Integer -> Integer) -> [Integer] -> Bool
-prop_uniqOn2 f xs =
- sortBy (compare `on` f) (uniqOn f xs) == uniqOn f xs
-
-- | Compute the common suffix of two lists.
commonSuffix :: Eq a => [a] -> [a] -> [a]
commonSuffix xs ys = reverse $ (commonPrefix `on` reverse) xs ys
@@ -424,22 +355,6 @@ commonPrefix (x:xs) (y:ys)
| x == y = x : commonPrefix xs ys
| otherwise = []
-prop_commonPrefix :: [Integer] -> [Integer] -> [Integer] -> Bool
-prop_commonPrefix xs ys zs =
- and [ isPrefixOf zs zs'
- , isPrefixOf zs' (zs ++ xs)
- , isPrefixOf zs' (zs ++ ys) ]
- where
- zs' = commonPrefix (zs ++ xs) (zs ++ ys)
-
-prop_commonSuffix :: [Integer] -> [Integer] -> [Integer] -> Bool
-prop_commonSuffix xs ys zs =
- and [ isSuffixOf zs zs'
- , isSuffixOf zs' (xs ++ zs)
- , isSuffixOf zs' (ys ++ zs) ]
- where
- zs' = commonSuffix (xs ++ zs) (ys ++ zs)
-
editDistanceSpec :: Eq a => [a] -> [a] -> Int
editDistanceSpec [] ys = length ys
editDistanceSpec xs [] = length xs
@@ -462,31 +377,3 @@ editDistance xs ys = editD 0 0
(x : xs, y : ys)
| x == y -> editD (i + 1) (j + 1)
| otherwise -> 1 + minimum [ editD (i + 1) j, editD i (j + 1), editD (i + 1) (j + 1) ]
-
-prop_editDistance :: Property
-prop_editDistance =
- forAllShrink (choose (0, 10)) shrink $ \ n ->
- forAllShrink (choose (0, 10)) shrink $ \ m ->
- forAllShrink (vector n) shrink $ \ xs ->
- forAllShrink (vector m) shrink $ \ ys ->
- editDistanceSpec xs ys == editDistance xs (ys :: [Integer])
-
--- Hack to make $quickCheckAll work under ghc-7.8
-return []
-
-------------------------------------------------------------------------
--- All tests
-
-tests :: IO Bool
-tests = do
- putStrLn "Agda.Utils.List"
- $quickCheckAll
-
--- tests = runTests "Agda.Utils.List"
--- [ quickCheck' prop_distinct_fastDistinct
--- , quickCheck' prop_groupBy'
--- , quickCheck' prop_extractNthElement
--- , quickCheck' prop_genericElemIndex
--- , quickCheck' prop_zipWith'
--- , quickCheck' prop_uniqOn
--- ]