module Agda.Utils.List where
import Data.Functor ((<$>))
import Data.Function
import Data.List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Text.Show.Functions ()
import Test.QuickCheck
import Test.QuickCheck.All
import Agda.Utils.Bag (Bag)
import qualified Agda.Utils.Bag as Bag
import Agda.Utils.TestHelpers
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
caseList :: [a] -> b -> (a -> [a] -> b) -> b
caseList [] n c = n
caseList (x:xs) n c = c x xs
listCase :: b -> (a -> [a] -> b) -> [a] -> b
listCase n c [] = n
listCase n c (x:xs) = c x xs
headMaybe :: [a] -> Maybe a
headMaybe = listToMaybe
headWithDefault :: a -> [a] -> a
headWithDefault def = fromMaybe def . headMaybe
lastMaybe :: [a] -> Maybe a
lastMaybe [] = Nothing
lastMaybe xs = Just $ last xs
uncons :: [a] -> Maybe (a, [a])
uncons [] = Nothing
uncons (x:xs) = Just (x,xs)
mcons :: Maybe a -> [a] -> [a]
mcons ma as = maybe as (:as) ma
initLast :: [a] -> Maybe ([a],a)
initLast [] = Nothing
initLast as = Just $ loop as where
loop [] = __IMPOSSIBLE__
loop [a] = ([], a)
loop (a : as) = mapFst (a:) $ loop as
(!!!) :: [a] -> Int -> Maybe a
_ !!! n | n < 0 = __IMPOSSIBLE__
[] !!! _ = Nothing
(x : _) !!! 0 = Just x
(_ : xs) !!! n = xs !!! (n 1)
downFrom :: Integral a => a -> [a]
downFrom n | n <= 0 = []
| otherwise = let n' = n1 in n' : downFrom n'
updateLast :: (a -> a) -> [a] -> [a]
updateLast f [] = []
updateLast f [a] = [f a]
updateLast f (a : as@(_ : _)) = a : updateLast f as
mapEither :: (a -> Either b c) -> [a] -> ([b],[c])
mapEither f xs = foldr (deal f) ([],[]) xs
deal :: (a -> Either b c) -> a -> ([b],[c]) -> ([b],[c])
deal f a ~(bs,cs) = case f a of
Left b -> (b:bs, cs)
Right c -> (bs, c:cs)
takeWhileJust :: (a -> Maybe b) -> [a] -> [b]
takeWhileJust p = loop
where
loop (a : as) | Just b <- p a = b : loop as
loop _ = []
spanJust :: (a -> Maybe b) -> [a] -> ([b], [a])
spanJust p = loop
where
loop (a : as) | Just b <- p a = mapFst (b :) $ loop as
loop as = ([], as)
partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])
partitionMaybe f = loop
where
loop [] = ([], [])
loop (a : as) = case f a of
Nothing -> mapFst (a :) $ loop as
Just b -> mapSnd (b :) $ loop as
isSublistOf :: Eq a => [a] -> [a] -> Bool
isSublistOf [] ys = True
isSublistOf (x : xs) ys =
case dropWhile (x /=) ys of
[] -> False
(_:ys) -> isSublistOf xs ys
type Prefix a = [a]
type Suffix a = [a]
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
data PreOrSuffix a
= IsPrefix a [a]
| IsSuffix a [a]
| IsBothfix
| IsNofix
preOrSuffix :: Eq a => [a] -> [a] -> PreOrSuffix a
preOrSuffix [] [] = IsBothfix
preOrSuffix [] (b:bs) = IsPrefix b bs
preOrSuffix (a:as) [] = IsSuffix a as
preOrSuffix (a:as) (b:bs)
| a == b = preOrSuffix as bs
| otherwise = IsNofix
wordsBy :: (a -> Bool) -> [a] -> [[a]]
wordsBy p xs = yesP xs
where
yesP xs = noP (dropWhile p xs)
noP [] = []
noP xs = ys : yesP zs
where
(ys,zs) = break p xs
chop :: Int -> [a] -> [[a]]
chop _ [] = []
chop n xs = ys : chop n zs
where (ys,zs) = splitAt n xs
holes :: [a] -> [(a, [a])]
holes [] = []
holes (x:xs) = (x, xs) : map (id -*- (x:)) (holes xs)
sorted :: Ord a => [a] -> Bool
sorted [] = True
sorted xs = and $ zipWith (<=) xs (tail xs)
distinct :: Eq a => [a] -> Bool
distinct [] = True
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
allEqual :: Eq a => [a] -> Bool
allEqual [] = True
allEqual (x : xs) = all (== x) xs
duplicates :: Ord a => [a] -> [a]
duplicates = mapMaybe dup . Bag.groups . Bag.fromList
where
dup (a : _ : _) = Just a
dup _ = Nothing
groupBy' :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy' _ [] = []
groupBy' p xxs@(x : xs) = grp x $ zipWith (\x y -> (p x y, y)) xxs xs
where
grp x ys = (x : map snd xs) : tail
where (xs, rest) = span fst ys
tail = case rest of
[] -> []
((_, 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 :: Ord b => (a -> b) -> [a] -> [[a]]
groupOn f = groupBy ((==) `on` f) . sortBy (compare `on` f)
splitExactlyAt :: Integral n => n -> [a] -> Maybe ([a], [a])
splitExactlyAt 0 xs = return ([], xs)
splitExactlyAt n [] = Nothing
splitExactlyAt n (x : xs) = mapFst (x :) <$> splitExactlyAt (n1) xs
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
genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe i
genericElemIndex x xs =
listToMaybe $
map fst $
filter snd $
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
zipWith' :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith' f [] [] = []
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
uniqOn :: Ord b => (a -> b) -> [a] -> [a]
uniqOn key = Map.elems . Map.fromList . map (\ a -> (key a, a))
prop_uniqOn :: [Integer] -> Bool
prop_uniqOn xs = sort (nub xs) == uniqOn id xs
commonSuffix :: Eq a => [a] -> [a] -> [a]
commonSuffix xs ys = reverse $ (commonPrefix `on` reverse) xs ys
commonPrefix :: Eq a => [a] -> [a] -> [a]
commonPrefix [] _ = []
commonPrefix _ [] = []
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)
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Utils.List"
$quickCheckAll