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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.List

Description

Utility functions for lists.

Synopsis

- (!!) :: HasCallStack => [a] -> Int -> a
- type Prefix a = [a]
- asum :: Alternative m => [m a] -> m a
- align :: [a] -> [b] -> [These a b]
- snoc :: [a] -> a -> [a]
- dropEnd :: Int -> [a] -> Prefix a
- spanEnd :: (a -> Bool) -> [a] -> (Prefix a, Suffix a)
- stripSuffix :: Eq a => Suffix a -> [a] -> Maybe (Prefix a)
- unzipWith :: (a -> (b, c)) -> [a] -> ([b], [c])
- updateAt :: Int -> (a -> a) -> [a] -> [a]
- zipWith' :: (a -> b -> c) -> [a] -> [b] -> Maybe [c]
- chop :: Int -> [a] -> [[a]]
- downFrom :: Integral a => a -> [a]
- headWithDefault :: a -> [a] -> a
- indexWithDefault :: a -> [a] -> Int -> a
- hasElem :: Ord a => [a] -> a -> Bool
- initLast1 :: a -> [a] -> ([a], a)
- nubOn :: Ord b => (a -> b) -> [a] -> [a]
- caseList :: [a] -> b -> (a -> [a] -> b) -> b
- last1 :: a -> [a] -> a
- updateHead :: (a -> a) -> [a] -> [a]
- updateLast :: (a -> a) -> [a] -> [a]
- chopWhen :: (a -> Bool) -> [a] -> [[a]]
- duplicates :: Ord a => [a] -> [a]
- initWithDefault :: [a] -> [a] -> [a]
- lastWithDefault :: a -> [a] -> a
- lastMaybe :: [a] -> Maybe a
- spanJust :: (a -> Maybe b) -> [a] -> (Prefix b, Suffix a)
- type Suffix a = [a]
- initLast :: [a] -> Maybe ([a], a)
- tailWithDefault :: [a] -> [a] -> [a]
- splitExactlyAt :: Integral n => n -> [a] -> Maybe (Prefix a, Suffix a)
- (!!!) :: [a] -> Int -> Maybe a
- caseListM :: Monad m => m [a] -> m b -> (a -> [a] -> m b) -> m b
- editDistance :: Eq a => [a] -> [a] -> Int
- dropFrom :: Eq a => List1 a -> [a] -> [a]
- init1 :: a -> [a] -> [a]
- last2 :: [a] -> Maybe (a, a)
- listCase :: b -> (a -> [a] -> b) -> [a] -> b
- tailMaybe :: [a] -> Maybe [a]
- last2' :: a -> a -> [a] -> (a, a)
- mcons :: Maybe a -> [a] -> [a]
- initMaybe :: [a] -> Maybe [a]
- asum1 :: Alternative m => m a -> [m a] -> m a
- findWithIndex :: (a -> Bool) -> [a] -> Maybe (a, Int)
- genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe i
- breakAfter1 :: (a -> Bool) -> a -> [a] -> (List1 a, [a])
- breakAfter :: (a -> Bool) -> [a] -> ([a], [a])
- takeWhileJust :: (a -> Maybe b) -> [a] -> Prefix b
- partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])
- filterAndRest :: (a -> Bool) -> [a] -> ([a], Suffix a)
- mapMaybeAndRest :: (a -> Maybe b) -> [a] -> ([b], Suffix a)
- holes :: [a] -> [(a, [a])]
- commonPrefix :: Eq a => [a] -> [a] -> Prefix a
- dropCommon :: [a] -> [b] -> (Suffix a, Suffix b)
- stripPrefixBy :: (a -> a -> Bool) -> Prefix a -> [a] -> Maybe (Suffix a)
- commonSuffix :: Eq a => [a] -> [a] -> Suffix a
- stripReversedSuffix :: Eq a => ReversedSuffix a -> [a] -> Maybe (Prefix a)
- type ReversedSuffix a = [a]
- data StrSufSt a
  - = SSSMismatch
  - | SSSStrip (ReversedSuffix a)
  - | SSSResult [a]
