module Data.Functor.Invariant.DecAlt (
DecAlt(.., Swerve, Reject)
, runCoDecAlt
, runContraDecAlt
, decAltListF
, decAltListF_
, decAltDec
, foldDecAlt
, swerve, swerved
, assembleDecAlt
, concatDecAlt
, DecAlt1(.., DecAlt1)
, runCoDecAlt1
, runContraDecAlt1
, decAltNonEmptyF
, decAltNonEmptyF_
, decAltDec1
, foldDecAlt1
, swerve1, swerved1
, assembleDecAlt1
, concatDecAlt1
) 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
runCoDecAlt1
:: forall f g. Alt g
=> f ~> g
-> DecAlt1 f ~> g
runCoDecAlt1 :: (f ~> g) -> DecAlt1 f ~> g
runCoDecAlt1 f :: f ~> g
f = (f ~> g) -> (Night f g ~> g) -> DecAlt1 f ~> g
forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Night f g ~> g) -> DecAlt1 f ~> g
foldDecAlt1 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)
runContraDecAlt1
:: forall f g. Decide g
=> f ~> g
-> DecAlt1 f ~> g
runContraDecAlt1 :: (f ~> g) -> DecAlt1 f ~> g
runContraDecAlt1 f :: f ~> g
f = (f ~> g) -> (Night f g ~> g) -> DecAlt1 f ~> g
forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Night f g ~> g) -> DecAlt1 f ~> g
foldDecAlt1 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)
decAltDec :: DecAlt f ~> Dec f
decAltDec :: DecAlt f x -> Dec f x
decAltDec = (f ~> Dec f) -> DecAlt f ~> Dec f
forall (f :: * -> *) (g :: * -> *).
Conclude g =>
(f ~> g) -> DecAlt f ~> g
runContraDecAlt f ~> Dec f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
decAltDec1 :: DecAlt1 f ~> Dec1 f
decAltDec1 :: DecAlt1 f x -> Dec1 f x
decAltDec1 = (f ~> Dec1 f) -> DecAlt1 f ~> Dec1 f
forall (f :: * -> *) (g :: * -> *).
Decide g =>
(f ~> g) -> DecAlt1 f ~> g
runContraDecAlt1 f ~> Dec1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
runCoDecAlt
:: forall f g. Plus g
=> f ~> g
-> DecAlt f ~> g
runCoDecAlt :: (f ~> g) -> DecAlt f ~> g
runCoDecAlt f :: f ~> g
f = (forall x. (x -> Void) -> g x) -> (Night f g ~> g) -> DecAlt f ~> g
forall (g :: * -> *) (f :: * -> *).
(forall x. (x -> Void) -> g x) -> (Night f g ~> g) -> DecAlt f ~> g
foldDecAlt (g x -> (x -> Void) -> 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)
runContraDecAlt
:: forall f g. Conclude g
=> f ~> g
-> DecAlt f ~> g
runContraDecAlt :: (f ~> g) -> DecAlt f ~> g
runContraDecAlt f :: f ~> g
f = (forall x. (x -> Void) -> g x) -> (Night f g ~> g) -> DecAlt f ~> g
forall (g :: * -> *) (f :: * -> *).
(forall x. (x -> Void) -> g x) -> (Night f g ~> g) -> DecAlt f ~> g
foldDecAlt forall x. (x -> Void) -> g x
forall (f :: * -> *) a. Conclude f => (a -> Void) -> f a
conclude ((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)
decAltListF :: Functor f => DecAlt f ~> ListF f
decAltListF :: DecAlt f ~> ListF f
decAltListF = (f ~> ListF f) -> DecAlt f ~> ListF f
forall (f :: * -> *) (g :: * -> *).
Plus g =>
(f ~> g) -> DecAlt f ~> g
runCoDecAlt f ~> ListF f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
decAltListF_ :: DecAlt f ~> CT.ComposeT ListF CY.Coyoneda f
decAltListF_ :: DecAlt f x -> ComposeT ListF Coyoneda f x
decAltListF_ = (forall x. (x -> Void) -> ComposeT ListF Coyoneda f x)
-> (Night f (ComposeT ListF Coyoneda f)
~> ComposeT ListF Coyoneda f)
-> DecAlt f ~> ComposeT ListF Coyoneda f
forall (g :: * -> *) (f :: * -> *).
(forall x. (x -> Void) -> g x) -> (Night f g ~> g) -> DecAlt f ~> g
foldDecAlt (ComposeT ListF Coyoneda f x
-> (x -> Void) -> 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 []))) ((Night f (ComposeT ListF Coyoneda f) ~> ComposeT ListF Coyoneda f)
-> DecAlt f x -> ComposeT ListF Coyoneda f x)
-> (Night f (ComposeT ListF Coyoneda f)
~> ComposeT ListF Coyoneda f)
-> DecAlt f x
-> ComposeT ListF Coyoneda f x
forall a b. (a -> b) -> a -> b
$ \case
Night x :: f b
x (CT.ComposeT (ListF xs)) _ f :: b -> x
f g :: c -> x
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
decAltNonEmptyF :: Functor f => DecAlt1 f ~> NonEmptyF f
decAltNonEmptyF :: DecAlt1 f ~> NonEmptyF f
decAltNonEmptyF = (f ~> NonEmptyF f) -> DecAlt1 f ~> NonEmptyF f
forall (f :: * -> *) (g :: * -> *).
Alt g =>
(f ~> g) -> DecAlt1 f ~> g
runCoDecAlt1 f ~> NonEmptyF f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
decAltNonEmptyF_ :: DecAlt1 f ~> CT.ComposeT NonEmptyF CY.Coyoneda f
decAltNonEmptyF_ :: DecAlt1 f x -> ComposeT NonEmptyF Coyoneda f x
decAltNonEmptyF_ = (f ~> ComposeT NonEmptyF Coyoneda f)
-> (Night f (ComposeT NonEmptyF Coyoneda f)
~> ComposeT NonEmptyF Coyoneda f)
-> DecAlt1 f ~> ComposeT NonEmptyF Coyoneda f
forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Night f g ~> g) -> DecAlt1 f ~> g
foldDecAlt1 f ~> ComposeT NonEmptyF Coyoneda f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject ((Night f (ComposeT NonEmptyF Coyoneda f)
~> ComposeT NonEmptyF Coyoneda f)
-> DecAlt1 f x -> ComposeT NonEmptyF Coyoneda f x)
-> (Night f (ComposeT NonEmptyF Coyoneda f)
~> ComposeT NonEmptyF Coyoneda f)
-> DecAlt1 f x
-> ComposeT NonEmptyF Coyoneda f x
forall a b. (a -> b) -> a -> b
$ \case
Night x :: f b
x (CT.ComposeT (NonEmptyF xs)) _ f :: b -> x
f g :: c -> x
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
foldDecAlt
:: (forall x. (x -> Void) -> g x)
-> (Night f g ~> g)
-> DecAlt f ~> g
foldDecAlt :: (forall x. (x -> Void) -> g x) -> (Night f g ~> g) -> DecAlt f ~> g
foldDecAlt f :: forall x. (x -> Void) -> g x
f g :: Night f g ~> g
g = (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 x. (x -> Void) -> g x
f ((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) Night f g ~> g
g (Chain Night Not f x -> g x)
-> (DecAlt f x -> Chain Night Not f x) -> DecAlt f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DecAlt f x -> Chain Night Not f x
forall (f :: * -> *) a. DecAlt f a -> Chain Night Not f a
unDecAlt
foldDecAlt1
:: (f ~> g)
-> (Night f g ~> g)
-> DecAlt1 f ~> g
foldDecAlt1 :: (f ~> g) -> (Night f g ~> g) -> DecAlt1 f ~> g
foldDecAlt1 f :: f ~> g
f g :: Night f g ~> g
g = (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 Night f g ~> g
g (Chain1 Night f x -> g x)
-> (DecAlt1 f x -> Chain1 Night f x) -> DecAlt1 f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DecAlt1 f x -> Chain1 Night f x
forall (f :: * -> *) a. DecAlt1 f a -> Chain1 Night f a
unDecAlt1
pattern Swerve :: (a -> Either b c) -> (b -> a) -> (c -> a) -> f b -> DecAlt f c -> DecAlt f a
pattern $bSwerve :: (a -> Either b c)
-> (b -> a) -> (c -> a) -> f b -> DecAlt f c -> DecAlt f a
$mSwerve :: forall r a (f :: * -> *).
DecAlt f a
-> (forall b c.
(a -> Either b c)
-> (b -> a) -> (c -> a) -> f b -> DecAlt 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 :: DecAlt f c
xs = Chain Night Not f a -> DecAlt f a
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt (Chain Night Not f a -> DecAlt f a)
-> Chain Night Not f a -> DecAlt 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 (DecAlt f c -> Chain Night Not f c
forall (f :: * -> *) a. DecAlt f a -> Chain Night Not f a
unDecAlt DecAlt f c
xs) a -> Either b c
f b -> a
g c -> a
h
unSwerve_ :: DecAlt f ~> MaybeF (Night f (DecAlt f))
unSwerve_ :: DecAlt f x -> MaybeF (Night f (DecAlt f)) x
unSwerve_ = \case
DecAlt (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 (DecAlt f) x) -> MaybeF (Night f (DecAlt f)) x
forall k (f :: k -> *) (a :: k). Maybe (f a) -> MaybeF f a
MaybeF (Maybe (Night f (DecAlt f) x) -> MaybeF (Night f (DecAlt f)) x)
-> (Night f (DecAlt f) x -> Maybe (Night f (DecAlt f) x))
-> Night f (DecAlt f) x
-> MaybeF (Night f (DecAlt f)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Night f (DecAlt f) x -> Maybe (Night f (DecAlt f) x)
forall a. a -> Maybe a
Just (Night f (DecAlt f) x -> MaybeF (Night f (DecAlt f)) x)
-> Night f (DecAlt f) x -> MaybeF (Night f (DecAlt f)) x
forall a b. (a -> b) -> a -> b
$ f b
-> DecAlt f c
-> (x -> Either b c)
-> (b -> x)
-> (c -> x)
-> Night f (DecAlt 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 -> DecAlt f c
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt Chain Night Not f c
xs) x -> Either b c
g b -> x
f c -> x
h
DecAlt (Done _ ) -> Maybe (Night f (DecAlt f) x) -> MaybeF (Night f (DecAlt f)) x
forall k (f :: k -> *) (a :: k). Maybe (f a) -> MaybeF f a
MaybeF Maybe (Night f (DecAlt f) x)
forall a. Maybe a
Nothing
pattern Reject :: (a -> Void) -> DecAlt f a
pattern $bReject :: (a -> Void) -> DecAlt f a
$mReject :: forall r a (f :: * -> *).
DecAlt f a -> ((a -> Void) -> r) -> (Void# -> r) -> r
Reject x = DecAlt (Done (Not x))
{-# COMPLETE Swerve, Reject #-}
pattern DecAlt1 :: Invariant f => (a -> Either b c) -> (b -> a) -> (c -> a) -> f b -> DecAlt f c -> DecAlt1 f a
pattern $bDecAlt1 :: (a -> Either b c)
-> (b -> a) -> (c -> a) -> f b -> DecAlt f c -> DecAlt1 f a
$mDecAlt1 :: forall r (f :: * -> *) a.
Invariant f =>
DecAlt1 f a
-> (forall b c.
(a -> Either b c)
-> (b -> a) -> (c -> a) -> f b -> DecAlt f c -> r)
-> (Void# -> r)
-> r
DecAlt1 f g h x xs <- (coerce splitChain1->Night x xs f g h)
where
DecAlt1 f :: a -> Either b c
f g :: b -> a
g h :: c -> a
h x :: f b
x xs :: DecAlt f c
xs = Night f (ListBy Night f) a -> DecAlt1 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 -> DecAlt1 f a)
-> Night f (ListBy Night f) a -> DecAlt1 f a
forall a b. (a -> b) -> a -> b
$ f b
-> DecAlt f c
-> (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> Night f (DecAlt 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 DecAlt f c
xs a -> Either b c
f b -> a
g c -> a
h
{-# COMPLETE DecAlt1 #-}
swerve
:: (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> DecAlt f b
-> DecAlt f c
-> DecAlt f a
swerve :: (a -> Either b c)
-> (b -> a) -> (c -> a) -> DecAlt f b -> DecAlt f c -> DecAlt f a
swerve f :: a -> Either b c
f g :: b -> a
g h :: c -> a
h x :: DecAlt f b
x y :: DecAlt f c
y = (Night (Chain Night Not f) (Chain Night Not f) a
-> Chain Night Not f a)
-> Night (DecAlt f) (DecAlt f) a -> DecAlt 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 (DecAlt f b
-> DecAlt f c
-> (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> Night (DecAlt f) (DecAlt 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 DecAlt f b
x DecAlt f c
y a -> Either b c
f b -> a
g c -> a
h)
swerved
:: DecAlt f a
-> DecAlt f b
-> DecAlt f (Either a b)
swerved :: DecAlt f a -> DecAlt f b -> DecAlt f (Either a b)
swerved = (Either a b -> Either a b)
-> (a -> Either a b)
-> (b -> Either a b)
-> DecAlt f a
-> DecAlt f b
-> DecAlt f (Either a b)
forall a b c (f :: * -> *).
(a -> Either b c)
-> (b -> a) -> (c -> a) -> DecAlt f b -> DecAlt f c -> DecAlt 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)
-> DecAlt1 f b
-> DecAlt1 f c
-> DecAlt1 f a
swerve1 :: (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> DecAlt1 f b
-> DecAlt1 f c
-> DecAlt1 f a
swerve1 f :: a -> Either b c
f g :: b -> a
g h :: c -> a
h x :: DecAlt1 f b
x y :: DecAlt1 f c
y = (Night (Chain1 Night f) (Chain1 Night f) a -> Chain1 Night f a)
-> Night (DecAlt1 f) (DecAlt1 f) a -> DecAlt1 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 (DecAlt1 f b
-> DecAlt1 f c
-> (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> Night (DecAlt1 f) (DecAlt1 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 DecAlt1 f b
x DecAlt1 f c
y a -> Either b c
f b -> a
g c -> a
h)
swerved1
:: Invariant f
=> DecAlt1 f a
-> DecAlt1 f b
-> DecAlt1 f (Either a b)
swerved1 :: DecAlt1 f a -> DecAlt1 f b -> DecAlt1 f (Either a b)
swerved1 = (Either a b -> Either a b)
-> (a -> Either a b)
-> (b -> Either a b)
-> DecAlt1 f a
-> DecAlt1 f b
-> DecAlt1 f (Either a b)
forall (f :: * -> *) a b c.
Invariant f =>
(a -> Either b c)
-> (b -> a)
-> (c -> a)
-> DecAlt1 f b
-> DecAlt1 f c
-> DecAlt1 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
assembleDecAlt
:: NP f as
-> DecAlt f (NS I as)
assembleDecAlt :: NP f as -> DecAlt f (NS I as)
assembleDecAlt = \case
Nil -> Chain Night Not f (NS I as) -> DecAlt f (NS I as)
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt (Chain Night Not f (NS I as) -> DecAlt f (NS I as))
-> Chain Night Not f (NS I as) -> DecAlt 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)) -> DecAlt f (NS I as)
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt (Chain Night Not f (NS I (x : xs)) -> DecAlt f (NS I as))
-> Chain Night Not f (NS I (x : xs)) -> DecAlt 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
(DecAlt f (NS I xs) -> Chain Night Not f (NS I xs)
forall (f :: * -> *) a. DecAlt f a -> Chain Night Not f a
unDecAlt (DecAlt f (NS I xs) -> Chain Night Not f (NS I xs))
-> DecAlt f (NS I xs) -> Chain Night Not f (NS I xs)
forall a b. (a -> b) -> a -> b
$ NP f xs -> DecAlt f (NS I xs)
forall (f :: * -> *) (as :: [*]). NP f as -> DecAlt f (NS I as)
assembleDecAlt 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
concatDecAlt
:: NP (DecAlt f) as
-> DecAlt f (NS I as)
concatDecAlt :: NP (DecAlt f) as -> DecAlt f (NS I as)
concatDecAlt = \case
Nil -> Chain Night Not f (NS I as) -> DecAlt f (NS I as)
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt (Chain Night Not f (NS I as) -> DecAlt f (NS I as))
-> Chain Night Not f (NS I as) -> DecAlt 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 :: DecAlt f x
x :* xs :: NP (DecAlt 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 (DecAlt f) (Chain Night Not f) (NS I (x : xs))
-> DecAlt 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 (DecAlt f) (Chain Night Not f) (NS I (x : xs))
-> DecAlt f (NS I as))
-> Night (DecAlt f) (Chain Night Not f) (NS I (x : xs))
-> DecAlt f (NS I as)
forall a b. (a -> b) -> a -> b
$ DecAlt 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 (DecAlt 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
DecAlt f x
x
(DecAlt f (NS I xs) -> Chain Night Not f (NS I xs)
forall (f :: * -> *) a. DecAlt f a -> Chain Night Not f a
unDecAlt (DecAlt f (NS I xs) -> Chain Night Not f (NS I xs))
-> DecAlt f (NS I xs) -> Chain Night Not f (NS I xs)
forall a b. (a -> b) -> a -> b
$ NP (DecAlt f) xs -> DecAlt f (NS I xs)
forall (f :: * -> *) (as :: [*]).
NP (DecAlt f) as -> DecAlt f (NS I as)
concatDecAlt NP (DecAlt 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
assembleDecAlt1
:: Invariant f
=> NP f (a ': as)
-> DecAlt1 f (NS I (a ': as))
assembleDecAlt1 :: NP f (a : as) -> DecAlt1 f (NS I (a : as))
assembleDecAlt1 = \case
x :: f x
x :* xs :: NP f xs
xs -> Chain1 Night f (NS I (a : as)) -> DecAlt1 f (NS I (a : as))
forall (f :: * -> *) a. Chain1 Night f a -> DecAlt1 f a
DecAlt1_ (Chain1 Night f (NS I (a : as)) -> DecAlt1 f (NS I (a : as)))
-> Chain1 Night f (NS I (a : as)) -> DecAlt1 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
(DecAlt1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs))
forall (f :: * -> *) a. DecAlt1 f a -> Chain1 Night f a
unDecAlt1 (DecAlt1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs)))
-> DecAlt1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs))
forall a b. (a -> b) -> a -> b
$ NP f (x : xs) -> DecAlt1 f (NS I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP f (a : as) -> DecAlt1 f (NS I (a : as))
assembleDecAlt1 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
concatDecAlt1
:: Invariant f
=> NP (DecAlt1 f) (a ': as)
-> DecAlt1 f (NS I (a ': as))
concatDecAlt1 :: NP (DecAlt1 f) (a : as) -> DecAlt1 f (NS I (a : as))
concatDecAlt1 = \case
x :: DecAlt1 f x
x :* xs :: NP (DecAlt1 f) xs
xs -> case NP (DecAlt1 f) xs
xs of
Nil -> (x -> NS I '[x])
-> (NS I '[x] -> x) -> DecAlt1 f x -> DecAlt1 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) DecAlt1 f x
x
_ :* _ -> (Night (Chain1 Night f) (Chain1 Night f) (NS I (a : x : xs))
-> Chain1 Night f (NS I (a : x : xs)))
-> Night (DecAlt1 f) (Chain1 Night f) (NS I (x : x : xs))
-> DecAlt1 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 (DecAlt1 f) (Chain1 Night f) (NS I (x : x : xs))
-> DecAlt1 f (NS I (a : as)))
-> Night (DecAlt1 f) (Chain1 Night f) (NS I (x : x : xs))
-> DecAlt1 f (NS I (a : as))
forall a b. (a -> b) -> a -> b
$ DecAlt1 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 (DecAlt1 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
DecAlt1 f x
x
(DecAlt1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs))
forall (f :: * -> *) a. DecAlt1 f a -> Chain1 Night f a
unDecAlt1 (DecAlt1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs)))
-> DecAlt1 f (NS I (x : xs)) -> Chain1 Night f (NS I (x : xs))
forall a b. (a -> b) -> a -> b
$ NP (DecAlt1 f) (x : xs) -> DecAlt1 f (NS I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP (DecAlt1 f) (a : as) -> DecAlt1 f (NS I (a : as))
concatDecAlt1 NP (DecAlt1 f) xs
NP (DecAlt1 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