Agda.Utils.List

A variant of !! that might provide more informative error messages if the index is out of bounds.

Precondition: The index should not be out of bounds.

Lookup function (safe). O(min n index).

Analogous to zip, combines two lists by taking the union using These (strict).

Check whether all consecutive elements of a list satisfy the given relation. O(n).

Remove the first representative for each list element. Thus, returns all duplicate copies. O(n log n).

allDuplicates xs == sort $ xs \ nub xs.

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

A version of Foldable.asum that avoids a final empty. It is right-folding just like Foldable.asum.

Precondition: the right-unit law holds, i.e. m | A.empty = m.

A right-folding Foldable.asum for nonempty lists, never producing empty.

Breaks a list just after an element satisfying the predicate is found.

>>> breakAfter even [1,3,5,2,4,7,8]([1,3,5,2],[4,7,8])

Breaks a list just after an element satisfying the predicate is found.

>>> breakAfter1 even 1 [3,5,2,4,7,8](1 :| [3,5,2],[4,7,8])

Case distinction for lists, with list first. O(1).

Cf. ifNull.

Case distinction for lists, with list first. O(1).

Cf. ifNull.

Chop up a list in chunks of a given length. O(n).

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. O(n).

intercalate [x] (chopWhen (== x) xs) == xs

Compute the common prefix of two lists. O(min n m).

Compute the common suffix of two lists. O(n + m).

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

O(n²) in the worst case distinct xs == True.

downFrom n = [n-1,..1,0]. O(n).

Drops from both lists simultaneously until one list is empty. O(min n m).

Drop from the end of a list. O(length).

dropEnd n = reverse . drop n . reverse

Forces the whole list even for n==0.

dropFrom marker xs drops everything from xs starting with (and including) marker.

If the marker does not appear, the string is returned unchanged.

The following two properties hold provided marker has no overlap with xs:

  dropFrom marker (xs ++ marker ++ ys) == xs
  dropFrom marker xs == xs

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

Implemented using dynamic programming and Data.Array. O(n*m).

Implemented using tree recursion, don't run me at home! O(3^(min n m)).

An optimised version of distinct. O(n log n).

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

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

Find the longest suffix of the first string xs that is a prefix of the second string ys. So, basically, find the overlap where the strings can be glued together. Returns the index where the overlap starts and the length of the overlap. The length of the overlap plus the index is the length of the first string. Note that in the worst case, the empty overlap (length xs,0) is returned.

Worst-case time complexity is quadratic: O(min(n,m)²) where n = length xs and m = length ys.

There might be asymptotically better implementations following Knuth-Morris-Pratt (KMP), but for rather short lists this is good enough.

Find an element satisfying a predicate and return it with its index. O(n) in the worst case, e.g. findWithIndex f xs = Nothing.

TODO: more efficient implementation!?

A generalised variant of elemIndex. O(n).

Check membership for the same list often. Use partially applied to create membership predicate hasElem xs :: a -> Bool.

• First time: O(n log n) in the worst case.

• Subsequently: O(log n).

Specification: hasElem xs == (elem xs).

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

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

All ways of removing one element from a list. O(n²).

Lookup function with default value for index out of range. O(min n index).

The name is chosen akin to genericIndex.

init of non-empty list, safe. O(n). init1 a as = init (a:as)

init and last in one go, safe. O(n).

init and last of non-empty list, safe. O(n). initLast1 a as = (init (a:as), last (a:as)

init, safe. O(n).

init, safe. O(n).

Last element of non-empty list (safe). O(n). last1 a as = last (a : as)

Last two elements (safe). O(n).

last2' x y zs computes the last two elements of x:y:zs. O(n).

Last element (safe). O(n).

Last element (safe). Returns a default list on empty lists. O(n).

Case distinction for lists, with list last. O(1).

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

Maybe cons. O(1). mcons ma as = maybeToList ma ++ as

Partition a list into first and later occurrences of elements (modulo some quotient given by a representation function).

Time: O(n log n).

Specification:

nubAndDuplicatesOn f xs = (ys, xs List.\\ ys)
  where ys = nubOn f xs

A variant of nubOn that is parametrised by a function that is used to select which element from a group of equal elements that is returned. The returned elements keep the order that they had in the input list.

Precondition: The length of the input list must be at most maxBound :: Int.

Non-efficient, monadic nub. O(n²).

Efficient variant of nubBy for lists, using a set to store already seen elements. O(n log n)

Specification:

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

Partition a list into Nothings and Justs. O(n).

partitionMaybe f = partitionEithers . map ( a -> maybe (Left a) Right (f a))

Note: mapMaybe f = snd . partitionMaybe f.

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

Check whether a list is sorted. O(n).

Assumes that the Ord instance implements a partial order.

Split off the largest suffix whose elements satisfy a predicate. O(n).

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

A generalized version of span. O(length . fst . spanJust f).

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

Check if a list has a given prefix. If so, return the list minus the prefix. O(length prefix).

stripReversedSuffix rsuf xs = Just pre iff xs = pre ++ reverse suf. O(n).

stripSuffix suf xs = Just pre iff xs = pre ++ suf. O(n).

Returns a list with one boolean for each non-empty suffix of the list, starting with the longest suffix (the entire list). Each boolean is True exactly when every element in the corresponding suffix satisfies the predicate.

An example: suffixesSatisfying isLower AbCde = [False, False, False, True, True]

For total predicates p and finite and total lists xs the following holds: suffixesSatisfying p xs = map (all p) (init (tails xs))

Tail function (safe). O(1).

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

A generalized version of takeWhile. (Cf. mapMaybe vs. filter). @O(length . takeWhileJust f).

takeWhileJust f = fst . spanJust f.

Efficient variant of nubBy for finite lists. O(n log n).

uniqOn f == 'List.sortBy' (compare `'on'` f) . 'nubBy' ((==) `'on'` f)

If there are several elements with the same f-representative, the first of these is kept.

Update nth element of a list, if it exists. O(min index n).

Precondition: the index is >= 0.

Update the first element of a list, if it exists. O(1).

Update the last element of a list, if it exists. O(n).

Requires both lists to have the same length. O(n).

Otherwise, Nothing is returned.

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

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

Internal state for stripping suffix.

\mathcal{O}(1). Decompose a list into its head and tail.

• If the list is empty, returns Nothing.

• If the list is non-empty, returns Just (x, xs), where x is the head of the list and xs its tail.

Examples

>>> uncons []Nothing

>>> uncons [1]Just (1,[])

>>> uncons [1, 2, 3]Just (1,[2,3])