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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Utils.List1

Description

Non-empty lists.

Better name `List1` for non-empty lists, plus missing functionality.

Import: @

{-# LANGUAGE PatternSynonyms #-}

import Agda.Utils.List1 (List1, pattern (:|)) import qualified Agda.Utils.List1 as List1

@

Synopsis

- type List1 = NonEmpty
- initLast :: List1 a -> ([a], a)
- appendList :: List1 a -> [a] -> List1 a
- prependList :: [a] -> List1 a -> List1 a
- snoc :: [a] -> a -> List1 a
- groupBy' :: forall a. (a -> a -> Bool) -> [a] -> [List1 a]
- breakAfter :: (a -> Bool) -> List1 a -> (List1 a, [a])
- concat :: [List1 a] -> [a]
- union :: Eq a => List1 a -> List1 a -> List1 a
- ifNull :: [a] -> b -> (List1 a -> b) -> b
- ifNotNull :: [a] -> (List1 a -> b) -> b -> b
- unlessNull :: Null m => [a] -> (List1 a -> m) -> m
- allEqual :: Eq a => List1 a -> Bool
- catMaybes :: List1 (Maybe a) -> [a]
- mapMaybe :: (a -> Maybe b) -> List1 a -> [b]
- partitionEithers :: List1 (Either a b) -> ([a], [b])
- lefts :: List1 (Either a b) -> [a]
- rights :: List1 (Either a b) -> [b]
- nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a)
- zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c)
- zipWithM_ :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m ()
- zipWith :: (a -> b -> c) -> NonEmpty a -> NonEmpty b -> NonEmpty c
- zip :: NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
- xor :: NonEmpty Bool -> Bool
- unzip :: Functor f => f (a, b) -> (f a, f b)
- unfoldr :: (a -> (b, Maybe a)) -> a -> NonEmpty b
- unfold :: (a -> (b, Maybe a)) -> a -> NonEmpty b
- uncons :: NonEmpty a -> (a, Maybe (NonEmpty a))
- transpose :: NonEmpty (NonEmpty a) -> NonEmpty (NonEmpty a)
- toList :: NonEmpty a -> [a]
- takeWhile :: (a -> Bool) -> NonEmpty a -> [a]
- take :: Int -> NonEmpty a -> [a]
- tails :: Foldable f => f a -> NonEmpty [a]
- tail :: NonEmpty a -> [a]
- splitAt :: Int -> NonEmpty a -> ([a], [a])
- span :: (a -> Bool) -> NonEmpty a -> ([a], [a])
- sortWith :: Ord o => (a -> o) -> NonEmpty a -> NonEmpty a
- sortBy :: (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
- sort :: Ord a => NonEmpty a -> NonEmpty a
- some1 :: Alternative f => f a -> f (NonEmpty a)
- singleton :: a -> NonEmpty a
- scanr1 :: (a -> a -> a) -> NonEmpty a -> NonEmpty a
- scanr :: Foldable f => (a -> b -> b) -> b -> f a -> NonEmpty b
- scanl1 :: (a -> a -> a) -> NonEmpty a -> NonEmpty a
- scanl :: Foldable f => (b -> a -> b) -> b -> f a -> NonEmpty b
- reverse :: NonEmpty a -> NonEmpty a
- repeat :: a -> NonEmpty a
- partition :: (a -> Bool) -> NonEmpty a -> ([a], [a])
- nubBy :: (a -> a -> Bool) -> NonEmpty a -> NonEmpty a
- nub :: Eq a => NonEmpty a -> NonEmpty a
- nonEmpty :: [a] -> Maybe (NonEmpty a)
- map :: (a -> b) -> NonEmpty a -> NonEmpty b
- length :: NonEmpty a -> Int
- last :: NonEmpty a -> a
- iterate :: (a -> a) -> a -> NonEmpty a
- isPrefixOf :: Eq a => [a] -> NonEmpty a -> Bool
- intersperse :: a -> NonEmpty a -> NonEmpty a
- insert :: (Foldable f, Ord a) => a -> f a -> NonEmpty a
- inits :: Foldable f => f a -> NonEmpty [a]
- init :: NonEmpty a -> [a]
- head :: NonEmpty a -> a
- groupWith1 :: Eq b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a)
- groupWith :: (Foldable f, Eq b) => (a -> b) -> f a -> [NonEmpty a]
- groupBy1 :: (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
- groupBy :: Foldable f => (a -> a -> Bool) -> f a -> [NonEmpty a]
- groupAllWith1 :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a)
- groupAllWith :: Ord b => (a -> b) -> [a] -> [NonEmpty a]
- group1 :: Eq a => NonEmpty a -> NonEmpty (NonEmpty a)
- group :: (Foldable f, Eq a) => f a -> [NonEmpty a]
- fromList :: [a] -> NonEmpty a
- filter :: (a -> Bool) -> NonEmpty a -> [a]
- dropWhile :: (a -> Bool) -> NonEmpty a -> [a]
- drop :: Int -> NonEmpty a -> [a]
- cycle :: NonEmpty a -> NonEmpty a
- cons :: a -> NonEmpty a -> NonEmpty a
- break :: (a -> Bool) -> NonEmpty a -> ([a], [a])
- (<|) :: a -> NonEmpty a -> NonEmpty a
- (!!) :: NonEmpty a -> Int -> a
- pattern (:|) :: a -> [a] -> NonEmpty a

