Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Utils.List

Description

Utitlity functions on lists.

Synopsis

- mhead :: [a] -> Maybe a
- uncons :: [a] -> Maybe (a, [a])
- downFrom :: Integral a => a -> [a]
- updateLast :: (a -> a) -> [a] -> [a]
- mapEither :: (a -> Either b c) -> [a] -> ([b], [c])
- deal :: (a -> Either b c) -> a -> ([b], [c]) -> ([b], [c])
- isSublistOf :: Eq a => [a] -> [a] -> Bool
- type Prefix a = [a]
- type Suffix a = [a]
- maybePrefixMatch :: Eq a => Prefix a -> [a] -> Maybe (Suffix a)
- wordsBy :: (a -> Bool) -> [a] -> [[a]]
- chop :: Int -> [a] -> [[a]]
- holes :: [a] -> [(a, [a])]
- sorted :: Ord a => [a] -> Bool
- distinct :: Eq a => [a] -> Bool
- fastDistinct :: Ord a => [a] -> Bool
- prop_distinct_fastDistinct :: [Integer] -> Bool
- allEqual :: Eq a => [a] -> Bool
- groupBy' :: (a -> a -> Bool) -> [a] -> [[a]]
- prop_groupBy' :: (Bool -> Bool -> Bool) -> [Bool] -> Property
- groupOn :: Ord b => (a -> b) -> [a] -> [[a]]
- extractNthElement' :: Integral i => i -> [a] -> ([a], a, [a])
- extractNthElement :: Integral i => i -> [a] -> (a, [a])
- prop_extractNthElement :: Integer -> [Integer] -> Property
- genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe i
- prop_genericElemIndex :: Integer -> [Integer] -> Property
- zipWith' :: (a -> b -> c) -> [a] -> [b] -> [c]
- prop_zipWith' :: (Integer -> Integer -> Integer) -> Property
- zipWithTails :: (a -> b -> c) -> [a] -> [b] -> ([c], [a], [b])
- uniqBy :: Ord b => (a -> b) -> [a] -> [a]
- prop_uniqBy :: [Integer] -> Bool
- tests :: IO Bool

# Documentation

mhead :: [a] -> Maybe a

Head function (safe).

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

Opposite of cons `(:)`, safe.

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

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.

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)`.

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

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

zipWithTails :: (a -> b -> c) -> [a] -> [b] -> ([c], [a], [b])

Like zipWith, but returns the leftover elements of the input lists.

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