-- | Lists of length at least 2.
--
--   Import as:
--   @
--      import Agda.Utils.List2 (List2(List2))
--      import qualified Agda.Utils.List2 as List2
--   @

module Agda.Utils.List2
  ( module Agda.Utils.List2
  , module Reexport
  ) where

import Control.DeepSeq
import Control.Monad                   ( (<=<) )

import Data.Data                       ( Data )
import qualified Data.List as List

import GHC.Exts                        ( IsList(..) )
import qualified GHC.Exts  as Reexport ( toList )

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

import Agda.Utils.Impossible

-- | Lists of length ≥2.
data List2 a = List2 a a [a]
  deriving (List2 a -> List2 a -> Bool
(List2 a -> List2 a -> Bool)
-> (List2 a -> List2 a -> Bool) -> Eq (List2 a)
forall a. Eq a => List2 a -> List2 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: List2 a -> List2 a -> Bool
$c/= :: forall a. Eq a => List2 a -> List2 a -> Bool
== :: List2 a -> List2 a -> Bool
$c== :: forall a. Eq a => List2 a -> List2 a -> Bool
Eq, Eq (List2 a)
Eq (List2 a)
-> (List2 a -> List2 a -> Ordering)
-> (List2 a -> List2 a -> Bool)
-> (List2 a -> List2 a -> Bool)
-> (List2 a -> List2 a -> Bool)
-> (List2 a -> List2 a -> Bool)
-> (List2 a -> List2 a -> List2 a)
-> (List2 a -> List2 a -> List2 a)
-> Ord (List2 a)
List2 a -> List2 a -> Bool
List2 a -> List2 a -> Ordering
List2 a -> List2 a -> List2 a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {a}. Ord a => Eq (List2 a)
forall a. Ord a => List2 a -> List2 a -> Bool
forall a. Ord a => List2 a -> List2 a -> Ordering
forall a. Ord a => List2 a -> List2 a -> List2 a
min :: List2 a -> List2 a -> List2 a
$cmin :: forall a. Ord a => List2 a -> List2 a -> List2 a
max :: List2 a -> List2 a -> List2 a
$cmax :: forall a. Ord a => List2 a -> List2 a -> List2 a
>= :: List2 a -> List2 a -> Bool
$c>= :: forall a. Ord a => List2 a -> List2 a -> Bool
> :: List2 a -> List2 a -> Bool
$c> :: forall a. Ord a => List2 a -> List2 a -> Bool
<= :: List2 a -> List2 a -> Bool
$c<= :: forall a. Ord a => List2 a -> List2 a -> Bool
< :: List2 a -> List2 a -> Bool
$c< :: forall a. Ord a => List2 a -> List2 a -> Bool
compare :: List2 a -> List2 a -> Ordering
$ccompare :: forall a. Ord a => List2 a -> List2 a -> Ordering
Ord, Int -> List2 a -> ShowS
[List2 a] -> ShowS
List2 a -> String
(Int -> List2 a -> ShowS)
-> (List2 a -> String) -> ([List2 a] -> ShowS) -> Show (List2 a)
forall a. Show a => Int -> List2 a -> ShowS
forall a. Show a => [List2 a] -> ShowS
forall a. Show a => List2 a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [List2 a] -> ShowS
$cshowList :: forall a. Show a => [List2 a] -> ShowS
show :: List2 a -> String
$cshow :: forall a. Show a => List2 a -> String
showsPrec :: Int -> List2 a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> List2 a -> ShowS
Show, Typeable (List2 a)
Typeable (List2 a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> List2 a -> c (List2 a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (List2 a))
-> (List2 a -> Constr)
-> (List2 a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (List2 a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (List2 a)))
-> ((forall b. Data b => b -> b) -> List2 a -> List2 a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> List2 a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> List2 a -> r)
-> (forall u. (forall d. Data d => d -> u) -> List2 a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> List2 a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> List2 a -> m (List2 a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> List2 a -> m (List2 a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> List2 a -> m (List2 a))
-> Data (List2 a)
List2 a -> DataType
List2 a -> Constr
(forall b. Data b => b -> b) -> List2 a -> List2 a
forall {a}. Data a => Typeable (List2 a)
forall a. Data a => List2 a -> DataType
forall a. Data a => List2 a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> List2 a -> List2 a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> List2 a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> List2 a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> List2 a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> List2 a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> List2 a -> m (List2 a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> List2 a -> m (List2 a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (List2 a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> List2 a -> c (List2 a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (List2 a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (List2 a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> List2 a -> u
forall u. (forall d. Data d => d -> u) -> List2 a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> List2 a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> List2 a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> List2 a -> m (List2 a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> List2 a -> m (List2 a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (List2 a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> List2 a -> c (List2 a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (List2 a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (List2 a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> List2 a -> m (List2 a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> List2 a -> m (List2 a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> List2 a -> m (List2 a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> List2 a -> m (List2 a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> List2 a -> m (List2 a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> List2 a -> m (List2 a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> List2 a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> List2 a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> List2 a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> List2 a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> List2 a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> List2 a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> List2 a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> List2 a -> r
gmapT :: (forall b. Data b => b -> b) -> List2 a -> List2 a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> List2 a -> List2 a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (List2 a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (List2 a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (List2 a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (List2 a))
dataTypeOf :: List2 a -> DataType
$cdataTypeOf :: forall a. Data a => List2 a -> DataType
toConstr :: List2 a -> Constr
$ctoConstr :: forall a. Data a => List2 a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (List2 a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (List2 a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> List2 a -> c (List2 a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> List2 a -> c (List2 a)
Data, (forall a b. (a -> b) -> List2 a -> List2 b)
-> (forall a b. a -> List2 b -> List2 a) -> Functor List2
forall a b. a -> List2 b -> List2 a
forall a b. (a -> b) -> List2 a -> List2 b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> List2 b -> List2 a
$c<$ :: forall a b. a -> List2 b -> List2 a
fmap :: forall a b. (a -> b) -> List2 a -> List2 b
$cfmap :: forall a b. (a -> b) -> List2 a -> List2 b
Functor, (forall m. Monoid m => List2 m -> m)
-> (forall m a. Monoid m => (a -> m) -> List2 a -> m)
-> (forall m a. Monoid m => (a -> m) -> List2 a -> m)
-> (forall a b. (a -> b -> b) -> b -> List2 a -> b)
-> (forall a b. (a -> b -> b) -> b -> List2 a -> b)
-> (forall b a. (b -> a -> b) -> b -> List2 a -> b)
-> (forall b a. (b -> a -> b) -> b -> List2 a -> b)
-> (forall a. (a -> a -> a) -> List2 a -> a)
-> (forall a. (a -> a -> a) -> List2 a -> a)
-> (forall a. List2 a -> [a])
-> (forall a. List2 a -> Bool)
-> (forall a. List2 a -> Int)
-> (forall a. Eq a => a -> List2 a -> Bool)
-> (forall a. Ord a => List2 a -> a)
-> (forall a. Ord a => List2 a -> a)
-> (forall a. Num a => List2 a -> a)
-> (forall a. Num a => List2 a -> a)
-> Foldable List2
forall a. Eq a => a -> List2 a -> Bool
forall a. Num a => List2 a -> a
forall a. Ord a => List2 a -> a
forall m. Monoid m => List2 m -> m
forall a. List2 a -> Bool
forall a. List2 a -> Int
forall a. List2 a -> [a]
forall a. (a -> a -> a) -> List2 a -> a
forall m a. Monoid m => (a -> m) -> List2 a -> m
forall b a. (b -> a -> b) -> b -> List2 a -> b
forall a b. (a -> b -> b) -> b -> List2 a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => List2 a -> a
$cproduct :: forall a. Num a => List2 a -> a
sum :: forall a. Num a => List2 a -> a
$csum :: forall a. Num a => List2 a -> a
minimum :: forall a. Ord a => List2 a -> a
$cminimum :: forall a. Ord a => List2 a -> a
maximum :: forall a. Ord a => List2 a -> a
$cmaximum :: forall a. Ord a => List2 a -> a
elem :: forall a. Eq a => a -> List2 a -> Bool
$celem :: forall a. Eq a => a -> List2 a -> Bool
length :: forall a. List2 a -> Int
$clength :: forall a. List2 a -> Int
null :: forall a. List2 a -> Bool
$cnull :: forall a. List2 a -> Bool
toList :: forall a. List2 a -> [a]
$ctoList :: forall a. List2 a -> [a]
foldl1 :: forall a. (a -> a -> a) -> List2 a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> List2 a -> a
foldr1 :: forall a. (a -> a -> a) -> List2 a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> List2 a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> List2 a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> List2 a -> b
foldl :: forall b a. (b -> a -> b) -> b -> List2 a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> List2 a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> List2 a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> List2 a -> b
foldr :: forall a b. (a -> b -> b) -> b -> List2 a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> List2 a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> List2 a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> List2 a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> List2 a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> List2 a -> m
fold :: forall m. Monoid m => List2 m -> m
$cfold :: forall m. Monoid m => List2 m -> m
Foldable, Functor List2
Foldable List2
Functor List2
-> Foldable List2
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> List2 a -> f (List2 b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    List2 (f a) -> f (List2 a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> List2 a -> m (List2 b))
-> (forall (m :: * -> *) a. Monad m => List2 (m a) -> m (List2 a))
-> Traversable List2
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => List2 (m a) -> m (List2 a)
forall (f :: * -> *) a. Applicative f => List2 (f a) -> f (List2 a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> List2 a -> m (List2 b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> List2 a -> f (List2 b)
sequence :: forall (m :: * -> *) a. Monad m => List2 (m a) -> m (List2 a)
$csequence :: forall (m :: * -> *) a. Monad m => List2 (m a) -> m (List2 a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> List2 a -> m (List2 b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> List2 a -> m (List2 b)
sequenceA :: forall (f :: * -> *) a. Applicative f => List2 (f a) -> f (List2 a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => List2 (f a) -> f (List2 a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> List2 a -> f (List2 b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> List2 a -> f (List2 b)
Traversable)

-- | Safe. O(1).
head :: List2 a -> a
head :: forall a. List2 a -> a
head (List2 a
a a
_ [a]
_) = a
a

-- | Safe. O(1).
tail :: List2 a -> List1 a
tail :: forall a. List2 a -> List1 a
tail (List2 a
a a
b [a]
cs) = a
b a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
cs

-- | Safe. O(n).
init :: List2 a -> List1 a
init :: forall a. List2 a -> List1 a
init (List2 a
a a
b [a]
cs) = a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| NonEmpty a -> [a]
forall a. NonEmpty a -> [a]
List1.init (a
b a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
cs)

-- | Safe. O(1).
fromListMaybe :: [a] -> Maybe (List2 a)
fromListMaybe :: forall a. [a] -> Maybe (List2 a)
fromListMaybe = List1 a -> Maybe (List2 a)
forall a. List1 a -> Maybe (List2 a)
fromList1Maybe (List1 a -> Maybe (List2 a))
-> ([a] -> Maybe (List1 a)) -> [a] -> Maybe (List2 a)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< [a] -> Maybe (List1 a)
forall a. [a] -> Maybe (NonEmpty a)
List1.nonEmpty

-- | Safe. O(1).
fromList1Maybe :: List1 a -> Maybe (List2 a)
fromList1Maybe :: forall a. List1 a -> Maybe (List2 a)
fromList1Maybe = \case
  (a
a :| a
b : [a]
cs) -> List2 a -> Maybe (List2 a)
forall a. a -> Maybe a
Just (a -> a -> [a] -> List2 a
forall a. a -> a -> [a] -> List2 a
List2 a
a a
b [a]
cs)
  List1 a
_ -> Maybe (List2 a)
forall a. Maybe a
Nothing

instance IsList (List2 a) where
  type Item (List2 a) = a

  -- Unsafe! O(1).
  fromList :: [a] -> List2 a
  fromList :: [a] -> List2 a
fromList (a
a : a
b : [a]
cs) = a -> a -> [a] -> List2 a
forall a. a -> a -> [a] -> List2 a
List2 a
a a
b [a]
cs
  fromList [a]
_            = List2 a
forall a. HasCallStack => a
__IMPOSSIBLE__

  toList :: List2 a -> [a]
  toList :: List2 a -> [a]
toList (List2 a
a a
b [a]
cs) = a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: a
b a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
cs

-- | Safe. O(1).
toList1 :: List2 a -> List1 a
toList1 :: forall a. List2 a -> List1 a
toList1 (List2 a
a a
b [a]
cs) = a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| a
b a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
cs

-- | Unsafe!
fromList1 :: List1 a -> List2 a
fromList1 :: forall a. List1 a -> List2 a
fromList1 (a
a :| a
b : [a]
cs) = a -> a -> [a] -> List2 a
forall a. a -> a -> [a] -> List2 a
List2 a
a a
b [a]
cs
fromList1 NonEmpty a
_             = List2 a
forall a. HasCallStack => a
__IMPOSSIBLE__

break :: (a -> Bool) -> List2 a -> ([a],[a])
break :: forall a. (a -> Bool) -> List2 a -> ([a], [a])
break a -> Bool
p = (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.break a -> Bool
p ([a] -> ([a], [a])) -> (List2 a -> [a]) -> List2 a -> ([a], [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List2 a -> [a]
forall l. IsList l => l -> [Item l]
toList

instance NFData a => NFData (List2 a) where
  rnf :: List2 a -> ()
rnf (List2 a
a a
b [a]
cs) = a -> ()
forall a. NFData a => a -> ()
rnf a
a () -> () -> ()
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
b () -> () -> ()
`seq` [a] -> ()
forall a. NFData a => a -> ()
rnf [a]
cs