# Documentation

type List1 = NonEmpty Source #

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

Return the last element and the rest.

appendList :: List1 a -> [a] -> List1 a Source #

Build a list with one element.

Append a list to a non-empty list.

prependList :: [a] -> List1 a -> List1 a Source #

Prepend a list to a non-empty list.

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

More precise type for `snoc`.

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

More precise type for `groupBy'`.

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

breakAfter :: (a -> Bool) -> List1 a -> (List1 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])

concat :: [List1 a] -> [a] Source #

Concatenate one or more non-empty lists.

union :: Eq a => List1 a -> List1 a -> List1 a Source #

Like `union`. Duplicates in the first list are not removed. O(nm).

ifNull :: [a] -> b -> (List1 a -> b) -> b Source #

ifNotNull :: [a] -> (List1 a -> b) -> b -> b Source #

unlessNull :: Null m => [a] -> (List1 a -> m) -> m Source #

allEqual :: Eq a => List1 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).

catMaybes :: List1 (Maybe a) -> [a] Source #

Like `catMaybes`.

mapMaybe :: (a -> Maybe b) -> List1 a -> [b] Source #

Like `filter`.

partitionEithers :: List1 (Either a b) -> ([a], [b]) Source #

Like `partitionEithers`.

lefts :: List1 (Either a b) -> [a] Source #

Like `lefts`.

rights :: List1 (Either a b) -> [b] Source #

Like `rights`.

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

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

zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c) Source #

Like `zipWithM`.

zipWithM_ :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m () Source #

Like `zipWithM`.

zipWith :: (a -> b -> c) -> NonEmpty a -> NonEmpty b -> NonEmpty c Source #

The `zipWith` function generalizes `zip`. Rather than tupling the elements, the elements are combined using the function passed as the first argument.

zip :: NonEmpty a -> NonEmpty b -> NonEmpty (a, b) Source #

The `zip` function takes two streams and returns a stream of corresponding pairs.

xor :: NonEmpty Bool -> Bool Source #

Compute n-ary logic exclusive OR operation on `NonEmpty` list.

unzip :: Functor f => f (a, b) -> (f a, f b) Source #

The `unzip` function is the inverse of the `zip` function.

unfoldr :: (a -> (b, Maybe a)) -> a -> NonEmpty b Source #

The `unfoldr` function is analogous to Data.List's `unfoldr` operation.

unfold :: (a -> (b, Maybe a)) -> a -> NonEmpty b Source #

`unfold` produces a new stream by repeatedly applying the unfolding function to the seed value to produce an element of type `b` and a new seed value. When the unfolding function returns `Nothing` instead of a new seed value, the stream ends.

uncons :: NonEmpty a -> (a, Maybe (NonEmpty a)) Source #

`uncons` produces the first element of the stream, and a stream of the remaining elements, if any.

transpose :: NonEmpty (NonEmpty a) -> NonEmpty (NonEmpty a) Source #

`transpose` for `NonEmpty`, behaves the same as `transpose` The rows/columns need not be the same length, in which case > transpose . transpose /= id

