{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE EmptyCase            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
-- | NP with optional values
--
--
-- Intended for qualified import
--
-- > import           Ouroboros.Consensus.Util.OptNP (OptNP (..), ViewOptNP (..))
-- > import qualified Ouroboros.Consensus.Util.OptNP as OptNP
module Ouroboros.Consensus.Util.OptNP (
    NonEmptyOptNP
  , OptNP (..)
  , at
  , empty
  , fromNP
  , fromNonEmptyNP
  , fromSingleton
  , singleton
  , toNP
    -- * View
  , ViewOptNP (..)
  , view
    -- * Combining
  , combine
  , combineWith
  , zipWith
  ) where

import           Prelude hiding (zipWith)

import           Control.Monad (guard)
import           Data.Functor.These (These1 (..))
import           Data.Kind (Type)
import           Data.Maybe (isJust)
import           Data.SOP.Strict hiding (And)
import           Data.Type.Bool (type (&&))
import           Data.Type.Equality
import           GHC.Stack (HasCallStack)

import           Ouroboros.Consensus.Util.SOP

type NonEmptyOptNP = OptNP 'False

-- | Like an 'NP', but with optional values
data OptNP (empty :: Bool) (f :: k -> Type) (xs :: [k]) where
  OptNil  :: OptNP 'True f '[]
  OptCons :: !(f x) -> !(OptNP empty f xs) -> OptNP 'False f (x ': xs)
  OptSkip :: !(OptNP empty f xs) -> OptNP empty f (x ': xs)

type instance AllN    (OptNP empty) c = All c
type instance SListIN (OptNP empty)   = SListI
type instance Prod    (OptNP empty)   = NP

deriving instance All (Show `Compose` f) xs => Show (OptNP empty f xs)

eq ::
     All (Eq `Compose` f) xs
  => OptNP empty f xs
  -> OptNP empty' f xs -> Maybe (empty :~: empty')
