content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  -- | 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 Prelude hiding ( zip, zipWith )
  
  import Control.DeepSeq
  import Control.Monad                   ( (<=<) )
  
  import qualified Data.List as List
  import Data.Semigroup (sconcat)
  
  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 (Eq, Ord, Show, Functor, Foldable, Traversable)
  
  -- * Conversion from and to other list types.
  
  -- | 'fromList' is unsafe.
  instance IsList (List2 a) where
    type Item (List2 a) = a
  
    -- Unsafe! O(1).
    fromList :: [a] -> List2 a
    fromList (a : b : cs) = List2 a b cs
    fromList _            = __IMPOSSIBLE__
  
    toList :: List2 a -> [a]
    toList (List2 a b cs) = a : b : cs
  
  -- | Unsafe! O(1).
  fromList1 :: List1 a -> List2 a
  fromList1 (a :| b : cs) = List2 a b cs
  fromList1 _             = __IMPOSSIBLE__
  
  -- | Safe. O(1).
  toList1 :: List2 a -> List1 a
  toList1 (List2 a b cs) = a :| b : cs
  
  -- | Safe. O(1).
  fromListMaybe :: [a] -> Maybe (List2 a)
  fromListMaybe = fromList1Maybe <=< List1.nonEmpty
  
  -- | Safe. O(1).
  fromList1Maybe :: List1 a -> Maybe (List2 a)
  fromList1Maybe = \case
    (a :| b : cs) -> Just (List2 a b cs)
    _ -> Nothing
  
  -- | Any 'List1' is either a singleton or a 'List2'. O(1).
  fromList1Either :: List1 a -> Either a (List2 a)
  fromList1Either (a :| as) = case as of
    []   -> Left a
    b:bs -> Right (List2 a b bs)
  
  -- | Inverse of 'fromList1Either'. O(1).
  toList1Either :: Either a (List2 a) -> List1 a
  toList1Either = \case
    Left  a              -> a :| []
    Right (List2 a b bs) -> a :| b : bs
  
  -- * Construction
  
  -- | O(1).
  cons :: a -> List1 a -> List2 a
  cons x (y :| ys) = List2 x y ys
  
  -- | O(n).
  snoc :: List1 a -> a -> List2 a
  snoc (x :| xs) z = List2 x y ys
    where
      y :| ys = List1.snoc xs z
  
  -- | O(length first list).
  append :: List1 a -> List1 a -> List2 a
  append (x :| xs) ys = cons x $ List1.prependList xs ys
  
  -- | O(length first list).
  appendList :: List2 a -> [a] -> List2 a
  appendList (List2 x y ys) zs = List2 x y $ mappend ys zs
  
  -- | Concatenate at least 2 lists of length at least 1.
  concat21 :: List2 (List1 a) -> List2 a
  concat21 (List2 xs ys zss) = append xs $ sconcat $ ys :| zss
  
  -- * Destruction
  
  -- | Safe. O(1).
  head :: List2 a -> a
  head (List2 a _ _) = a
  
  -- | Safe. O(1).
  tail :: List2 a -> List1 a
  tail (List2 a b cs) = b :| cs
  
  -- | Safe. O(n).
  init :: List2 a -> List1 a
  init (List2 a b cs) = a :| List1.init (b :| cs)
  
  -- * Partition
  
  break :: (a -> Bool) -> List2 a -> ([a],[a])
  break p = List.break p . toList
  
  instance NFData a => NFData (List2 a) where
    rnf (List2 a b cs) = rnf a `seq` rnf b `seq` rnf cs
  
  -- * Zip
  
  zipWith :: (a -> b -> c) -> List2 a -> List2 b -> List2 c
  zipWith f (List2 a1 a2 as) (List2 b1 b2 bs) = List2 (f a1 b1) (f a2 b2) (List.zipWith f as bs)
  
  zip :: List2 a -> List2 b -> List2 (a, b)
  zip = zipWith (,)
  