module Data.Functor.Invariant.Night.Chain (
NightChain
, pattern Swerve, pattern Reject
, runCoNightChain
, runContraNightChain
, chainListF
, chainListF_
, chainDec
, swerve, swerved
, assembleNightChain
, concatNightChain
, NightChain1
, pattern NightChain1
, runCoNightChain1
, runContraNightChain1
, chainNonEmptyF
, chainNonEmptyF_
, chainDec1
, swerve1, swerved1
, assembleNightChain1
, concatNightChain1
) where
import Control.Applicative.ListF
import Control.Natural
import Data.Coerce
import Data.Functor.Alt
import Data.Functor.Contravariant.Conclude
import Data.Functor.Contravariant.Decide
import Data.Functor.Contravariant.Divisible.Free
import Data.Functor.Invariant
import Data.Functor.Invariant.Night
import Data.Functor.Plus
import Data.HBifunctor.Tensor hiding (elim1, elim2, intro1, intro2)
import Data.HFunctor
import Data.HFunctor.Chain
import Data.HFunctor.Chain.Internal
import Data.SOP
import Data.Void
import qualified Control.Monad.Trans.Compose as CT
import qualified Data.Functor.Coyoneda as CY
import qualified Data.List.NonEmpty as NE
runCoNightChain1
:: forall f g. Alt g
=> f ~> g
-> NightChain1 f ~> g
runCoNightChain1 :: (f ~> g) -> NightChain1 f ~> g
runCoNightChain1 f :: f ~> g
f = (f ~> g) -> (Night f g ~> g) -> Chain1 Night f ~> g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(g :: k -> *).
HBifunctor t =>
(f ~> g) -> (t f g ~> g) -> Chain1 t f ~> g
foldChain1 f ~> g
f ((f ~> g) -> (g ~> g) -> Night f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Alt h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNightAlt f ~> g
f forall a. a -> a
g ~> g
id)
(Chain1 Night f x -> g x)
-> (NightChain1 f x -> Chain1 Night f x) -> NightChain1 f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NightChain1 f x -> Chain1 Night f x
forall (f :: * -> *) a. NightChain1 f a -> Chain1 Night f a
unNightChain1
runContraNightChain1
:: forall f g. Decide g
=> f ~> g
-> NightChain1 f ~> g
runContraNightChain1 :: (f ~> g) -> NightChain1 f ~> g
runContraNightChain1 f :: f ~> g
f = (f ~> g) -> (Night f g ~> g) -> Chain1 Night f ~> g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(g :: k -> *).
HBifunctor t =>
(f ~> g) -> (t f g ~> g) -> Chain1 t f ~> g
foldChain1 f ~> g
f ((f ~> g) -> (g ~> g) -> Night f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Decide h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNightDecide f ~> g
f forall a. a -> a
g ~> g
id)
(Chain1 Night f x -> g x)
-> (NightChain1 f x -> Chain1 Night f x) -> NightChain1 f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NightChain1 f x -> Chain1 Night f x
forall (f :: * -> *) a. NightChain1 f a -> Chain1 Night f a
unNightChain1
chainDec :: NightChain f ~> Dec f
chainDec :: NightChain f x -> Dec f x
chainDec = (f ~> Dec f) -> NightChain f ~> Dec f
forall (f :: * -> *) (g :: * -> *).
Conclude g =>
(f ~> g) -> NightChain f ~> g
runContraNightChain f ~> Dec f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
chainDec1 :: NightChain1 f ~> Dec1 f
chainDec1 :: NightChain1 f x -> Dec1 f x
chainDec1 = (f ~> Dec1 f) -> NightChain1 f ~> Dec1 f
forall (f :: * -> *) (g :: * -> *).
Decide g =>
(f ~> g) -> NightChain1 f ~> g
runContraNightChain1 f ~> Dec1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
runCoNightChain
:: forall f g. Plus g
=> f ~> g
-> NightChain f ~> g
runCoNightChain :: (f ~> g) -> NightChain f ~> g
runCoNightChain f :: f ~> g
f = (Not ~> g) -> (Night f g ~> g) -> Chain Night Not f ~> g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (i :: k -> *)
(f :: k -> *) (g :: k -> *).
HBifunctor t =>
(i ~> g) -> (t f g ~> g) -> Chain t i f ~> g
foldChain (g x -> Not x -> g x
forall a b. a -> b -> a
const g x
forall (f :: * -> *) a. Plus f => f a
zero) ((f ~> g) -> (g ~> g) -> Night f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Alt h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNightAlt f ~> g
f forall a. a -> a
g ~> g
id)
(Chain Night Not f x -> g x)
-> (NightChain f x -> Chain Night Not f x) -> NightChain f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NightChain f x -> Chain Night Not f x
forall (f :: * -> *) a. NightChain f a -> Chain Night Not f a
unNightChain
runContraNightChain
:: forall f g. Conclude g
=> f ~> g
-> NightChain f ~> g
runContraNightChain :: (f ~> g) -> NightChain f ~> g
runContraNightChain f :: f ~> g
f = (Not ~> g) -> (Night f g ~> g) -> Chain Night Not f ~> g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (i :: k -> *)
(f :: k -> *) (g :: k -> *).
HBifunctor t =>
(i ~> g) -> (t f g ~> g) -> Chain t i f ~> g
foldChain ((x -> Void) -> g x
forall (f :: * -> *) a. Conclude f => (a -> Void) -> f a
conclude ((x -> Void) -> g x) -> (Not x -> x -> Void) -> Not x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Not x -> x -> Void
forall a. Not a -> a -> Void
refute) ((f ~> g) -> (g ~> g) -> Night f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Decide h =>
(f ~> h) -> (g ~> h) -> Night f g ~> h
runNightDecide f ~> g
f forall a. a -> a
g ~> g
id)
(Chain Night Not f x -> g x)
-> (NightChain f x -> Chain Night Not f x) -> NightChain f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NightChain f x -> Chain Night Not f x
forall (f :: * -> *) a. NightChain f a -> Chain Night Not f a
unNightChain
chainListF :: Functor f => NightChain f ~> ListF f
chainListF :: NightChain f ~> ListF f
chainListF = (f ~> ListF f) -> NightChain f ~> ListF f
forall (f :: * -> *) (g :: * -> *).
Plus g =>
(f ~> g) -> NightChain f ~> g
runCoNightChain f ~> ListF f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
chainListF_ :: NightChain f ~> CT.ComposeT ListF CY.Coyoneda f
chainListF_ :: NightChain f x -> ComposeT ListF Coyoneda f x
chainListF_ = (Not ~> ComposeT ListF Coyoneda f)
-> (Night f (ComposeT ListF Coyoneda f)
~> ComposeT ListF Coyoneda f)
-> Chain Night Not f ~> ComposeT ListF Coyoneda f
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (i :: k -> *)
(f :: k -> *) (g :: k -> *).
HBifunctor t =>
(i ~> g) -> (t f g ~> g) -> Chain t i f ~> g
foldChain (ComposeT ListF Coyoneda f x -> Not x -> ComposeT ListF Coyoneda f x
forall a b. a -> b -> a
const (ListF (Coyoneda f) x -> ComposeT ListF Coyoneda f x
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(m :: * -> *) a.
f (g m) a -> ComposeT f g m a
CT.ComposeT ([Coyoneda f x] -> ListF (Coyoneda f) x
forall k (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF []))) (\case
Night x (CT.ComposeT (ListF xs)) _ f g -> ListF (Coyoneda f) x -> ComposeT ListF Coyoneda f x
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(m :: * -> *) a.
f (g m) a -> ComposeT f g m a
CT.ComposeT (ListF (Coyoneda f) x -> ComposeT ListF Coyoneda f x)
-> ([Coyoneda f x] -> ListF (Coyoneda f) x)
-> [Coyoneda f x]
-> ComposeT ListF Coyoneda f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Coyoneda f x] -> ListF (Coyoneda f) x
forall k (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF ([Coyoneda f x] -> ComposeT ListF Coyoneda f x)
-> [Coyoneda f x] -> ComposeT ListF Coyoneda f x
forall a b. (a -> b) -> a -> b
$
(b -> x) -> f b -> Coyoneda f x
forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda b -> x
f f b
x Coyoneda f x -> [Coyoneda f x] -> [Coyoneda f x]
forall a. a -> [a] -> [a]
: ((Coyoneda f c -> Coyoneda f x) -> [Coyoneda f c] -> [Coyoneda f x]
forall a b. (a -> b) -> [a] -> [b]
map ((Coyoneda f c -> Coyoneda f x)
-> [Coyoneda f c] -> [Coyoneda f x])
-> ((c -> x) -> Coyoneda f c -> Coyoneda f x)
-> (c -> x)
-> [Coyoneda f c]
-> [Coyoneda f x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> x) -> Coyoneda f c -> Coyoneda f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) c -> x
g [Coyoneda f c]
xs
) (Chain Night Not f x -> ComposeT ListF Coyoneda f x)
-> (NightChain f x -> Chain Night Not f x)
-> NightChain f x
-> ComposeT ListF Coyoneda f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NightChain f x -> Chain Night Not f x
forall (f :: * -> *) a. NightChain f a -> Chain Night Not f a
unNightChain
chainNonEmptyF :: Functor f => NightChain1 f ~> NonEmptyF f
chainNonEmptyF :: NightChain1 f ~> NonEmptyF f
chainNonEmptyF = (f ~> NonEmptyF f) -> NightChain1 f ~> NonEmptyF f
forall (f :: * -> *) (g :: * -> *).
Alt g =>
(f ~> g) -> NightChain1 f ~> g
runCoNightChain1 f ~> NonEmptyF f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
chainNonEmptyF_ :: NightChain1 f ~> CT.ComposeT NonEmptyF CY.Coyoneda f
chainNonEmptyF_ :: NightChain1 f x -> ComposeT NonEmptyF Coyoneda f x
chainNonEmptyF_ = (f ~> ComposeT NonEmptyF Coyoneda f)
-> (Night f (ComposeT NonEmptyF Coyoneda f)
~> ComposeT NonEmptyF Coyoneda f)
-> Chain1 Night f ~> ComposeT NonEmptyF Coyoneda f
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(g :: k -> *).
HBifunctor t =>
(f ~> g) -> (t f g ~> g) -> Chain1 t f ~> g
foldChain1 f ~> ComposeT NonEmptyF Coyoneda f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject (\case
Night x (CT.ComposeT (NonEmptyF xs)) _ f g -> NonEmptyF (Coyoneda f) x -> ComposeT NonEmptyF Coyoneda f x
forall (f :: (* -> *) -> * -> *) (g :: (* -> *) -> * -> *)
(m :: * -> *) a.
f (g m) a -> ComposeT f g m a
CT.ComposeT (NonEmptyF (Coyoneda f) x -> ComposeT NonEmptyF Coyoneda f x)
-> (NonEmpty (Coyoneda f x) -> NonEmptyF (Coyoneda f) x)
-> NonEmpty (Coyoneda f x)
-> ComposeT NonEmptyF Coyoneda f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (Coyoneda f x) -> NonEmptyF (Coyoneda f) x
forall k (f :: k -> *) (a :: k). NonEmpty (f a) -> NonEmptyF f a
NonEmptyF (NonEmpty (Coyoneda f x) -> ComposeT NonEmptyF Coyoneda f x)
-> NonEmpty (Coyoneda f x) -> ComposeT NonEmptyF Coyoneda f x
forall a b. (a -> b) -> a -> b
$
(b -> x) -> f b -> Coyoneda f x
forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda b -> x
f f b
x Coyoneda f x -> NonEmpty (Coyoneda f x) -> NonEmpty (Coyoneda f x)
forall a. a -> NonEmpty a -> NonEmpty a
NE.<| ((Coyoneda f c -> Coyoneda f x)
-> NonEmpty (Coyoneda f c) -> NonEmpty (Coyoneda f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Coyoneda f c -> Coyoneda f x)
-> NonEmpty (Coyoneda f c) -> NonEmpty (Coyoneda f x))
-> ((c -> x) -> Coyoneda f c -> Coyoneda f x)
-> (c -> x)
-> NonEmpty (Coyoneda f c)
-> NonEmpty (Coyoneda f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> x) -> Coyoneda f c -> Coyoneda f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) c -> x
g NonEmpty (Coyoneda f c)
xs
) (Chain1 Night f x -> ComposeT NonEmptyF Coyoneda f x)
-> (NightChain1 f x -> Chain1 Night f x)
-> NightChain1 f x
-> ComposeT NonEmptyF Coyoneda f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NightChain1 f x -> Chain1 Night f x
forall (f :: * -> *) a. NightChain1 f a -> Chain1 Night f a
unNightChain1
pattern Swerve :: (a -> Either b c) -> (b -> a) -> (c -> a) -> f b -> NightChain f c -> NightChain f a
pattern $bSwerve :: (a -> Either b c)
-> (b -> a) -> (c -> a) -> f b -> NightChain f c -> NightChain f a
$mSwerve :: forall r a (f :: * -> *).
NightChain f a
-> (forall b c.
(a -> Either b c)
-> (b -> a) -> (c -> a) -> f b -> NightChain f c -> r)
-> (Void# -> r)
-> r
Swerve f g h x xs <- (unSwerve_->MaybeF (Just (Night x xs f g h)))
where
Swerve f :: a -> Either b c
f g :: b -> a
g h :: c -> a
h x :: f b
x xs :: NightChain f c
xs = Chain Night Not f a -> NightChain f a
forall (f :: * -> *) a. Chain Night Not f a -> NightChain f a
NightChain (Chain Night Not f a -> NightChain f a)
-> Chain Night Not f a -> NightChain f a
forall a b. (a -> b) -> a -> b
$ Night f (Chain Night Not f) a -> Chain Night Not f a
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
t f (Chain t i f) a -> Chain t i f a
More (Night f (Chain Night Not f) a -> Chain Night Not f a)
-> Night f (Chain Night Not f) a -> Chain Night Not f a
forall a b. (a -> b) -> a -> b
$ f b
-> Chain Night Not f c
-> (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> Night f (Chain Night Not f) a
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night f b
x (NightChain f c -> Chain Night Not f c
forall (f :: * -> *) a. NightChain f a -> Chain Night Not f a
unNightChain NightChain f c
xs) a -> Either b c
f b -> a
g c -> a
h
unSwerve_ :: NightChain f ~> MaybeF (Night f (NightChain f))
unSwerve_ :: NightChain f x -> MaybeF (Night f (NightChain f)) x
unSwerve_ = \case
NightChain (More (Night x :: f b
x xs :: Chain Night Not f c
xs g :: x -> Either b c
g f :: b -> x
f h :: c -> x
h)) -> Maybe (Night f (NightChain f) x)
-> MaybeF (Night f (NightChain f)) x
forall k (f :: k -> *) (a :: k). Maybe (f a) -> MaybeF f a
MaybeF (Maybe (Night f (NightChain f) x)
-> MaybeF (Night f (NightChain f)) x)
-> (Night f (NightChain f) x -> Maybe (Night f (NightChain f) x))
-> Night f (NightChain f) x
-> MaybeF (Night f (NightChain f)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Night f (NightChain f) x -> Maybe (Night f (NightChain f) x)
forall a. a -> Maybe a
Just (Night f (NightChain f) x -> MaybeF (Night f (NightChain f)) x)
-> Night f (NightChain f) x -> MaybeF (Night f (NightChain f)) x
forall a b. (a -> b) -> a -> b
$ f b
-> NightChain f c
-> (x -> Either b c)
-> (b -> x)
-> (c -> x)
-> Night f (NightChain f) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night f b
x (Chain Night Not f c -> NightChain f c
forall (f :: * -> *) a. Chain Night Not f a -> NightChain f a
NightChain Chain Night Not f c
xs) x -> Either b c
g b -> x
f c -> x
h
NightChain (Done _ ) -> Maybe (Night f (NightChain f) x)
-> MaybeF (Night f (NightChain f)) x
forall k (f :: k -> *) (a :: k). Maybe (f a) -> MaybeF f a
MaybeF Maybe (Night f (NightChain f) x)
forall a. Maybe a
Nothing
pattern Reject :: (a -> Void) -> NightChain f a
pattern $bReject :: (a -> Void) -> NightChain f a
$mReject :: forall r a (f :: * -> *).
NightChain f a -> ((a -> Void) -> r) -> (Void# -> r) -> r
Reject x = NightChain (Done (Not x))
{-# COMPLETE Swerve, Reject #-}
pattern NightChain1 :: Invariant f => (a -> Either b c) -> (b -> a) -> (c -> a) -> f b -> NightChain f c -> NightChain1 f a
pattern $bNightChain1 :: (a -> Either b c)
-> (b -> a) -> (c -> a) -> f b -> NightChain f c -> NightChain1 f a
$mNightChain1 :: forall r (f :: * -> *) a.
Invariant f =>
NightChain1 f a
-> (forall b c.
(a -> Either b c)
-> (b -> a) -> (c -> a) -> f b -> NightChain f c -> r)
-> (Void# -> r)
-> r
NightChain1 f g h x xs <- (coerce splitChain1->Night x xs f g h)
where
NightChain1 f :: a -> Either b c
f g :: b -> a
g h :: c -> a
h x :: f b
x xs :: NightChain f c
xs = Night f (ListBy Night f) a -> NightChain1 f a
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE (Night f (ListBy Night f) a -> NightChain1 f a)
-> Night f (ListBy Night f) a -> NightChain1 f a
forall a b. (a -> b) -> a -> b
$ f b
-> NightChain f c
-> (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> Night f (NightChain f) a
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night f b
x NightChain f c
xs a -> Either b c
f b -> a
g c -> a
h
{-# COMPLETE NightChain1 #-}
swerve
:: (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> NightChain f b
-> NightChain f c
-> NightChain f a
swerve :: (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> NightChain f b
-> NightChain f c
-> NightChain f a
swerve f :: a -> Either b c
f g :: b -> a
g h :: c -> a
h x :: NightChain f b
x y :: NightChain f c
y = (Night (Chain Night Not f) (Chain Night Not f) a
-> Chain Night Not f a)
-> Night (NightChain f) (NightChain f) a -> NightChain f a
forall a b. Coercible a b => a -> b
coerce Night (Chain Night Not f) (Chain Night Not f) a
-> Chain Night Not f a
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t (Chain t i f) (Chain t i f) ~> Chain t i f
appendChain (NightChain f b
-> NightChain f c
-> (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> Night (NightChain f) (NightChain f) a
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night NightChain f b
x NightChain f c
y a -> Either b c
f b -> a
g c -> a
h)
swerved
:: NightChain f a
-> NightChain f b
-> NightChain f (Either a b)
swerved :: NightChain f a -> NightChain f b -> NightChain f (Either a b)
swerved = (Either a b -> Either a b)
-> (a -> Either a b)
-> (b -> Either a b)
-> NightChain f a
-> NightChain f b
-> NightChain f (Either a b)
forall a b c (f :: * -> *).
(a -> Either b c)
-> (b -> a)
-> (c -> a)
-> NightChain f b
-> NightChain f c
-> NightChain f a
swerve Either a b -> Either a b
forall a. a -> a
id a -> Either a b
forall a b. a -> Either a b
Left b -> Either a b
forall a b. b -> Either a b
Right
swerve1
:: Invariant f
=> (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> NightChain1 f b
-> NightChain1 f c
-> NightChain1 f a
swerve1 :: (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> NightChain1 f b
-> NightChain1 f c
-> NightChain1 f a
swerve1 f :: a -> Either b c
f g :: b -> a
g h :: c -> a
h x :: NightChain1 f b
x y :: NightChain1 f c
y = (Night (Chain1 Night f) (Chain1 Night f) a -> Chain1 Night f a)
-> Night (NightChain1 f) (NightChain1 f) a -> NightChain1 f a
forall a b. Coercible a b => a -> b
coerce Night (Chain1 Night f) (Chain1 Night f) a -> Chain1 Night f a
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
(Associative t, FunctorBy t f) =>
t (Chain1 t f) (Chain1 t f) ~> Chain1 t f
appendChain1 (NightChain1 f b
-> NightChain1 f c
-> (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> Night (NightChain1 f) (NightChain1 f) a
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night NightChain1 f b
x NightChain1 f c
y a -> Either b c
f b -> a
g c -> a
h)
swerved1
:: Invariant f
=> NightChain1 f a
-> NightChain1 f b
-> NightChain1 f (Either a b)
swerved1 :: NightChain1 f a -> NightChain1 f b -> NightChain1 f (Either a b)
swerved1 = (Either a b -> Either a b)
-> (a -> Either a b)
-> (b -> Either a b)
-> NightChain1 f a
-> NightChain1 f b
-> NightChain1 f (Either a b)
forall (f :: * -> *) a b c.
Invariant f =>
(a -> Either b c)
-> (b -> a)
-> (c -> a)
-> NightChain1 f b
-> NightChain1 f c
-> NightChain1 f a
swerve1 Either a b -> Either a b
forall a. a -> a
id a -> Either a b
forall a b. a -> Either a b
Left b -> Either a b
forall a b. b -> Either a b
Right
assembleNightChain
:: NP f as
-> NightChain f (NS I as)
assembleNightChain :: NP f as -> NightChain f (NS I as)
assembleNightChain = \case
Nil -> Chain Night Not f (NS I as) -> NightChain f (NS I as)
forall (f :: * -> *) a. Chain Night Not f a -> NightChain f a
NightChain (Chain Night Not f (NS I as) -> NightChain f (NS I as))
-> Chain Night Not f (NS I as) -> NightChain f (NS I as)
forall a b. (a -> b) -> a -> b
$ Not (NS I as) -> Chain Night Not f (NS I as)
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
i a -> Chain t i f a
Done (Not (NS I as) -> Chain Night Not f (NS I as))
-> Not (NS I as) -> Chain Night Not f (NS I as)
forall a b. (a -> b) -> a -> b
$ (NS I as -> Void) -> Not (NS I as)
forall a. (a -> Void) -> Not a
Not (\case {})
x :: f x
x :* xs :: NP f xs
xs -> Chain Night Not f (NS I (x : xs)) -> NightChain f (NS I as)
forall (f :: * -> *) a. Chain Night Not f a -> NightChain f a
NightChain (Chain Night Not f (NS I (x : xs)) -> NightChain f (NS I as))
-> Chain Night Not f (NS I (x : xs)) -> NightChain f (NS I as)
forall a b. (a -> b) -> a -> b
$ Night f (Chain Night Not f) (NS I (x : xs))
-> Chain Night Not f (NS I (x : xs))
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
t f (Chain t i f) a -> Chain t i f a
More (Night f (Chain Night Not f) (NS I (x : xs))
-> Chain Night Not f (NS I (x : xs)))
-> Night f (Chain Night Not f) (NS I (x : xs))
-> Chain Night Not f (NS I (x : xs))
forall a b. (a -> b) -> a -> b
$ f x
-> Chain Night Not f (NS I xs)
-> (NS I (x : xs) -> Either x (NS I xs))
-> (x -> NS I (x : xs))
-> (NS I xs -> NS I (x : xs))
-> Night f (Chain Night Not f) (NS I (x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night
f x
x
(NightChain f (NS I xs) -> Chain Night Not f (NS I xs)
forall (f :: * -> *) a. NightChain f a -> Chain Night Not f a
unNightChain (NightChain f (NS I xs) -> Chain Night Not f (NS I xs))
-> NightChain f (NS I xs) -> Chain Night Not f (NS I xs)
forall a b. (a -> b) -> a -> b
$ NP f xs -> NightChain f (NS I xs)
forall (f :: * -> *) (as :: [*]). NP f as -> NightChain f (NS I as)
assembleNightChain NP f xs
xs)
NS I (x : xs) -> Either x (NS I xs)
forall a (as :: [*]). NS I (a : as) -> Either a (NS I as)
unconsNSI
(I x -> NS I (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I (x : xs)) -> (x -> I x) -> x -> NS I (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I)
NS I xs -> NS I (x : xs)
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S
concatNightChain
:: NP (NightChain f) as
-> NightChain f (NS I as)
concatNightChain :: NP (NightChain f) as -> NightChain f (NS I as)
concatNightChain = \case
Nil -> Chain Night Not f (NS I as) -> NightChain f (NS I as)
forall (f :: * -> *) a. Chain Night Not f a -> NightChain f a
NightChain (Chain Night Not f (NS I as) -> NightChain f (NS I as))
-> Chain Night Not f (NS I as) -> NightChain f (NS I as)
forall a b. (a -> b) -> a -> b
$ Not (NS I as) -> Chain Night Not f (NS I as)
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
i a -> Chain t i f a
Done (Not (NS I as) -> Chain Night Not f (NS I as))
-> Not (NS I as) -> Chain Night Not f (NS I as)
forall a b. (a -> b) -> a -> b
$ (NS I as -> Void) -> Not (NS I as)
forall a. (a -> Void) -> Not a
Not (\case {})
x :: NightChain f x
x :* xs :: NP (NightChain f) xs
xs -> (Night (Chain Night Not f) (Chain Night Not f) (NS I (x : xs))
-> Chain Night Not f (NS I (x : xs)))
-> Night (NightChain f) (Chain Night Not f) (NS I (x : xs))
-> NightChain f (NS I as)
forall a b. Coercible a b => a -> b
coerce Night (Chain Night Not f) (Chain Night Not f) (NS I (x : xs))
-> Chain Night Not f (NS I (x : xs))
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t (Chain t i f) (Chain t i f) ~> Chain t i f
appendChain (Night (NightChain f) (Chain Night Not f) (NS I (x : xs))
-> NightChain f (NS I as))
-> Night (NightChain f) (Chain Night Not f) (NS I (x : xs))
-> NightChain f (NS I as)
forall a b. (a -> b) -> a -> b
$ NightChain f x
-> Chain Night Not f (NS I xs)
-> (NS I (x : xs) -> Either x (NS I xs))
-> (x -> NS I (x : xs))
-> (NS I xs -> NS I (x : xs))
-> Night (NightChain f) (Chain Night Not f) (NS I (x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night
NightChain f x
x
(NightChain f (NS I xs) -> Chain Night Not f (NS I xs)
forall (f :: * -> *) a. NightChain f a -> Chain Night Not f a
unNightChain (NightChain f (NS I xs) -> Chain Night Not f (NS I xs))
-> NightChain f (NS I xs) -> Chain Night Not f (NS I xs)
forall a b. (a -> b) -> a -> b
$ NP (NightChain f) xs -> NightChain f (NS I xs)
forall (f :: * -> *) (as :: [*]).
NP (NightChain f) as -> NightChain f (NS I as)
concatNightChain NP (NightChain f) xs
xs)
NS I (x : xs) -> Either x (NS I xs)
forall a (as :: [*]). NS I (a : as) -> Either a (NS I as)
unconsNSI
(I x -> NS I (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I (x : xs)) -> (x -> I x) -> x -> NS I (x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I)
NS I xs -> NS I (x : xs)
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S
assembleNightChain1
:: Invariant f
=> NP f (a ': as)
-> NightChain1 f (NS I (a ': as))
assembleNightChain1 :: NP f (a : as) -> NightChain1 f (NS I (a : as))
assembleNightChain1 = \case
x :: f x
x :* xs :: NP f xs
xs -> Chain1 Night f (NS I (a : as)) -> NightChain1 f (NS I (a : as))
forall (f :: * -> *) a. Chain1 Night f a -> NightChain1 f a
NightChain1_ (Chain1 Night f (NS I (a : as)) -> NightChain1 f (NS I (a : as)))
-> Chain1 Night f (NS I (a : as)) -> NightChain1 f (NS I (a : as))
forall a b. (a -> b) -> a -> b
$ case NP f xs
xs of
Nil -> f (NS I '[x]) -> Chain1 Night f (NS I (a : as))
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
f a -> Chain1 t f a
Done1 (f (NS I '[x]) -> Chain1 Night f (NS I (a : as)))
-> f (NS I '[x]) -> Chain1 Night f (NS I (a : as))
forall a b. (a -> b) -> a -> b
$ (x -> NS I '[x]) -> (NS I '[x] -> x) -> f x -> f (NS I '[x])
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (I x -> NS I '[x]
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I '[x]) -> (x -> I x) -> x -> NS I '[x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I) (I x -> x
forall a. I a -> a
unI (I x -> x) -> (NS I '[x] -> I x) -> NS I '[x] -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS I '[x] -> I x
forall k (f :: k -> *) (x :: k). NS f '[x] -> f x
unZ) f x
x
_ :* _ -> Night f (Chain1 Night f) (NS I (x : x : xs))
-> Chain1 Night f (NS I (a : as))
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 (Night f (Chain1 Night f) (NS I (x : x : xs))
-> Chain1 Night f (NS I (a : as)))
-> Night f (Chain1 Night f) (NS I (x : x : xs))
-> Chain1 Night f (NS I (a : as))
forall a b. (a -> b) -> a -> b
$ f x
-> Chain1 Night f (NS I (x : xs))
-> (NS I (x : x : xs) -> Either x (NS I (x : xs)))
-> (x -> NS I (x : x : xs))
-> (NS I (x : xs) -> NS I (x : x : xs))
-> Night f (Chain1 Night f) (NS I (x : x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night
f x
x
(NightChain1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs))
forall (f :: * -> *) a. NightChain1 f a -> Chain1 Night f a
unNightChain1 (NightChain1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs)))
-> NightChain1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs))
forall a b. (a -> b) -> a -> b
$ NP f (x : xs) -> NightChain1 f (NS I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP f (a : as) -> NightChain1 f (NS I (a : as))
assembleNightChain1 NP f xs
NP f (x : xs)
xs)
NS I (x : x : xs) -> Either x (NS I (x : xs))
forall a (as :: [*]). NS I (a : as) -> Either a (NS I as)
unconsNSI
(I x -> NS I (x : x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I (x : x : xs)) -> (x -> I x) -> x -> NS I (x : x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I)
NS I (x : xs) -> NS I (x : x : xs)
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S
concatNightChain1
:: Invariant f
=> NP (NightChain1 f) (a ': as)
-> NightChain1 f (NS I (a ': as))
concatNightChain1 :: NP (NightChain1 f) (a : as) -> NightChain1 f (NS I (a : as))
concatNightChain1 = \case
x :: NightChain1 f x
x :* xs :: NP (NightChain1 f) xs
xs -> case NP (NightChain1 f) xs
xs of
Nil -> (x -> NS I '[x])
-> (NS I '[x] -> x) -> NightChain1 f x -> NightChain1 f (NS I '[x])
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (I x -> NS I '[x]
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I '[x]) -> (x -> I x) -> x -> NS I '[x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I) (I x -> x
forall a. I a -> a
unI (I x -> x) -> (NS I '[x] -> I x) -> NS I '[x] -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS I '[x] -> I x
forall k (f :: k -> *) (x :: k). NS f '[x] -> f x
unZ) NightChain1 f x
x
_ :* _ -> (Night (Chain1 Night f) (Chain1 Night f) (NS I (a : x : xs))
-> Chain1 Night f (NS I (a : x : xs)))
-> Night (NightChain1 f) (Chain1 Night f) (NS I (x : x : xs))
-> NightChain1 f (NS I (a : as))
forall a b. Coercible a b => a -> b
coerce Night (Chain1 Night f) (Chain1 Night f) (NS I (a : x : xs))
-> Chain1 Night f (NS I (a : x : xs))
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
(Associative t, FunctorBy t f) =>
t (Chain1 t f) (Chain1 t f) ~> Chain1 t f
appendChain1 (Night (NightChain1 f) (Chain1 Night f) (NS I (x : x : xs))
-> NightChain1 f (NS I (a : as)))
-> Night (NightChain1 f) (Chain1 Night f) (NS I (x : x : xs))
-> NightChain1 f (NS I (a : as))
forall a b. (a -> b) -> a -> b
$ NightChain1 f x
-> Chain1 Night f (NS I (x : xs))
-> (NS I (x : x : xs) -> Either x (NS I (x : xs)))
-> (x -> NS I (x : x : xs))
-> (NS I (x : xs) -> NS I (x : x : xs))
-> Night (NightChain1 f) (Chain1 Night f) (NS I (x : x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (a -> Either b c) -> (b -> a) -> (c -> a) -> Night f g a
Night
NightChain1 f x
x
(NightChain1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs))
forall (f :: * -> *) a. NightChain1 f a -> Chain1 Night f a
unNightChain1 (NightChain1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs)))
-> NightChain1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs))
forall a b. (a -> b) -> a -> b
$ NP (NightChain1 f) (x : xs) -> NightChain1 f (NS I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP (NightChain1 f) (a : as) -> NightChain1 f (NS I (a : as))
concatNightChain1 NP (NightChain1 f) xs
NP (NightChain1 f) (x : xs)
xs)
NS I (x : x : xs) -> Either x (NS I (x : xs))
forall a (as :: [*]). NS I (a : as) -> Either a (NS I as)
unconsNSI
(I x -> NS I (x : x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I x -> NS I (x : x : xs)) -> (x -> I x) -> x -> NS I (x : x : xs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I)
NS I (x : xs) -> NS I (x : x : xs)
forall k (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S
unconsNSI :: NS I (a ': as) -> Either a (NS I as)
unconsNSI :: NS I (a : as) -> Either a (NS I as)
unconsNSI = \case
Z (I x :: x
x) -> x -> Either x (NS I as)
forall a b. a -> Either a b
Left x
x
S xs :: NS I xs
xs -> NS I xs -> Either a (NS I xs)
forall a b. b -> Either a b
Right NS I xs
xs