Safe Haskell | None |
---|---|
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
- allEqual :: Eq a => List1 a -> Bool
- breakAfter :: (a -> Bool) -> List1 a -> (List1 a, [a])
- catMaybes :: List1 (Maybe a) -> [a]
- concat :: [List1 a] -> [a]
- concatMap1 :: (a -> List1 b) -> List1 a -> List1 b
- find :: (a -> Bool) -> List1 a -> Maybe a
- foldr :: (a -> b -> b) -> (a -> b) -> List1 a -> b
- fromListSafe :: List1 a -> [a] -> List1 a
- groupBy' :: (a -> a -> Bool) -> [a] -> [List1 a]
- groupByFst :: Eq a => [(a, b)] -> [(a, List1 b)]
- groupByFst1 :: Eq a => List1 (a, b) -> List1 (a, List1 b)
- groupOn :: Ord b => (a -> b) -> [a] -> [List1 a]
- groupOn1 :: Ord b => (a -> b) -> List1 a -> List1 (List1 a)
- ifNotNull :: [a] -> (List1 a -> b) -> b -> b
- ifNull :: [a] -> b -> (List1 a -> b) -> b
- initLast :: List1 a -> ([a], a)
- last2 :: List1 a -> Maybe (a, a)
- lefts :: List1 (Either a b) -> [a]
- lensHead :: Functor f => (a -> f a) -> List1 a -> f (List1 a)
- lensLast :: Functor f => (a -> f a) -> List1 a -> f (List1 a)
- liftList1 :: (List1 a -> List1 b) -> [a] -> [b]
- mapMaybe :: (a -> Maybe b) -> List1 a -> [b]
- nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a)
- partitionEithers :: List1 (Either a b) -> ([a], [b])
- rights :: List1 (Either a b) -> [b]
- snoc :: [a] -> a -> List1 a
- toList' :: Maybe (List1 a) -> [a]
- union :: Eq a => List1 a -> List1 a -> List1 a
- unlessNull :: Applicative m => [a] -> (List1 a -> m ()) -> m ()
- unlessNullM :: Monad m => m [a] -> (List1 a -> m ()) -> m ()
- unwords :: List1 String -> String
- unzipWith :: (a -> (b, c)) -> List1 a -> (List1 b, List1 c)
- updateHead :: (a -> a) -> List1 a -> List1 a
- updateLast :: (a -> a) -> List1 a -> List1 a
- wordsBy :: (a -> Bool) -> [a] -> [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 ()
- type List1 = NonEmpty
- type String1 = List1 Char
- (!!) :: HasCallStack => NonEmpty a -> Int -> a
- (<|) :: a -> NonEmpty a -> NonEmpty a
- append :: NonEmpty a -> NonEmpty a -> NonEmpty a
- appendList :: NonEmpty a -> [a] -> NonEmpty a
- break :: (a -> Bool) -> NonEmpty a -> ([a], [a])
- compareLength :: NonEmpty a -> Int -> Ordering
- cons :: a -> NonEmpty a -> NonEmpty a
- cycle :: NonEmpty a -> NonEmpty a
- drop :: Int -> NonEmpty a -> [a]
- dropWhile :: (a -> Bool) -> NonEmpty a -> [a]
- filter :: (a -> Bool) -> NonEmpty a -> [a]
- group :: (Foldable f, Eq a) => f a -> [NonEmpty a]
- group1 :: Eq a => NonEmpty a -> NonEmpty (NonEmpty a)
- groupAllWith :: Ord b => (a -> b) -> [a] -> [NonEmpty a]
- groupAllWith1 :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a)
- groupBy :: Foldable f => (a -> a -> Bool) -> f a -> [NonEmpty a]
- groupBy1 :: (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
- groupWith :: (Foldable f, Eq b) => (a -> b) -> f a -> [NonEmpty a]
- groupWith1 :: Eq b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a)
- head :: NonEmpty a -> a
- init :: NonEmpty a -> [a]
- inits :: Foldable f => f a -> NonEmpty [a]
- inits1 :: NonEmpty a -> NonEmpty (NonEmpty a)
- insert :: (Foldable f, Ord a) => a -> f a -> NonEmpty a
- intersperse :: a -> NonEmpty a -> NonEmpty a
- isPrefixOf :: Eq a => [a] -> NonEmpty a -> Bool
- iterate :: (a -> a) -> a -> NonEmpty a
- last :: NonEmpty a -> a
- length :: NonEmpty a -> Int
- map :: (a -> b) -> NonEmpty a -> NonEmpty b
- nonEmpty :: [a] -> Maybe (NonEmpty a)
- nub :: Eq a => NonEmpty a -> NonEmpty a
- nubBy :: (a -> a -> Bool) -> NonEmpty a -> NonEmpty a
- partition :: (a -> Bool) -> NonEmpty a -> ([a], [a])
- permutations :: [a] -> NonEmpty [a]
- permutations1 :: NonEmpty a -> NonEmpty (NonEmpty a)
- prependList :: [a] -> NonEmpty a -> NonEmpty a
- repeat :: a -> NonEmpty a
- reverse :: NonEmpty a -> NonEmpty a
- scanl :: Foldable f => (b -> a -> b) -> b -> f a -> NonEmpty b
- scanl1 :: (a -> a -> a) -> NonEmpty a -> NonEmpty a
- scanr :: Foldable f => (a -> b -> b) -> b -> f a -> NonEmpty b
- scanr1 :: (a -> a -> a) -> NonEmpty a -> NonEmpty a
- singleton :: a -> NonEmpty a
- some1 :: Alternative f => f a -> f (NonEmpty a)
- sort :: Ord a => NonEmpty a -> NonEmpty a
- sortBy :: (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
- sortOn :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty a
- sortWith :: Ord o => (a -> o) -> NonEmpty a -> NonEmpty a
- span :: (a -> Bool) -> NonEmpty a -> ([a], [a])
- splitAt :: Int -> NonEmpty a -> ([a], [a])
- tail :: NonEmpty a -> [a]
- tails :: Foldable f => f a -> NonEmpty [a]
- tails1 :: NonEmpty a -> NonEmpty (NonEmpty a)
- take :: Int -> NonEmpty a -> [a]
- takeWhile :: (a -> Bool) -> NonEmpty a -> [a]
- transpose :: NonEmpty (NonEmpty a) -> NonEmpty (NonEmpty a)
- uncons :: NonEmpty a -> (a, Maybe (NonEmpty a))
- unfold :: (a -> (b, Maybe a)) -> a -> NonEmpty b
- unfoldr :: (a -> (b, Maybe a)) -> a -> NonEmpty b
- xor :: NonEmpty Bool -> Bool
- zip :: NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
- zipWith :: (a -> b -> c) -> NonEmpty a -> NonEmpty b -> NonEmpty c
- data NonEmpty a = a :| [a]
- class IsList l where
- type family Item l
- unzip :: Functor f => f (a, b) -> (f a, f b)
Documentation
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).
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])
foldr :: (a -> b -> b) -> (a -> b) -> List1 a -> b Source #
List foldr
but with a base case for the singleton list.
Arguments
:: List1 a | Default value if convertee is empty. |
-> [a] | List to convert, supposedly non-empty. |
-> List1 a | Converted list. |
Safe version of fromList
.
groupByFst :: Eq a => [(a, b)] -> [(a, List1 b)] Source #
Group consecutive items that share the same first component.
groupByFst1 :: Eq a => List1 (a, b) -> List1 (a, List1 b) Source #
Group consecutive items that share the same first component.
lensHead :: Functor f => (a -> f a) -> List1 a -> f (List1 a) Source #
Focus on the first element of a non-empty list. O(1).
lensLast :: Functor f => (a -> f a) -> List1 a -> f (List1 a) Source #
Focus on the last element of a non-empty list. O(n).
nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a) Source #
Non-efficient, monadic nub
.
O(n²).
partitionEithers :: List1 (Either a b) -> ([a], [b]) Source #
Like partitionEithers
.
union :: Eq a => List1 a -> List1 a -> List1 a Source #
Like union
. Duplicates in the first list are not removed.
O(nm).
unlessNull :: Applicative m => [a] -> (List1 a -> m ()) -> m () Source #
The more general type Null m => [a] -> (List1 a -> m) -> m
often causes type inference to fail, as we do not in general have
instance Applicative m => Null (m ())
.
unlessNullM :: Monad m => m [a] -> (List1 a -> m ()) -> m () Source #
updateHead :: (a -> a) -> List1 a -> List1 a Source #
Update the first element of a non-empty list. O(1).
updateLast :: (a -> a) -> List1 a -> List1 a Source #
Update the last element of a non-empty list. O(n).
zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c) Source #
Like zipWithM
.
(!!) :: HasCallStack => NonEmpty a -> Int -> a infixl 9 #
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.
appendList :: NonEmpty a -> [a] -> NonEmpty a #
Attach a list at the end of a NonEmpty
.
>>>
appendList (1 :| [2,3]) []
1 :| [2,3]
>>>
appendList (1 :| [2,3]) [4,5]
1 :| [2,3,4,5]
Since: base-4.16
compareLength :: NonEmpty a -> Int -> Ordering #
Use compareLength
xs
n
as a safer and faster alternative
to compare
(length
xs
) n
. Similarly, it's better
to write compareLength xs 10 == LT
instead of length xs < 10
.
While length
would force and traverse
the entire spine of xs
(which could even diverge if xs
is infinite),
compareLength
traverses at most n
elements to determine its result.
>>>
compareLength ('a' :| []) 1
EQ>>>
compareLength ('a' :| ['b']) 3
LT>>>
compareLength (0 :| [1..]) 100
GT>>>
compareLength undefined 0
GT>>>
compareLength ('a' :| 'b' : undefined) 1
GT
Since: base-4.21.0.0
cycle :: NonEmpty a -> NonEmpty a #
returns the infinite repetition of cycle
xsxs
:
cycle (1 :| [2,3]) = 1 :| [2,3,1,2,3,...]
drop :: Int -> NonEmpty a -> [a] #
drops the first drop
n xsn
elements off the front of
the sequence xs
.
filter :: (a -> Bool) -> NonEmpty a -> [a] #
removes any elements from filter
p xsxs
that do not satisfy p
.
group :: (Foldable f, Eq a) => f a -> [NonEmpty a] #
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, and consecutive equal elements
of the input end up in the same stream of the output list.
For example, in list notation:
>>>
group "Mississippi"
['M' :| "",'i' :| "",'s' :| "s",'i' :| "",'s' :| "s",'i' :| "",'p' :| "p",'i' :| ""]
groupAllWith :: Ord b => (a -> b) -> [a] -> [NonEmpty a] #
groupAllWith
operates like groupWith
, but sorts the list
first so that each equivalence class has, at most, one list in the
output
groupAllWith1 :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a) #
groupAllWith1
is to groupWith1
as groupAllWith
is to groupWith
groupWith1 :: Eq b => (a -> b) -> NonEmpty a -> NonEmpty (NonEmpty a) #
groupWith1
is to group1
as groupWith
is to group
insert :: (Foldable f, Ord a) => a -> f a -> NonEmpty a #
inserts insert
x xsx
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.
intersperse :: a -> NonEmpty a -> NonEmpty a #
'intersperse x xs' alternates elements of the list with copies of x
.
intersperse 0 (1 :| [2,3]) == 1 :| [0,2,0,3]
isPrefixOf :: Eq a => [a] -> NonEmpty a -> Bool #
The isPrefixOf
function returns True
if the first argument is
a prefix of the second.
iterate :: (a -> a) -> a -> NonEmpty a #
produces the infinite sequence
of repeated applications of iterate
f xf
to x
.
iterate f x = x :| [f x, f (f x), ..]
partition :: (a -> Bool) -> NonEmpty a -> ([a], [a]) #
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)
permutations :: [a] -> NonEmpty [a] #
The permutations
function returns the list of all permutations of the argument.
Since: base-4.20.0.0
permutations1 :: NonEmpty a -> NonEmpty (NonEmpty a) #
permutations1
operates like permutations
, but uses the knowledge that its input is
non-empty to produce output where every element is non-empty.
permutations1 = fmap fromList . permutations . toList
Since: base-4.20.0.0
prependList :: [a] -> NonEmpty a -> NonEmpty a #
Attach a list at the beginning of a NonEmpty
.
>>>
prependList [] (1 :| [2,3])
1 :| [2,3]
>>>
prependList [negate 1, 0] (1 :| [2, 3])
-1 :| [0,1,2,3]
Since: base-4.16
some1 :: Alternative f => f a -> f (NonEmpty a) #
sequences some1
xx
one or more times.
sortOn :: Ord b => (a -> b) -> NonEmpty a -> NonEmpty a #
Sort a NonEmpty
on a user-supplied projection of its elements.
See sortOn
for more detailed information.
Examples
>>>
sortOn fst $ (2, "world") :| [(4, "!"), (1, "Hello")]
(1,"Hello") :| [(2,"world"),(4,"!")]
>>>
sortOn List.length ("jim" :| ["creed", "pam", "michael", "dwight", "kevin"])
"jim" :| ["pam","creed","kevin","dwight","michael"]
Performance notes
This function minimises the projections performed, by materialising the projections in an intermediate list.
For trivial projections, you should prefer using sortBy
with
comparing
, for example:
>>>
sortBy (comparing fst) $ (3, 1) :| [(2, 2), (1, 3)]
(1,3) :| [(2,2),(3,1)]
Or, for the exact same API as sortOn
, you can use `sortBy . comparing`:
>>>
(sortBy . comparing) fst $ (3, 1) :| [(2, 2), (1, 3)]
(1,3) :| [(2,2),(3,1)]
sortWith
is an alias for `sortBy . comparing`.
Since: base-4.20.0.0
span :: (a -> Bool) -> NonEmpty a -> ([a], [a]) #
returns the longest prefix of span
p xsxs
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
splitAt :: Int -> NonEmpty a -> ([a], [a]) #
returns a pair consisting of the prefix of splitAt
n xsxs
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
takeWhile :: (a -> Bool) -> NonEmpty a -> [a] #
returns the longest prefix of the stream
takeWhile
p xsxs
for which the predicate p
holds.
uncons :: NonEmpty a -> (a, Maybe (NonEmpty a)) #
uncons
produces the first element of the stream, and a stream of the
remaining elements, if any.
zip :: NonEmpty a -> NonEmpty b -> NonEmpty (a, b) #
The zip
function takes two streams and returns a stream of
corresponding pairs.
Non-empty (and non-strict) list type.
Since: base-4.9.0.0
Constructors
a :| [a] infixr 5 |
Instances
The IsList
class and its methods are intended to be used in
conjunction with the OverloadedLists extension.
Since: base-4.7.0.0
Methods
The fromList
function constructs the structure l
from the given
list of Item l
fromListN :: Int -> [Item l] -> l #
The fromListN
function takes the input list's length and potentially
uses it to construct the structure l
more efficiently compared to
fromList
. If the given number does not equal to the input list's length
the behaviour of fromListN
is not specified.
fromListN (length xs) xs == fromList xs
The toList
function extracts a list of Item l
from the structure l
.
It should satisfy fromList . toList = id.
Instances
IsList CharString # | |||||
Defined in Data.ListLike.CharString Associated Types
Methods fromList :: [Item CharString] -> CharString # fromListN :: Int -> [Item CharString] -> CharString # toList :: CharString -> [Item CharString] # | |||||
IsList CharStringLazy # | |||||
Defined in Data.ListLike.CharString Associated Types
Methods fromList :: [Item CharStringLazy] -> CharStringLazy # fromListN :: Int -> [Item CharStringLazy] -> CharStringLazy # toList :: CharStringLazy -> [Item CharStringLazy] # | |||||
IsList Chars # | |||||
IsList ByteArray # | Since: base-4.17.0.0 | ||||
IsList Builder # | For long or infinite lists use | ||||
IsList ByteString # | Since: bytestring-0.10.12.0 | ||||
Defined in Data.ByteString.Internal.Type Associated Types
Methods fromList :: [Item ByteString] -> ByteString # fromListN :: Int -> [Item ByteString] -> ByteString # toList :: ByteString -> [Item ByteString] # | |||||
IsList ByteString # | Since: bytestring-0.10.12.0 | ||||
Defined in Data.ByteString.Lazy.Internal Associated Types
Methods fromList :: [Item ByteString] -> ByteString # fromListN :: Int -> [Item ByteString] -> ByteString # toList :: ByteString -> [Item ByteString] # | |||||
IsList ShortByteString # | Since: bytestring-0.10.12.0 | ||||
Defined in Data.ByteString.Short.Internal Associated Types
Methods fromList :: [Item ShortByteString] -> ShortByteString # fromListN :: Int -> [Item ShortByteString] -> ShortByteString # toList :: ShortByteString -> [Item ShortByteString] # | |||||
IsList IntSet # | Since: containers-0.5.6.2 | ||||
IsList Version # | Since: base-4.8.0.0 | ||||
IsList CallStack # | Be aware that 'fromList . toList = id' only for unfrozen Since: base-4.9.0.0 | ||||
IsList ShortText # | Note: Surrogate pairs ( Since: text-short-0.1.2 | ||||
IsList (List2 a) Source # |
| ||||
IsList (KeyMap v) # | Since: aeson-2.0.2.0 | ||||
IsList (IntMap a) # | Since: containers-0.5.6.2 | ||||
IsList (Seq a) # | |||||
Ord a => IsList (Set a) # | Since: containers-0.5.6.2 | ||||
IsList (DNonEmpty a) # | |||||
Defined in Data.DList.DNonEmpty.Internal Associated Types
| |||||
IsList (DList a) # | |||||
Enum a => IsList (EnumSet a) # | |||||
IsList (NonEmpty a) # | Since: base-4.9.0.0 | ||||
IsList (ZipList a) # | Since: base-4.15.0.0 | ||||
IsList (Array a) # | |||||
Prim a => IsList (PrimArray a) # | Since: primitive-0.6.4.0 | ||||
Defined in Data.Primitive.PrimArray Associated Types
| |||||
IsList (SmallArray a) # | |||||
Defined in Data.Primitive.SmallArray Associated Types
Methods fromList :: [Item (SmallArray a)] -> SmallArray a # fromListN :: Int -> [Item (SmallArray a)] -> SmallArray a # toList :: SmallArray a -> [Item (SmallArray a)] # | |||||
(Eq a, Hashable a) => IsList (HashSet a) # | |||||
IsList (Vector a) # | |||||
Prim a => IsList (Vector a) # | |||||
Storable a => IsList (Vector a) # | |||||
IsList (Vector a) # | |||||
IsList [a] # | Since: base-4.7.0.0 | ||||
Ord k => IsList (Map k v) # | Since: containers-0.5.6.2 | ||||
Enum k => IsList (EnumMap k a) # | |||||
(Eq k, Hashable k) => IsList (HashMap k v) # | |||||
Defined in Data.HashMap.Internal Associated Types
|
The Item
type function returns the type of items of the structure
l
.
Instances
type Item CharString # | |
Defined in Data.ListLike.CharString | |
type Item CharStringLazy # | |
Defined in Data.ListLike.CharString | |
type Item Chars # | |
Defined in Data.ListLike.Chars | |
type Item ByteArray # | |
Defined in Data.Array.Byte | |
type Item Builder # | |
Defined in Data.ByteString.Builder.Internal | |
type Item ByteString # | |
Defined in Data.ByteString.Internal.Type | |
type Item ByteString # | |
Defined in Data.ByteString.Lazy.Internal | |
type Item ShortByteString # | |
Defined in Data.ByteString.Short.Internal | |
type Item IntSet # | |
Defined in Data.IntSet.Internal | |
type Item Version # | |
Defined in GHC.Internal.IsList | |
type Item CallStack # | |
Defined in GHC.Internal.IsList | |
type Item Text # | |
type Item Builder # | |
Defined in Data.ListLike.Text.Builder | |
type Item Text # | |
Defined in Data.Text.Lazy | |
type Item ShortText # | |
Defined in Data.Text.Short.Internal | |
type Item (List2 a) Source # | |
Defined in Agda.Utils.List2 | |
type Item (KeyMap v) # | |
Defined in Data.Aeson.KeyMap | |
type Item (IntMap a) # | |
Defined in Data.IntMap.Internal | |
type Item (Seq a) # | |
Defined in Data.Sequence.Internal | |
type Item (Set a) # | |
Defined in Data.Set.Internal | |
type Item (DNonEmpty a) # | |
Defined in Data.DList.DNonEmpty.Internal | |
type Item (DList a) # | |
Defined in Data.DList.Internal | |
type Item (EnumSet a) # | |
Defined in Data.EnumSet | |
type Item (FMList a) # | |
Defined in Data.ListLike.FMList | |
type Item (NonEmpty a) # | |
Defined in GHC.Internal.IsList | |
type Item (ZipList a) # | |
Defined in GHC.Internal.IsList | |
type Item (Array a) # | |
Defined in Data.Primitive.Array | |
type Item (PrimArray a) # | |
Defined in Data.Primitive.PrimArray | |
type Item (SmallArray a) # | |
Defined in Data.Primitive.SmallArray | |
type Item (HashSet a) # | |
Defined in Data.HashSet.Internal | |
type Item (UTF8 ByteString) # | |
Defined in Data.ListLike.UTF8 | |
type Item (UTF8 ByteString) # | |
Defined in Data.ListLike.UTF8 | |
type Item (Vector a) # | |
Defined in Data.Vector | |
type Item (Vector a) # | |
Defined in Data.Vector.Primitive | |
type Item (Vector a) # | |
Defined in Data.Vector.Storable | |
type Item (Vector a) # | |
Defined in Data.Vector.Strict | |
type Item (Vector e) # | |
Defined in Data.Vector.Unboxed | |
type Item [a] # | |
Defined in GHC.Internal.IsList type Item [a] = a | |
type Item (Map k v) # | |
Defined in Data.Map.Internal | |
type Item (EnumMap k a) # | |
Defined in Data.EnumMap.Base | |
type Item (Array i e) # | |
Defined in Data.ListLike.Instances | |
type Item (HashMap k v) # | |
Defined in Data.HashMap.Internal |