eq :: OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty')
eq OptNP empty f xs
OptNil         OptNP empty' f xs
OptNil         = (empty :~: empty) -> Maybe (empty :~: empty)
forall a. a -> Maybe a
Just empty :~: empty
forall k (a :: k). a :~: a
Refl
eq (OptSkip   OptNP empty f xs
xs) (OptSkip   OptNP empty' f xs
ys) = OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty')
forall k (f :: k -> *) (xs :: [k]) (empty :: Bool)
       (empty' :: Bool).
All (Compose Eq f) xs =>
OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty')
eq OptNP empty f xs
xs OptNP empty' f xs
OptNP empty' f xs
ys
eq (OptCons f x
x OptNP empty f xs
xs) (OptCons f x
y OptNP empty f xs
ys) = do Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (f x
x f x -> f x -> Bool
forall a. Eq a => a -> a -> Bool
== f x
f x
y)
                                      empty :~: empty
Refl <- OptNP empty f xs -> OptNP empty f xs -> Maybe (empty :~: empty)
forall k (f :: k -> *) (xs :: [k]) (empty :: Bool)
       (empty' :: Bool).
All (Compose Eq f) xs =>
OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty')
eq OptNP empty f xs
xs OptNP empty f xs
OptNP empty f xs
ys
                                      (empty :~: empty) -> Maybe (empty :~: empty)
forall (m :: * -> *) a. Monad m => a -> m a
return empty :~: empty
forall k (a :: k). a :~: a
Refl
eq OptNP empty f xs
_              OptNP empty' f xs
_              = Maybe (empty :~: empty')
forall a. Maybe a
Nothing

instance All (Eq `Compose` f) xs => Eq (OptNP empty f xs) where
  OptNP empty f xs
xs == :: OptNP empty f xs -> OptNP empty f xs -> Bool
== OptNP empty f xs
ys = Maybe (empty :~: empty) -> Bool
forall a. Maybe a -> Bool
isJust (OptNP empty f xs -> OptNP empty f xs -> Maybe (empty :~: empty)
forall k (f :: k -> *) (xs :: [k]) (empty :: Bool)
       (empty' :: Bool).
All (Compose Eq f) xs =>
OptNP empty f xs -> OptNP empty' f xs -> Maybe (empty :~: empty')
eq OptNP empty f xs
xs OptNP empty f xs
ys)

empty :: forall f xs. SListI xs => OptNP 'True f xs
empty :: OptNP 'True f xs
empty = case SListI xs => SList xs
forall k (xs :: [k]). SListI xs => SList xs
sList @xs of
    SList xs
SNil  -> OptNP 'True f xs
forall k (f :: k -> *). OptNP 'True f '[]
OptNil
    SList xs
SCons -> OptNP 'True f xs -> OptNP 'True f (x : xs)
forall a (empty :: Bool) (f :: a -> *) (xs :: [a]) (x :: a).
OptNP empty f xs -> OptNP empty f (x : xs)
OptSkip OptNP 'True f xs
forall k (f :: k -> *) (xs :: [k]). SListI xs => OptNP 'True f xs
empty

fromNonEmptyNP :: forall f xs. IsNonEmpty xs => NP f xs -> NonEmptyOptNP f xs
fromNonEmptyNP :: NP f xs -> NonEmptyOptNP f xs
fromNonEmptyNP NP f xs
xs = 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 {} ->
      case NP f xs
xs of
        f x
x :* NP f xs
xs' -> (forall (empty :: Bool). OptNP empty f xs -> NonEmptyOptNP f xs)
-> NP f xs -> NonEmptyOptNP f xs
forall k (f :: k -> *) (xs :: [k]) r.
(forall (empty :: Bool). OptNP empty f xs -> r) -> NP f xs -> r
fromNP (f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]).
f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
OptCons f x
x) NP f xs
xs'

fromNP :: (forall empty. OptNP empty f xs -> r) -> NP f xs -> r
fromNP :: (forall (empty :: Bool). OptNP empty f xs -> r) -> NP f xs -> r
fromNP forall (empty :: Bool). OptNP empty f xs -> r
k NP f xs
Nil       = OptNP 'True f xs -> r
forall (empty :: Bool). OptNP empty f xs -> r
k OptNP 'True f xs
forall k (f :: k -> *). OptNP 'True f '[]
OptNil
fromNP forall (empty :: Bool). OptNP empty f xs -> r
k (f x
x :* NP f xs
xs) = (forall (empty :: Bool). OptNP empty f xs -> r) -> NP f xs -> r
forall k (f :: k -> *) (xs :: [k]) r.
(forall (empty :: Bool). OptNP empty f xs -> r) -> NP f xs -> r
fromNP (OptNP 'False f xs -> r
forall (empty :: Bool). OptNP empty f xs -> r
k (OptNP 'False f xs -> r)
-> (OptNP empty f xs -> OptNP 'False f xs) -> OptNP empty f xs -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]).
f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
OptCons f x
x) NP f xs
xs

toNP :: OptNP empty f xs -> NP (Maybe :.: f) xs
toNP :: OptNP empty f xs -> NP (Maybe :.: f) xs
toNP = OptNP empty f xs -> NP (Maybe :.: f) xs
forall k (empty :: Bool) (f :: k -> *) (xs :: [k]).
OptNP empty f xs -> NP (Maybe :.: f) xs
go
  where
    go :: OptNP empty f xs -> NP (Maybe :.: f) xs
    go :: OptNP empty f xs -> NP (Maybe :.: f) xs
go OptNP empty f xs
OptNil         = NP (Maybe :.: f) xs
forall k (f :: k -> *). NP f '[]
Nil
    go (OptCons f x
x OptNP empty f xs
xs) = Maybe (f x) -> (:.:) Maybe f x
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (f x -> Maybe (f x)
forall a. a -> Maybe a
Just f x
x) (:.:) Maybe f x -> NP (Maybe :.: f) xs -> NP (Maybe :.: f) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* OptNP empty f xs -> NP (Maybe :.: f) xs
forall k (empty :: Bool) (f :: k -> *) (xs :: [k]).
OptNP empty f xs -> NP (Maybe :.: f) xs
go OptNP empty f xs
xs
    go (OptSkip   OptNP empty f xs
xs) = Maybe (f x) -> (:.:) Maybe f x
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp Maybe (f x)
forall a. Maybe a
Nothing  (:.:) Maybe f x -> NP (Maybe :.: f) xs -> NP (Maybe :.: f) (x : xs)
forall a (f :: a -> *) (x :: a) (xs :: [a]).
f x -> NP f xs -> NP f (x : xs)
:* OptNP empty f xs -> NP (Maybe :.: f) xs
forall k (empty :: Bool) (f :: k -> *) (xs :: [k]).
OptNP empty f xs -> NP (Maybe :.: f) xs
go OptNP empty f xs
xs

at :: SListI xs => f x -> Index xs x -> NonEmptyOptNP f xs
at :: f x -> Index xs x -> NonEmptyOptNP f xs
at f x
x Index xs x
IZ         = f x -> OptNP 'True f xs -> OptNP 'False f (x : xs)
forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]).
f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
OptCons f x
x OptNP 'True f xs
forall k (f :: k -> *) (xs :: [k]). SListI xs => OptNP 'True f xs
empty
at f x
x (IS Index xs x
index) = OptNP 'False f xs -> OptNP 'False f (y : xs)
forall a (empty :: Bool) (f :: a -> *) (xs :: [a]) (x :: a).
OptNP empty f xs -> OptNP empty f (x : xs)
OptSkip (f x -> Index xs x -> OptNP 'False f xs
forall k (xs :: [k]) (f :: k -> *) (x :: k).
SListI xs =>
f x -> Index xs x -> NonEmptyOptNP f xs
at f x
x Index xs x
index)

singleton :: f x -> NonEmptyOptNP f '[x]
singleton :: f x -> NonEmptyOptNP f '[x]
singleton f x
x = f x -> OptNP 'True f '[] -> NonEmptyOptNP f '[x]
forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]).
f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
OptCons f x
x OptNP 'True f '[]
forall k (f :: k -> *). OptNP 'True f '[]
OptNil

