{-# 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
  ) where

import Prelude hiding (filter)

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)
import qualified Data.List.NonEmpty as List1 (toList)

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' :: forall a. Maybe (List1 a) -> [a]
toList' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] forall l. IsList l => l -> [Item l]
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 :: forall a b. (List1 a -> List1 b) -> [a] -> [b]
liftList1 List1 a -> List1 b
f = forall a. Maybe (List1 a) -> [a]
toList' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap List1 a -> List1 b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Maybe (NonEmpty a)
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 :: forall a. List1 a -> [a] -> List1 a
fromListSafe List1 a
err   [] = List1 a
err
fromListSafe List1 a
_ (a
x:[a]
xs) = a
x forall a. a -> [a] -> NonEmpty a
:| [a]
xs

-- | Return the last element and the rest.

initLast :: List1 a -> ([a], a)
initLast :: forall a. List1 a -> ([a], a)
initLast = forall a. NonEmpty a -> [a]
List1.init forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall a. NonEmpty a -> a
List1.last
  -- traverses twice, but does not create intermediate pairs

-- | Last two elements (safe).
--   O(n).
last2 :: List1 a -> Maybe (a, a)
last2 :: forall a. List1 a -> Maybe (a, a)
last2 (a
x :| a
y : [a]
xs) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> a -> [a] -> (a, a)
List.last2' a
x a
y [a]
xs
last2 NonEmpty a
_ = forall a. Maybe a
Nothing

-- | Build a list with one element.

#if !(MIN_VERSION_base(4,15,0))
singleton :: a -> List1 a
singleton = (:| [])
#endif

#if !MIN_VERSION_base(4,16,0)
-- | Append a list to a non-empty list.

appendList :: List1 a -> [a] -> List1 a
appendList (x :| xs) ys = x :| mappend xs ys

-- | Prepend a list to a non-empty list.

prependList :: [a] -> List1 a -> List1 a
prependList as bs = Prelude.foldr (<|) bs as
#endif

-- | More precise type for @snoc@.

snoc :: [a] -> a -> List1 a
snoc :: forall a. [a] -> a -> List1 a
snoc [a]
as a
a = forall a. [a] -> NonEmpty a -> NonEmpty a
prependList [a]
as forall a b. (a -> b) -> a -> b
$ a
a forall a. a -> [a] -> NonEmpty a
:| []

