Agda.Utils.List

Utitlity functions on lists.

Documentation

caseList :: [a] -> b -> (a -> [a] -> b) -> b

Case distinction for lists, with list first. Cf. ifNull.

listCase :: b -> (a -> [a] -> b) -> [a] -> b

Case distinction for lists, with list last.

headMaybe :: [a] -> Maybe a

Head function (safe).

headWithDefault :: a -> [a] -> a

Head function (safe). Returns a value on empty lists.

headWithDefault 42 []      = 42
headWithDefault 42 [1,2,3] = 1

lastMaybe :: [a] -> Maybe a

Last element (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 (partially safe).

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

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

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

Update the first element of a list, if it exists.

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

prop_updateHead :: Eq a => (a -> a) -> [a] -> Bool

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

Update the last element of a list, if it exists.

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

prop_updateLast :: Eq a => (a -> a) -> [a] -> Bool

updateAt :: Int -> (a -> a) -> [a] -> [a]

Update nth element of a list, if it exists. Precondition: the index is >= 0.

spec_updateAt :: Int -> (a -> a) -> [a] -> [a]

prop_updateAt :: Eq a => NonNegative Int -> (a -> a) -> [a] -> Bool

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.

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

Chop a list at the positions when the predicate holds. Contrary to wordsBy, consecutive separator elements will result in an empty segment in the result. > intercalate [x] (chopWhen (== x) xs) == xs

prop_chop_intercalate :: Property

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.

duplicates :: Ord a => [a] -> [a]

Returns an (arbitrary) representative for each list element that occurs more than once.

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

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

Efficient variant of nubBy for finite lists.

Specification:

nubOn f xs == 'nubBy' ((==) `'on'` f) xs.

prop_nubOn :: (Integer -> Integer) -> [Integer] -> Bool

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

Efficient variant of nubBy for finite lists.

Specification: For each list xs there is a list ys which is a permutation of xs such that

uniqOn f xs == 'nubBy' ((==) `'on'` f) ys.

Furthermore

sortBy (compare `on` f) (uniqOn f xs) == uniqOn f xs.

prop_uniqOn1 :: (Integer -> Integer) -> [Integer] -> Bool

prop_uniqOn2 :: (Integer -> Integer) -> [Integer] -> Bool

commonSuffix :: Eq a => [a] -> [a] -> [a]

Compute the common suffix of two lists.

commonPrefix :: Eq a => [a] -> [a] -> [a]

Compute the common prefix of two lists.

prop_commonPrefix :: [Integer] -> [Integer] -> [Integer] -> Bool

prop_commonSuffix :: [Integer] -> [Integer] -> [Integer] -> Bool

editDistanceSpec :: Eq a => [a] -> [a] -> Int

editDistance :: Eq a => [a] -> [a] -> Int

prop_editDistance :: Property

tests :: IO Bool