content: {-# LANGUAGE CPP #-}
  
  -- | 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
  --
  --   @
  
  {-# OPTIONS_GHC -Wno-incomplete-patterns #-}
    -- because of https://gitlab.haskell.org/ghc/ghc/issues/10339
  
  module Agda.Utils.List1
    ( module Agda.Utils.List1
    , module List1
    , module IsList
    , module Unzip
    ) where
  
  import Prelude hiding (filter, unzip)
  
  import Control.Arrow ((&&&))
  import Control.Monad (filterM)
  import qualified Control.Monad as List (zipWithM, zipWithM_)
  
  import qualified Data.Either as Either
  import Data.Function ( on )
  import qualified Data.List as List
  import qualified Data.Maybe as Maybe
  
  import Data.List.NonEmpty as List1 hiding (fromList, toList, unzip)
  import qualified Data.List.NonEmpty as List1 (toList)
  
  -- Prevent warning -Wx-data-list-nonempty-unzip
  #if MIN_VERSION_base(4,19,0)
  import Data.Functor as Unzip (unzip)
  #else
  import Data.List.NonEmpty as Unzip (unzip)
  #endif
  
  import GHC.Exts as IsList ( IsList(..) )
  
  import Agda.Utils.Functor ((<.>), (<&>))
  import Agda.Utils.Null (Null(..))
  import qualified Agda.Utils.List as List
  
  -- Set up doctest.
  -- $setup
  -- >>> :seti -XOverloadedLists
  
  type List1 = NonEmpty
  type String1 = List1 Char
  
  -- | Lossless 'toList', opposite of 'nonEmpty'.
  --
  toList' :: Maybe (List1 a) -> [a]
  toList' = maybe [] toList
  
  -- | Lift a function on non-empty lists to a function on lists.
  --
  -- This is in essence 'fmap' for 'Maybe', if we take @[a] = Maybe (List1 a)@.
  --
  liftList1 :: (List1 a -> List1 b) -> [a] -> [b]
  liftList1 f = toList' . fmap f . nonEmpty
  
  -- | Safe version of 'Data.List.NonEmpty.fromList'.
  
  fromListSafe
    :: List1 a  -- ^ Default value if convertee is empty.
    -> [a]      -- ^ List to convert, supposedly non-empty.
    -> List1 a  -- ^ Converted list.
  fromListSafe err   [] = err
  fromListSafe _ (x:xs) = x :| xs
  
  -- | Return the last element and the rest.
  
  initLast :: List1 a -> ([a], a)
  initLast = List1.init &&& List1.last
    -- traverses twice, but does not create intermediate pairs
  
  -- | Last two elements (safe).
  --   O(n).
  last2 :: List1 a -> Maybe (a, a)
  last2 (x :| y : xs) = Just $ List.last2' x y xs
  last2 _ = Nothing
  
  -- | More precise type for @snoc@.
  
  snoc :: [a] -> a -> List1 a
  snoc as a = prependList as $ a :| []
  
  -- | Append an element to a non-empty list.
  
  snoc1 :: List1 a -> a -> List1 a
  snoc1 as a = as <> (a :| [])
  
  -- | @'groupOn' f = 'groupBy' (('==') \`on\` f) '.' 'List.sortBy' ('compare' \`on\` f)@.
  -- O(n log n).
  groupOn :: Ord b => (a -> b) -> [a] -> [List1 a]
  groupOn f = List1.groupBy ((==) `on` f) . List.sortBy (compare `on` f)
  
  groupOn1 :: Ord b => (a -> b) -> List1 a -> List1 (List1 a)
  groupOn1 f = List1.groupBy1 ((==) `on` f) . List1.sortBy (compare `on` f)
  
  -- | More precise type for 'Agda.Utils.List.groupBy''.
  --
  -- A variant of 'List.groupBy' which applies the predicate to consecutive
  -- pairs.
  -- O(n).
  groupBy' :: forall a. (a -> a -> Bool) -> [a] -> [List1 a]
  groupBy' _ []           = []
  groupBy' p xxs@(x : xs) = grp x $ List.zipWith (\ x y -> (p x y, y)) xxs xs
    where
    grp :: a -> [(Bool,a)] -> [List1 a]
    grp x ys
      | let (xs, rest) = List.span fst ys
      = (x :| List.map snd xs) : case rest of
        []                 -> []
        ((_false, z) : zs) -> grp z zs
  
  -- | Group consecutive items that share the same first component.
  --
  groupByFst :: forall a b. Eq a => [(a,b)] -> [(a, List1 b)]
  groupByFst =
      List.map (\ ((tag, b) :| xs) -> (tag, b :| List.map snd xs))
        -- Float the grouping to the top level
    . List1.groupBy ((==) `on` fst)
        -- Group together characters in the same role.
  
  -- | Group consecutive items that share the same first component.
  --
  groupByFst1 :: forall a b. Eq a => List1 (a, b) -> List1 (a, List1 b)
  groupByFst1 =
      fmap (\ ((tag, b) :| xs) -> (tag, b :| List.map snd xs))
        -- Float the grouping to the top level
    . List1.groupBy1 ((==) `on` fst)
        -- Group together characters in the same role.
  
  -- | Split a list into sublists. Generalisation of the prelude function
  --   @words@.
  --   Same as 'Data.List.Split.wordsBy' and 'Data.List.Extra.wordsBy',
  --   but with the non-emptyness guarantee on the chunks.
  --   O(n).
  --
  --   > words xs == wordsBy isSpace xs
  wordsBy :: (a -> Bool) -> [a] -> [List1 a]
  wordsBy p = loop
    where
    loop as = case List.dropWhile p as of
      []   -> []
      x:xs -> (x :| ys) : loop zs where (ys, zs) = List.break p xs
  
  -- | 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])
  
  breakAfter :: (a -> Bool) -> List1 a -> (List1 a, [a])
  breakAfter p (x :| xs) = List.breakAfter1 p x xs
  
  -- | Concatenate one or more non-empty lists.
  
  concat :: [List1 a] -> [a]
  concat = concatMap toList
  
  concatMap1 :: (a -> List1 b) -> List1 a -> List1 b
  concatMap1 = (=<<)
  
  -- | Like 'Data.List.union'.  Duplicates in the first list are not removed.
  -- O(nm).
  union :: Eq a => List1 a -> List1 a -> List1 a
  union (a :| as) bs = a :| List.union as (filter (/= a) bs)
  
  -- * Recovering non-emptyness.
  
  ifNull :: [a] -> b -> (List1 a -> b) -> b
  ifNull []       b _ = b
  ifNull (a : as) _ f = f $ a :| as
  
  ifNotNull :: [a] -> (List1 a -> b) -> b -> b
  ifNotNull []       _ b = b
  ifNotNull (a : as) f _ = f $ a :| as
  
  -- | 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 ())@.
  unlessNull :: Applicative m => [a] -> (List1 a -> m ()) -> m ()
  unlessNull []       _ = pure ()
  unlessNull (x : xs) f = f $ x :| xs
  
  unlessNullM :: Monad m => m [a] -> (List1 a -> m ()) -> m ()
  unlessNullM m k = m >>= (`unlessNull` k)
  
  -- * List functions with no special behavior for non-empty lists.
  
  -- | Checks if all the elements in the list are equal. Assumes that
  --   the 'Eq' instance stands for an equivalence relation.
  --   O(n).
  allEqual :: Eq a => List1 a -> Bool
  allEqual (x :| xs) = all (== x) xs
  
  -- | Like 'Maybe.catMaybes'.
  
  catMaybes :: List1 (Maybe a) -> [a]
  catMaybes =  Maybe.catMaybes . List1.toList
  
  -- | Like 'Maybe.mapMaybe'.
  
  #if !MIN_VERSION_base(4,23,0)
  -- Will be part of base with GHC 9.16 (base-4.23)
  mapMaybe :: (a -> Maybe b) -> List1 a -> [b]
  mapMaybe f = Maybe.mapMaybe f . List1.toList
  #endif
  
  -- | Like 'List.find'.
  
  find :: (a -> Bool) -> List1 a -> Maybe a
  find f = List.find f . List1.toList
  
  -- | Like 'Data.Either.partitionEithers'.
  
  partitionEithers :: List1 (Either a b) -> ([a], [b])
  partitionEithers = Either.partitionEithers . List1.toList
  
  -- | Like 'Data.Either.lefts'.
  
  lefts :: List1 (Either a b) -> [a]
  lefts = Either.lefts  . List1.toList
  
  -- | Like 'Data.Either.rights'.
  
  rights :: List1 (Either a b) -> [b]
  rights = Either.rights  . List1.toList
  
  -- | Like 'Data.List.unwords'.
  
  unwords :: List1 String -> String
  unwords = List.unwords . List1.toList
  
  -- | Non-efficient, monadic 'nub'.
  -- O(n²).
  nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a)
  nubM eq (a :| as) = (a :|) <$> do List.nubM eq =<< filterM (not <.> eq a) as
  
  -- | Like 'Agda.Utils.List.unzipWith'.
  
  unzipWith :: (a -> (b, c)) -> List1 a -> (List1 b, List1 c)
  unzipWith f = unzip . fmap f
  
  -- | Like 'Control.Monad.zipWithM'.
  
  zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c)
  zipWithM f (a :| as) (b :| bs) = (:|) <$> f a b <*> List.zipWithM f as bs
  
  -- | Like 'Control.Monad.zipWithM'.
  
  zipWithM_ :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m ()
  zipWithM_ f (a :| as) (b :| bs) = f a b *> List.zipWithM_ f as bs
  
  -- | List 'Data.List.foldr' but with a base case for the singleton list.
  
  foldr :: (a -> b -> b) -> (a -> b) -> List1 a -> b
  foldr f g (x :| xs) = loop x xs
    where
    loop x []       = g x
    loop x (y : ys) = f x $ loop y ys
  
  -- | Update the first element of a non-empty list.
  --   O(1).
  updateHead :: (a -> a) -> List1 a -> List1 a
  updateHead f (a :| as) = f a :| as
  
  -- | Update the last element of a non-empty list.
  --   O(n).
  updateLast :: (a -> a) -> List1 a -> List1 a
  updateLast f (a :| as) = loop a as
    where
    loop a []       = singleton $ f a
    loop a (b : bs) = cons a $ loop b bs
  
  -- | Focus on the first element of a non-empty list.
  --   O(1).
  lensHead :: Functor f => (a -> f a) -> List1 a -> f (List1 a)
  lensHead f (a :| as) = f a <&> (:| as)
  
  -- | Focus on the last element of a non-empty list.
  --   O(n).
  lensLast :: Functor f => (a -> f a) -> List1 a -> f (List1 a)
  lensLast f (a :| as) = loop a as
    where
    loop a []       = singleton <$> f a
    loop a (b : bs) = cons a <$> loop b bs
  