{-# LANGUAGE ScopedTypeVariables #-}
module Agda.Utils.List where
import Control.Arrow (first)
import Data.Functor ((<$>))
import Data.Function
import qualified Data.List as List
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set
import Text.Show.Functions ()
import qualified Agda.Utils.Bag as Bag
import Agda.Utils.Tuple
snoc :: [a] -> a -> [a]
snoc xs x = xs ++ [x]
caseList :: [a] -> b -> (a -> [a] -> b) -> b
caseList xs n c = listCase n c xs
caseListM :: Monad m => m [a] -> m b -> (a -> [a] -> m b) -> m b
caseListM mxs n c = listCase n c =<< mxs
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
tailMaybe :: [a] -> Maybe [a]
tailMaybe = fmap snd . uncons
tailWithDefault :: [a] -> [a] -> [a]
tailWithDefault def = fromMaybe def . tailMaybe
lastMaybe :: [a] -> Maybe a
lastMaybe [] = Nothing
lastMaybe xs = Just $ last xs
last2 :: [a] -> Maybe (a, a)
last2 (x : y : xs) = Just $ loop x y xs
where
loop x y [] = (x, y)
loop x y (z:xs) = loop y z xs
last2 _ = Nothing
dropEnd :: forall a. Int -> [a] -> [a]
dropEnd n = snd . foldr f (n, [])
where
f :: a -> (Int, [a]) -> (Int, [a])
f x (n, xs)
| n <= 0 = (0, x:xs)
| otherwise = (n-1, 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 (a:as) = Just $ loop a as where
loop a [] = ([], a)
loop a (b : bs) = mapFst (a:) $ loop b bs
initMaybe :: [a] -> Maybe [a]
initMaybe = fmap fst . initLast
(!!!) :: [a] -> Int -> Maybe a
[] !!! _ = Nothing
(x : _) !!! 0 = Just x
(_ : xs) !!! n = xs !!! (n - 1)
indexWithDefault :: a -> [a] -> Int -> a
indexWithDefault a [] _ = a
indexWithDefault a (x : _) 0 = x
indexWithDefault a (_ : xs) n = indexWithDefault a xs (n - 1)
findWithIndex :: (a -> Bool) -> [a] -> Maybe (a, Int)
findWithIndex p as = headMaybe $ filter (p . fst) $ zip as [0..]
downFrom :: Integral a => a -> [a]
downFrom n | n <= 0 = []
| otherwise = let n' = n-1 in n' : downFrom n'
updateHead :: (a -> a) -> [a] -> [a]
updateHead f [] = []
updateHead f (a : as) = f a : as
updateLast :: (a -> a) -> [a] -> [a]
updateLast f [] = []
updateLast f [a] = [f a]
updateLast f (a : as@(_ : _)) = a : 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 (n-1) f as
mapEither :: (a -> Either b c) -> [a] -> ([b],[c])
{-# INLINE mapEither #-}
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)
spanEnd :: forall a. (a -> Bool) -> [a] -> ([a], [a])
spanEnd p = snd . foldr f (True, ([], []))
where
f :: a -> (Bool, ([a], [a])) -> (Bool, ([a], [a]))
f x (b', (xs, ys)) = (b, if b then (xs, x:ys) else (x:xs, ys))
where b = b' && p x
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
filterAndRest :: (a -> Bool) -> [a] -> ([a],[a])
filterAndRest p = mapMaybeAndRest $ \ a -> if p a then Just a else 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
dropCommon :: [a] -> [b] -> ([a],[b])
dropCommon (x : xs) (y : ys) = dropCommon xs ys
dropCommon xs ys = (xs, ys)
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]
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
stripSuffix :: Eq a => Suffix a -> [a] -> Maybe (Prefix a)
stripSuffix [] = Just
stripSuffix s = stripReversedSuffix (reverse s)
type ReversedSuffix a = [a]
stripReversedSuffix :: forall a. Eq a => ReversedSuffix a -> [a] -> Maybe (Prefix a)
stripReversedSuffix rs = final . foldr step (SSSStrip rs)
where
step :: a -> StrSufSt a -> StrSufSt a
step x = \case
SSSMismatch -> SSSMismatch
SSSResult xs -> SSSResult (x:xs)
SSSStrip [] -> SSSResult [x]
SSSStrip (y:ys)
| x == y -> SSSStrip ys
| otherwise -> SSSMismatch
final :: StrSufSt a -> Maybe (Prefix a)
final = \case
SSSResult xs -> Just xs
SSSStrip [] -> Just []
_ -> Nothing
data StrSufSt a
= SSSMismatch
| SSSStrip (ReversedSuffix a)
| SSSResult [a]
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
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
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
groupOn :: Ord b => (a -> b) -> [a] -> [[a]]
groupOn f = List.groupBy ((==) `on` f) . List.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 (n-1) xs
genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe i
genericElemIndex x xs =
listToMaybe $
map fst $
filter snd $
zip [0..] $
map (== x) xs
zipWith' :: (a -> b -> c) -> [a] -> [b] -> Maybe [c]
zipWith' f = loop
where
loop [] [] = Just []
loop (x : xs) (y : ys) = (f x y :) <$> loop xs ys
loop [] (_ : _) = Nothing
loop (_ : _) [] = Nothing
zipWithKeepRest :: (a -> b -> b) -> [a] -> [b] -> [b]
zipWithKeepRest f = loop
where
loop [] bs = bs
loop as [] = []
loop (a : as) (b : bs) = f a b : loop as bs
nubOn :: Ord b => (a -> b) -> [a] -> [a]
nubOn tag =
map snd
. List.sortBy (compare `on` fst)
. map (snd . head)
. List.groupBy ((==) `on` fst)
. List.sortBy (compare `on` fst)
. map (\p@(_, x) -> (tag x, p))
. zip [1..]
uniqOn :: Ord b => (a -> b) -> [a] -> [a]
uniqOn key = Map.elems . Map.fromList . map (\ a -> (key a, a))
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 = []
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 = List.tails xs
yss = List.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) ]