{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE EmptyCase             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE StandaloneDeriving    #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

-- | Strict variant of SOP
--
-- This does not currently attempt to be exhaustive.
module Data.SOP.Strict (
    -- * NP
    NP (..)
  , hd
  , singletonNP
  , tl
    -- * NS
  , NS (..)
  , index_NS
  , unZ
    -- * Injections
  , Injection
  , injections
    -- * Re-exports from @sop-core@
  , module Data.SOP
  , module Data.SOP.Constraint
  ) where

import           Data.Coerce
import           Data.Kind (Type)
import           NoThunks.Class (NoThunks (..), allNoThunks)

import           Data.SOP hiding (Injection, NP (..), NS (..), hd, injections,
                     shiftInjection, tl, unZ)
import           Data.SOP.Classes (Same)
import           Data.SOP.Constraint

{-------------------------------------------------------------------------------
  NP
-------------------------------------------------------------------------------}

data NP :: (k -> Type) -> [k] -> Type where
  Nil  :: NP f '[]
  (:*) :: !(f x) -> !(NP f xs) -> NP f (x ': xs)

infixr 5 :*

type instance CollapseTo NP a = [a]
type instance AllN       NP c = All c
type instance AllZipN    NP c = AllZip c
type instance Prod       NP   = NP
type instance SListIN    NP   = SListI
type instance Same       NP   = NP

singletonNP :: f x -> NP f '[x]
singletonNP :: f x -> NP f '[x]
singletonNP f x
fx = f x
fx f x -> NP f '[] -> NP f '[x]
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP f '[]
forall k (f :: k -> *). NP f '[]
Nil

hd :: NP f (x ': xs) -> f x
hd :: NP f (x : xs) -> f x
hd (f x
x :* NP f xs
_) = f x
f x
x

tl :: NP f (x ': xs) -> NP f xs
tl :: NP f (x : xs) -> NP f xs
tl (f x
_ :* NP f xs
xs) = NP f xs
NP f xs
xs

ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP :: NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP NP (f -.-> g) xs
Nil          NP f xs
Nil       = NP g xs
forall k (f :: k -> *). NP f '[]
Nil
ap_NP (Fn f x -> g x
f :* NP (f -.-> g) xs
fs) (f x
x :* NP f xs
xs) = f x -> g x
f f x
f x
x g x -> NP g xs -> NP g (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NP (f -.-> g) xs -> NP f xs -> NP g xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP NP (f -.-> g) xs
fs NP f xs
NP f xs
xs

pure_NP :: SListI xs => (forall a. f a) -> NP f xs
pure_NP :: (forall (a :: k). f a) -> NP f xs
pure_NP = Proxy Top -> (forall (a :: k). Top a => f a) -> NP f xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)

cpure_NP :: forall c xs proxy f. All c xs
         => proxy c -> (forall a. c a => f a) -> NP f xs
cpure_NP :: proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP proxy c
_ forall (a :: k). c a => f a
f = SList xs -> NP f xs
forall (xs' :: [k]). All c xs' => SList xs' -> NP f xs'
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: All c xs' => SList xs' -> NP f xs'
    go :: SList xs' -> NP f xs'
go SList xs'
SNil  = NP f xs'
forall k (f :: k -> *). NP f '[]
Nil
    go SList xs'
SCons = f x
forall (a :: k). c a => f a
f f x -> NP f xs -> NP f (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* SList xs -> NP f xs
forall (xs' :: [k]). All c xs' => SList xs' -> NP f xs'
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList

collapse_NP :: NP (K a) xs -> [a]
collapse_NP :: NP (K a) xs -> [a]
collapse_NP = NP (K a) xs -> [a]
forall k a (xs :: [k]). NP (K a) xs -> [a]
go
  where
    go :: NP (K a) xs -> [a]
    go :: NP (K a) xs -> [a]
go NP (K a) xs
Nil         = []
    go (K a
x :* NP (K a) xs
xs) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: NP (K a) xs -> [a]
forall k a (xs :: [k]). NP (K a) xs -> [a]
go NP (K a) xs
xs

ctraverse'_NP  ::
     forall c proxy xs f f' g. (All c xs,  Applicative g)
  => proxy c -> (forall a. c a => f a -> g (f' a)) -> NP f xs  -> g (NP f' xs)
ctraverse'_NP :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
ctraverse'_NP proxy c
_ forall (a :: k). c a => f a -> g (f' a)
f = NP f xs -> g (NP f' xs)
forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys)
go
  where
    go :: All c ys => NP f ys -> g (NP f' ys)
    go :: NP f ys -> g (NP f' ys)
go NP f ys
Nil       = NP f' '[] -> g (NP f' '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure NP f' '[]
forall k (f :: k -> *). NP f '[]
Nil
    go (f x
x :* NP f xs
xs) = f' x -> NP f' xs -> NP f' (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
(:*) (f' x -> NP f' xs -> NP f' (x : xs))
-> g (f' x) -> g (NP f' xs -> NP f' (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> g (f' x)
forall (a :: k). c a => f a -> g (f' a)
f f x
x g (NP f' xs -> NP f' (x : xs))
-> g (NP f' xs) -> g (NP f' (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> NP f xs -> g (NP f' xs)
forall (ys :: [k]). All c ys => NP f ys -> g (NP f' ys)
go NP f xs
xs

ctraverse__NP ::
     forall c proxy xs f g. (All c xs, Applicative g)
  => proxy c -> (forall a. c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP :: proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP proxy c
_ forall (a :: k). c a => f a -> g ()
f = NP f xs -> g ()
forall (ys :: [k]). All c ys => NP f ys -> g ()
go
  where
    go :: All c ys => NP f ys -> g ()
    go :: NP f ys -> g ()
go NP f ys
Nil       = () -> g ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    go (f x
x :* NP f xs
xs) = f x -> g ()
forall (a :: k). c a => f a -> g ()
f f x
x g () -> g () -> g ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> NP f xs -> g ()
forall (ys :: [k]). All c ys => NP f ys -> g ()
go NP f xs
xs

traverse__NP ::
     forall xs f g. (SListI xs, Applicative g)
  => (forall a. f a -> g ()) -> NP f xs -> g ()
traverse__NP :: (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
traverse__NP forall (a :: k). f a -> g ()
f =
  Proxy Top
-> (forall (a :: k). Top a => f a -> g ()) -> NP f xs -> g ()
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top) forall (a :: k). f a -> g ()
forall (a :: k). Top a => f a -> g ()
f

trans_NP ::
     AllZip c xs ys
  => proxy c
  -> (forall x y . c x y => f x -> g y)
  -> NP f xs -> NP g ys
trans_NP :: proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP proxy c
_ forall (x :: k) (y :: k). c x y => f x -> g y
_t NP f xs
Nil       = NP g ys
forall k (f :: k -> *). NP f '[]
Nil
trans_NP proxy c
p  forall (x :: k) (y :: k). c x y => f x -> g y
t (f x
x :* NP f xs
xs) = f x -> g (Head ys)
forall (x :: k) (y :: k). c x y => f x -> g y
t f x
x g (Head ys) -> NP g (Tail ys) -> NP g (Head ys : Tail ys)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g (Tail ys)
forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP proxy c
p forall (x :: k) (y :: k). c x y => f x -> g y
t NP f xs
xs

coerce_NP ::
     forall f g xs ys .
     AllZip (LiftedCoercible f g) xs ys
  => NP f xs -> NP g ys
coerce_NP :: NP f xs -> NP g ys
coerce_NP = Proxy (LiftedCoercible f g)
-> (forall (x :: k) (y :: k).
    LiftedCoercible f g x y =>
    f x -> g y)
-> NP f xs
-> NP g ys
forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP (Proxy (LiftedCoercible f g)
forall k (t :: k). Proxy t
Proxy @(LiftedCoercible f g)) forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y
coerce

instance HPure NP where
  hpure :: (forall (a :: k). f a) -> NP f xs
hpure  = (forall (a :: k). f a) -> NP f xs
forall k (xs :: [k]) (f :: k -> *).
SListI xs =>
(forall (a :: k). f a) -> NP f xs
pure_NP
  hcpure :: proxy c -> (forall (a :: k). c a => f a) -> NP f xs
hcpure = proxy c -> (forall (a :: k). c a => f a) -> NP f xs
forall k (c :: k -> Constraint) (xs :: [k])
       (proxy :: (k -> Constraint) -> *) (f :: k -> *).
All c xs =>
proxy c -> (forall (a :: k). c a => f a) -> NP f xs
cpure_NP

instance HAp NP where
  hap :: Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
hap = Prod NP (f -.-> g) xs -> NP f xs -> NP g xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NP f xs -> NP g xs
ap_NP

instance HCollapse NP where
  hcollapse :: NP (K a) xs -> CollapseTo NP a
hcollapse = NP (K a) xs -> CollapseTo NP a
forall k a (xs :: [k]). NP (K a) xs -> [a]
collapse_NP

instance HSequence NP where
  hctraverse' :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
hctraverse' = proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
ctraverse'_NP
  htraverse' :: (forall (a :: k). f a -> g (f' a)) -> NP f xs -> g (NP f' xs)
htraverse'  = Proxy Top
-> (forall (a :: k). Top a => f a -> g (f' a))
-> NP f xs
-> g (NP f' xs)
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (g :: * -> *) (proxy :: (k -> Constraint) -> *)
       (f :: k -> *) (f' :: k -> *).
(HSequence h, AllN h c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> h f xs
-> g (h f' xs)
hctraverse' (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)
  hsequence' :: NP (f :.: g) xs -> f (NP g xs)
hsequence'  = (forall (a :: k). (:.:) f g a -> f (g a))
-> NP (f :.: g) xs -> f (NP g xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (g :: * -> *)
       (f :: k -> *) (f' :: k -> *).
(HSequence h, SListIN h xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs)
htraverse' forall (a :: k). (:.:) f g a -> f (g a)
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp

instance HTraverse_ NP where
  hctraverse_ :: proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
hctraverse_ = proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (g :: * -> *).
(All c xs, Applicative g) =>
proxy c -> (forall (a :: k). c a => f a -> g ()) -> NP f xs -> g ()
ctraverse__NP
  htraverse_ :: (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
htraverse_  = (forall (a :: k). f a -> g ()) -> NP f xs -> g ()
forall k (xs :: [k]) (f :: k -> *) (g :: * -> *).
(SListI xs, Applicative g) =>
(forall (a :: k). f a -> g ()) -> NP f xs -> g ()
traverse__NP

instance HTrans NP NP where
  htrans :: proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> NP f xs
-> NP g ys
htrans = proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> NP f xs
-> NP g ys
forall k k (c :: k -> k -> Constraint) (xs :: [k]) (ys :: [k])
       (proxy :: (k -> k -> Constraint) -> *) (f :: k -> *) (g :: k -> *).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NP f xs
-> NP g ys
trans_NP
  hcoerce :: NP f xs -> NP g ys
hcoerce = NP f xs -> NP g ys
forall k k (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
AllZip (LiftedCoercible f g) xs ys =>
NP f xs -> NP g ys
coerce_NP

{-------------------------------------------------------------------------------
  NS
-------------------------------------------------------------------------------}

data NS :: (k -> Type) -> [k] -> Type where
  Z :: !(f x) -> NS f (x ': xs)
  S :: !(NS f xs) -> NS f (x ': xs)

type instance CollapseTo NS a = a
type instance AllN       NS c = All c
type instance Prod       NS   = NP
type instance SListIN    NS   = SListI
type instance Same       NS   = NS

unZ :: NS f '[x] -> f x
unZ :: NS f '[x] -> f x
unZ (Z f x
x) = f x
f x
x

index_NS :: forall f xs . NS f xs -> Int
index_NS :: NS f xs -> Int
index_NS = Int -> NS f xs -> Int
forall (ys :: [k]). Int -> NS f ys -> Int
go Int
0
  where
    go :: forall ys . Int -> NS f ys -> Int
    go :: Int -> NS f ys -> Int
go !Int
acc (Z f x
_) = Int
acc
    go !Int
acc (S NS f xs
x) = Int -> NS f xs -> Int
forall (ys :: [k]). Int -> NS f ys -> Int
go (Int
acc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) NS f xs
x

expand_NS :: SListI xs => (forall x. f x) -> NS f xs -> NP f xs
expand_NS :: (forall (x :: k). f x) -> NS f xs -> NP f xs
expand_NS = Proxy Top -> (forall (x :: k). Top x => f x) -> NS f xs -> NP f xs
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (f :: k -> *) (xs :: [k]).
All c xs =>
proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
cexpand_NS (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)

cexpand_NS :: forall c proxy f xs. All c xs
           => proxy c -> (forall x. c x => f x) -> NS f xs -> NP f xs
cexpand_NS :: proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
cexpand_NS proxy c
p forall (x :: k). c x => f x
d = NS f xs -> NP f xs
forall (xs' :: [k]). All c xs' => NS f xs' -> NP f xs'
go
  where
    go :: forall xs'. All c xs' => NS f xs' -> NP f xs'
    go :: NS f xs' -> NP f xs'
go (Z f x
x) = f x
x f x -> NP f xs -> NP f (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* proxy c -> (forall (x :: k). c x => f x) -> NP f xs
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *).
(HPure h, AllN h c xs) =>
proxy c -> (forall (a :: k). c a => f a) -> h f xs
hcpure proxy c
p forall (x :: k). c x => f x
d
    go (S NS f xs
i) = f x
forall (x :: k). c x => f x
d f x -> NP f xs -> NP f (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* NS f xs -> NP f xs
forall (xs' :: [k]). All c xs' => NS f xs' -> NP f xs'
go NS f xs
i

ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs
ap_NS :: NP (f -.-> g) xs -> NS f xs -> NS g xs
ap_NS = NP (f -.-> g) xs -> NS f xs -> NS g xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NS f xs -> NS g xs
go
  where
    go :: NP (f -.-> g) xs -> NS f xs -> NS g xs
    go :: NP (f -.-> g) xs -> NS f xs -> NS g xs
go ((-.->) f g x
f :* NP (f -.-> g) xs
_)  (Z f x
x)  = g x -> NS g (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z (g x -> NS g (x : xs)) -> g x -> NS g (x : xs)
forall a b. (a -> b) -> a -> b
$ (-.->) f g x -> f x -> g x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(-.->) f g a -> f a -> g a
apFn (-.->) f g x
f f x
f x
x
    go ((-.->) f g x
_ :* NP (f -.-> g) xs
fs) (S NS f xs
xs) = NS g xs -> NS g (x : xs)
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (NS g xs -> NS g (x : xs)) -> NS g xs -> NS g (x : xs)
forall a b. (a -> b) -> a -> b
$ NP (f -.-> g) xs -> NS f xs -> NS g xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NS f xs -> NS g xs
go NP (f -.-> g) xs
fs NS f xs
NS f xs
xs
    go NP (f -.-> g) xs
Nil       NS f xs
x      = case NS f xs
x of {}

collapse_NS :: NS (K a) xs -> a
collapse_NS :: NS (K a) xs -> a
collapse_NS = NS (K a) xs -> a
forall k a (xs :: [k]). NS (K a) xs -> a
go
  where
    go :: NS (K a) xs  -> a
    go :: NS (K a) xs -> a
go (Z (K a
x)) = a
x
    go (S NS (K a) xs
xs)    = NS (K a) xs -> a
forall k a (xs :: [k]). NS (K a) xs -> a
go NS (K a) xs
xs

ctraverse'_NS  :: forall c proxy xs f f' g. (All c xs,  Functor g)
               => proxy c
               -> (forall a. c a => f a -> g (f' a))
               -> NS f xs  -> g (NS f' xs)
ctraverse'_NS :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
ctraverse'_NS proxy c
_ forall (a :: k). c a => f a -> g (f' a)
f = NS f xs -> g (NS f' xs)
forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys)
go
  where
    go :: All c ys => NS f ys -> g (NS f' ys)
    go :: NS f ys -> g (NS f' ys)
go (Z f x
x)  = f' x -> NS f' (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z (f' x -> NS f' (x : xs)) -> g (f' x) -> g (NS f' (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f x -> g (f' x)
forall (a :: k). c a => f a -> g (f' a)
f f x
x
    go (S NS f xs
xs) = NS f' xs -> NS f' (x : xs)
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (NS f' xs -> NS f' (x : xs)) -> g (NS f' xs) -> g (NS f' (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NS f xs -> g (NS f' xs)
forall (ys :: [k]). All c ys => NS f ys -> g (NS f' ys)
go NS f xs
xs

trans_NS :: forall proxy c f g xs ys. AllZip c xs ys
         => proxy c
         -> (forall x y . c x y => f x -> g y)
         -> NS f xs -> NS g ys
trans_NS :: proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NS f xs
-> NS g ys
trans_NS proxy c
_ forall (x :: k) (y :: k). c x y => f x -> g y
t = NS f xs -> NS g ys
forall (xs' :: [k]) (ys' :: [k]).
AllZip c xs' ys' =>
NS f xs' -> NS g ys'
go
  where
    go :: AllZip c xs' ys' => NS f xs' -> NS g ys'
    go :: NS f xs' -> NS g ys'
go (Z f x
x) = g (Head ys') -> NS g (Head ys' : Tail ys')
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z (f x -> g (Head ys')
forall (x :: k) (y :: k). c x y => f x -> g y
t f x
x)
    go (S NS f xs
x) = NS g (Tail ys') -> NS g (Head ys' : Tail ys')
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (NS f xs -> NS g (Tail ys')
forall (xs' :: [k]) (ys' :: [k]).
AllZip c xs' ys' =>
NS f xs' -> NS g ys'
go NS f xs
x)

-- TODO: @sop-core@ defines this in terms of @unsafeCoerce@. Currently we
-- don't make much use of this function, so I prefer this more strongly
-- typed version.
coerce_NS :: forall f g xs ys. AllZip (LiftedCoercible f g) xs ys
          => NS f xs -> NS g ys
coerce_NS :: NS f xs -> NS g ys
coerce_NS = Proxy (LiftedCoercible f g)
-> (forall (x :: k) (y :: k).
    LiftedCoercible f g x y =>
    f x -> g y)
-> NS f xs
-> NS g ys
forall k k (proxy :: (k -> k -> Constraint) -> *)
       (c :: k -> k -> Constraint) (f :: k -> *) (g :: k -> *) (xs :: [k])
       (ys :: [k]).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NS f xs
-> NS g ys
trans_NS (Proxy (LiftedCoercible f g)
forall k (t :: k). Proxy t
Proxy @(LiftedCoercible f g)) forall (x :: k) (y :: k). LiftedCoercible f g x y => f x -> g y
coerce

instance HExpand NS where
  hexpand :: (forall (x :: k). f x) -> NS f xs -> Prod NS f xs
hexpand  = (forall (x :: k). f x) -> NS f xs -> Prod NS f xs
forall k (xs :: [k]) (f :: k -> *).
SListI xs =>
(forall (x :: k). f x) -> NS f xs -> NP f xs
expand_NS
  hcexpand :: proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod NS f xs
hcexpand = proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> Prod NS f xs
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (f :: k -> *) (xs :: [k]).
All c xs =>
proxy c -> (forall (x :: k). c x => f x) -> NS f xs -> NP f xs
cexpand_NS

instance HAp NS where
  hap :: Prod NS (f -.-> g) xs -> NS f xs -> NS g xs
hap = Prod NS (f -.-> g) xs -> NS f xs -> NS g xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
NP (f -.-> g) xs -> NS f xs -> NS g xs
ap_NS

instance HCollapse NS where
  hcollapse :: NS (K a) xs -> CollapseTo NS a
hcollapse = NS (K a) xs -> CollapseTo NS a
forall k a (xs :: [k]). NS (K a) xs -> a
collapse_NS

instance HSequence NS where
  hctraverse' :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
hctraverse' = proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (xs :: [k]) (f :: k -> *) (f' :: k -> *) (g :: * -> *).
(All c xs, Functor g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
ctraverse'_NS
  htraverse' :: (forall (a :: k). f a -> g (f' a)) -> NS f xs -> g (NS f' xs)
htraverse'  = Proxy Top
-> (forall (a :: k). Top a => f a -> g (f' a))
-> NS f xs
-> g (NS f' xs)
forall k l (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (g :: * -> *) (proxy :: (k -> Constraint) -> *)
       (f :: k -> *) (f' :: k -> *).
(HSequence h, AllN h c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> h f xs
-> g (h f' xs)
hctraverse' (Proxy Top
forall k (t :: k). Proxy t
Proxy @Top)
  hsequence' :: NS (f :.: g) xs -> f (NS g xs)
hsequence'  = (forall (a :: k). (:.:) f g a -> f (g a))
-> NS (f :.: g) xs -> f (NS g xs)
forall k l (h :: (k -> *) -> l -> *) (xs :: l) (g :: * -> *)
       (f :: k -> *) (f' :: k -> *).
(HSequence h, SListIN h xs, Applicative g) =>
(forall (a :: k). f a -> g (f' a)) -> h f xs -> g (h f' xs)
htraverse' forall (a :: k). (:.:) f g a -> f (g a)
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
(:.:) f g p -> f (g p)
unComp

instance HTrans NS NS where
  htrans :: proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> NS f xs
-> NS g ys
htrans  = proxy c
-> (forall (x :: k1) (y :: k2). c x y => f x -> g y)
-> NS f xs
-> NS g ys
forall k k (proxy :: (k -> k -> Constraint) -> *)
       (c :: k -> k -> Constraint) (f :: k -> *) (g :: k -> *) (xs :: [k])
       (ys :: [k]).
AllZip c xs ys =>
proxy c
-> (forall (x :: k) (y :: k). c x y => f x -> g y)
-> NS f xs
-> NS g ys
trans_NS
  hcoerce :: NS f xs -> NS g ys
hcoerce = NS f xs -> NS g ys
forall k k (f :: k -> *) (g :: k -> *) (xs :: [k]) (ys :: [k]).
AllZip (LiftedCoercible f g) xs ys =>
NS f xs -> NS g ys
coerce_NS

{-------------------------------------------------------------------------------
  Injections
-------------------------------------------------------------------------------}

type Injection (f :: k -> Type) (xs :: [k]) = f -.-> K (NS f xs)

injections :: forall xs f. SListI xs => NP (Injection f xs) xs
injections :: NP (Injection f xs) xs
injections = SList xs -> NP (Injection f xs) xs
forall (xs' :: [k]). SList xs' -> NP (Injection f xs') xs'
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList
  where
    go :: SList xs' -> NP (Injection f xs') xs'
    go :: SList xs' -> NP (Injection f xs') xs'
go SList xs'
SNil  = NP (Injection f xs') xs'
forall k (f :: k -> *). NP f '[]
Nil
    go SList xs'
SCons = (f x -> K (NS f (x : xs)) x) -> (-.->) f (K (NS f (x : xs))) x
forall k (f :: k -> *) (a :: k) (f' :: k -> *).
(f a -> f' a) -> (-.->) f f' a
fn (NS f (x : xs) -> K (NS f (x : xs)) x
forall k a (b :: k). a -> K a b
K (NS f (x : xs) -> K (NS f (x : xs)) x)
-> (f x -> NS f (x : xs)) -> f x -> K (NS f (x : xs)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> NS f (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]). f x -> NS f (x : xs)
Z) (-.->) f (K (NS f (x : xs))) x
-> NP (f -.-> K (NS f (x : xs))) xs
-> NP (f -.-> K (NS f (x : xs))) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* (forall (a :: k).
 Injection f xs a -> (-.->) f (K (NS f (x : xs))) a)
-> NP (Injection f xs) xs -> NP (f -.-> K (NS f (x : xs))) 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 forall (a :: k). Injection f xs a -> (-.->) f (K (NS f (x : xs))) a
forall a (f :: a -> *) (xs :: [a]) (a :: a) (x :: a).
Injection f xs a -> Injection f (x : xs) a
shiftInjection (SList xs -> NP (Injection f xs) xs
forall (xs' :: [k]). SList xs' -> NP (Injection f xs') xs'
go SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList)

shiftInjection :: Injection f xs a -> Injection f (x ': xs) a
shiftInjection :: Injection f xs a -> Injection f (x : xs) a
shiftInjection (Fn f a -> K (NS f xs) a
f) = (f a -> K (NS f (x : xs)) a) -> Injection f (x : xs) a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
(f a -> g a) -> (-.->) f g a
Fn ((f a -> K (NS f (x : xs)) a) -> Injection f (x : xs) a)
-> (f a -> K (NS f (x : xs)) a) -> Injection f (x : xs) a
forall a b. (a -> b) -> a -> b
$ NS f (x : xs) -> K (NS f (x : xs)) a
forall k a (b :: k). a -> K a b
K (NS f (x : xs) -> K (NS f (x : xs)) a)
-> (f a -> NS f (x : xs)) -> f a -> K (NS f (x : xs)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS f xs -> NS f (x : xs)
forall a (f :: a -> *) (xs :: [a]) (x :: a).
NS f xs -> NS f (x : xs)
S (NS f xs -> NS f (x : xs))
-> (f a -> NS f xs) -> f a -> NS f (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K (NS f xs) a -> NS f xs
forall k a (b :: k). K a b -> a
unK (K (NS f xs) a -> NS f xs)
-> (f a -> K (NS f xs) a) -> f a -> NS f xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> K (NS f xs) a
f

{-------------------------------------------------------------------------------
  Instances
-------------------------------------------------------------------------------}

deriving instance All (Show `Compose` f) xs => Show (NS f xs)
deriving instance All (Eq   `Compose` f) xs => Eq   (NS f xs)
deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NS f xs)

-- | Copied from sop-core
--
-- Not derived, since derived instance ignores associativity info
instance All (Show `Compose` f) xs => Show (NP f xs) where
  showsPrec :: Int -> NP f xs -> ShowS
showsPrec Int
_ NP f xs
Nil       = String -> ShowS
showString String
"Nil"
  showsPrec Int
d (f x
f :* NP f xs
fs) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5)
                        (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> f x -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
5 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) f x
f
                        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :* "
                        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NP f xs -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
5 NP f xs
fs

deriving instance  All (Eq `Compose` f) xs                            => Eq  (NP f xs)
deriving instance (All (Eq `Compose` f) xs, All (Ord `Compose` f) xs) => Ord (NP f xs)

{-------------------------------------------------------------------------------
  NoThunks
-------------------------------------------------------------------------------}

instance All (Compose NoThunks f) xs
      => NoThunks (NS (f :: k -> Type) (xs :: [k])) where
  showTypeOf :: Proxy (NS f xs) -> String
showTypeOf Proxy (NS f xs)
_ = String
"NS"
  wNoThunks :: Context -> NS f xs -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt = \case
      Z f x
l -> Context -> f x -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks (String
"Z" String -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) f x
l
      S NS f xs
r -> Context -> NS f xs -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks (String
"S" String -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) NS f xs
r

instance All (Compose NoThunks f) xs
      => NoThunks (NP (f :: k -> Type) (xs :: [k])) where
  showTypeOf :: Proxy (NP f xs) -> String
showTypeOf Proxy (NP f xs)
_ = String
"NP"
  wNoThunks :: Context -> NP f xs -> IO (Maybe ThunkInfo)
wNoThunks Context
ctxt = \case
      NP f xs
Nil     -> Maybe ThunkInfo -> IO (Maybe ThunkInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ThunkInfo
forall a. Maybe a
Nothing
      f x
x :* NP f xs
xs -> [IO (Maybe ThunkInfo)] -> IO (Maybe ThunkInfo)
allNoThunks [
                     Context -> f x -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks (String
"fst" String -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) f x
x
                   , Context -> NP f xs -> IO (Maybe ThunkInfo)
forall a. NoThunks a => Context -> a -> IO (Maybe ThunkInfo)
noThunks (String
"snd" String -> Context -> Context
forall a. a -> [a] -> [a]
: Context
ctxt) NP f xs
xs
                   ]