module Agda.Utils.List where
import Data.Functor ((<$>))
import Data.Function
import Data.List
import Data.Maybe
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.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'
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
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
updateAt :: Int -> (a -> a) -> [a] -> [a]
updateAt _ f [] = []
updateAt 0 f (a : as) = f a : as
updateAt n f (a : as) = a : updateAt (n1) 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
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
chopWhen :: (a -> Bool) -> [a] -> [[a]]
chopWhen p [] = []
chopWhen p xs =
case break p xs of
(w, []) -> [w]
(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)
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
nubOn :: Ord b => (a -> b) -> [a] -> [a]
nubOn tag =
map snd
. sortBy (compare `on` fst)
. map (snd . head)
. groupBy ((==) `on` fst)
. sortBy (compare `on` fst)
. 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
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
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)
editDistanceSpec :: Eq a => [a] -> [a] -> Int
editDistanceSpec [] ys = length ys
editDistanceSpec xs [] = length xs
editDistanceSpec (x : xs) (y : ys)
| x == y = editDistanceSpec xs ys
| otherwise = 1 + minimum [ editDistanceSpec (x : xs) ys
, editDistanceSpec xs (y : ys)
, editDistanceSpec xs ys ]
editDistance :: Eq a => [a] -> [a] -> Int
editDistance xs ys = editD 0 0
where xss = tails xs
yss = tails ys
tbl = Map.fromList [ ((i, j), editD' i j) | i <- [0..length xss 1], j <- [0..length yss 1] ]
editD i j = tbl Map.! (i, j)
editD' i j =
case (xss !! i, yss !! j) of
([], ys) -> length ys
(xs, []) -> length xs
(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])
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Utils.List"
$quickCheckAll