{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

-- | Type-level counting
--
-- Intended for unqualified import.
module Data.SOP.Counting (
    AtMost (..)
  , Exactly (.., ExactlyNil, ExactlyCons)
    -- * Working with 'Exactly'
  , exactlyHead
  , exactlyOne
  , exactlyReplicate
  , exactlyTail
  , exactlyTwo
  , exactlyWeaken
  , exactlyWeakenNonEmpty
  , exactlyZip
  , exactlyZipFoldable
    -- * Working with 'AtMost'
  , atMostFromNonEmpty
  , atMostHead
  , atMostInit
  , atMostLast
  , atMostNonEmpty
  , atMostOne
  , atMostZipFoldable
  ) where

import qualified Data.Foldable as Foldable
import           Data.Kind
import           Data.SOP.BasicFunctors
import           Data.SOP.Constraint
import           Data.SOP.Dict (Dict (..), all_NP)
import           Data.SOP.NonEmpty
import           Data.SOP.Strict

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

newtype Exactly xs a = Exactly { forall (xs :: [*]) a. Exactly xs a -> NP (K a) xs
getExactly :: NP (K a) xs }

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

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

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

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

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

{-# COMPLETE ExactlyNil, ExactlyCons #-}
pattern ExactlyCons :: () => xs' ~ (x ': xs) => a -> Exactly xs a -> Exactly xs' a
pattern $mExactlyCons :: forall {r} {xs' :: [*]} {a}.
Exactly xs' a
-> (forall {x} {xs :: [*]}.
    (xs' ~ (x : xs)) =>
    a -> Exactly xs a -> r)
-> ((# #) -> r)
-> r
$bExactlyCons :: forall (xs' :: [*]) a x (xs :: [*]).
(xs' ~ (x : xs)) =>
a -> Exactly xs a -> Exactly xs' a
ExactlyCons x xs <- (Exactly (K x :* (Exactly -> xs)))
  where
    ExactlyCons a
x Exactly xs a
xs = NP (K a) xs' -> Exactly 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 {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* 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 $mExactlyNil :: forall {r} {xs :: [*]} {a}.
Exactly xs a -> ((xs ~ '[]) => r) -> ((# #) -> r) -> r
$bExactlyNil :: forall (xs :: [*]) a. (xs ~ '[]) => Exactly xs a
ExactlyNil = Exactly 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 :: forall a b. (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 :: forall m a. Monoid m => (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 m a. Monoid m => (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 (xs :: [*]) a.
SListIN NP xs =>
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 :: forall (f :: * -> *) a b.
Applicative f =>
(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 a b. (a -> b) -> f a -> f 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 (xs :: [*]) (f :: * -> *) (g :: * -> *).
(SListIN NP xs, Applicative f) =>
NP (f :.: g) xs -> f (NP g 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 a
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 :: SListI xs => 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 (xs :: [*]) (f :: * -> *).
SListIN NP xs =>
(forall a. f a) -> NP f 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 Dict (Compose Show (K a)) a
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 :: SListI xs => 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 (xs :: [*]) (f :: * -> *).
SListIN NP xs =>
(forall a. f a) -> NP f 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 Dict (Compose Eq (K a)) a
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 :: forall a x. 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 {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* NP (K a) '[]
forall {k} (f :: k -> *). NP f '[]
Nil

-- | From a pair
exactlyTwo :: a -> a -> Exactly '[x, y] a
exactlyTwo :: forall a x y. 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 {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* 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 {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* NP (K a) '[]
forall {k} (f :: k -> *). NP f '[]
Nil

-- | Analogue of 'head'
exactlyHead :: Exactly (x ': xs) a -> a
exactlyHead :: forall x (xs :: [*]) a. 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 :: forall x (xs :: [*]) a. 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 :: forall (xs :: [*]) a b.
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 a
x) (K b
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 :: forall (t :: * -> *) (xs :: [*]) a b.
Foldable t =>
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 a. t a -> [a]
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 :: forall a (xs :: [*]) b. 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) xs1
as) (b
b:[b]
bs) = (a, b) -> AtMost xs1 (a, b) -> AtMost (x : xs1) (a, b)
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons (a
a, b
b) (AtMost xs1 (a, b) -> AtMost (x : xs1) (a, b))
-> AtMost xs1 (a, b) -> AtMost (x : xs1) (a, b)
forall a b. (a -> b) -> a -> b
$ NP (K a) xs1 -> [b] -> AtMost xs1 (a, b)
forall a (xs :: [*]) b. NP (K a) xs -> [b] -> AtMost xs (a, b)
go NP (K a) xs1
as [b]
bs

exactlyWeaken :: Exactly xs a -> AtMost xs a
exactlyWeaken :: forall (xs :: [*]) a. 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 :: forall a (xs :: [*]). 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) xs1
xs) = a -> AtMost xs1 a -> AtMost (x : xs1) a
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons a
x (NP (K a) xs1 -> AtMost xs1 a
forall a (xs :: [*]). NP (K a) xs -> AtMost xs a
go NP (K a) xs1
xs)

exactlyWeakenNonEmpty :: Exactly (x ': xs) a -> NonEmpty (x ': xs) a
exactlyWeakenNonEmpty :: forall x (xs :: [*]) a. 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 :: forall a x (xs :: [*]). NP (K a) (x : xs) -> NonEmpty (x : xs) a
go (K a
x :* NP (K a) xs1
Nil)         = a -> NonEmpty (x : xs) a
forall a x (xs1 :: [*]). a -> NonEmpty (x : xs1) a
NonEmptyOne a
x
    go (K a
x :* xs :: NP (K a) xs1
xs@(K a x
_ :* NP (K a) xs1
_)) = a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (xs1 :: [*]) x.
a -> NonEmpty xs1 a -> NonEmpty (x : xs1) a
NonEmptyCons a
x (NP (K a) (x : xs1) -> NonEmpty (x : xs1) a
forall a x (xs :: [*]). NP (K a) (x : xs) -> NonEmpty (x : xs) a
go NP (K a) xs1
NP (K a) (x : xs1)
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 :: forall a r.
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 {k} (f :: k -> *) (x :: k) (xs1 :: [k]).
f x -> NP f xs1 -> NP f (x : xs1)
:* NP (K a) xs
xs)

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

-- | Singleton
atMostOne :: a -> AtMost (x ': xs) a
atMostOne :: forall a x (xs :: [*]). 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 :: forall (xs :: [*]) a. 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 :: forall (xs :: [*]) a. 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 xs a, a) -> Maybe (AtMost xs a, a)
forall a. a -> Maybe a
Just ((AtMost xs a, a) -> Maybe (AtMost xs a, a))
-> (AtMost xs a, a) -> Maybe (AtMost 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 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 :: forall (xs :: [*]) a. 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 :: forall (xs :: [*]) a. AtMost xs a -> Maybe a
atMostLast = ((AtMost xs a, a) -> a) -> Maybe (AtMost xs a, a) -> Maybe a
forall a b. (a -> b) -> Maybe a -> Maybe b
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 :: forall (t :: * -> *) (xs :: [*]) a b.
Foldable t =>
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 a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Foldable.toList t b
bs)
  where
    go :: AtMost xs a -> [b] -> AtMost xs (a, b)
    go :: forall (xs :: [*]) a b. 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 :: forall x (xs :: [*]) a.
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
AtMost xs a
xs
  where
    go :: a -> AtMost xs a -> NonEmpty (x ': xs) a
    go :: forall a (xs :: [*]) x. a -> AtMost xs a -> NonEmpty (x : xs) a
go a
x AtMost xs a
AtMostNil         = a -> NonEmpty (x : xs) a
forall a x (xs1 :: [*]). a -> NonEmpty (x : xs1) a
NonEmptyOne  a
x
    go a
x (AtMostCons a
y AtMost xs a
zs) = a -> NonEmpty xs a -> NonEmpty (x : xs) a
forall a (xs1 :: [*]) x.
a -> NonEmpty xs1 a -> NonEmpty (x : xs1) 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)

atMostFromNonEmpty :: NonEmpty xs a -> AtMost xs a
atMostFromNonEmpty :: forall (xs :: [*]) a. NonEmpty xs a -> AtMost xs a
atMostFromNonEmpty = 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 :: forall (xs :: [*]) a. NonEmpty xs a -> AtMost xs a
go (NonEmptyOne  a
x)    = a -> AtMost xs1 a -> AtMost (x : xs1) a
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons a
x AtMost xs1 a
forall (xs :: [*]) a. AtMost xs a
AtMostNil
    go (NonEmptyCons a
x NonEmpty xs1 a
xs) = a -> AtMost xs1 a -> AtMost (x : xs1) a
forall a (xs :: [*]) x. a -> AtMost xs a -> AtMost (x : xs) a
AtMostCons a
x (NonEmpty xs1 a -> AtMost xs1 a
forall (xs :: [*]) a. NonEmpty xs a -> AtMost xs a
go NonEmpty xs1 a
xs)