-- | If 'OptNP' is not empty, it must contain at least one value
fromSingleton :: NonEmptyOptNP f '[x] -> f x
fromSingleton :: NonEmptyOptNP f '[x] -> f x
fromSingleton (OptCons f x
x OptNP empty f xs
_) = f x
f x
x

ap ::
     NP (f -.-> g) xs
  -> OptNP empty f xs
  -> OptNP empty g xs
ap :: NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs
ap = NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) (empty :: Bool).
NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs
go
  where
    go :: NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs
    go :: NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs
go ((-.->) f g x
f :* NP (f -.-> g) xs
fs) (OptCons f x
x OptNP empty f xs
xs) = g x -> OptNP empty g xs -> OptNP 'False g (x : xs)
forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]).
f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
OptCons ((-.->) 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) (NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) (empty :: Bool).
NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs
go NP (f -.-> g) xs
fs OptNP empty f xs
OptNP empty f xs
xs)
    go ((-.->) f g x
_ :* NP (f -.-> g) xs
fs) (OptSkip   OptNP empty f xs
xs) = OptNP empty g xs -> OptNP empty g (x : xs)
forall a (empty :: Bool) (f :: a -> *) (xs :: [a]) (x :: a).
OptNP empty f xs -> OptNP empty f (x : xs)
OptSkip            (NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs
forall k (f :: k -> *) (g :: k -> *) (xs :: [k]) (empty :: Bool).
NP (f -.-> g) xs -> OptNP empty f xs -> OptNP empty g xs
go NP (f -.-> g) xs
fs OptNP empty f xs
OptNP empty f xs
xs)
    go NP (f -.-> g) xs
Nil       OptNP empty f xs
OptNil         = OptNP empty g xs
forall k (f :: k -> *). OptNP 'True f '[]
OptNil

