{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveFoldable      #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DeriveTraversable   #-}
{-# LANGUAGE EmptyCase           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE ViewPatterns        #-}

-- | Type-level counting
--
-- Intended for unqualified import.
module Ouroboros.Consensus.Util.Counting (
    AtMost (..)
  , Exactly (.., ExactlyNil, ExactlyCons)
  , NonEmpty (..)
    -- * Working with 'Exactly'
  , exactlyHead
  , exactlyOne
  , exactlyReplicate
  , exactlyTail
  , exactlyTwo
  , exactlyWeaken
  , exactlyWeakenNonEmpty
  , exactlyZip
  , exactlyZipFoldable
    -- * Working with 'AtMost'
  , atMostHead
  , atMostInit
  , atMostLast
  , atMostNonEmpty
  , atMostOne
  , atMostZipFoldable
    -- * Working with 'NonEmpty'
  , nonEmptyFromList
  , nonEmptyHead
  , nonEmptyInit
  , nonEmptyLast
  , nonEmptyMapOne
  , nonEmptyMapTwo
  , nonEmptyStrictPrefixes
  , nonEmptyToList
  , nonEmptyWeaken
  ) where

import           Control.Applicative
import qualified Data.Foldable as Foldable
import           Data.Kind (Type)
import           Data.SOP.Dict
import           Data.SOP.Strict

import           Ouroboros.Consensus.Util.SOP

{-------------------------------------------------------------------------------
  Types
-------------------------------------------------------------------------------}

newtype Exactly xs a = Exactly { Exactly xs a -> NP (K a) xs
getExactly :: NP (K a) xs }

-- | At most one value for each type level index
data AtMost :: [Type] -> Type -> Type where
  AtMostNil  :: AtMost xs a
  AtMostCons :: !a -> !(AtMost xs a) -> AtMost (x ': xs) a

-- | Non-empty variation on 'AtMost'
data NonEmpty :: [Type] -> Type -> Type where
  NonEmptyOne  :: !a -> NonEmpty (x ': xs) a
  NonEmptyCons :: !a -> !(NonEmpty xs a) -> NonEmpty (x ': xs) a

deriving instance Eq a => Eq (AtMost   xs a)
deriving instance Eq a => Eq (NonEmpty xs a)

deriving instance Show a => Show (AtMost   xs a)
deriving instance Show a => Show (NonEmpty xs a)

deriving instance Functor     (AtMost xs)
deriving instance Foldable    (AtMost xs)
deriving instance Traversable (AtMost xs)

deriving instance Functor     (NonEmpty xs)
deriving instance Foldable    (NonEmpty xs)
deriving instance Traversable (NonEmpty xs)

{-------------------------------------------------------------------------------
  Pattern synonyms for 'Exactly'
-------------------------------------------------------------------------------}

-- | Internal: view on 'Exactly'
--
-- Used for the pattern synonyms only.
data ExactlyView xs a where
  ENil  :: ExactlyView '[] a
  ECons :: a -> Exactly xs a -> ExactlyView (x : xs) a

-- | Internal: construct the view on 'Exactly'
--
-- Used for the pattern synonyms only.
exactlyView :: Exactly xs a -> ExactlyView xs a
exactlyView :: Exactly xs a -> ExactlyView xs a
exactlyView (Exactly (K a
x :* NP (K a) xs
xs)) = a -> Exactly xs a -> ExactlyView (x : xs) a
forall a (xs :: [*]) x. a -> Exactly xs a -> ExactlyView (x : xs) a
ECons a
x (NP (K a) xs -> Exactly xs a
forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a
Exactly NP (K a) xs
xs)
exactlyView (Exactly NP (K a) xs
Nil)         = ExactlyView xs a
forall a. ExactlyView '[] a
ENil

{-# COMPLETE ExactlyNil, ExactlyCons #-}

pattern ExactlyCons ::
     ()
  => xs' ~ (x ': xs)
  => a -> Exactly xs a -> Exactly xs' a
pattern $bExactlyCons :: a -> Exactly xs a -> Exactly xs' a
$mExactlyCons :: forall r (xs' :: [*]) a.
Exactly xs' a
-> (forall x (xs :: [*]).
    (xs' ~ (x : xs)) =>
    a -> Exactly xs a -> r)
-> (Void# -> r)
-> r
ExactlyCons x xs <- (exactlyView -> ECons x xs)
  where
    ExactlyCons a
x Exactly xs a
xs = NP (K a) (x : xs) -> Exactly (x : xs) a
forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a
Exactly (a -> K a x
forall k a (b :: k). a -> K a b
K a
x K a x -> NP (K a) xs -> NP (K a) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* (Exactly xs a -> NP (K a) xs
forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs
getExactly Exactly xs a
xs))

pattern ExactlyNil ::
     ()
  => xs ~ '[]
  => Exactly xs a
pattern $bExactlyNil :: Exactly xs a
$mExactlyNil :: forall r (xs :: [*]) a.
Exactly xs a -> ((xs ~ '[]) => r) -> (Void# -> r) -> r
ExactlyNil <- (exactlyView -> ENil)
  where
    ExactlyNil = NP (K a) '[] -> Exactly '[] a
forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a
Exactly NP (K a) '[]
forall k (f :: k -> *). NP f '[]
Nil

{-------------------------------------------------------------------------------
  Type class instances for 'Exactly'

  For 'AtMost' and 'NonEmpty' we can just derive these, but for 'Exactly'
  we need to do a bit more work.
-------------------------------------------------------------------------------}

instance Functor (Exactly xs) where
  fmap :: (a -> b) -> Exactly xs a -> Exactly xs b
fmap a -> b
f (Exactly NP (K a) xs
xs) = NP (K a) xs -> (SListI xs => Exactly xs b) -> Exactly xs b
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (K a) xs
xs ((SListI xs => Exactly xs b) -> Exactly xs b)
-> (SListI xs => Exactly xs b) -> Exactly xs b
forall a b. (a -> b) -> a -> b
$ NP (K b) xs -> Exactly xs b
forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a
Exactly (NP (K b) xs -> Exactly xs b) -> NP (K b) xs -> Exactly xs b
forall a b. (a -> b) -> a -> b
$
      (forall a. K a a -> K b a) -> NP (K a) xs -> NP (K b) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap ((a -> b) -> K a a -> K b a
forall k1 k2 a b (c :: k1) (d :: k2). (a -> b) -> K a c -> K b d
mapKK a -> b
f) NP (K a) xs
xs

instance Foldable (Exactly xs) where
  foldMap :: (a -> m) -> Exactly xs a -> m
foldMap a -> m
f (Exactly NP (K a) xs
xs) = NP (K a) xs -> (SListI xs => m) -> m
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (K a) xs
xs ((SListI xs => m) -> m) -> (SListI xs => m) -> m
forall a b. (a -> b) -> a -> b
$
      (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f (NP (K a) xs -> CollapseTo NP a
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse NP (K a) xs
xs)

instance Traversable (Exactly xs) where
  traverse :: (a -> f b) -> Exactly xs a -> f (Exactly xs b)
traverse a -> f b
f (Exactly NP (K a) xs
xs) = NP (K a) xs -> (SListI xs => f (Exactly xs b)) -> f (Exactly xs b)
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (K a) xs
xs ((SListI xs => f (Exactly xs b)) -> f (Exactly xs b))
-> (SListI xs => f (Exactly xs b)) -> f (Exactly xs b)
forall a b. (a -> b) -> a -> b
$ (NP (K b) xs -> Exactly xs b)
-> f (NP (K b) xs) -> f (Exactly xs b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NP (K b) xs -> Exactly xs b
forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a
Exactly (f (NP (K b) xs) -> f (Exactly xs b))
-> f (NP (K b) xs) -> f (Exactly xs b)
forall a b. (a -> b) -> a -> b
$
      NP (f :.: K b) xs -> f (NP (K b) xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: * -> *)
       (g :: k -> *).
(HSequence h, SListIN h xs, Applicative f) =>
h (f :.: g) xs -> f (h g xs)
hsequence' (NP (f :.: K b) xs -> f (NP (K b) xs))
-> NP (f :.: K b) xs -> f (NP (K b) xs)
forall a b. (a -> b) -> a -> b
$ (forall a. K a a -> (:.:) f (K b) a)
-> NP (K a) xs -> NP (f :.: K b) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *).
(SListIN (Prod h) xs, HAp h) =>
(forall (a :: k). f a -> f' a) -> h f xs -> h f' xs
hmap (\(K x) -> f (K b a) -> (:.:) f (K b) a
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (f (K b a) -> (:.:) f (K b) a) -> f (K b a) -> (:.:) f (K b) a
forall a b. (a -> b) -> a -> b
$ b -> K b a
forall k a (b :: k). a -> K a b
K (b -> K b a) -> f b -> f (K b a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x) NP (K a) xs
xs

instance Show a => Show (Exactly xs a) where
  show :: Exactly xs a -> String
show (Exactly NP (K a) xs
xs) = NP (K a) xs -> (SListI xs => String) -> String
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (K a) xs
xs ((SListI xs => String) -> String)
-> (SListI xs => String) -> String
forall a b. (a -> b) -> a -> b
$
      case Dict (All (Compose Show (K a))) xs
SListI xs => Dict (All (Compose Show (K a))) xs
dict of
        Dict (All (Compose Show (K a))) xs
Dict -> NP (K a) xs -> String
forall a. Show a => a -> String
show NP (K a) xs
xs
    where
      dict :: SListI xs => Dict (All (Compose Show (K a))) xs
      dict :: Dict (All (Compose Show (K a))) xs
dict = NP (Dict (Compose Show (K a))) xs
-> Dict (All (Compose Show (K a))) xs
forall k (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP ((forall a. Dict (Compose Show (K a)) a)
-> NP (Dict (Compose Show (K a))) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure forall a. Dict (Compose Show (K a)) a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict)

instance Eq a => Eq (Exactly xs a) where
  Exactly NP (K a) xs
xs == :: Exactly xs a -> Exactly xs a -> Bool
== Exactly NP (K a) xs
xs' = NP (K a) xs -> (SListI xs => Bool) -> Bool
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (K a) xs
xs ((SListI xs => Bool) -> Bool) -> (SListI xs => Bool) -> Bool
forall a b. (a -> b) -> a -> b
$
      case Dict (All (Compose Eq (K a))) xs
SListI xs => Dict (All (Compose Eq (K a))) xs
dict of
        Dict (All (Compose Eq (K a))) xs
Dict -> NP (K a) xs
xs NP (K a) xs -> NP (K a) xs -> Bool
forall a. Eq a => a -> a -> Bool
== NP (K a) xs
xs'
    where
      dict :: SListI xs => Dict (All (Compose Eq (K a))) xs
      dict :: Dict (All (Compose Eq (K a))) xs
dict = NP (Dict (Compose Eq (K a))) xs -> Dict (All (Compose Eq (K a))) xs
forall k (c :: k -> Constraint) (xs :: [k]).
NP (Dict c) xs -> Dict (All c) xs
all_NP ((forall a. Dict (Compose Eq (K a)) a)
-> NP (Dict (Compose Eq (K a))) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *).
(HPure h, SListIN h xs) =>
(forall (a :: k). f a) -> h f xs
hpure forall a. Dict (Compose Eq (K a)) a
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict)

{-------------------------------------------------------------------------------
  Working with 'Exactly'
-------------------------------------------------------------------------------}

-- | Singleton
exactlyOne :: a -> Exactly '[x] a
exactlyOne :: a -> Exactly '[x] a
exactlyOne a
a = NP (K a) '[x] -> Exactly '[x] a
forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a
Exactly (NP (K a) '[x] -> Exactly '[x] a)
-> NP (K a) '[x] -> Exactly '[x] a
forall a b. (a -> b) -> a -> b
$ a -> K a x
forall k a (b :: k). a -> K a b
K a
a K a x -> NP (K a) '[] -> NP (K a) '[x]
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP (K a) '[]
forall k (f :: k -> *). NP f '[]
Nil

-- | From a pair
exactlyTwo :: a -> a -> Exactly '[x, y] a
exactlyTwo :: a -> a -> Exactly '[x, y] a
exactlyTwo a
a1 a
a2 = NP (K a) '[x, y] -> Exactly '[x, y] a
forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a
Exactly (NP (K a) '[x, y] -> Exactly '[x, y] a)
-> NP (K a) '[x, y] -> Exactly '[x, y] a
forall a b. (a -> b) -> a -> b
$ a -> K a x
forall k a (b :: k). a -> K a b
K a
a1 K a x -> NP (K a) '[y] -> NP (K a) '[x, y]
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* a -> K a y
forall k a (b :: k). a -> K a b
K a
a2 K a y -> NP (K a) '[] -> NP (K a) '[y]
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP (K a) '[]
forall k (f :: k -> *). NP f '[]
Nil

-- | Analogue of 'head'
exactlyHead :: Exactly (x ': xs) a -> a
exactlyHead :: Exactly (x : xs) a -> a
exactlyHead = K a x -> a
forall k a (b :: k). K a b -> a
unK (K a x -> a)
-> (Exactly (x : xs) a -> K a x) -> Exactly (x : xs) a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K a) (x : xs) -> K a x
forall k (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x
hd (NP (K a) (x : xs) -> K a x)
-> (Exactly (x : xs) a -> NP (K a) (x : xs))
-> Exactly (x : xs) a
-> K a x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exactly (x : xs) a -> NP (K a) (x : xs)
forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs
getExactly

-- | Analogue of 'tail'
exactlyTail :: Exactly (x ': xs) a -> Exactly xs a
exactlyTail :: Exactly (x : xs) a -> Exactly xs a
exactlyTail = NP (K a) xs -> Exactly xs a
forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a
Exactly (NP (K a) xs -> Exactly xs a)
-> (Exactly (x : xs) a -> NP (K a) xs)
-> Exactly (x : xs) a
-> Exactly xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K a) (x : xs) -> NP (K a) xs
forall k (f :: k -> *) (x :: k) (xs :: [k]).
NP f (x : xs) -> NP f xs
tl (NP (K a) (x : xs) -> NP (K a) xs)
-> (Exactly (x : xs) a -> NP (K a) (x : xs))
-> Exactly (x : xs) a
-> NP (K a) xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exactly (x : xs) a -> NP (K a) (x : xs)
forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs
getExactly

-- | Analogue of 'zip'
exactlyZip :: Exactly xs a -> Exactly xs b -> Exactly xs (a, b)
exactlyZip :: Exactly xs a -> Exactly xs b -> Exactly xs (a, b)
exactlyZip (Exactly NP (K a) xs
np) (Exactly NP (K b) xs
np') = NP (K (a, b)) xs -> Exactly xs (a, b)
forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a
Exactly (NP (K (a, b)) xs -> Exactly xs (a, b))
-> NP (K (a, b)) xs -> Exactly xs (a, b)
forall a b. (a -> b) -> a -> b
$
    NP (K a) xs -> (SListI xs => NP (K (a, b)) xs) -> NP (K (a, b)) xs
forall k (a :: k -> *) (xs :: [k]) r.
NP a xs -> (SListI xs => r) -> r
npToSListI NP (K a) xs
np ((SListI xs => NP (K (a, b)) xs) -> NP (K (a, b)) xs)
-> (SListI xs => NP (K (a, b)) xs) -> NP (K (a, b)) xs
forall a b. (a -> b) -> a -> b
$
      (forall a. K a a -> K b a -> K (a, b) a)
-> Prod NP (K a) xs -> NP (K b) xs -> NP (K (a, b)) xs
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (f :: k -> *)
       (f' :: k -> *) (f'' :: k -> *).
(SListIN (Prod h) xs, HAp h, HAp (Prod h)) =>
(forall (a :: k). f a -> f' a -> f'' a)
-> Prod h f xs -> h f' xs -> h f'' xs
hzipWith (\(K x) (K y) -> (a, b) -> K (a, b) a
forall k a (b :: k). a -> K a b
K (a
x, b
y)) Prod NP (K a) xs
NP (K a) xs
np NP (K b) xs
np'

-- | Analogue of 'zip' where the length of second argument is unknown
exactlyZipFoldable :: Foldable t => Exactly xs a -> t b -> AtMost xs (a, b)
exactlyZipFoldable :: Exactly xs a -> t b -> AtMost xs (a, b)
exactlyZipFoldable = \(Exactly NP (K a) xs
as) t b
bs -> NP (K a) xs -> [b] -> AtMost xs (a, b)
forall a (xs :: [*]) b. NP (K a) xs -> [b] -> AtMost xs (a, b)
go NP (K a) xs
as (t b -> [b]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList t b
bs)
  where
    go :: NP (K a) xs -> [b] -> AtMost xs (a, b)
    go :: NP (K a) xs -> [b] -> AtMost xs (a, b)
go NP (K a) xs
_           []     = AtMost xs (a, b)
forall (xs :: [*]) a. AtMost xs a
AtMostNil
    go NP (K a) xs
Nil         [b]
_      = AtMost xs (a, b)
forall (xs :: [*]) a. AtMost xs a
AtMostNil
    go (K a
a :* NP (K a) xs
as) (b
b:[b]
bs) = (a, b) -> AtMost xs (a, b) -> AtMost (x : xs) (a, b)
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons (a
a, b
b) (AtMost xs (a, b) -> AtMost (x : xs) (a, b))
-> AtMost xs (a, b) -> AtMost (x : xs) (a, b)
forall a b. (a -> b) -> a -> b
$ NP (K a) xs -> [b] -> AtMost xs (a, b)
forall a (xs :: [*]) b. NP (K a) xs -> [b] -> AtMost xs (a, b)
go NP (K a) xs
as [b]
bs

exactlyWeaken :: Exactly xs a -> AtMost xs a
exactlyWeaken :: Exactly xs a -> AtMost xs a
exactlyWeaken = NP (K a) xs -> AtMost xs a
forall a (xs :: [*]). NP (K a) xs -> AtMost xs a
go (NP (K a) xs -> AtMost xs a)
-> (Exactly xs a -> NP (K a) xs) -> Exactly xs a -> AtMost xs a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exactly xs a -> NP (K a) xs
forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs
getExactly
  where
    go :: NP (K a) xs -> AtMost xs a
    go :: NP (K a) xs -> AtMost xs a
go NP (K a) xs
Nil         = AtMost xs a
forall (xs :: [*]) a. AtMost xs a
AtMostNil
    go (K a
x :* NP (K a) xs
xs) = a -> AtMost xs a -> AtMost (x : xs) a
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons a
x (NP (K a) xs -> AtMost xs a
forall a (xs :: [*]). NP (K a) xs -> AtMost xs a
go NP (K a) xs
xs)

exactlyWeakenNonEmpty :: Exactly (x ': xs) a -> NonEmpty (x ': xs) a
exactlyWeakenNonEmpty :: Exactly (x : xs) a -> NonEmpty (x : xs) a
exactlyWeakenNonEmpty = NP (K a) (x : xs) -> NonEmpty (x : xs) a
forall a x (xs :: [*]). NP (K a) (x : xs) -> NonEmpty (x : xs) a
go (NP (K a) (x : xs) -> NonEmpty (x : xs) a)
-> (Exactly (x : xs) a -> NP (K a) (x : xs))
-> Exactly (x : xs) a
-> NonEmpty (x : xs) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exactly (x : xs) a -> NP (K a) (x : xs)
forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs
getExactly
  where
    go :: NP (K a) (x ': xs) -> NonEmpty (x ': xs) a
    go :: NP (K a) (x : xs) -> NonEmpty (x : xs) a
go (K a
x :* NP (K a) xs
Nil)         = a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
x
    go (K a
x :* xs :: NP (K a) xs
xs@(K a x
_ :* NP (K a) xs
_)) = a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
x (NP (K a) (x : xs) -> NonEmpty (x : xs) a
forall a x (xs :: [*]). NP (K a) (x : xs) -> NonEmpty (x : xs) a
go NP (K a) xs
NP (K a) (x : xs)
xs)

-- | Analogue of 'replicate'
--
-- In CPS style because the @xs@ type parameter is not statically known.
exactlyReplicate :: forall a r. Word -> a -> (forall xs. Exactly xs a -> r) -> r
exactlyReplicate :: Word -> a -> (forall (xs :: [*]). Exactly xs a -> r) -> r
exactlyReplicate = \Word
n a
a forall (xs :: [*]). Exactly xs a -> r
k -> Word -> a -> (forall (xs :: [*]). NP (K a) xs -> r) -> r
go Word
n a
a (Exactly xs a -> r
forall (xs :: [*]). Exactly xs a -> r
k (Exactly xs a -> r)
-> (NP (K a) xs -> Exactly xs a) -> NP (K a) xs -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K a) xs -> Exactly xs a
forall (xs :: [*]) a. NP (K a) xs -> Exactly xs a
Exactly)
  where
    go :: Word -> a -> (forall xs. NP (K a) xs -> r) -> r
    go :: Word -> a -> (forall (xs :: [*]). NP (K a) xs -> r) -> r
go Word
0 a
_ forall (xs :: [*]). NP (K a) xs -> r
k = NP (K a) '[] -> r
forall (xs :: [*]). NP (K a) xs -> r
k NP (K a) '[]
forall k (f :: k -> *). NP f '[]
Nil
    go Word
n a
a forall (xs :: [*]). NP (K a) xs -> r
k = Word -> a -> (forall (xs :: [*]). NP (K a) xs -> r) -> r
go (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) a
a ((forall (xs :: [*]). NP (K a) xs -> r) -> r)
-> (forall (xs :: [*]). NP (K a) xs -> r) -> r
forall a b. (a -> b) -> a -> b
$ \NP (K a) xs
xs -> NP (K a) (Any : xs) -> r
forall (xs :: [*]). NP (K a) xs -> r
k (a -> K a Any
forall k a (b :: k). a -> K a b
K a
a K a Any -> NP (K a) xs -> NP (K a) (Any : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP (K a) xs
xs)

{-------------------------------------------------------------------------------
  Working with 'AtMost'
-------------------------------------------------------------------------------}

-- | Singleton
atMostOne :: a -> AtMost (x ': xs) a
atMostOne :: a -> AtMost (x : xs) a
atMostOne a
x = a -> AtMost xs a -> AtMost (x : xs) a
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons a
x AtMost xs a
forall (xs :: [*]) a. AtMost xs a
AtMostNil

-- | Analogue of 'init'
--
-- For simplicity we don't shrink the type-level index.
atMostInit :: AtMost xs a -> Maybe (AtMost xs a, a)
atMostInit :: AtMost xs a -> Maybe (AtMost xs a, a)
atMostInit = AtMost xs a -> Maybe (AtMost xs a, a)
forall (xs :: [*]) a. AtMost xs a -> Maybe (AtMost xs a, a)
go
  where
    go :: AtMost xs a -> Maybe (AtMost xs a, a)
    go :: AtMost xs a -> Maybe (AtMost xs a, a)
go AtMost xs a
AtMostNil         = Maybe (AtMost xs a, a)
forall a. Maybe a
Nothing
    go (AtMostCons a
a AtMost xs a
as) = (AtMost (x : xs) a, a) -> Maybe (AtMost (x : xs) a, a)
forall a. a -> Maybe a
Just ((AtMost (x : xs) a, a) -> Maybe (AtMost (x : xs) a, a))
-> (AtMost (x : xs) a, a) -> Maybe (AtMost (x : xs) a, a)
forall a b. (a -> b) -> a -> b
$
                             case AtMost xs a -> Maybe (AtMost xs a, a)
forall (xs :: [*]) a. AtMost xs a -> Maybe (AtMost xs a, a)
go AtMost xs a
as of
                               Maybe (AtMost xs a, a)
Nothing        -> (AtMost (x : xs) a
forall (xs :: [*]) a. AtMost xs a
AtMostNil, a
a)
                               Just (AtMost xs a
as', a
a') -> (a -> AtMost xs a -> AtMost (x : xs) a
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons a
a AtMost xs a
as', a
a')

-- | Analogue of 'head'
atMostHead :: AtMost xs a -> Maybe a
atMostHead :: AtMost xs a -> Maybe a
atMostHead AtMost xs a
AtMostNil        = Maybe a
forall a. Maybe a
Nothing
atMostHead (AtMostCons a
x AtMost xs a
_) = a -> Maybe a
forall a. a -> Maybe a
Just a
x

-- | Analogue of 'last'
atMostLast :: AtMost xs a -> Maybe a
atMostLast :: AtMost xs a -> Maybe a
atMostLast = ((AtMost xs a, a) -> a) -> Maybe (AtMost xs a, a) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (AtMost xs a, a) -> a
forall a b. (a, b) -> b
snd (Maybe (AtMost xs a, a) -> Maybe a)
-> (AtMost xs a -> Maybe (AtMost xs a, a))
-> AtMost xs a
-> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AtMost xs a -> Maybe (AtMost xs a, a)
forall (xs :: [*]) a. AtMost xs a -> Maybe (AtMost xs a, a)
atMostInit

atMostZipFoldable :: Foldable t => AtMost xs a -> t b -> AtMost xs (a, b)
atMostZipFoldable :: AtMost xs a -> t b -> AtMost xs (a, b)
atMostZipFoldable = \AtMost xs a
as t b
bs -> AtMost xs a -> [b] -> AtMost xs (a, b)
forall (xs :: [*]) a b. AtMost xs a -> [b] -> AtMost xs (a, b)
go AtMost xs a
as (t b -> [b]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList t b
bs)
  where
    go :: AtMost xs a -> [b] -> AtMost xs (a, b)
    go :: AtMost xs a -> [b] -> AtMost xs (a, b)
go AtMost xs a
AtMostNil         [b]
_      = AtMost xs (a, b)
forall (xs :: [*]) a. AtMost xs a
AtMostNil
    go AtMost xs a
_                 []     = AtMost xs (a, b)
forall (xs :: [*]) a. AtMost xs a
AtMostNil
    go (AtMostCons a
a AtMost xs a
as) (b
b:[b]
bs) = (a, b) -> AtMost xs (a, b) -> AtMost (x : xs) (a, b)
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons (a
a, b
b) (AtMost xs a -> [b] -> AtMost xs (a, b)
forall (xs :: [*]) a b. AtMost xs a -> [b] -> AtMost xs (a, b)
go AtMost xs a
as [b]
bs)

atMostNonEmpty :: AtMost (x ': xs) a -> Maybe (NonEmpty (x ': xs) a)
atMostNonEmpty :: AtMost (x : xs) a -> Maybe (NonEmpty (x : xs) a)
atMostNonEmpty = \case
    AtMost (x : xs) a
AtMostNil       -> Maybe (NonEmpty (x : xs) a)
forall a. Maybe a
Nothing
    AtMostCons a
x AtMost xs a
xs -> NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a)
forall a. a -> Maybe a
Just (NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a))
-> NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a)
forall a b. (a -> b) -> a -> b
$ a -> AtMost xs a -> NonEmpty (x : xs) a
forall a (xs :: [*]) x. a -> AtMost xs a -> NonEmpty (x : xs) a
go a
x AtMost xs a
xs
  where
    go :: a -> AtMost xs a -> NonEmpty (x ': xs) a
    go :: a -> AtMost xs a -> NonEmpty (x : xs) a
go a
x AtMost xs a
AtMostNil         = a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne  a
x
    go a
x (AtMostCons a
y AtMost xs a
zs) = a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
x (a -> AtMost xs a -> NonEmpty (x : xs) a
forall a (xs :: [*]) x. a -> AtMost xs a -> NonEmpty (x : xs) a
go a
y AtMost xs a
zs)

{-------------------------------------------------------------------------------
  Working with 'NonEmpty'
-------------------------------------------------------------------------------}

instance IsNonEmpty xs => Applicative (NonEmpty xs) where
  pure :: a -> NonEmpty xs a
pure a
x = case Proxy xs -> ProofNonEmpty xs
forall a (xs :: [a]) (proxy :: [a] -> *).
IsNonEmpty xs =>
proxy xs -> ProofNonEmpty xs
isNonEmpty (Proxy xs
forall k (t :: k). Proxy t
Proxy @xs) of
             ProofNonEmpty{} -> a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
x
  <*> :: NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b
(<*>) = NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b
forall (xs' :: [*]) a b.
NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
go
    where
      go :: NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
      go :: NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
go (NonEmptyOne  a -> b
f)    (NonEmptyOne  a
x)    = b -> NonEmpty (x : xs) b
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne  (a -> b
f a
x)
      go (NonEmptyCons a -> b
f NonEmpty xs (a -> b)
_)  (NonEmptyOne  a
x)    = b -> NonEmpty (x : xs) b
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne  (a -> b
f a
x)
      go (NonEmptyOne  a -> b
f)    (NonEmptyCons a
x NonEmpty xs a
_)  = b -> NonEmpty (x : xs) b
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne  (a -> b
f a
x)
      go (NonEmptyCons a -> b
f NonEmpty xs (a -> b)
fs) (NonEmptyCons a
x NonEmpty xs a
xs) = b -> NonEmpty xs b -> NonEmpty (x : xs) b
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons (a -> b
f a
x) (NonEmpty xs (a -> b) -> NonEmpty xs a -> NonEmpty xs b
forall (xs' :: [*]) a b.
NonEmpty xs' (a -> b) -> NonEmpty xs' a -> NonEmpty xs' b
go NonEmpty xs (a -> b)
fs NonEmpty xs a
NonEmpty xs a
xs)

-- | Analogue of 'head'
nonEmptyHead :: NonEmpty xs a -> a
nonEmptyHead :: NonEmpty xs a -> a
nonEmptyHead (NonEmptyOne  a
x)   = a
x
nonEmptyHead (NonEmptyCons a
x NonEmpty xs a
_) = a
x

-- | Analogue of 'last'
nonEmptyLast :: NonEmpty xs a -> a
nonEmptyLast :: NonEmpty xs a -> a
nonEmptyLast = (Maybe (NonEmpty xs a), a) -> a
forall a b. (a, b) -> b
snd ((Maybe (NonEmpty xs a), a) -> a)
-> (NonEmpty xs a -> (Maybe (NonEmpty xs a), a))
-> NonEmpty xs a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit

-- | Analogue of 'init'
nonEmptyInit :: NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit :: NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit (NonEmptyOne  a
x)    = (Maybe (NonEmpty xs a)
forall a. Maybe a
Nothing, a
x)
nonEmptyInit (NonEmptyCons a
x NonEmpty xs a
xs) =
    case NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
forall (xs :: [*]) a. NonEmpty xs a -> (Maybe (NonEmpty xs a), a)
nonEmptyInit NonEmpty xs a
xs of
      (Maybe (NonEmpty xs a)
Nothing  , a
final) -> (NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a)
forall a. a -> Maybe a
Just (a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne  a
x)     , a
final)
      (Just NonEmpty xs a
xs' , a
final) -> (NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a)
forall a. a -> Maybe a
Just (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
x NonEmpty xs a
xs') , a
final)

-- | Build a 'NonEmpty' from a list. Returns 'Nothing' when the list is empty
-- or when it's longer than @xs@.
nonEmptyFromList :: forall xs a. SListI xs => [a] -> Maybe (NonEmpty xs a)
nonEmptyFromList :: [a] -> Maybe (NonEmpty xs a)
nonEmptyFromList = SList xs -> [a] -> Maybe (NonEmpty xs a)
forall (xs' :: [*]). SList xs' -> [a] -> Maybe (NonEmpty xs' a)
go (SListI xs => SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList @xs)
  where
    go :: forall xs'. SList xs' -> [a] -> Maybe (NonEmpty xs' a)
    go :: SList xs' -> [a] -> Maybe (NonEmpty xs' a)
go SList xs'
s [a]
ys = case (SList xs'
s, [a]
ys) of
        (SList xs'
SCons, [a
y])   -> NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a)
forall a. a -> Maybe a
Just (NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a))
-> NonEmpty (x : xs) a -> Maybe (NonEmpty (x : xs) a)
forall a b. (a -> b) -> a -> b
$ a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
y
        (SList xs'
SCons, a
y:[a]
ys') -> a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
y (NonEmpty xs a -> NonEmpty (x : xs) a)
-> Maybe (NonEmpty xs a) -> Maybe (NonEmpty (x : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SList xs -> [a] -> Maybe (NonEmpty xs a)
forall (xs' :: [*]). SList xs' -> [a] -> Maybe (NonEmpty xs' a)
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList [a]
ys'
        (SList xs'
SCons, [])    -> Maybe (NonEmpty xs' a)
forall a. Maybe a
Nothing
        (SList xs'
SNil,  [a]
_)     -> Maybe (NonEmpty xs' a)
forall a. Maybe a
Nothing

-- | Convert a 'NonEmpty' to a list.
nonEmptyToList :: forall xs a. NonEmpty xs a -> [a]
nonEmptyToList :: NonEmpty xs a -> [a]
nonEmptyToList = NonEmpty xs a -> [a]
forall (xs' :: [*]). NonEmpty xs' a -> [a]
go
  where
    go :: forall xs'. NonEmpty xs' a -> [a]
    go :: NonEmpty xs' a -> [a]
go (NonEmptyOne  a
x)    = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: []
    go (NonEmptyCons a
x NonEmpty xs a
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: NonEmpty xs a -> [a]
forall (xs' :: [*]). NonEmpty xs' a -> [a]
go NonEmpty xs a
xs

nonEmptyWeaken :: NonEmpty xs a -> AtMost xs a
nonEmptyWeaken :: NonEmpty xs a -> AtMost xs a
nonEmptyWeaken = NonEmpty xs a -> AtMost xs a
forall (xs :: [*]) a. NonEmpty xs a -> AtMost xs a
go
  where
    go :: NonEmpty xs a -> AtMost xs a
    go :: NonEmpty xs a -> AtMost xs a
go (NonEmptyOne  a
x)    = a -> AtMost xs a -> AtMost (x : xs) a
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons a
x AtMost xs a
forall (xs :: [*]) a. AtMost xs a
AtMostNil
    go (NonEmptyCons a
x NonEmpty xs a
xs) = a -> AtMost xs a -> AtMost (x : xs) a
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons a
x (NonEmpty xs a -> AtMost xs a
forall (xs :: [*]) a. NonEmpty xs a -> AtMost xs a
go NonEmpty xs a
xs)

-- | A strict prefixes
--
-- >    nonEmptyStrictPrefixes (fromJust (nonEmptyFromList [1..4]))
-- > == [ NonEmptyOne  1
-- >    , NonEmptyCons 1 $ NonEmptyOne  2
-- >    , NonEmptyCons 1 $ NonEmptyCons 2 $ NonEmptyOne 3
-- >    ]
nonEmptyStrictPrefixes :: NonEmpty xs a -> [NonEmpty xs a]
nonEmptyStrictPrefixes :: NonEmpty xs a -> [NonEmpty xs a]
nonEmptyStrictPrefixes = NonEmpty xs a -> [NonEmpty xs a]
forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a]
go
  where
    go :: NonEmpty xs a -> [NonEmpty xs a]
    go :: NonEmpty xs a -> [NonEmpty xs a]
go (NonEmptyOne  a
_)    = []
    go (NonEmptyCons a
x NonEmpty xs a
xs) = a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
x NonEmpty (x : xs) a
-> [NonEmpty (x : xs) a] -> [NonEmpty (x : xs) a]
forall a. a -> [a] -> [a]
: (NonEmpty xs a -> NonEmpty (x : xs) a)
-> [NonEmpty xs a] -> [NonEmpty (x : xs) a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
x) (NonEmpty xs a -> [NonEmpty xs a]
forall (xs :: [*]) a. NonEmpty xs a -> [NonEmpty xs a]
go NonEmpty xs a
xs)

-- | Apply the specified function to exactly one element
nonEmptyMapOne :: forall m xs a. Alternative m
               => (a -> m a) -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapOne :: (a -> m a) -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapOne a -> m a
f = NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go
  where
    go :: NonEmpty xs' a -> m (NonEmpty xs' a)
    go :: NonEmpty xs' a -> m (NonEmpty xs' a)
go (NonEmptyOne  a
x)    = a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (a -> NonEmpty (x : xs) a) -> m a -> m (NonEmpty (x : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
f a
x
    go (NonEmptyCons a
x NonEmpty xs a
xs) = [m (NonEmpty (x : xs) a)] -> m (NonEmpty (x : xs) a)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Foldable.asum [
          (\a
x' -> a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
x' NonEmpty xs a
xs) (a -> NonEmpty (x : xs) a) -> m a -> m (NonEmpty (x : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
f a
x
        , a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
x (NonEmpty xs a -> NonEmpty (x : xs) a)
-> m (NonEmpty xs a) -> m (NonEmpty (x : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go NonEmpty xs a
xs
        ]

-- | Variation on 'nonEmptyMapOne' where we try to apply the function to
-- /pairs/ of elements
nonEmptyMapTwo :: forall m xs a. Alternative m
               => (a -> m a) -- Used when we reached the end of the list
               -> (a -> a -> m (a, a))
               -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapTwo :: (a -> m a)
-> (a -> a -> m (a, a)) -> NonEmpty xs a -> m (NonEmpty xs a)
nonEmptyMapTwo a -> m a
f a -> a -> m (a, a)
g = NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go
  where
    go :: NonEmpty xs' a -> m (NonEmpty xs' a)
    go :: NonEmpty xs' a -> m (NonEmpty xs' a)
go (NonEmptyOne a
x) =
        a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne (a -> NonEmpty (x : xs) a) -> m a -> m (NonEmpty (x : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m a
f a
x
    go (NonEmptyCons a
x xs :: NonEmpty xs a
xs@(NonEmptyOne a
y)) = [m (NonEmpty (x : x : xs) a)] -> m (NonEmpty (x : x : xs) a)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Foldable.asum [
          (\(a
x', a
y') -> a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
x' (a -> NonEmpty (x : xs) a
forall a x (xs :: [*]). a -> NonEmpty (x : xs) a
NonEmptyOne a
y')) ((a, a) -> NonEmpty (x : x : xs) a)
-> m (a, a) -> m (NonEmpty (x : x : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> m (a, a)
g a
x a
y
        , a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
x (NonEmpty xs a -> NonEmpty (x : xs) a)
-> m (NonEmpty xs a) -> m (NonEmpty (x : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go NonEmpty xs a
xs
        ]
    go (NonEmptyCons a
x xs :: NonEmpty xs a
xs@(NonEmptyCons a
y NonEmpty xs a
zs)) = [m (NonEmpty (x : x : xs) a)] -> m (NonEmpty (x : x : xs) a)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
Foldable.asum [
          (\(a
x', a
y') -> a -> NonEmpty (x : xs) a -> NonEmpty (x : x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
x' (a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
y' NonEmpty xs a
zs)) ((a, a) -> NonEmpty (x : x : xs) a)
-> m (a, a) -> m (NonEmpty (x : x : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> a -> m (a, a)
g a
x a
y
        , a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (xs :: [*]) x. a -> NonEmpty xs a -> NonEmpty (x : xs) a
NonEmptyCons a
x (NonEmpty xs a -> NonEmpty (x : xs) a)
-> m (NonEmpty xs a) -> m (NonEmpty (x : xs) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty xs a -> m (NonEmpty xs a)
forall (xs' :: [*]). NonEmpty xs' a -> m (NonEmpty xs' a)
go NonEmpty xs a
xs
        ]