- suffixesSatisfying :: (a -> Bool) -> [a] -> [Bool]
- findOverlap :: Eq a => [a] -> [a] -> (Int, Int)
- sorted :: Ord a => [a] -> Bool
- allConsecutive :: (a -> a -> Bool) -> [a] -> Bool
- distinct :: Eq a => [a] -> Bool
- fastDistinct :: Ord a => [a] -> Bool
- allDuplicates :: Ord a => [a] -> [a]
- nubAndDuplicatesOn :: Ord b => (a -> b) -> [a] -> ([a], [a])
- nubFavouriteOn :: forall a b c. (Ord b, Eq c, Hashable c) => (a -> b) -> (a -> c) -> [a] -> [a]
- uniqOn :: Ord b => (a -> b) -> [a] -> [a]
- allEqual :: Eq a => [a] -> Bool
- nubM :: Monad m => (a -> a -> m Bool) -> [a] -> m [a]
- zipWithKeepRest :: (a -> b -> b) -> [a] -> [b] -> [b]
- editDistanceSpec :: Eq a => [a] -> [a] -> Int
- mergeStrictlyOrderedBy :: (a -> a -> Bool) -> [a] -> [a] -> Maybe [a]
- uncons :: [a] -> Maybe (a, [a])

# Documentation

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

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.

type Prefix a Source #

Arguments

= [a] | The list before the split point.

asum :: Alternative m => [m a] -> m a Source #

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

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

align :: [a] -> [b] -> [These a b] Source #

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

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

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

dropEnd :: Int -> [a] -> Prefix a Source #

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

    dropEnd n = reverse . drop n . reverse

Forces the whole list even for `n==0`.

spanEnd :: (a -> Bool) -> [a] -> (Prefix a, Suffix a) Source #

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

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

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

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

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

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

Precondition: the index is >= 0.

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

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

Otherwise, `Nothing` is returned.

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

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

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

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

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

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

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

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

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

The name is chosen akin to `genericIndex`.

hasElem :: Ord a => [a] -> a -> Bool Source #

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

initLast1 :: a -> [a] -> ([a], a) Source #

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

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

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.

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

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

Cf. `ifNull`.

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

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

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

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

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

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

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

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

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

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

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

`init`, safe. O(n).

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

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

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

Last element (safe). O(n).

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

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

type Suffix a Source #

Arguments

= [a] | The list after the split point.

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

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

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

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

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

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

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

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

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

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

Cf. `ifNull`.

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

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

dropFrom :: Eq a => List1 a -> [a] -> [a] Source #

`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

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

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

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

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

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

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

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

Tail function (safe). O(1).

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

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

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

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

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

`init`, safe. O(n).

asum1 :: Alternative m => m a -> [m a] -> m a Source #

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

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

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!?

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

A generalised variant of `elemIndex`. O(n).

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

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

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

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

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

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

`takeWhileJust f = fst . spanJust f`.

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

Partition a list into `Nothing`s and `Just`s. O(n).

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

Note: ``mapMaybe` f = snd . partitionMaybe f`.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type ReversedSuffix a = [a] Source #

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.

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

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

findOverlap :: Eq a => [a] -> [a] -> (Int, Int) Source #

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.

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

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

Assumes that the `Ord` instance implements a partial order.

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

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

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.

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

fastDistinct :: Ord a => [a] -> Bool Source #

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

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

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

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

`allDuplicates xs == sort $ xs \ nub xs`.

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

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

nubFavouriteOn Source #

Arguments

:: forall a b c. (Ord b, Eq c, Hashable c) |
=> (a -> b) | The values returned by this function are used to determine which element from a group of equal elements that is returned: the smallest one is chosen (and if two elements are equally small, then the first one is chosen).
-> (a -> c) | Two elements are treated as equal if this function returns the same value for both elements.
-> [a] |
-> [a] |

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

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

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.

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

nubM :: Monad m => (a -> a -> m Bool) -> [a] -> m [a] Source #

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

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

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

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

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

mergeStrictlyOrderedBy :: (a -> a -> Bool) -> [a] -> [a] -> Maybe [a] Source #

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

\(\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

Expand

    >>> uncons []
    Nothing

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

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

Since: base-4.8.0.0