ctraverse' ::
     forall c proxy empty xs f f' g. (All c xs, Applicative g)
  => proxy c
  -> (forall a. c a => f a -> g (f' a))
  -> OptNP empty f xs  -> g (OptNP empty f' xs)
ctraverse' :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> OptNP empty f xs
-> g (OptNP empty f' xs)
ctraverse' proxy c
_ forall (a :: k). c a => f a -> g (f' a)
f = OptNP empty f xs -> g (OptNP empty f' xs)
forall (ys :: [k]) (empty' :: Bool).
All c ys =>
OptNP empty' f ys -> g (OptNP empty' f' ys)
go
  where
    go :: All c ys => OptNP empty' f ys -> g (OptNP empty' f' ys)
    go :: OptNP empty' f ys -> g (OptNP empty' f' ys)
go (OptCons f x
x OptNP empty f xs
xs) = f' x -> OptNP empty f' xs -> OptNP 'False f' (x : xs)
forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]).
f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
OptCons (f' x -> OptNP empty f' xs -> OptNP 'False f' (x : xs))
-> g (f' x) -> g (OptNP empty f' xs -> OptNP 'False 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 (OptNP empty f' xs -> OptNP 'False f' (x : xs))
-> g (OptNP empty f' xs) -> g (OptNP 'False f' (x : xs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> OptNP empty f xs -> g (OptNP empty f' xs)
forall (ys :: [k]) (empty' :: Bool).
All c ys =>
OptNP empty' f ys -> g (OptNP empty' f' ys)
go OptNP empty f xs
xs
    go (OptSkip   OptNP empty' f xs
xs) = OptNP empty' f' xs -> OptNP empty' f' (x : xs)
forall a (empty :: Bool) (f :: a -> *) (xs :: [a]) (x :: a).
OptNP empty f xs -> OptNP empty f (x : xs)
OptSkip (OptNP empty' f' xs -> OptNP empty' f' (x : xs))
-> g (OptNP empty' f' xs) -> g (OptNP empty' f' (x : xs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>         OptNP empty' f xs -> g (OptNP empty' f' xs)
forall (ys :: [k]) (empty' :: Bool).
All c ys =>
OptNP empty' f ys -> g (OptNP empty' f' ys)
go OptNP empty' f xs
xs
    go OptNP empty' f ys
OptNil         = OptNP 'True f' '[] -> g (OptNP 'True f' '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure OptNP 'True f' '[]
forall k (f :: k -> *). OptNP 'True f '[]
OptNil

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

instance HSequence (OptNP empty) where
  hctraverse' :: proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> OptNP empty f xs
-> g (OptNP empty f' xs)
hctraverse' = proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> OptNP empty f xs
-> g (OptNP empty f' xs)
forall k (c :: k -> Constraint) (proxy :: (k -> Constraint) -> *)
       (empty :: Bool) (xs :: [k]) (f :: k -> *) (f' :: k -> *)
       (g :: * -> *).
(All c xs, Applicative g) =>
proxy c
-> (forall (a :: k). c a => f a -> g (f' a))
-> OptNP empty f xs
-> g (OptNP empty f' xs)
ctraverse'
  htraverse' :: (forall (a :: k). f a -> g (f' a))
-> OptNP empty f xs -> g (OptNP empty f' xs)
htraverse'  = Proxy Top
-> (forall (a :: k). Top a => f a -> g (f' a))
-> OptNP empty f xs
-> g (OptNP empty 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' :: OptNP empty (f :.: g) xs -> f (OptNP empty g xs)
hsequence'  = (forall (a :: k). (:.:) f g a -> f (g a))
-> OptNP empty (f :.: g) xs -> f (OptNP empty 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

{-------------------------------------------------------------------------------
  View
-------------------------------------------------------------------------------}

data ViewOptNP f xs where
  OptNP_ExactlyOne :: f x -> ViewOptNP f '[x]
  OptNP_AtLeastTwo ::        ViewOptNP f (x ': y ': zs)

view :: forall f xs. NonEmptyOptNP f xs -> ViewOptNP f xs
view :: NonEmptyOptNP f xs -> ViewOptNP f xs
view = \case
    OptCons f x
x  OptNP empty f xs
OptNil       -> f x -> ViewOptNP f '[x]
forall k (f :: k -> *) (x :: k). f x -> ViewOptNP f '[x]
OptNP_ExactlyOne f x
x
    OptCons f x
_ (OptCons f x
_ OptNP empty f xs
_) -> ViewOptNP f xs
forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k]).
ViewOptNP f (x : y : zs)
OptNP_AtLeastTwo
    OptCons f x
_ (OptSkip OptNP empty f xs
_)   -> ViewOptNP f xs
forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k]).
ViewOptNP f (x : y : zs)
OptNP_AtLeastTwo
    OptSkip   (OptCons f x
_ OptNP empty f xs
_) -> ViewOptNP f xs
forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k]).
ViewOptNP f (x : y : zs)
OptNP_AtLeastTwo
    OptSkip   (OptSkip OptNP 'False f xs
_)   -> ViewOptNP f xs
forall k (f :: k -> *) (x :: k) (y :: k) (zs :: [k]).
ViewOptNP f (x : y : zs)
OptNP_AtLeastTwo

{-------------------------------------------------------------------------------
  Combining
-------------------------------------------------------------------------------}

zipWith ::
     forall f g h xs.
     (forall a. These1 f g a -> h a)
  -> NonEmptyOptNP f xs
  -> NonEmptyOptNP g xs
  -> NonEmptyOptNP h xs
zipWith :: (forall a. These1 f g a -> h a)
-> NonEmptyOptNP f xs -> NonEmptyOptNP g xs -> NonEmptyOptNP h xs
zipWith = (forall a. These1 f g a -> h a)
-> NonEmptyOptNP f xs -> NonEmptyOptNP g xs -> NonEmptyOptNP h xs
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) (empty1 :: Bool)
       (empty2 :: Bool) (xs :: [*]).
(forall a. These1 f g a -> h a)
-> OptNP empty1 f xs
-> OptNP empty2 g xs
-> OptNP (empty1 && empty2) h xs
polyZipWith

-- | NOT EXPORTED
polyZipWith ::
     forall f g h empty1 empty2 xs.
     (forall a. These1 f g a -> h a)
  -> OptNP empty1             f xs
  -> OptNP empty2             g xs
  -> OptNP (empty1 && empty2) h xs
polyZipWith :: (forall a. These1 f g a -> h a)
-> OptNP empty1 f xs
-> OptNP empty2 g xs
-> OptNP (empty1 && empty2) h xs
polyZipWith forall a. These1 f g a -> h a
f =
    OptNP empty1 f xs
-> OptNP empty2 g xs -> OptNP (empty1 && empty2) h xs
forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool).
OptNP empty1' f xs'
-> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs'
go
  where
    go :: OptNP empty1'              f xs'
       -> OptNP empty2'              g xs'
       -> OptNP (empty1' && empty2') h xs'
    go :: OptNP empty1' f xs'
-> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs'
go OptNP empty1' f xs'
OptNil         OptNP empty2' g xs'
OptNil         = OptNP (empty1' && empty2') h xs'
forall k (f :: k -> *). OptNP 'True f '[]
OptNil
    go (OptCons f x
x OptNP empty f xs
xs) (OptSkip   OptNP empty2' g xs
ys) = h x -> OptNP (empty && empty2') h xs -> OptNP 'False h (x : xs)
forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]).
f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
OptCons (These1 f g x -> h x
forall a. These1 f g a -> h a
f (f x -> These1 f g x
forall (f :: * -> *) (g :: * -> *) a. f a -> These1 f g a
This1  f x
x  )) (OptNP empty f xs
-> OptNP empty2' g xs -> OptNP (empty && empty2') h xs
forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool).
OptNP empty1' f xs'
-> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs'
go OptNP empty f xs
xs OptNP empty2' g xs
OptNP empty2' g xs
ys)
    go (OptSkip   OptNP empty1' f xs
xs) (OptCons g x
y OptNP empty g xs
ys) = h x -> OptNP (empty1' && empty) h xs -> OptNP 'False h (x : xs)
forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]).
f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
OptCons (These1 f g x -> h x
forall a. These1 f g a -> h a
f (g x -> These1 f g x
forall (f :: * -> *) (g :: * -> *) a. g a -> These1 f g a
That1    g x
y)) (OptNP empty1' f xs
-> OptNP empty g xs -> OptNP (empty1' && empty) h xs
forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool).
OptNP empty1' f xs'
-> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs'
go OptNP empty1' f xs
xs OptNP empty g xs
OptNP empty g xs
ys)
    go (OptCons f x
x OptNP empty f xs
xs) (OptCons g x
y OptNP empty g xs
ys) = h x -> OptNP (empty && empty) h xs -> OptNP 'False h (x : xs)
forall a (f :: a -> *) (x :: a) (empty :: Bool) (xs :: [a]).
f x -> OptNP empty f xs -> OptNP 'False f (x : xs)
OptCons (These1 f g x -> h x
forall a. These1 f g a -> h a
f (f x -> g x -> These1 f g x
forall (f :: * -> *) (g :: * -> *) a. f a -> g a -> These1 f g a
These1 f x
x g x
g x
y)) (OptNP empty f xs -> OptNP empty g xs -> OptNP (empty && empty) h xs
forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool).
OptNP empty1' f xs'
-> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs'
go OptNP empty f xs
xs OptNP empty g xs
OptNP empty g xs
ys)
    go (OptSkip   OptNP empty1' f xs
xs) (OptSkip   OptNP empty2' g xs
ys) = OptNP (empty1' && empty2') h xs
-> OptNP (empty1' && empty2') h (x : xs)
forall a (empty :: Bool) (f :: a -> *) (xs :: [a]) (x :: a).
OptNP empty f xs -> OptNP empty f (x : xs)
OptSkip                  (OptNP empty1' f xs
-> OptNP empty2' g xs -> OptNP (empty1' && empty2') h xs
forall (empty1' :: Bool) (xs' :: [*]) (empty2' :: Bool).
OptNP empty1' f xs'
-> OptNP empty2' g xs' -> OptNP (empty1' && empty2') h xs'
go OptNP empty1' f xs
xs OptNP empty2' g xs
OptNP empty2' g xs
ys)

combineWith ::
     SListI xs
  => (forall a. These1 f g a -> h a)
  -> Maybe (NonEmptyOptNP f xs)
  -> Maybe (NonEmptyOptNP g xs)
  -> Maybe (NonEmptyOptNP h xs)
combineWith :: (forall a. These1 f g a -> h a)
-> Maybe (NonEmptyOptNP f xs)
-> Maybe (NonEmptyOptNP g xs)
-> Maybe (NonEmptyOptNP h xs)
combineWith forall a. These1 f g a -> h a
_ Maybe (NonEmptyOptNP f xs)
Nothing   Maybe (NonEmptyOptNP g xs)
Nothing   = Maybe (NonEmptyOptNP h xs)
forall a. Maybe a
Nothing
combineWith forall a. These1 f g a -> h a
f (Just NonEmptyOptNP f xs
xs) Maybe (NonEmptyOptNP g xs)
Nothing   = NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs)
forall a. a -> Maybe a
Just (NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs))
-> NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs)
forall a b. (a -> b) -> a -> b
$ (forall a. These1 f g a -> h a)
-> NonEmptyOptNP f xs
-> OptNP 'True g xs
-> OptNP ('False && 'True) h xs
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) (empty1 :: Bool)
       (empty2 :: Bool) (xs :: [*]).
(forall a. These1 f g a -> h a)
-> OptNP empty1 f xs
-> OptNP empty2 g xs
-> OptNP (empty1 && empty2) h xs
polyZipWith forall a. These1 f g a -> h a
f NonEmptyOptNP f xs
xs    OptNP 'True g xs
forall k (f :: k -> *) (xs :: [k]). SListI xs => OptNP 'True f xs
empty
combineWith forall a. These1 f g a -> h a
f Maybe (NonEmptyOptNP f xs)
Nothing   (Just NonEmptyOptNP g xs
ys) = NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs)
forall a. a -> Maybe a
Just (NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs))
-> NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs)
forall a b. (a -> b) -> a -> b
$ (forall a. These1 f g a -> h a)
-> OptNP 'True f xs
-> NonEmptyOptNP g xs
-> OptNP ('True && 'False) h xs
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) (empty1 :: Bool)
       (empty2 :: Bool) (xs :: [*]).
