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 = foldChain1 f (runNightAlt f id)
. unNightChain1
runContraNightChain1
:: forall f g. Decide g
=> f ~> g
-> NightChain1 f ~> g
runContraNightChain1 f = foldChain1 f (runNightDecide f id)
. unNightChain1
chainDec :: NightChain f ~> Dec f
chainDec = runContraNightChain inject
chainDec1 :: NightChain1 f ~> Dec1 f
chainDec1 = runContraNightChain1 inject
runCoNightChain
:: forall f g. Plus g
=> f ~> g
-> NightChain f ~> g
runCoNightChain f = foldChain (const zero) (runNightAlt f id)
. unNightChain
runContraNightChain
:: forall f g. Conclude g
=> f ~> g
-> NightChain f ~> g
runContraNightChain f = foldChain (conclude . refute) (runNightDecide f id)
. unNightChain
chainListF :: Functor f => NightChain f ~> ListF f
chainListF = runCoNightChain inject
chainListF_ :: NightChain f ~> CT.ComposeT ListF CY.Coyoneda f
chainListF_ = foldChain (const (CT.ComposeT (ListF []))) (\case
Night x (CT.ComposeT (ListF xs)) _ f g -> CT.ComposeT . ListF $
CY.Coyoneda f x : (map . fmap) g xs
) . unNightChain
chainNonEmptyF :: Functor f => NightChain1 f ~> NonEmptyF f
chainNonEmptyF = runCoNightChain1 inject
chainNonEmptyF_ :: NightChain1 f ~> CT.ComposeT NonEmptyF CY.Coyoneda f
chainNonEmptyF_ = foldChain1 inject (\case
Night x (CT.ComposeT (NonEmptyF xs)) _ f g -> CT.ComposeT . NonEmptyF $
CY.Coyoneda f x NE.<| (fmap . fmap) g xs
) . unNightChain1
pattern Swerve :: (a -> Either b c) -> (b -> a) -> (c -> a) -> f b -> NightChain f c -> NightChain f a
pattern Swerve f g h x xs <- (unSwerve_->MaybeF (Just (Night x xs f g h)))
where
Swerve f g h x xs = NightChain $ More $ Night x (unNightChain xs) f g h
unSwerve_ :: NightChain f ~> MaybeF (Night f (NightChain f))
unSwerve_ = \case
NightChain (More (Night x xs g f h)) -> MaybeF . Just $ Night x (NightChain xs) g f h
NightChain (Done _ ) -> MaybeF Nothing
pattern Reject :: (a -> Void) -> NightChain f a
pattern 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 NightChain1 f g h x xs <- (coerce splitChain1->Night x xs f g h)
where
NightChain1 f g h x xs = unsplitNE $ Night x xs f g h
{-# COMPLETE NightChain1 #-}
swerve
:: (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> NightChain f b
-> NightChain f c
-> NightChain f a
swerve f g h x y = coerce appendChain (Night x y f g h)
swerved
:: NightChain f a
-> NightChain f b
-> NightChain f (Either a b)
swerved = swerve id Left Right
swerve1
:: Invariant f
=> (a -> Either b c)
-> (b -> a)
-> (c -> a)
-> NightChain1 f b
-> NightChain1 f c
-> NightChain1 f a
swerve1 f g h x y = coerce appendChain1 (Night x y f g h)
swerved1
:: Invariant f
=> NightChain1 f a
-> NightChain1 f b
-> NightChain1 f (Either a b)
swerved1 = swerve1 id Left Right
assembleNightChain
:: NP f as
-> NightChain f (NS I as)
assembleNightChain = \case
Nil -> NightChain $ Done $ Not (\case {})
x :* xs -> NightChain $ More $ Night
x
(unNightChain $ assembleNightChain xs)
unconsNSI
(Z . I)
S
concatNightChain
:: NP (NightChain f) as
-> NightChain f (NS I as)
concatNightChain = \case
Nil -> NightChain $ Done $ Not (\case {})
x :* xs -> coerce appendChain $ Night
x
(unNightChain $ concatNightChain xs)
unconsNSI
(Z . I)
S
assembleNightChain1
:: Invariant f
=> NP f (a ': as)
-> NightChain1 f (NS I (a ': as))
assembleNightChain1 = \case
x :* xs -> NightChain1_ $ case xs of
Nil -> Done1 $ invmap (Z . I) (unI . unZ) x
_ :* _ -> More1 $ Night
x
(unNightChain1 $ assembleNightChain1 xs)
unconsNSI
(Z . I)
S
concatNightChain1
:: Invariant f
=> NP (NightChain1 f) (a ': as)
-> NightChain1 f (NS I (a ': as))
concatNightChain1 = \case
x :* xs -> case xs of
Nil -> invmap (Z . I) (unI . unZ) x
_ :* _ -> coerce appendChain1 $ Night
x
(unNightChain1 $ concatNightChain1 xs)
unconsNSI
(Z . I)
S
unconsNSI :: NS I (a ': as) -> Either a (NS I as)
unconsNSI = \case
Z (I x) -> Left x
S xs -> Right xs