{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.Functor.Invariant.Inplicative.Free (
DivAp(.., Gather, Knot)
, runCoDivAp
, runContraDivAp
, divApAp
, divApDiv
, foldDivAp
, assembleDivAp
, assembleDivApRec
, DivAp1(.., DivAp1)
, runCoDivAp1
, runContraDivAp1
, divApAp1
, divApDiv1
, foldDivAp1
, assembleDivAp1
, assembleDivAp1Rec
) where
import Control.Applicative
import Control.Applicative.Free (Ap(..))
import Control.Applicative.ListF (MaybeF(..))
import Control.Natural
import Data.Coerce
import Data.Functor.Apply
import Data.Functor.Apply.Free (Ap1(..))
import Data.Functor.Contravariant.Divise
import Data.Functor.Contravariant.Divisible
import Data.Functor.Contravariant.Divisible.Free (Div(..), Div1)
import Data.Functor.Identity
import Data.Functor.Invariant
import Data.Functor.Invariant.Day
import Data.Functor.Invariant.Inplicative
import Data.HBifunctor.Tensor hiding (elim1, elim2, intro1, intro2)
import Data.HFunctor
import Data.HFunctor.Chain
import Data.HFunctor.Chain.Internal
import Data.HFunctor.Interpret
import Data.SOP hiding (hmap)
import qualified Data.Vinyl as V
import qualified Data.Vinyl.Functor as V
runCoDivAp1
:: forall f g. Apply g
=> f ~> g
-> DivAp1 f ~> g
runCoDivAp1 :: (f ~> g) -> DivAp1 f ~> g
runCoDivAp1 f ~> g
f = (f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
foldDivAp1 f ~> g
f ((f ~> g) -> (g ~> g) -> Day f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Apply h =>
(f ~> h) -> (g ~> h) -> Day f g ~> h
runDayApply f ~> g
f forall a. a -> a
g ~> g
id)
runContraDivAp1
:: forall f g. Divise g
=> f ~> g
-> DivAp1 f ~> g
runContraDivAp1 :: (f ~> g) -> DivAp1 f ~> g
runContraDivAp1 f ~> g
f = (f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
foldDivAp1 f ~> g
f ((f ~> g) -> (g ~> g) -> Day f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Divise h =>
(f ~> h) -> (g ~> h) -> Day f g ~> h
runDayDivise f ~> g
f forall a. a -> a
g ~> g
id)
runCoDivAp
:: forall f g. Applicative g
=> f ~> g
-> DivAp f ~> g
runCoDivAp :: (f ~> g) -> DivAp f ~> g
runCoDivAp f ~> g
f = (forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
forall (g :: * -> *) (f :: * -> *).
(forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
foldDivAp forall x. x -> g x
forall (f :: * -> *) a. Applicative f => a -> f a
pure (\case Day f b
x g c
y b -> c -> x
h x -> (b, c)
_ -> (b -> c -> x) -> g b -> g c -> g x
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 b -> c -> x
h (f b -> g b
f ~> g
f f b
x) g c
y)
runContraDivAp
:: forall f g. Divisible g
=> f ~> g
-> DivAp f ~> g
runContraDivAp :: (f ~> g) -> DivAp f ~> g
runContraDivAp f ~> g
f = (forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
forall (g :: * -> *) (f :: * -> *).
(forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
foldDivAp (g x -> x -> g x
forall a b. a -> b -> a
const g x
forall (f :: * -> *) a. Divisible f => f a
conquer) (\case Day f b
x g c
y b -> c -> x
_ x -> (b, c)
g -> (x -> (b, c)) -> g b -> g c -> g x
forall (f :: * -> *) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide x -> (b, c)
g (f b -> g b
f ~> g
f f b
x) g c
y)
foldDivAp
:: (forall x. x -> g x)
-> (Day f g ~> g)
-> DivAp f ~> g
foldDivAp :: (forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
foldDivAp forall x. x -> g x
f Day f g ~> g
g = (Identity ~> g) -> (Day f g ~> g) -> Chain Day Identity 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 -> g x
forall x. x -> g x
f (x -> g x) -> (Identity x -> x) -> Identity x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity x -> x
forall a. Identity a -> a
runIdentity) Day f g ~> g
g (Chain Day Identity f x -> g x)
-> (DivAp f x -> Chain Day Identity f x) -> DivAp f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DivAp f x -> Chain Day Identity f x
forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp
foldDivAp1
:: (f ~> g)
-> (Day f g ~> g)
-> DivAp1 f ~> g
foldDivAp1 :: (f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
foldDivAp1 f ~> g
f Day f g ~> g
g = (f ~> g) -> (Day f g ~> g) -> Chain1 Day 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 Day f g ~> g
g (Chain1 Day f x -> g x)
-> (DivAp1 f x -> Chain1 Day f x) -> DivAp1 f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DivAp1 f x -> Chain1 Day f x
forall (f :: * -> *) a. DivAp1 f a -> Chain1 Day f a
unDivAp1
divApAp :: DivAp f ~> Ap f
divApAp :: DivAp f x -> Ap f x
divApAp = (f ~> Ap f) -> DivAp f ~> Ap f
forall (f :: * -> *) (g :: * -> *).
Applicative g =>
(f ~> g) -> DivAp f ~> g
runCoDivAp f ~> Ap f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
divApAp1 :: DivAp1 f ~> Ap1 f
divApAp1 :: DivAp1 f x -> Ap1 f x
divApAp1 = (f ~> Ap1 f) -> DivAp1 f ~> Ap1 f
forall (f :: * -> *) (g :: * -> *).
Apply g =>
(f ~> g) -> DivAp1 f ~> g
runCoDivAp1 f ~> Ap1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
divApDiv :: DivAp f ~> Div f
divApDiv :: DivAp f x -> Div f x
divApDiv = (f ~> Div f) -> DivAp f ~> Div f
forall (f :: * -> *) (g :: * -> *).
Divisible g =>
(f ~> g) -> DivAp f ~> g
runContraDivAp f ~> Div f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
divApDiv1 :: DivAp1 f ~> Div1 f
divApDiv1 :: DivAp1 f x -> Div1 f x
divApDiv1 = (f ~> Div1 f) -> DivAp1 f ~> Div1 f
forall (f :: * -> *) (g :: * -> *).
Divise g =>
(f ~> g) -> DivAp1 f ~> g
runContraDivAp1 f ~> Div1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
pattern Gather :: (b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> DivAp f a
pattern $bGather :: (b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> DivAp f a
$mGather :: forall r a (f :: * -> *).
DivAp f a
-> (forall b c.
(b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> r)
-> (Void# -> r)
-> r
Gather f g x xs <- (unGather_->MaybeF (Just (Day x xs f g)))
where
Gather b -> c -> a
f a -> (b, c)
g f b
x DivAp f c
xs = Chain Day Identity f a -> DivAp f a
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f a -> DivAp f a)
-> Chain Day Identity f a -> DivAp f a
forall a b. (a -> b) -> a -> b
$ Day f (Chain Day Identity f) a -> Chain Day Identity 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 (Day f (Chain Day Identity f) a -> Chain Day Identity f a)
-> Day f (Chain Day Identity f) a -> Chain Day Identity f a
forall a b. (a -> b) -> a -> b
$ f b
-> Chain Day Identity f c
-> (b -> c -> a)
-> (a -> (b, c))
-> Day f (Chain Day Identity f) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f b
x (DivAp f c -> Chain Day Identity f c
forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp DivAp f c
xs) b -> c -> a
f a -> (b, c)
g
unGather_ :: DivAp f ~> MaybeF (Day f (DivAp f))
unGather_ :: DivAp f x -> MaybeF (Day f (DivAp f)) x
unGather_ = \case
DivAp (More (Day f b
x Chain Day Identity f c
xs b -> c -> x
g x -> (b, c)
f)) -> Maybe (Day f (DivAp f) x) -> MaybeF (Day f (DivAp f)) x
forall k (f :: k -> *) (a :: k). Maybe (f a) -> MaybeF f a
MaybeF (Maybe (Day f (DivAp f) x) -> MaybeF (Day f (DivAp f)) x)
-> (Day f (DivAp f) x -> Maybe (Day f (DivAp f) x))
-> Day f (DivAp f) x
-> MaybeF (Day f (DivAp f)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Day f (DivAp f) x -> Maybe (Day f (DivAp f) x)
forall a. a -> Maybe a
Just (Day f (DivAp f) x -> MaybeF (Day f (DivAp f)) x)
-> Day f (DivAp f) x -> MaybeF (Day f (DivAp f)) x
forall a b. (a -> b) -> a -> b
$ f b
-> DivAp f c -> (b -> c -> x) -> (x -> (b, c)) -> Day f (DivAp f) x
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f b
x (Chain Day Identity f c -> DivAp f c
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp Chain Day Identity f c
xs) b -> c -> x
g x -> (b, c)
f
DivAp (Done Identity x
_ ) -> Maybe (Day f (DivAp f) x) -> MaybeF (Day f (DivAp f)) x
forall k (f :: k -> *) (a :: k). Maybe (f a) -> MaybeF f a
MaybeF Maybe (Day f (DivAp f) x)
forall a. Maybe a
Nothing
pattern Knot :: a -> DivAp f a
pattern $bKnot :: a -> DivAp f a
$mKnot :: forall r a (f :: * -> *).
DivAp f a -> (a -> r) -> (Void# -> r) -> r
Knot x = DivAp (Done (Identity x))
{-# COMPLETE Gather, Knot #-}
instance Inply (DivAp f) where
gather :: (b -> c -> a)
-> (a -> (b, c)) -> DivAp f b -> DivAp f c -> DivAp f a
gather = ((b -> c -> a)
-> (a -> (b, c))
-> Chain Day Identity f b
-> Chain Day Identity f c
-> Chain Day Identity f a)
-> (b -> c -> a)
-> (a -> (b, c))
-> DivAp f b
-> DivAp f c
-> DivAp f a
coerce (forall b c a.
Inply (Chain Day Identity f) =>
(b -> c -> a)
-> (a -> (b, c))
-> Chain Day Identity f b
-> Chain Day Identity f c
-> Chain Day Identity f a
forall (f :: * -> *) b c a.
Inply f =>
(b -> c -> a) -> (a -> (b, c)) -> f b -> f c -> f a
gather @(Chain Day Identity _))
instance Inplicative (DivAp f) where
knot :: a -> DivAp f a
knot = (a -> Chain Day Identity f a) -> a -> DivAp f a
coerce (forall a.
Inplicative (Chain Day Identity f) =>
a -> Chain Day Identity f a
forall (f :: * -> *) a. Inplicative f => a -> f a
knot @(Chain Day Identity _))
pattern DivAp1 :: Invariant f => (b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> DivAp1 f a
pattern $bDivAp1 :: (b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> DivAp1 f a
$mDivAp1 :: forall r (f :: * -> *) a.
Invariant f =>
DivAp1 f a
-> (forall b c.
(b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> r)
-> (Void# -> r)
-> r
DivAp1 f g x xs <- (coerce splitChain1->Day x xs f g)
where
DivAp1 b -> c -> a
f a -> (b, c)
g f b
x DivAp f c
xs = Day f (ListBy Day f) a -> NonEmptyBy Day f a
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE (Day f (ListBy Day f) a -> NonEmptyBy Day f a)
-> Day f (ListBy Day f) a -> NonEmptyBy Day f a
forall a b. (a -> b) -> a -> b
$ f b
-> DivAp f c -> (b -> c -> a) -> (a -> (b, c)) -> Day f (DivAp f) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f b
x DivAp f c
xs b -> c -> a
f a -> (b, c)
g
{-# COMPLETE DivAp1 #-}
instance Invariant f => Inply (DivAp1 f) where
gather :: (b -> c -> a)
-> (a -> (b, c)) -> DivAp1 f b -> DivAp1 f c -> DivAp1 f a
gather = ((b -> c -> a)
-> (a -> (b, c))
-> Chain1 Day f b
-> Chain1 Day f c
-> Chain1 Day f a)
-> (b -> c -> a)
-> (a -> (b, c))
-> DivAp1 f b
-> DivAp1 f c
-> DivAp1 f a
coerce (forall b c a.
Inply (Chain1 Day f) =>
(b -> c -> a)
-> (a -> (b, c))
-> Chain1 Day f b
-> Chain1 Day f c
-> Chain1 Day f a
forall (f :: * -> *) b c a.
Inply f =>
(b -> c -> a) -> (a -> (b, c)) -> f b -> f c -> f a
gather @(Chain1 Day _))
assembleDivAp
:: NP f as
-> DivAp f (NP I as)
assembleDivAp :: NP f as -> DivAp f (NP I as)
assembleDivAp = \case
NP f as
Nil -> Chain Day Identity f (NP I '[]) -> DivAp f (NP I '[])
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f (NP I '[]) -> DivAp f (NP I '[]))
-> Chain Day Identity f (NP I '[]) -> DivAp f (NP I '[])
forall a b. (a -> b) -> a -> b
$ Identity (NP I '[]) -> Chain Day Identity f (NP I '[])
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
i a -> Chain t i f a
Done (Identity (NP I '[]) -> Chain Day Identity f (NP I '[]))
-> Identity (NP I '[]) -> Chain Day Identity f (NP I '[])
forall a b. (a -> b) -> a -> b
$ NP I '[] -> Identity (NP I '[])
forall a. a -> Identity a
Identity NP I '[]
forall k (a :: k -> *). NP a '[]
Nil
f x
x :* NP f xs
xs -> Chain Day Identity f (NP I (x : xs)) -> DivAp f (NP I (x : xs))
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f (NP I (x : xs)) -> DivAp f (NP I (x : xs)))
-> Chain Day Identity f (NP I (x : xs)) -> DivAp f (NP I (x : xs))
forall a b. (a -> b) -> a -> b
$ Day f (Chain Day Identity f) (NP I (x : xs))
-> Chain Day Identity f (NP 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 (Day f (Chain Day Identity f) (NP I (x : xs))
-> Chain Day Identity f (NP I (x : xs)))
-> Day f (Chain Day Identity f) (NP I (x : xs))
-> Chain Day Identity f (NP I (x : xs))
forall a b. (a -> b) -> a -> b
$ f x
-> Chain Day Identity f (NP I xs)
-> (x -> NP I xs -> NP I (x : xs))
-> (NP I (x : xs) -> (x, NP I xs))
-> Day f (Chain Day Identity f) (NP I (x : xs))
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day
f x
x
(DivAp f (NP I xs) -> Chain Day Identity f (NP I xs)
forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp (NP f xs -> DivAp f (NP I xs)
forall (f :: * -> *) (as :: [*]). NP f as -> DivAp f (NP I as)
assembleDivAp NP f xs
xs))
(\x
y NP I xs
ys -> x -> I x
forall a. a -> I a
I x
y I x -> NP I xs -> NP I (x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I xs
ys)
(\case I x
y :* NP I xs
ys -> (x
x
y, NP I xs
NP I xs
ys))
assembleDivAp1
:: Invariant f
=> NP f (a ': as)
-> DivAp1 f (NP I (a ': as))
assembleDivAp1 :: NP f (a : as) -> DivAp1 f (NP I (a : as))
assembleDivAp1 (f x
x :* NP f xs
xs) = Chain1 Day f (NP I (a : as)) -> DivAp1 f (NP I (a : as))
forall (f :: * -> *) a. Chain1 Day f a -> DivAp1 f a
DivAp1_ (Chain1 Day f (NP I (a : as)) -> DivAp1 f (NP I (a : as)))
-> Chain1 Day f (NP I (a : as)) -> DivAp1 f (NP I (a : as))
forall a b. (a -> b) -> a -> b
$ case NP f xs
xs of
NP f xs
Nil -> f (NP I '[x]) -> Chain1 Day f (NP I '[x])
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
f a -> Chain1 t f a
Done1 (f (NP I '[x]) -> Chain1 Day f (NP I '[x]))
-> f (NP I '[x]) -> Chain1 Day f (NP I '[x])
forall a b. (a -> b) -> a -> b
$ (x -> NP I '[x]) -> (NP I '[x] -> x) -> f x -> f (NP I '[x])
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap ((I x -> NP I '[] -> NP I '[x]
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I '[]
forall k (a :: k -> *). NP a '[]
Nil) (I x -> NP I '[x]) -> (x -> I x) -> x -> NP 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) -> (NP I '[x] -> I x) -> NP I '[x] -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP I '[x] -> I x
forall k (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x
hd) f x
x
f x
_ :* NP f xs
_ -> Day f (Chain1 Day f) (NP I (x : x : xs))
-> Chain1 Day f (NP I (x : x : xs))
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 (Day f (Chain1 Day f) (NP I (x : x : xs))
-> Chain1 Day f (NP I (x : x : xs)))
-> Day f (Chain1 Day f) (NP I (x : x : xs))
-> Chain1 Day f (NP I (x : x : xs))
forall a b. (a -> b) -> a -> b
$ f x
-> Chain1 Day f (NP I (x : xs))
-> (x -> NP I (x : xs) -> NP I (x : x : xs))
-> (NP I (x : x : xs) -> (x, NP I (x : xs)))
-> Day f (Chain1 Day f) (NP I (x : x : xs))
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day
f x
x
(DivAp1 f (NP I (x : xs)) -> Chain1 Day f (NP I (x : xs))
forall (f :: * -> *) a. DivAp1 f a -> Chain1 Day f a
unDivAp1 (NP f (x : xs) -> DivAp1 f (NP I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP f (a : as) -> DivAp1 f (NP I (a : as))
assembleDivAp1 NP f xs
NP f (x : xs)
xs))
(\x
y NP I (x : xs)
ys -> x -> I x
forall a. a -> I a
I x
y I x -> NP I (x : xs) -> NP I (x : x : xs)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I (x : xs)
ys)
(\case I x
y :* NP I xs
ys -> (x
x
y, NP I xs
NP I (x : xs)
ys))
assembleDivApRec
:: V.Rec f as
-> DivAp f (V.XRec V.Identity as)
assembleDivApRec :: Rec f as -> DivAp f (XRec Identity as)
assembleDivApRec = \case
Rec f as
V.RNil -> Chain Day Identity f (Rec (XData Identity) '[])
-> DivAp f (Rec (XData Identity) '[])
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f (Rec (XData Identity) '[])
-> DivAp f (Rec (XData Identity) '[]))
-> Chain Day Identity f (Rec (XData Identity) '[])
-> DivAp f (Rec (XData Identity) '[])
forall a b. (a -> b) -> a -> b
$ Identity (Rec (XData Identity) '[])
-> Chain Day Identity f (Rec (XData Identity) '[])
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
i a -> Chain t i f a
Done (Identity (Rec (XData Identity) '[])
-> Chain Day Identity f (Rec (XData Identity) '[]))
-> Identity (Rec (XData Identity) '[])
-> Chain Day Identity f (Rec (XData Identity) '[])
forall a b. (a -> b) -> a -> b
$ Rec (XData Identity) '[] -> Identity (Rec (XData Identity) '[])
forall a. a -> Identity a
Identity Rec (XData Identity) '[]
forall u (a :: u -> *). Rec a '[]
V.RNil
f r
x V.:& Rec f rs
xs -> Chain Day Identity f (XRec Identity (r : rs))
-> DivAp f (XRec Identity (r : rs))
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f (XRec Identity (r : rs))
-> DivAp f (XRec Identity (r : rs)))
-> Chain Day Identity f (XRec Identity (r : rs))
-> DivAp f (XRec Identity (r : rs))
forall a b. (a -> b) -> a -> b
$ Day f (Chain Day Identity f) (XRec Identity (r : rs))
-> Chain Day Identity f (XRec Identity (r : rs))
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 (Day f (Chain Day Identity f) (XRec Identity (r : rs))
-> Chain Day Identity f (XRec Identity (r : rs)))
-> Day f (Chain Day Identity f) (XRec Identity (r : rs))
-> Chain Day Identity f (XRec Identity (r : rs))
forall a b. (a -> b) -> a -> b
$ f r
-> Chain Day Identity f (XRec Identity rs)
-> (r -> XRec Identity rs -> XRec Identity (r : rs))
-> (XRec Identity (r : rs) -> (r, XRec Identity rs))
-> Day f (Chain Day Identity f) (XRec Identity (r : rs))
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day
f r
x
(DivAp f (XRec Identity rs)
-> Chain Day Identity f (XRec Identity rs)
forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp (Rec f rs -> DivAp f (XRec Identity rs)
forall (f :: * -> *) (as :: [*]).
Rec f as -> DivAp f (XRec Identity as)
assembleDivApRec Rec f rs
xs))
r -> XRec Identity rs -> XRec Identity (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
HKD f r -> XRec f rs -> XRec f (r : rs)
(V.::&)
XRec Identity (r : rs) -> (r, XRec Identity rs)
forall a (as :: [*]).
XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec
assembleDivAp1Rec
:: Invariant f
=> V.Rec f (a ': as)
-> DivAp1 f (V.XRec V.Identity (a ': as))
assembleDivAp1Rec :: Rec f (a : as) -> DivAp1 f (XRec Identity (a : as))
assembleDivAp1Rec (f r
x V.:& Rec f rs
xs) = case Rec f rs
xs of
Rec f rs
V.RNil -> Chain1 Day f (XRec Identity '[a]) -> DivAp1 f (XRec Identity '[a])
forall (f :: * -> *) a. Chain1 Day f a -> DivAp1 f a
DivAp1_ (Chain1 Day f (XRec Identity '[a])
-> DivAp1 f (XRec Identity '[a]))
-> Chain1 Day f (XRec Identity '[a])
-> DivAp1 f (XRec Identity '[a])
forall a b. (a -> b) -> a -> b
$ f (XRec Identity '[a]) -> Chain1 Day f (XRec Identity '[a])
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
f a -> Chain1 t f a
Done1 (f (XRec Identity '[a]) -> Chain1 Day f (XRec Identity '[a]))
-> f (XRec Identity '[a]) -> Chain1 Day f (XRec Identity '[a])
forall a b. (a -> b) -> a -> b
$ (r -> XRec Identity '[a])
-> (XRec Identity '[a] -> r) -> f r -> f (XRec Identity '[a])
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (HKD Identity a -> Rec (XData Identity) '[] -> XRec Identity '[a]
forall a (f :: a -> *) (r :: a) (rs :: [a]).
HKD f r -> XRec f rs -> XRec f (r : rs)
V.::& Rec (XData Identity) '[]
forall u (a :: u -> *). Rec a '[]
V.RNil) (\case HKD Identity a
z V.::& Rec (XData Identity) '[]
_ -> r
HKD Identity a
z) f r
x
f r
_ V.:& Rec f rs
_ -> Chain1 Day f (XRec Identity (r : r : rs))
-> DivAp1 f (XRec Identity (r : r : rs))
forall (f :: * -> *) a. Chain1 Day f a -> DivAp1 f a
DivAp1_ (Chain1 Day f (XRec Identity (r : r : rs))
-> DivAp1 f (XRec Identity (r : r : rs)))
-> Chain1 Day f (XRec Identity (r : r : rs))
-> DivAp1 f (XRec Identity (r : r : rs))
forall a b. (a -> b) -> a -> b
$ Day f (Chain1 Day f) (XRec Identity (r : r : rs))
-> Chain1 Day f (XRec Identity (r : r : rs))
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 (Day f (Chain1 Day f) (XRec Identity (r : r : rs))
-> Chain1 Day f (XRec Identity (r : r : rs)))
-> Day f (Chain1 Day f) (XRec Identity (r : r : rs))
-> Chain1 Day f (XRec Identity (r : r : rs))
forall a b. (a -> b) -> a -> b
$ f r
-> Chain1 Day f (XRec Identity (r : rs))
-> (r -> XRec Identity (r : rs) -> XRec Identity (r : r : rs))
-> (XRec Identity (r : r : rs) -> (r, XRec Identity (r : rs)))
-> Day f (Chain1 Day f) (XRec Identity (r : r : rs))
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day
f r
x
(DivAp1 f (XRec Identity (r : rs))
-> Chain1 Day f (XRec Identity (r : rs))
forall (f :: * -> *) a. DivAp1 f a -> Chain1 Day f a
unDivAp1 (Rec f (r : rs) -> DivAp1 f (XRec Identity (r : rs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
Rec f (a : as) -> DivAp1 f (XRec Identity (a : as))
assembleDivAp1Rec Rec f rs
Rec f (r : rs)
xs))
r -> XRec Identity (r : rs) -> XRec Identity (r : r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
HKD f r -> XRec f rs -> XRec f (r : rs)
(V.::&)
XRec Identity (r : r : rs) -> (r, XRec Identity (r : rs))
forall a (as :: [*]).
XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec
unconsRec :: V.XRec V.Identity (a ': as) -> (a, V.XRec V.Identity as)
unconsRec :: XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec (HKD Identity a
y V.::& XRec Identity as
ys) = (a
HKD Identity a
y, XRec Identity as
ys)
instance Inply f => Interpret DivAp1 f where
interpret :: (g ~> f) -> DivAp1 g ~> f
interpret g ~> f
f (DivAp1_ Chain1 Day g x
x) = (g ~> f) -> (Day g f ~> f) -> Chain1 Day g x -> f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(g :: k -> *).
HBifunctor t =>
(f ~> g) -> (t f g ~> g) -> Chain1 t f ~> g
foldChain1 g ~> f
f ((g ~> f) -> (f ~> f) -> Day g f ~> f
forall (h :: * -> *) (f :: * -> *) (g :: * -> *).
Inply h =>
(f ~> h) -> (g ~> h) -> Day f g ~> h
runDay g ~> f
f forall a. a -> a
f ~> f
id) Chain1 Day g x
x
instance Inplicative f => Interpret DivAp f where
interpret :: (g ~> f) -> DivAp g ~> f
interpret g ~> f
f (DivAp Chain Day Identity g x
x) = (Identity ~> f) -> (Day g f ~> f) -> Chain Day Identity g x -> f x
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 -> f x
forall (f :: * -> *) a. Inplicative f => a -> f a
knot (x -> f x) -> (Identity x -> x) -> Identity x -> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity x -> x
forall a. Identity a -> a
runIdentity) ((g ~> f) -> (f ~> f) -> Day g f ~> f
forall (h :: * -> *) (f :: * -> *) (g :: * -> *).
Inply h =>
(f ~> h) -> (g ~> h) -> Day f g ~> h
runDay g ~> f
f forall a. a -> a
f ~> f
id) Chain Day Identity g x
x