(forall a. These1 f g a -> h a)
-> OptNP empty1 f xs
-> OptNP empty2 g xs
-> OptNP (empty1 && empty2) h xs
polyZipWith forall a. These1 f g a -> h a
f OptNP 'True f xs
forall k (f :: k -> *) (xs :: [k]). SListI xs => OptNP 'True f xs
empty NonEmptyOptNP g xs
ys
combineWith forall a. These1 f g a -> h a
f (Just NonEmptyOptNP f xs
xs) (Just NonEmptyOptNP g xs
ys) = NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs)
forall a. a -> Maybe a
Just (NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs))
-> NonEmptyOptNP h xs -> Maybe (NonEmptyOptNP h xs)
forall a b. (a -> b) -> a -> b
$ (forall a. These1 f g a -> h a)
-> NonEmptyOptNP f xs
-> NonEmptyOptNP g xs
-> OptNP ('False && 'False) h xs
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) (empty1 :: Bool)
       (empty2 :: Bool) (xs :: [*]).
(forall a. These1 f g a -> h a)
-> OptNP empty1 f xs
-> OptNP empty2 g xs
-> OptNP (empty1 && empty2) h xs
polyZipWith forall a. These1 f g a -> h a
f NonEmptyOptNP f xs
xs    NonEmptyOptNP g xs
ys

