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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.List

Contents

- Variants of list case, cons, head, tail, init, last
- Lookup and indexing
- Update
- Sublist extraction and partitioning
- Prefix and suffix
  - Prefix
  - Suffix
  - Finding overlap
- Groups and chunks
- List as sets
- Zipping
- Unzipping
- Edit distance

Description

Utility functions for lists.

Synopsis

- snoc :: [a] -> a -> [a]
- caseList :: [a] -> b -> (a -> [a] -> b) -> b
- caseListM :: Monad m => m [a] -> m b -> (a -> [a] -> m b) -> m b
- listCase :: b -> (a -> [a] -> b) -> [a] -> b
- headWithDefault :: a -> [a] -> a
- tailMaybe :: [a] -> Maybe [a]
- tailWithDefault :: [a] -> [a] -> [a]
- lastMaybe :: [a] -> Maybe a
- lastWithDefault :: a -> [a] -> a
- last1 :: a -> [a] -> a
- last2 :: [a] -> Maybe (a, a)
- uncons :: [a] -> Maybe (a, [a])
- mcons :: Maybe a -> [a] -> [a]
- initLast :: [a] -> Maybe ([a], a)
- initLast1 :: a -> [a] -> ([a], a)
- init1 :: a -> [a] -> [a]
- initMaybe :: [a] -> Maybe [a]
- initWithDefault :: [a] -> [a] -> [a]
- (!!!) :: [a] -> Int -> Maybe a
- indexWithDefault :: a -> [a] -> Int -> a
- findWithIndex :: (a -> Bool) -> [a] -> Maybe (a, Int)
- genericElemIndex :: (Eq a, Integral i) => a -> [a] -> Maybe i
- downFrom :: Integral a => a -> [a]
- updateHead :: (a -> a) -> [a] -> [a]
- updateLast :: (a -> a) -> [a] -> [a]
- updateAt :: Int -> (a -> a) -> [a] -> [a]
- type Prefix a = [a]
- type Suffix a = [a]
- splitExactlyAt :: Integral n => n -> [a] -> Maybe (Prefix a, Suffix a)
- dropEnd :: forall a. Int -> [a] -> Prefix a
- spanEnd :: forall a. (a -> Bool) -> [a] -> (Prefix a, Suffix a)
- breakAfter1 :: (a -> Bool) -> a -> [a] -> (List1 a, [a])
- breakAfter :: (a -> Bool) -> [a] -> ([a], [a])
- takeWhileJust :: (a -> Maybe b) -> [a] -> Prefix b
- spanJust :: (a -> Maybe b) -> [a] -> (Prefix b, Suffix a)
- partitionMaybe :: (a -> Maybe b) -> [a] -> ([a], [b])
- filterAndRest :: (a -> Bool) -> [a] -> ([a], Suffix a)
- mapMaybeAndRest :: (a -> Maybe b) -> [a] -> ([b], Suffix a)
- isSublistOf :: Eq a => [a] -> [a] -> Bool
- 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
- stripSuffix :: Eq a => Suffix a -> [a] -> Maybe (Prefix a)
- type ReversedSuffix a = [a]
- stripReversedSuffix :: forall a. Eq a => ReversedSuffix a -> [a] -> Maybe (Prefix a)
- data StrSufSt a
  - = SSSMismatch
  - | SSSStrip (ReversedSuffix a)
  - | SSSResult [a]
- findOverlap :: forall a. Eq a => [a] -> [a] -> (Int, Int)
- groupOn :: Ord b => (a -> b) -> [a] -> [[a]]
- groupBy' :: (a -> a -> Bool) -> [a] -> [[a]]
- wordsBy :: (a -> Bool) -> [a] -> [[a]]
- chop :: Int -> [a] -> [[a]]
- chopWhen :: forall a. (a -> Bool) -> [a] -> [[a]]
- hasElem :: Ord a => [a] -> a -> Bool
- sorted :: Ord a => [a] -> Bool
- distinct :: Eq a => [a] -> Bool
- fastDistinct :: Ord a => [a] -> Bool
- duplicates :: Ord a => [a] -> [a]
- allDuplicates :: Ord a => [a] -> [a]
- nubAndDuplicatesOn :: Ord b => (a -> b) -> [a] -> ([a], [a])
- nubOn :: Ord b => (a -> b) -> [a] -> [a]
- uniqOn :: Ord b => (a -> b) -> [a] -> [a]
- allEqual :: Eq a => [a] -> Bool
- nubM :: Monad m => (a -> a -> m Bool) -> [a] -> m [a]
- zipWith' :: (a -> b -> c) -> [a] -> [b] -> Maybe [c]
- zipWithKeepRest :: (a -> b -> b) -> [a] -> [b] -> [b]
- unzipWith :: (a -> (b, c)) -> [a] -> ([b], [c])
- editDistanceSpec :: Eq a => [a] -> [a] -> Int
- editDistance :: forall a. Eq a => [a] -> [a] -> Int
- mergeStrictlyOrderedBy :: (a -> a -> Bool) -> [a] -> [a] -> Maybe [a]

# Variants of list case, cons, head, tail, init, last

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

Cf. `ifNull`.

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

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

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

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

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

Tail function (safe). O(1).

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

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

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

Last element (safe). O(n).

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

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

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

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

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

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

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

Opposite of cons `(:)`, safe. O(1).

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

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

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

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

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

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

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

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

`init`, safe. O(n).

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

`init`, safe. O(n).

# Lookup and indexing

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

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

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

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

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

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

# Update

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

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.

# Sublist extraction and partitioning

type Prefix a Source #

Arguments

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

type Suffix a Source #

Arguments

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

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

dropEnd :: forall a. 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 :: forall a. (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)`.

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

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

A generalized version of `span`. `O(length . 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).

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

Sublist relation.

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

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

# Prefix and suffix

## Prefix

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

## Suffix

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

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

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

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

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

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.

## Finding overlap

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

Find out whether the first string `xs` has a suffix 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.

# Groups and chunks

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

``groupOn` f = `groupBy` ((`==`) `on` f) `.` `sortBy` (`compare` `on` f)`. O(n log n).

groupBy' :: (a -> a -> Bool) -> [a] -> [[a]] Source #

A variant of `groupBy` which applies the predicate to consecutive pairs. O(n). DEPRECATED in favor of `groupBy'`.

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

Split a list into sublists. Generalisation of the prelude function `words`. O(n).

    words xs == wordsBy isSpace xs

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

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

chopWhen :: forall a. (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

# List as sets

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

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

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

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.

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

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

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

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

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.

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

# Zipping

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

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

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

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

# Unzipping

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

# Edit distance

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

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

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

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

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