**diff options**

Diffstat (limited to 'src/full/Agda/Utils/List.hs')

-rw-r--r-- | src/full/Agda/Utils/List.hs | 175 |

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 --- ] |