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

Safe HaskellNone
LanguageHaskell98

Agda.Utils.List

Description

Utitlity functions on lists.

Synopsis

Documentation

mhead :: [a] -> Maybe a Source

Head function (safe).

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

Opposite of cons (:), safe.

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

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

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

init and last in one go, safe.

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

Lookup function (partially safe).

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

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

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

Update the last element of a list, if it exists

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

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

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

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

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

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

A generalized version of span.

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

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

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

Sublist relation.

type Prefix a = [a] Source

type Suffix a = [a] Source

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

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

data PreOrSuffix a Source

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 Source

Compare lists with respect to prefix partial order.

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

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

words xs == wordsBy isSpace xs

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

Chop up a list in chunks of a given length.

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

All ways of removing one element from a list.

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

Check whether a list is sorted.

Assumes that the Ord instance implements a partial order.

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

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 Source

An optimised version of distinct.

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

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

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

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

groupOn :: Ord b => (a -> b) -> [a] -> [[a]] Source

groupOn f = groupBy ((==) `on` f) . sortBy (compare `on` f).

splitExactlyAt :: Integral n => n -> [a] -> Maybe ([a], [a]) Source

splitExactlyAt n xs = Just (ys, zs) iff xs = ys ++ zs and genericLength ys = n.

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

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

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

A generalised variant of elemIndex.

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

Requires both lists to have the same length.

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

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