Agda.Utils.List

Utitlity functions on lists.

Documentation

mhead :: [a] -> Maybe a

Head function (safe).

uncons :: [a] -> Maybe (a, [a])

Opposite of cons (:), safe.

mcons :: Maybe a -> [a] -> [a]

Maybe cons. mcons ma as = maybeToList ma ++ as

initLast :: [a] -> Maybe ([a], a)

init and last in one go, safe.

(!!!) :: [a] -> Int -> Maybe a

Lookup function (safe).

predecessor :: (Num a, Ord a) => a -> a

downFrom :: Integral a => a -> [a]

downFrom n = [n-1,..1,0]

updateLast :: (a -> a) -> [a] -> [a]

Update the last element of a list, if it exists

mapEither :: (a -> Either b c) -> [a] -> ([b], [c])

A generalized version of partition. (Cf. mapMaybe vs. filter).

deal :: (a -> Either b c) -> a -> ([b], [c]) -> ([b], [c])

takeWhileJust :: (a -> Maybe b) -> [a] -> [b]

A generalized version of takeWhile. (Cf. mapMaybe vs. filter).

spanJust :: (a -> Maybe b) -> [a] -> ([b], [a])

A generalized version of span.

partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])

Partition a list into Nothings and Justs. mapMaybe f = snd . partitionMaybe f.

isSublistOf :: Eq a => [a] -> [a] -> Bool

Sublist relation.

type Prefix a = [a]

type Suffix a = [a]

maybePrefixMatch :: Eq a => Prefix a -> [a] -> Maybe (Suffix a)

Check if a list has a given prefix. If so, return the list minus the prefix.

data PreOrSuffix a

Result of preOrSuffix.

Constructors

IsPrefix a [a]

First list is prefix of second.

IsSuffix a [a]

First list is suffix of second.

IsBothfix

The lists are equal.

IsNofix

The lists are incomparable.

preOrSuffix :: Eq a => [a] -> [a] -> PreOrSuffix a

Compare lists with respect to prefix partial order.

wordsBy :: (a -> Bool) -> [a] -> [[a]]

Split a list into sublists. Generalisation of the prelude function words.

 words xs == wordsBy isSpace xs

chop :: Int -> [a] -> [[a]]

Chop up a list in chunks of a given length.

holes :: [a] -> [(a, [a])]

All ways of removing one element from a list.

sorted :: Ord a => [a] -> Bool

Check whether a list is sorted.

Assumes that the Ord instance implements a partial order.

distinct :: Eq a => [a] -> Bool

Check whether all elements in a list are distinct from each other. Assumes that the Eq instance stands for an equivalence relation.

fastDistinct :: Ord a => [a] -> Bool

An optimised version of distinct.

Precondition: The list's length must fit in an Int.

prop_distinct_fastDistinct :: [Integer] -> Bool

allEqual :: Eq a => [a] -> Bool

Checks if all the elements in the list are equal. Assumes that the Eq instance stands for an equivalence relation.

groupBy' :: (a -> a -> Bool) -> [a] -> [[a]]

A variant of groupBy which applies the predicate to consecutive pairs.

prop_groupBy' :: (Bool -> Bool -> Bool) -> [Bool] -> Property

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 n xs = Just (ys, zs) iff xs = ys ++ zs and genericLength ys = n.

extractNthElement' :: Integral i => i -> [a] -> ([a], a, [a])

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

prop_extractNthElement :: Integer -> [Integer] -> Property

genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe i

A generalised variant of elemIndex.

prop_genericElemIndex :: Integer -> [Integer] -> Property

zipWith' :: (a -> b -> c) -> [a] -> [b] -> [c]

Requires both lists to have the same length.

prop_zipWith' :: (Integer -> Integer -> Integer) -> Property

uniqBy :: Ord b => (a -> b) -> [a] -> [a]

Efficient version of nub that sorts the list first. The tag function is assumed to be cheap. If it isn't pair up the elements with their tags and call uniqBy fst (or snd).

prop_uniqBy :: [Integer] -> Bool

tests :: IO Bool