-- | Precondition: there is no overlap between the two given lists: if there is
-- a 'Just' at a given position in one, it must be 'Nothing' at the same
-- position in the other.
combine ::
     forall (f :: Type -> Type) xs.
     -- 'These1' is not kind-polymorphic
     (SListI xs, HasCallStack)
  => Maybe (NonEmptyOptNP f xs)
  -> Maybe (NonEmptyOptNP f xs)
  -> Maybe (NonEmptyOptNP f xs)
combine :: Maybe (NonEmptyOptNP f xs)
-> Maybe (NonEmptyOptNP f xs) -> Maybe (NonEmptyOptNP f xs)
combine = (forall a. These1 f f a -> f a)
-> Maybe (NonEmptyOptNP f xs)
-> Maybe (NonEmptyOptNP f xs)
-> Maybe (NonEmptyOptNP f xs)
forall (xs :: [*]) (f :: * -> *) (g :: * -> *) (h :: * -> *).
SListI xs =>
(forall a. These1 f g a -> h a)
-> Maybe (NonEmptyOptNP f xs)
-> Maybe (NonEmptyOptNP g xs)
-> Maybe (NonEmptyOptNP h xs)
combineWith ((forall a. These1 f f a -> f a)
 -> Maybe (NonEmptyOptNP f xs)
 -> Maybe (NonEmptyOptNP f xs)
 -> Maybe (NonEmptyOptNP f xs))
-> (forall a. These1 f f a -> f a)
-> Maybe (NonEmptyOptNP f xs)
-> Maybe (NonEmptyOptNP f xs)
-> Maybe (NonEmptyOptNP f xs)
forall a b. (a -> b) -> a -> b
$ \case
    This1 f a
x   -> f a
x
    That1 f a
y   -> f a
y
    These1 {} -> String -> f a
forall a. HasCallStack => String -> a
error String
"combine: precondition violated"