toList :: NonEmpty a -> [a] Source #

Convert a stream to a normal list efficiently.

takeWhile :: (a -> Bool) -> NonEmpty a -> [a] Source #

``takeWhile` p xs` returns the longest prefix of the stream `xs` for which the predicate `p` holds.

take :: Int -> NonEmpty a -> [a] Source #

``take` n xs` returns the first `n` elements of `xs`.

tails :: Foldable f => f a -> NonEmpty [a] Source #

The `tails` function takes a stream `xs` and returns all the suffixes of `xs`.

tail :: NonEmpty a -> [a] Source #

Extract the possibly-empty tail of the stream.

splitAt :: Int -> NonEmpty a -> ([a], [a]) Source #

``splitAt` n xs` returns a pair consisting of the prefix of `xs` of length `n` and the remaining stream immediately following this prefix.

    'splitAt' n xs == ('take' n xs, 'drop' n xs)
    xs == ys ++ zs where (ys, zs) = 'splitAt' n xs

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

``span` p xs` returns the longest prefix of `xs` that satisfies `p`, together with the remainder of the stream.

    'span' p xs == ('takeWhile' p xs, 'dropWhile' p xs)
    xs == ys ++ zs where (ys, zs) = 'span' p xs

sortWith :: Ord o => (a -> o) -> NonEmpty a -> NonEmpty a Source #

`sortWith` for `NonEmpty`, behaves the same as:

    sortBy . comparing

sortBy :: (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a Source #

`sortBy` for `NonEmpty`, behaves the same as `sortBy`

sort :: Ord a => NonEmpty a -> NonEmpty a Source #

Sort a stream.

some1 :: Alternative f => f a -> f (NonEmpty a) Source #

``some1` x` sequences `x` one or more times.

singleton :: a -> NonEmpty a Source #

Construct a `NonEmpty` list from a single element.

Since: base-4.15

scanr1 :: (a -> a -> a) -> NonEmpty a -> NonEmpty a Source #

`scanr1` is a variant of `scanr` that has no starting value argument.

scanr :: Foldable f => (a -> b -> b) -> b -> f a -> NonEmpty b Source #

`scanr` is the right-to-left dual of `scanl`. Note that

    head (scanr f z xs) == foldr f z xs.

scanl1 :: (a -> a -> a) -> NonEmpty a -> NonEmpty a Source #

`scanl1` is a variant of `scanl` that has no starting value argument:

    scanl1 f [x1, x2, ...] == x1 :| [x1 `f` x2, x1 `f` (x2 `f` x3), ...]

scanl :: Foldable f => (b -> a -> b) -> b -> f a -> NonEmpty b Source #

`scanl` is similar to `foldl`, but returns a stream of successive reduced values from the left:

    scanl f z [x1, x2, ...] == z :| [z `f` x1, (z `f` x1) `f` x2, ...]

Note that

    last (scanl f z xs) == foldl f z xs.

reverse :: NonEmpty a -> NonEmpty a Source #

`reverse` a finite NonEmpty stream.

repeat :: a -> NonEmpty a Source #

``repeat` x` returns a constant stream, where all elements are equal to `x`.

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

The `partition` function takes a predicate `p` and a stream `xs`, and returns a pair of lists. The first list corresponds to the elements of `xs` for which `p` holds; the second corresponds to the elements of `xs` for which `p` does not hold.

    'partition' p xs = ('filter' p xs, 'filter' (not . p) xs)

nubBy :: (a -> a -> Bool) -> NonEmpty a -> NonEmpty a Source #

The `nubBy` function behaves just like `nub`, except it uses a user-supplied equality predicate instead of the overloaded `==` function.

nub :: Eq a => NonEmpty a -> NonEmpty a Source #

The `nub` function removes duplicate elements from a list. In particular, it keeps only the first occurrence of each element. (The name `nub` means 'essence'.) It is a special case of `nubBy`, which allows the programmer to supply their own inequality test.

nonEmpty :: [a] -> Maybe (NonEmpty a) Source #

`nonEmpty` efficiently turns a normal list into a `NonEmpty` stream, producing `Nothing` if the input is empty.

map :: (a -> b) -> NonEmpty a -> NonEmpty b Source #

Map a function over a `NonEmpty` stream.

length :: NonEmpty a -> Int Source #

Number of elements in `NonEmpty` list.

last :: NonEmpty a -> a Source #

Extract the last element of the stream.

iterate :: (a -> a) -> a -> NonEmpty a Source #

``iterate` f x` produces the infinite sequence of repeated applications of `f` to `x`.

    iterate f x = x :| [f x, f (f x), ..]

isPrefixOf :: Eq a => [a] -> NonEmpty a -> Bool Source #

The `isPrefixOf` function returns `True` if the first argument is a prefix of the second.

intersperse :: a -> NonEmpty a -> NonEmpty a Source #

'intersperse x xs' alternates elements of the list with copies of `x`.

    intersperse 0 (1 :| [2,3]) == 1 :| [0,2,0,3]

insert :: (Foldable f, Ord a) => a -> f a -> NonEmpty a Source #

``insert` x xs` inserts `x` into the last position in `xs` where it is still less than or equal to the next element. In particular, if the list is sorted beforehand, the result will also be sorted.

inits :: Foldable f => f a -> NonEmpty [a] Source #

The `inits` function takes a stream `xs` and returns all the finite prefixes of `xs`.

init :: NonEmpty a -> [a] Source #

Extract everything except the last element of the stream.

head :: NonEmpty a -> a Source #

Extract the first element of the stream.

groupWith1 :: Eq b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a) Source #

