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

Agda.Utils.List

Description

Utility functions for lists.

Synopsis

# Documentation

snoc :: [a] -> a -> [a] Source #

Append a single element at the end. Time: O(length); use only on small lists.

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

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

caseListM :: Monad m => m [a] -> m b -> (a -> [a] -> m b) -> m b Source #

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

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

Case distinction for lists, with list last.

headMaybe :: [a] -> Maybe a Source #

headWithDefault :: a -> [a] -> a Source #

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

tailMaybe :: [a] -> Maybe [a] Source #

Tail function (safe).

tailWithDefault :: [a] -> [a] -> [a] Source #

Tail function (safe). Returns a default list on empty lists.

lastMaybe :: [a] -> Maybe a Source #

Last element (safe).

last2 :: [a] -> Maybe (a, a) Source #

Last two elements (safe).

dropEnd :: forall a. Int -> [a] -> [a] Source #

Drop from the end of a list. dropEnd n = reverse . drop n . reverse (Forces the whole list even for n==0.)

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.

initMaybe :: [a] -> Maybe [a] Source #

init, safe.

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

Lookup function (partially safe).

indexWithDefault :: a -> [a] -> Int -> a Source #

Lookup function with default value for index out of range. The name is chosen akin to genericIndex.

findWithIndex :: (a -> Bool) -> [a] -> Maybe (a, Int) Source #

Find an element satisfying a predicate and return it with its index. TODO: more efficient implementation!?

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

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

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

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

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

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

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

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

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 #

spanEnd :: forall a. (a -> Bool) -> [a] -> ([a], [a]) Source #

Split off the largest suffix whose elements satisfy a predicate.

spanEnd p xs = (ys, zs) where xs = ys ++ zs and all p zs and maybe True (not . p) (lastMaybe yz).

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.

filterAndRest :: (a -> Bool) -> [a] -> ([a], [a]) Source #

Like filter, but additionally return the last partition of the list where the predicate is False everywhere.

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

Like mapMaybe, but additionally return the last partition of the list where the function always returns Nothing.

dropCommon :: [a] -> [b] -> ([a], [b]) Source #

Drops from both lists simultaneously until one list is empty.

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

Sublist relation.

type Prefix a = [a] Source #

type Suffix a = [a] Source #

stripPrefixBy :: (a -> a -> Bool) -> Prefix a -> [a] -> Maybe (Suffix a) Source #

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

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

stripSuffix suf xs = Just pre iff xs = pre ++ suf.

type ReversedSuffix a = [a] Source #

stripReversedSuffix :: forall a. Eq a => ReversedSuffix a -> [a] -> Maybe (Prefix a) Source #

stripReversedSuffix rsuf xs = Just pre iff xs = pre ++ reverse suf.

data StrSufSt a Source #

Internal state for stripping suffix.

Constructors

 SSSMismatch Error. SSSStrip (ReversedSuffix a) "Negative string" to remove from end. List may be empty. SSSResult [a] "Positive string" (result). Non-empty list.

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.

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

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

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.

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

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

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.

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

A generalised variant of elemIndex.

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

Requires both lists to have the same length.

Otherwise, Nothing is returned.

zipWithKeepRest :: (a -> b -> b) -> [a] -> [b] -> [b] Source #

Like zipWith but keep the rest of the second list as-is (in case the second list is longer).

zipWithKeepRest f as bs == zipWith f as bs ++ drop (length as) bs

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

Efficient variant of nubBy for finite lists.

Specification:

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

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

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

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

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

Compute the common suffix of two lists.

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

Compute the common prefix of two lists.

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

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