-- | @'groupOn' f = 'groupBy' (('==') \`on\` f) '.' 'List.sortBy' ('compare' \`on\` f)@.
-- O(n log n).
groupOn :: Ord b => (a -> b) -> [a] -> [List1 a]
groupOn :: forall b a. Ord b => (a -> b) -> [a] -> [List1 a]
groupOn a -> b
f = forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f)

groupOn1 :: Ord b => (a -> b) -> List1 a -> List1 (List1 a)
groupOn1 :: forall b a. Ord b => (a -> b) -> List1 a -> List1 (List1 a)
groupOn1 a -> b
f = forall a. (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
List1.groupBy1 (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> NonEmpty a -> NonEmpty a
List1.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
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' :: forall a. (a -> a -> Bool) -> [a] -> [List1 a]
groupBy' a -> a -> Bool
_ []           = []
groupBy' a -> a -> Bool
p xxs :: [a]
xxs@(a
x : [a]
xs) = a -> [(Bool, a)] -> [List1 a]
grp a
x forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
List.zipWith (\ a
x a
y -> (a -> a -> Bool
p a
x a
y, a
y)) [a]
xxs [a]
xs
  where
  grp :: a -> [(Bool,a)] -> [List1 a]
  grp :: a -> [(Bool, a)] -> [List1 a]
grp a
x [(Bool, a)]
ys
    | let ([(Bool, a)]
xs, [(Bool, a)]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.span forall a b. (a, b) -> a
fst [(Bool, a)]
ys
    = (a
x forall a. a -> [a] -> NonEmpty a
:| forall a b. (a -> b) -> [a] -> [b]
List.map forall a b. (a, b) -> b
snd [(Bool, a)]
xs) forall a. a -> [a] -> [a]
: case [(Bool, a)]
rest of
      []                 -> []
      ((Bool
_false, a
z) : [(Bool, a)]
zs) -> a -> [(Bool, a)] -> [List1 a]
grp a
z [(Bool, a)]
zs

-- | Group consecutive items that share the same first component.
--
groupByFst :: forall a b. Eq a => [(a,b)] -> [(a, List1 b)]
groupByFst :: forall a b. Eq a => [(a, b)] -> [(a, List1 b)]
groupByFst =
    forall a b. (a -> b) -> [a] -> [b]
List.map (\ ((a
tag, b
b) :| [(a, b)]
xs) -> (a
tag, b
b forall a. a -> [a] -> NonEmpty a
:| forall a b. (a -> b) -> [a] -> [b]
List.map forall a b. (a, b) -> b
snd [(a, b)]
xs))
      -- Float the grouping to the top level
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
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 :: forall a b. Eq a => List1 (a, b) -> List1 (a, List1 b)
groupByFst1 =
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ ((a
tag, b
b) :| [(a, b)]
xs) -> (a
tag, b
b forall a. a -> [a] -> NonEmpty a
:| forall a b. (a -> b) -> [a] -> [b]
List.map forall a b. (a, b) -> b
snd [(a, b)]
xs))
      -- Float the grouping to the top level
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> NonEmpty a -> NonEmpty (NonEmpty a)
List1.groupBy1 (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
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 :: forall a. (a -> Bool) -> [a] -> [List1 a]
wordsBy a -> Bool
p = [a] -> [NonEmpty a]
loop
  where
  loop :: [a] -> [NonEmpty a]
loop [a]
as = case forall a. (a -> Bool) -> [a] -> [a]
List.dropWhile a -> Bool
p [a]
as of
    []   -> []
    a
x:[a]
xs -> (a
x forall a. a -> [a] -> NonEmpty a
:| [a]
ys) forall a. a -> [a] -> [a]
: [a] -> [NonEmpty a]
loop [a]
zs where ([a]
ys, [a]
zs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
List.break a -> Bool
p [a]
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 :: forall a. (a -> Bool) -> List1 a -> (List1 a, [a])
breakAfter a -> Bool
p (a
x :| [a]
xs) = forall a. (a -> Bool) -> a -> [a] -> (List1 a, [a])
List.breakAfter1 a -> Bool
p a
x [a]
xs

-- | Concatenate one or more non-empty lists.

concat :: [List1 a] -> [a]
concat :: forall a. [List1 a] -> [a]
concat = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall l. IsList l => l -> [Item l]
toList

concatMap1 :: (a -> List1 b) -> List1 a -> List1 b
concatMap1 :: forall a b. (a -> List1 b) -> List1 a -> List1 b
concatMap1 = forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
(=<<)

-- | Like 'Data.List.union'.  Duplicates in the first list are not removed.
-- O(nm).
union :: Eq a => List1 a -> List1 a -> List1 a
union :: forall a. Eq a => List1 a -> List1 a -> List1 a
union (a
a :| [a]
as) NonEmpty a
bs = a
a forall a. a -> [a] -> NonEmpty a
:| forall a. Eq a => [a] -> [a] -> [a]
List.union [a]
as (forall a. (a -> Bool) -> NonEmpty a -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= a
a) NonEmpty a
bs)

-- * Recovering non-emptyness.

ifNull :: [a] -> b -> (List1 a -> b) -> b
ifNull :: forall a b. [a] -> b -> (List1 a -> b) -> b
ifNull []       b
b List1 a -> b
_ = b
b
ifNull (a
a : [a]
as) b
_ List1 a -> b
f = List1 a -> b
f forall a b. (a -> b) -> a -> b
$ a
a forall a. a -> [a] -> NonEmpty a
:| [a]
as

ifNotNull :: [a] -> (List1 a -> b) -> b -> b
ifNotNull :: forall a b. [a] -> (List1 a -> b) -> b -> b
ifNotNull []       List1 a -> b
_ b
b = b
b
ifNotNull (a
a : [a]
as) List1 a -> b
f b
_ = List1 a -> b
f forall a b. (a -> b) -> a -> b
$ a
a forall a. a -> [a] -> NonEmpty a
:| [a]
as

unlessNull :: Null m => [a] -> (List1 a -> m) -> m
unlessNull :: forall m a. Null m => [a] -> (List1 a -> m) -> m
unlessNull []       List1 a -> m
_ = forall a. Null a => a
empty
unlessNull (a
x : [a]
xs) List1 a -> m
f = List1 a -> m
f forall a b. (a -> b) -> a -> b
$ a
x forall a. a -> [a] -> NonEmpty a
:| [a]
xs

-- * 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 :: forall a. Eq a => List1 a -> Bool
allEqual (a
x :| [a]
xs) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== a
x) [a]
xs

-- | Like 'Maybe.catMaybes'.

catMaybes :: List1 (Maybe a) -> [a]
catMaybes :: forall a. List1 (Maybe a) -> [a]
catMaybes =  forall a. [Maybe a] -> [a]
Maybe.catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList

-- | Like 'Maybe.mapMaybe'.

mapMaybe :: (a -> Maybe b) -> List1 a -> [b]
mapMaybe :: forall a b. (a -> Maybe b) -> List1 a -> [b]
mapMaybe a -> Maybe b
f = forall a b. (a -> Maybe b) -> [a] -> [b]
Maybe.mapMaybe a -> Maybe b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList

-- | Like 'List.find'.

find :: (a -> Bool) -> List1 a -> Maybe a
find :: forall a. (a -> Bool) -> List1 a -> Maybe a
find a -> Bool
f = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find a -> Bool
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList

-- | Like 'Data.Either.partitionEithers'.

partitionEithers :: List1 (Either a b) -> ([a], [b])
partitionEithers :: forall a b. List1 (Either a b) -> ([a], [b])
partitionEithers = forall a b. [Either a b] -> ([a], [b])
Either.partitionEithers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList

-- | Like 'Data.Either.lefts'.

lefts :: List1 (Either a b) -> [a]
lefts :: forall a b. List1 (Either a b) -> [a]
lefts = forall a b. [Either a b] -> [a]
Either.lefts  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList

-- | Like 'Data.Either.rights'.

rights :: List1 (Either a b) -> [b]
rights :: forall a b. List1 (Either a b) -> [b]
rights = forall a b. [Either a b] -> [b]
Either.rights  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList

-- | Like 'Data.List.unwords'.

unwords :: List1 String -> String
unwords :: List1 String -> String
unwords = [String] -> String
List.unwords forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
List1.toList

-- | Non-efficient, monadic 'nub'.
-- O(n²).
nubM :: Monad m => (a -> a -> m Bool) -> List1 a -> m (List1 a)
nubM :: forall (m :: * -> *) a.
Monad m =>
(a -> a -> m Bool) -> List1 a -> m (List1 a)
nubM a -> a -> m Bool
eq (a
a :| [a]
as) = (a
a forall a. a -> [a] -> NonEmpty a
:|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do forall (m :: * -> *) a.
Monad m =>
(a -> a -> m Bool) -> [a] -> m [a]
List.nubM a -> a -> m Bool
eq forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (Bool -> Bool
not forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> a -> a -> m Bool
eq a
a) [a]
as

-- | Like 'Control.Monad.zipWithM'.

zipWithM :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m (List1 c)
zipWithM :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> List1 a -> List1 b -> m (List1 c)
zipWithM a -> b -> m c
f (a
a :| [a]
as) (b
b :| [b]
bs) = forall a. a -> [a] -> NonEmpty a
(:|) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> b -> m c
f a
a b
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
List.zipWithM a -> b -> m c
f [a]
as [b]
bs

-- | Like 'Control.Monad.zipWithM'.

zipWithM_ :: Applicative m => (a -> b -> m c) -> List1 a -> List1 b -> m ()
zipWithM_ :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> List1 a -> List1 b -> m ()
zipWithM_ a -> b -> m c
f (a
a :| [a]
as) (b
b :| [b]
bs) = a -> b -> m c
f a
a b
b forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
List.zipWithM_ a -> b -> m c
f [a]
as [b]
bs

-- | List 'Data.List.foldr' but with a base case for the singleton list.

foldr :: (a -> b -> b) -> (a -> b) -> List1 a -> b
foldr :: forall a b. (a -> b -> b) -> (a -> b) -> List1 a -> b
foldr a -> b -> b
f a -> b
g (a
x :| [a]
xs) = a -> [a] -> b
loop a
x [a]
xs
  where
  loop :: a -> [a] -> b
loop a
x []       = a -> b
g a
x
  loop a
x (a
y : [a]
ys) = a -> b -> b
f a
x forall a b. (a -> b) -> a -> b
$ a -> [a] -> b
loop a
y [a]
ys

-- | Update the first element of a non-empty list.
--   O(1).
updateHead :: (a -> a) -> List1 a -> List1 a
updateHead :: forall a. (a -> a) -> List1 a -> List1 a
updateHead a -> a
f (a
a :| [a]
as) = a -> a
f a
a forall a. a -> [a] -> NonEmpty a
:| [a]
as

-- | Update the last element of a non-empty list.
--   O(n).
updateLast :: (a -> a) -> List1 a -> List1 a
updateLast :: forall a. (a -> a) -> List1 a -> List1 a
updateLast a -> a
f (a
a :| [a]
as) = a -> [a] -> NonEmpty a
loop a
a [a]
as
  where
  loop :: a -> [a] -> NonEmpty a
loop a
a []       = forall a. a -> NonEmpty a
singleton forall a b. (a -> b) -> a -> b
$ a -> a
f a
a
  loop a
a (a
b : [a]
bs) = forall a. a -> NonEmpty a -> NonEmpty a
cons a
a forall a b. (a -> b) -> a -> b
$ a -> [a] -> NonEmpty a
loop a
b [a]
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 :: forall (f :: * -> *) a.
Functor f =>
(a -> f a) -> List1 a -> f (List1 a)
lensHead a -> f a
f (a
a :| [a]
as) = a -> f a
f a
a forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall a. a -> [a] -> NonEmpty a
:| [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 :: forall (f :: * -> *) a.
Functor f =>
(a -> f a) -> List1 a -> f (List1 a)
lensLast a -> f a
f (a
a :| [a]
as) = a -> [a] -> f (NonEmpty a)
loop a
a [a]
as
  where
  loop :: a -> [a] -> f (NonEmpty a)
loop a
a []       = forall a. a -> NonEmpty a
singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f a
a
  loop a
a (a
b : [a]
bs) = forall a. a -> NonEmpty a -> NonEmpty a
cons a
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> [a] -> f (NonEmpty a)
loop a
b [a]
bs