module Agda.Utils.List where
import Agda.Utils.TestHelpers
import Agda.Utils.QuickCheck
import Agda.Utils.Tuple
import Text.Show.Functions
import Data.Function
import Data.List
import Data.Maybe
import qualified Data.Set as Set
#include "../undefined.h"
import Agda.Utils.Impossible
mhead :: [a] -> Maybe a
mhead [] = Nothing
mhead (x:_) = Just x
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
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)
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
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)
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
uniqBy :: Ord b => (a -> b) -> [a] -> [a]
uniqBy tag =
map head
. groupBy ((==) `on` tag)
. sortBy (compare `on` tag)
prop_uniqBy :: [Integer] -> Bool
prop_uniqBy xs = sort (nub xs) == uniqBy id xs
tests :: IO Bool
tests = runTests "Agda.Utils.List"
[ quickCheck' prop_distinct_fastDistinct
, quickCheck' prop_groupBy'
, quickCheck' prop_extractNthElement
, quickCheck' prop_genericElemIndex
, quickCheck' prop_zipWith'
, quickCheck' prop_uniqBy
]