`groupWith1` is to `group1` as `groupWith` is to `group`

groupWith :: (Foldable f, Eq b) => (a -> b) -> f a -> [NonEmpty a] Source #

`groupWith` operates like `group`, but uses the provided projection when comparing for equality

groupBy1 :: (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a) Source #

`groupBy1` is to `group1` as `groupBy` is to `group`.

groupBy :: Foldable f => (a -> a -> Bool) -> f a -> [NonEmpty a] Source #

`groupBy` operates like `group`, but uses the provided equality predicate instead of `==`.

groupAllWith1 :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a) Source #

`groupAllWith1` is to `groupWith1` as `groupAllWith` is to `groupWith`

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

`groupAllWith` operates like `groupWith`, but sorts the list first so that each equivalence class has, at most, one list in the output

group1 :: Eq a => NonEmpty a -> NonEmpty (NonEmpty a) Source #

`group1` operates like `group`, but uses the knowledge that its input is non-empty to produce guaranteed non-empty output.

group :: (Foldable f, Eq a) => f a -> [NonEmpty a] Source #

The `group` function takes a stream and returns a list of streams such that flattening the resulting list is equal to the argument. Moreover, each stream in the resulting list contains only equal elements. For example, in list notation:

    'group' $ 'cycle' "Mississippi"
      = "M" : "i" : "ss" : "i" : "ss" : "i" : "pp" : "i" : "M" : "i" : ...

fromList :: [a] -> NonEmpty a Source #

Converts a normal list to a `NonEmpty` stream.

Raises an error if given an empty list.

filter :: (a -> Bool) -> NonEmpty a -> [a] Source #

``filter` p xs` removes any elements from `xs` that do not satisfy `p`.

dropWhile :: (a -> Bool) -> NonEmpty a -> [a] Source #

``dropWhile` p xs` returns the suffix remaining after ``takeWhile` p xs`.

drop :: Int -> NonEmpty a -> [a] Source #

``drop` n xs` drops the first `n` elements off the front of the sequence `xs`.

cycle :: NonEmpty a -> NonEmpty a Source #

``cycle` xs` returns the infinite repetition of `xs`:

    cycle (1 :| [2,3]) = 1 :| [2,3,1,2,3,...]

cons :: a -> NonEmpty a -> NonEmpty a Source #

Synonym for `<|`.

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

The ``break` p` function is equivalent to ``span` (not . p)`.

(<|) :: a -> NonEmpty a -> NonEmpty a infixr 5 Source #

Prepend an element to the stream.

(!!) :: NonEmpty a -> Int -> a infixl 9 Source #

`xs !! n` returns the element of the stream `xs` at index `n`. Note that the head of the stream has index 0.

Beware: a negative or out-of-bounds index will cause an error.

pattern (:|) :: a -> [a] -> NonEmpty a infixr 5 Source #