{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.Functor.Invariant.Internative.Free (
DecAlt(.., Swerve, Reject)
, runCoDecAlt
, runContraDecAlt
, decAltListF
, decAltListF_
, decAltDec
, foldDecAlt
, assembleDecAlt
, DecAlt1(.., DecAlt1)
, runCoDecAlt1
, runContraDecAlt1
, decAltNonEmptyF
, decAltNonEmptyF_
, decAltDec1
, foldDecAlt1
, assembleDecAlt1
) 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.Internative
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 hiding (hmap)
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 :: forall (f :: * -> *) (g :: * -> *).
Alt g =>
(f ~> g) -> DecAlt1 f ~> g
runCoDecAlt1 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 x -> g x
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 x -> g x
f ~> g
f g x -> g x
forall a. a -> a
g ~> g
id)
runContraDecAlt1
:: forall f g. Decide g
=> f ~> g
-> DecAlt1 f ~> g
runContraDecAlt1 :: forall (f :: * -> *) (g :: * -> *).
Decide g =>
(f ~> g) -> DecAlt1 f ~> g
runContraDecAlt1 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 x -> g x
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 x -> g x
f ~> g
f g x -> g x
forall a. a -> a
g ~> g
id)
decAltDec :: DecAlt f ~> Dec f
decAltDec :: forall (f :: * -> *) x. 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 x -> Dec f x
f ~> Dec f
forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
forall (f :: * -> *). f ~> Dec f
inject
decAltDec1 :: DecAlt1 f ~> Dec1 f
decAltDec1 :: forall (f :: * -> *) x. 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 x -> Dec1 f x
f ~> Dec1 f
forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
forall (f :: * -> *). f ~> Dec1 f
inject
runCoDecAlt
:: forall f g. Plus g
=> f ~> g
-> DecAlt f ~> g
runCoDecAlt :: forall (f :: * -> *) (g :: * -> *).
Plus g =>
(f ~> g) -> DecAlt f ~> g
runCoDecAlt 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 a. g a
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 x -> g x
f ~> g
f g x -> g x
forall a. a -> a
g ~> g
id)
runContraDecAlt
:: forall f g. Conclude g
=> f ~> g
-> DecAlt f ~> g
runContraDecAlt :: forall (f :: * -> *) (g :: * -> *).
Conclude g =>
(f ~> g) -> DecAlt f ~> g
runContraDecAlt 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 (x -> Void) -> g x
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 x -> g x
f ~> g
f g x -> g x
forall a. a -> a
g ~> g
id)
decAltListF :: Functor f => DecAlt f ~> ListF f
decAltListF :: forall (f :: * -> *). Functor f => DecAlt f ~> ListF f
decAltListF = (f ~> ListF f) -> DecAlt f ~> ListF f
forall (f :: * -> *) (g :: * -> *).
Plus g =>
(f ~> g) -> DecAlt f ~> g
runCoDecAlt f x -> ListF f x
f ~> ListF f
forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
forall (f :: * -> *). f ~> ListF f
inject
decAltListF_ :: DecAlt f ~> CT.ComposeT ListF CY.Coyoneda f
decAltListF_ :: forall (f :: * -> *) x. DecAlt f x -> ComposeT ListF Coyoneda f x
decAltListF_ = (forall x. (x -> Void) -> ComposeT ListF Coyoneda f x)
-> (forall {x}.
Night f (ComposeT ListF Coyoneda f) x
-> ComposeT ListF Coyoneda f x)
-> forall {x}. DecAlt f x -> ComposeT ListF Coyoneda f x
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 []))) ((forall {x}.
Night f (ComposeT ListF Coyoneda f) x
-> ComposeT ListF Coyoneda f x)
-> forall {x}. DecAlt f x -> ComposeT ListF Coyoneda f x)
-> (forall {x}.
Night f (ComposeT ListF Coyoneda f) x
-> ComposeT ListF Coyoneda f x)
-> forall {x}. DecAlt f x -> ComposeT ListF Coyoneda f x
forall a b. (a -> b) -> a -> b
$ \case
Night f b1
x (CT.ComposeT (ListF [Coyoneda f c1]
xs)) b1 -> x
f c1 -> x
g x -> Either b1 c1
_ -> 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
$
(b1 -> x) -> f b1 -> Coyoneda f x
forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda b1 -> x
f f b1
x Coyoneda f x -> [Coyoneda f x] -> [Coyoneda f x]
forall a. a -> [a] -> [a]
: ((Coyoneda f c1 -> Coyoneda f x)
-> [Coyoneda f c1] -> [Coyoneda f x]
forall a b. (a -> b) -> [a] -> [b]
map ((Coyoneda f c1 -> Coyoneda f x)
-> [Coyoneda f c1] -> [Coyoneda f x])
-> ((c1 -> x) -> Coyoneda f c1 -> Coyoneda f x)
-> (c1 -> x)
-> [Coyoneda f c1]
-> [Coyoneda f x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c1 -> x) -> Coyoneda f c1 -> Coyoneda f x
forall a b. (a -> b) -> Coyoneda f a -> Coyoneda f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) c1 -> x
g [Coyoneda f c1]
xs
decAltNonEmptyF :: Functor f => DecAlt1 f ~> NonEmptyF f
decAltNonEmptyF :: forall (f :: * -> *). Functor f => DecAlt1 f ~> NonEmptyF f
decAltNonEmptyF = (f ~> NonEmptyF f) -> DecAlt1 f ~> NonEmptyF f
forall (f :: * -> *) (g :: * -> *).
Alt g =>
(f ~> g) -> DecAlt1 f ~> g
runCoDecAlt1 f x -> NonEmptyF f x
f ~> NonEmptyF f
forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
forall (f :: * -> *). f ~> NonEmptyF f
inject
decAltNonEmptyF_ :: DecAlt1 f ~> CT.ComposeT NonEmptyF CY.Coyoneda f
decAltNonEmptyF_ :: forall (f :: * -> *) x.
DecAlt1 f x -> ComposeT NonEmptyF Coyoneda f x
decAltNonEmptyF_ = (f ~> ComposeT NonEmptyF Coyoneda f)
-> (forall {x}.
Night f (ComposeT NonEmptyF Coyoneda f) x
-> ComposeT NonEmptyF Coyoneda f x)
-> forall {x}. DecAlt1 f x -> ComposeT NonEmptyF Coyoneda f x
forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Night f g ~> g) -> DecAlt1 f ~> g
foldDecAlt1 f x -> ComposeT NonEmptyF Coyoneda f x
f ~> ComposeT NonEmptyF Coyoneda f
forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
forall (f :: * -> *). f ~> ComposeT NonEmptyF Coyoneda f
inject ((forall {x}.
Night f (ComposeT NonEmptyF Coyoneda f) x
-> ComposeT NonEmptyF Coyoneda f x)
-> forall {x}. DecAlt1 f x -> ComposeT NonEmptyF Coyoneda f x)
-> (forall {x}.
Night f (ComposeT NonEmptyF Coyoneda f) x
-> ComposeT NonEmptyF Coyoneda f x)
-> forall {x}. DecAlt1 f x -> ComposeT NonEmptyF Coyoneda f x
forall a b. (a -> b) -> a -> b
$ \case
Night f b1
x (CT.ComposeT (NonEmptyF NonEmpty (Coyoneda f c1)
xs)) b1 -> x
f c1 -> x
g x -> Either b1 c1
_ -> 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
$
(b1 -> x) -> f b1 -> Coyoneda f x
forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda b1 -> x
f f b1
x Coyoneda f x -> NonEmpty (Coyoneda f x) -> NonEmpty (Coyoneda f x)
forall a. a -> NonEmpty a -> NonEmpty a
NE.<| ((Coyoneda f c1 -> Coyoneda f x)
-> NonEmpty (Coyoneda f c1) -> NonEmpty (Coyoneda f x)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Coyoneda f c1 -> Coyoneda f x)
-> NonEmpty (Coyoneda f c1) -> NonEmpty (Coyoneda f x))
-> ((c1 -> x) -> Coyoneda f c1 -> Coyoneda f x)
-> (c1 -> x)
-> NonEmpty (Coyoneda f c1)
-> NonEmpty (Coyoneda f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c1 -> x) -> Coyoneda f c1 -> Coyoneda f x
forall a b. (a -> b) -> Coyoneda f a -> Coyoneda f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) c1 -> x
g NonEmpty (Coyoneda f c1)
xs
foldDecAlt
:: (forall x. (x -> Void) -> g x)
-> (Night f g ~> g)
-> DecAlt f ~> g
foldDecAlt :: forall (g :: * -> *) (f :: * -> *).
(forall x. (x -> Void) -> g x) -> (Night f g ~> g) -> DecAlt f ~> g
foldDecAlt forall x. (x -> Void) -> g x
f 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 x -> g x
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 :: forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Night f g ~> g) -> DecAlt1 f ~> g
foldDecAlt1 f ~> g
f 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 x -> g x
f ~> g
f Night f g x -> g x
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 :: (b -> a) -> (c -> a) -> (a -> Either b c) -> f b -> DecAlt f c -> DecAlt f a
pattern $mSwerve :: forall {r} {a} {f :: * -> *}.
DecAlt f a
-> (forall {b} {c}.
(b -> a)
-> (c -> a) -> (a -> Either b c) -> f b -> DecAlt f c -> r)
-> ((# #) -> r)
-> r
$bSwerve :: forall a (f :: * -> *) b c.
(b -> a)
-> (c -> a) -> (a -> Either b c) -> f b -> DecAlt f c -> DecAlt f a
Swerve f g h x xs <- (unSwerve_->MaybeF (Just (Night x xs f g h)))
where
Swerve b -> a
f c -> a
g a -> Either b c
h f b
x 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} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
(f :: k) (a :: k1).
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
-> (b -> a)
-> (c -> a)
-> (a -> Either b c)
-> Night f (Chain Night Not f) a
forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1
-> b c1
-> (b1 -> c)
-> (c1 -> c)
-> (c -> Either b1 c1)
-> Night a b c
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) b -> a
f c -> a
g a -> Either b c
h
unSwerve_ :: DecAlt f ~> MaybeF (Night f (DecAlt f))
unSwerve_ :: forall (f :: * -> *) x. DecAlt f x -> MaybeF (Night f (DecAlt f)) x
unSwerve_ = \case
DecAlt (More (Night f b1
x Chain Night Not f c1
xs b1 -> x
g c1 -> x
f x -> Either b1 c1
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 b1
-> DecAlt f c1
-> (b1 -> x)
-> (c1 -> x)
-> (x -> Either b1 c1)
-> Night f (DecAlt f) x
forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1
-> b c1
-> (b1 -> c)
-> (c1 -> c)
-> (c -> Either b1 c1)
-> Night a b c
Night f b1
x (Chain Night Not f c1 -> DecAlt f c1
forall (f :: * -> *) a. Chain Night Not f a -> DecAlt f a
DecAlt Chain Night Not f c1
xs) b1 -> x
g c1 -> x
f x -> Either b1 c1
h
DecAlt (Done Not x
_ ) -> 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 $mReject :: forall {r} {a} {f :: * -> *}.
DecAlt f a -> ((a -> Void) -> r) -> ((# #) -> r) -> r
$bReject :: forall a (f :: * -> *). (a -> Void) -> DecAlt f a
Reject x = DecAlt (Done (Not x))
{-# COMPLETE Swerve, Reject #-}
instance Inalt (DecAlt f) where
swerve :: forall b a c.
(b -> a)
-> (c -> a)
-> (a -> Either b c)
-> DecAlt f b
-> DecAlt f c
-> DecAlt f a
swerve = ((b -> a)
-> (c -> a)
-> (a -> Either b c)
-> Chain Night Not f b
-> Chain Night Not f c
-> Chain Night Not f a)
-> (b -> a)
-> (c -> a)
-> (a -> Either b c)
-> DecAlt f b
-> DecAlt f c
-> DecAlt f a
forall a b. Coercible a b => a -> b
coerce (forall (f :: * -> *) b a c.
Inalt f =>
(b -> a) -> (c -> a) -> (a -> Either b c) -> f b -> f c -> f a
swerve @(Chain Night Not _))
instance Inplus (DecAlt f) where
reject :: forall a. (a -> Void) -> DecAlt f a
reject = ((a -> Void) -> Chain Night Not f a) -> (a -> Void) -> DecAlt f a
forall a b. Coercible a b => a -> b
coerce (forall (f :: * -> *) a. Inplus f => (a -> Void) -> f a
reject @(Chain Night Not _))
pattern DecAlt1 :: Invariant f => (b -> a) -> (c -> a) -> (a -> Either b c) -> f b -> DecAlt f c -> DecAlt1 f a
pattern $mDecAlt1 :: forall {r} {f :: * -> *} {a}.
Invariant f =>
DecAlt1 f a
-> (forall {b} {c}.
(b -> a)
-> (c -> a) -> (a -> Either b c) -> f b -> DecAlt f c -> r)
-> ((# #) -> r)
-> r
$bDecAlt1 :: forall (f :: * -> *) a b c.
Invariant f =>
(b -> a)
-> (c -> a)
-> (a -> Either b c)
-> f b
-> DecAlt f c
-> DecAlt1 f a
DecAlt1 f g h x xs <- (coerce splitChain1->Night x xs f g h)
where
DecAlt1 b -> a
f c -> a
g a -> Either b c
h f b
x DecAlt f c
xs = Night f (ListBy Night f) a -> NonEmptyBy Night f a
Night f (ListBy Night f) ~> NonEmptyBy Night f
forall (f :: * -> *).
FunctorBy Night f =>
Night f (ListBy Night f) ~> NonEmptyBy Night f
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 -> NonEmptyBy Night f a)
-> Night f (ListBy Night f) a -> NonEmptyBy Night f a
forall a b. (a -> b) -> a -> b
$ f b
-> DecAlt f c
-> (b -> a)
-> (c -> a)
-> (a -> Either b c)
-> Night f (DecAlt f) a
forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1
-> b c1
-> (b1 -> c)
-> (c1 -> c)
-> (c -> Either b1 c1)
-> Night a b c
Night f b
x DecAlt f c
xs b -> a
f c -> a
g a -> Either b c
h
{-# COMPLETE DecAlt1 #-}
instance Invariant f => Inalt (DecAlt1 f) where
swerve :: forall b a c.
(b -> a)
-> (c -> a)
-> (a -> Either b c)
-> DecAlt1 f b
-> DecAlt1 f c
-> DecAlt1 f a
swerve = ((b -> a)
-> (c -> a)
-> (a -> Either b c)
-> Chain1 Night f b
-> Chain1 Night f c
-> Chain1 Night f a)
-> (b -> a)
-> (c -> a)
-> (a -> Either b c)
-> DecAlt1 f b
-> DecAlt1 f c
-> DecAlt1 f a
forall a b. Coercible a b => a -> b
coerce (forall (f :: * -> *) b a c.
Inalt f =>
(b -> a) -> (c -> a) -> (a -> Either b c) -> f b -> f c -> f a
swerve @(Chain1 Night _))
assembleDecAlt
:: NP f as
-> DecAlt f (NS I as)
assembleDecAlt :: forall (f :: * -> *) (as :: [*]). NP f as -> DecAlt f (NS I as)
assembleDecAlt = \case
NP f as
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} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
(f :: k) (a :: k1).
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 {})
f x
x :* NP f xs
xs -> 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
$ Night f (Chain Night Not f) (NS I as)
-> Chain Night Not f (NS I as)
forall {k} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
(f :: k) (a :: k1).
t f (Chain t i f) a -> Chain t i f a
More (Night f (Chain Night Not f) (NS I as)
-> Chain Night Not f (NS I as))
-> Night f (Chain Night Not f) (NS I as)
-> Chain Night Not f (NS I as)
forall a b. (a -> b) -> a -> b
$ f x
-> Chain Night Not f (NS I xs)
-> (x -> NS I as)
-> (NS I xs -> NS I as)
-> (NS I as -> Either x (NS I xs))
-> Night f (Chain Night Not f) (NS I as)
forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1
-> b c1
-> (b1 -> c)
-> (c1 -> c)
-> (c -> Either b1 c1)
-> Night a b c
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)
(I x -> NS I as
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 as) -> (x -> I x) -> x -> NS I as
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I x
forall a. a -> I a
I)
NS I xs -> NS I as
NS I xs -> NS I (x : xs)
forall {k} (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S
(\case Z (I x
y) -> x -> Either x (NS I xs)
forall a b. a -> Either a b
Left x
x
y; S NS I xs
ys -> NS I xs -> Either x (NS I xs)
forall a b. b -> Either a b
Right NS I xs
NS I xs
ys)
assembleDecAlt1
:: Invariant f
=> NP f (a ': as)
-> DecAlt1 f (NS I (a ': as))
assembleDecAlt1 :: forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP f (a : as) -> DecAlt1 f (NS I (a : as))
assembleDecAlt1 (f x
x :* 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
NP f xs
Nil -> f (NS I (a : as)) -> 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 (a : as)) -> Chain1 Night f (NS I (a : as)))
-> f (NS I (a : as)) -> Chain1 Night f (NS I (a : as))
forall a b. (a -> b) -> a -> b
$ (a -> NS I (a : as))
-> (NS I (a : as) -> a) -> f a -> f (NS I (a : as))
forall a b. (a -> b) -> (b -> a) -> f a -> f b
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (I a -> NS I (a : as)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I a -> NS I (a : as)) -> (a -> I a) -> a -> NS I (a : as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> I a
forall a. a -> I a
I) (I a -> a
forall a. I a -> a
unI (I a -> a) -> (NS I (a : as) -> I a) -> NS I (a : as) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NS I (a : as) -> I a
NS I '[a] -> I a
forall {k} (f :: k -> *) (x :: k). NS f '[x] -> f x
unZ) f a
f x
x
f x
_ :* NP f xs
_ -> Night f (Chain1 Night f) (NS I (a : as))
-> 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 (a : as))
-> Chain1 Night f (NS I (a : as)))
-> Night f (Chain1 Night f) (NS I (a : as))
-> Chain1 Night f (NS I (a : as))
forall a b. (a -> b) -> a -> b
$ f x
-> Chain1 Night f (NS I (x : xs))
-> (x -> NS I (a : as))
-> (NS I (x : xs) -> NS I (a : as))
-> (NS I (a : as) -> Either x (NS I (x : xs)))
-> Night f (Chain1 Night f) (NS I (a : as))
forall (a :: * -> *) b1 (b :: * -> *) c1 c.
a b1
-> b c1
-> (b1 -> c)
-> (c1 -> c)
-> (c -> Either b1 c1)
-> Night a b c
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)
(I a -> NS I (a : as)
forall {k} (a :: k -> *) (x :: k) (xs :: [k]). a x -> NS a (x : xs)
Z (I a -> NS I (a : as)) -> (x -> I a) -> x -> NS I (a : as)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> I a
x -> I x
forall a. a -> I a
I)
NS I (x : xs) -> NS I (a : as)
NS I (x : xs) -> NS I (a : x : xs)
forall {k} (a :: k -> *) (xs :: [k]) (x :: k).
NS a xs -> NS a (x : xs)
S
(\case Z (I x
y) -> x -> Either x (NS I (x : xs))
forall a b. a -> Either a b
Left x
x
y; S NS I xs
ys -> NS I (x : xs) -> Either x (NS I (x : xs))
forall a b. b -> Either a b
Right NS I xs
NS I (x : xs)
ys)