module Data.Functor.Invariant.Day (
Day(..)
, day
, runDayApply
, runDayDivise
, toCoDay
, toContraDay
, assoc, unassoc
, intro1, intro2
, elim1, elim2
, swapped
, trans1, trans2
, DayChain
, pattern Gather, pattern Knot
, runCoDayChain
, runContraDayChain
, chainAp
, chainDiv
, assembleDayChain
, assembleDayChainRec
, concatDayChain
, concatDayChainRec
, DayChain1
, pattern DayChain1
, runCoDayChain1
, runContraDayChain1
, chainAp1
, chainDiv1
, assembleDayChain1
, assembleDayChain1Rec
, concatDayChain1
, concatDayChain1Rec
) where
import Control.Applicative
import Control.Applicative.Free (Ap)
import Control.Natural
import Control.Natural.IsoF
import Data.Bifunctor
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.HBifunctor
import Data.HBifunctor.Associative hiding (assoc)
import Data.HBifunctor.Tensor hiding (elim1, elim2, intro1, intro2)
import Data.HFunctor
import Data.HFunctor.Chain
import Data.Kind
import Data.SOP
import GHC.Generics
import qualified Data.Bifunctor.Assoc as B
import qualified Data.Bifunctor.Swap as B
import qualified Data.Functor.Contravariant.Day as CD
import qualified Data.Functor.Day as D
import qualified Data.HBifunctor.Tensor as T
import qualified Data.Vinyl as V
import qualified Data.Vinyl.Functor as V
data Day :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
Day :: f b
-> g c
-> (a -> (b, c))
-> (b -> c -> a)
-> Day f g a
day :: f a -> g b -> Day f g (a, b)
day :: f a -> g b -> Day f g (a, b)
day x :: f a
x y :: g b
y = f a
-> g b
-> ((a, b) -> (a, b))
-> (a -> b -> (a, b))
-> Day f g (a, b)
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day f a
x g b
y (a, b) -> (a, b)
forall a. a -> a
id (,)
runDayApply
:: forall f g h. Apply h
=> f ~> h
-> g ~> h
-> Day f g ~> h
runDayApply :: (f ~> h) -> (g ~> h) -> Day f g ~> h
runDayApply f :: f ~> h
f g :: g ~> h
g (Day x :: f b
x y :: g c
y _ j :: b -> c -> x
j) = (b -> c -> x) -> h b -> h c -> h x
forall (f :: * -> *) a b c.
Apply f =>
(a -> b -> c) -> f a -> f b -> f c
liftF2 b -> c -> x
j (f b -> h b
f ~> h
f f b
x) (g c -> h c
g ~> h
g g c
y)
runDayDivise
:: forall f g h. Divise h
=> f ~> h
-> g ~> h
-> Day f g ~> h
runDayDivise :: (f ~> h) -> (g ~> h) -> Day f g ~> h
runDayDivise f :: f ~> h
f g :: g ~> h
g (Day x :: f b
x y :: g c
y h :: x -> (b, c)
h _) = (x -> (b, c)) -> h b -> h c -> h x
forall (f :: * -> *) a b c.
Divise f =>
(a -> (b, c)) -> f b -> f c -> f a
divise x -> (b, c)
h (f b -> h b
f ~> h
f f b
x) (g c -> h c
g ~> h
g g c
y)
toCoDay :: Day f g ~> D.Day f g
toCoDay :: Day f g x -> Day f g x
toCoDay (Day x :: f b
x y :: g c
y _ g :: b -> c -> x
g) = f b -> g c -> (b -> c -> x) -> Day f g x
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> Day f g a
D.Day f b
x g c
y b -> c -> x
g
toContraDay :: Day f g ~> CD.Day f g
toContraDay :: Day f g x -> Day f g x
toContraDay (Day x :: f b
x y :: g c
y f :: x -> (b, c)
f _) = f b -> g c -> (x -> (b, c)) -> Day f g x
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
CD.Day f b
x g c
y x -> (b, c)
f
assoc :: Day f (Day g h) ~> Day (Day f g) h
assoc :: Day f (Day g h) x -> Day (Day f g) h x
assoc (Day x :: f b
x (Day y :: g b
y z :: h c
z f :: c -> (b, c)
f g :: b -> c -> c
g) h :: x -> (b, c)
h j :: b -> c -> x
j) =
Day f g (b, b)
-> h c
-> (x -> ((b, b), c))
-> ((b, b) -> c -> x)
-> Day (Day f g) h x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day (f b
-> g b
-> ((b, b) -> (b, b))
-> (b -> b -> (b, b))
-> Day f g (b, b)
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day f b
x g b
y (b, b) -> (b, b)
forall a. a -> a
id (,)) h c
z
((b, (b, c)) -> ((b, b), c)
forall (p :: * -> * -> *) a b c.
Assoc p =>
p a (p b c) -> p (p a b) c
B.unassoc ((b, (b, c)) -> ((b, b), c))
-> (x -> (b, (b, c))) -> x -> ((b, b), c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> (b, c)) -> (b, c) -> (b, (b, c))
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second c -> (b, c)
f ((b, c) -> (b, (b, c))) -> (x -> (b, c)) -> x -> (b, (b, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
h)
(\(a :: b
a,b :: b
b) c :: c
c -> b -> c -> x
j b
a (b -> c -> c
g b
b c
c))
unassoc :: Day (Day f g) h ~> Day f (Day g h)
unassoc :: Day (Day f g) h x -> Day f (Day g h) x
unassoc (Day (Day x :: f b
x y :: g c
y f :: b -> (b, c)
f g :: b -> c -> b
g) z :: h c
z h :: x -> (b, c)
h j :: b -> c -> x
j) =
f b
-> Day g h (c, c)
-> (x -> (b, (c, c)))
-> (b -> (c, c) -> x)
-> Day f (Day g h) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day f b
x (g c
-> h c
-> ((c, c) -> (c, c))
-> (c -> c -> (c, c))
-> Day g h (c, c)
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day g c
y h c
z (c, c) -> (c, c)
forall a. a -> a
id (,))
(((b, c), c) -> (b, (c, c))
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
B.assoc (((b, c), c) -> (b, (c, c)))
-> (x -> ((b, c), c)) -> x -> (b, (c, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> (b, c)) -> (b, c) -> ((b, c), c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> (b, c)
f ((b, c) -> ((b, c), c)) -> (x -> (b, c)) -> x -> ((b, c), c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
h)
(\a :: b
a (b :: c
b, c :: c
c) -> b -> c -> x
j (b -> c -> b
g b
a c
b) c
c)
intro1 :: g ~> Day Identity g
intro1 :: g x -> Day Identity g x
intro1 y :: g x
y = Identity ()
-> g x -> (x -> ((), x)) -> (() -> x -> x) -> Day Identity g x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day (() -> Identity ()
forall a. a -> Identity a
Identity ()) g x
y ((),) ((x -> x) -> () -> x -> x
forall a b. a -> b -> a
const x -> x
forall a. a -> a
id)
intro2 :: f ~> Day f Identity
intro2 :: f x -> Day f Identity x
intro2 x :: f x
x = f x
-> Identity ()
-> (x -> (x, ()))
-> (x -> () -> x)
-> Day f Identity x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day f x
x (() -> Identity ()
forall a. a -> Identity a
Identity ()) (,()) x -> () -> x
forall a b. a -> b -> a
const
elim1 :: Invariant g => Day Identity g ~> g
elim1 :: Day Identity g ~> g
elim1 (Day (Identity x :: b
x) y :: g c
y f :: x -> (b, c)
f g :: b -> c -> x
g) = (c -> x) -> (x -> c) -> g c -> g x
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (b -> c -> x
g b
x) ((b, c) -> c
forall a b. (a, b) -> b
snd ((b, c) -> c) -> (x -> (b, c)) -> x -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) g c
y
elim2 :: Invariant f => Day f Identity ~> f
elim2 :: Day f Identity ~> f
elim2 (Day x :: f b
x (Identity y :: c
y) f :: x -> (b, c)
f g :: b -> c -> x
g) = (b -> x) -> (x -> b) -> f b -> f x
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (b -> c -> x
`g` c
y) ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (x -> (b, c)) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) f b
x
swapped :: Day f g ~> Day g f
swapped :: Day f g x -> Day g f x
swapped (Day x :: f b
x y :: g c
y f :: x -> (b, c)
f g :: b -> c -> x
g) = g c -> f b -> (x -> (c, b)) -> (c -> b -> x) -> Day g f x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day g c
y f b
x ((b, c) -> (c, b)
forall (p :: * -> * -> *) a b. Swap p => p a b -> p b a
B.swap ((b, c) -> (c, b)) -> (x -> (b, c)) -> x -> (c, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) ((b -> c -> x) -> c -> b -> x
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> c -> x
g)
trans1 :: f ~> h -> Day f g ~> Day h g
trans1 :: (f ~> h) -> Day f g ~> Day h g
trans1 f :: f ~> h
f (Day x :: f b
x y :: g c
y g :: x -> (b, c)
g h :: b -> c -> x
h) = h b -> g c -> (x -> (b, c)) -> (b -> c -> x) -> Day h g x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day (f b -> h b
f ~> h
f f b
x) g c
y x -> (b, c)
g b -> c -> x
h
trans2 :: g ~> h -> Day f g ~> Day f h
trans2 :: (g ~> h) -> Day f g ~> Day f h
trans2 f :: g ~> h
f (Day x :: f b
x y :: g c
y g :: x -> (b, c)
g h :: b -> c -> x
h) = f b -> h c -> (x -> (b, c)) -> (b -> c -> x) -> Day f h x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day f b
x (g c -> h c
g ~> h
f g c
y) x -> (b, c)
g b -> c -> x
h
runCoDayChain1
:: forall f g. Apply g
=> f ~> g
-> DayChain1 f ~> g
runCoDayChain1 :: (f ~> g) -> DayChain1 f ~> g
runCoDayChain1 f :: f ~> g
f = (f ~> g) -> (Day f g ~> g) -> DayChain1 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) -> 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)
runContraDayChain1
:: forall f g. Divise g
=> f ~> g
-> DayChain1 f ~> g
runContraDayChain1 :: (f ~> g) -> DayChain1 f ~> g
runContraDayChain1 f :: f ~> g
f = (f ~> g) -> (Day f g ~> g) -> DayChain1 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) -> 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)
runCoDayChain
:: forall f g. Applicative g
=> f ~> g
-> DayChain f ~> g
runCoDayChain :: (f ~> g) -> DayChain f ~> g
runCoDayChain f :: f ~> g
f = (Identity ~> g) -> (Day f g ~> g) -> DayChain 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 (f :: * -> *) a. Applicative f => a -> f a
pure (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) -> Chain Day Identity f x -> g x)
-> (Day f g ~> g) -> Chain Day Identity f x -> g x
forall a b. (a -> b) -> a -> b
$ \case
Day x y _ h -> (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
runContraDayChain
:: forall f g. Divisible g
=> f ~> g
-> DayChain f ~> g
runContraDayChain :: (f ~> g) -> DayChain f ~> g
runContraDayChain f :: f ~> g
f = (Identity ~> g) -> (Day f g ~> g) -> DayChain 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 -> Identity x -> g x
forall a b. a -> b -> a
const g x
forall (f :: * -> *) a. Divisible f => f a
conquer) ((Day f g ~> g) -> Chain Day Identity f x -> g x)
-> (Day f g ~> g) -> Chain Day Identity f x -> g x
forall a b. (a -> b) -> a -> b
$ \case
Day x y 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
chainAp :: DayChain f ~> Ap f
chainAp :: DayChain f x -> Ap f x
chainAp = (f ~> Ap f) -> DayChain f ~> Ap f
forall (f :: * -> *) (g :: * -> *).
Applicative g =>
(f ~> g) -> DayChain f ~> g
runCoDayChain f ~> Ap f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
chainAp1 :: DayChain1 f ~> Ap1 f
chainAp1 :: DayChain1 f x -> Ap1 f x
chainAp1 = (f ~> Ap1 f) -> DayChain1 f ~> Ap1 f
forall (f :: * -> *) (g :: * -> *).
Apply g =>
(f ~> g) -> DayChain1 f ~> g
runCoDayChain1 f ~> Ap1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
chainDiv :: DayChain f ~> Div f
chainDiv :: DayChain f x -> Div f x
chainDiv = (f ~> Div f) -> DayChain f ~> Div f
forall (f :: * -> *) (g :: * -> *).
Divisible g =>
(f ~> g) -> DayChain f ~> g
runContraDayChain f ~> Div f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
chainDiv1 :: DayChain1 f ~> Div1 f
chainDiv1 :: DayChain1 f x -> Div1 f x
chainDiv1 = (f ~> Div1 f) -> DayChain1 f ~> Div1 f
forall (f :: * -> *) (g :: * -> *).
Divise g =>
(f ~> g) -> DayChain1 f ~> g
runContraDayChain1 f ~> Div1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
type DayChain = Chain Day Identity
pattern Gather :: (a -> (b, c)) -> (b -> c -> a) -> f b -> DayChain f c -> DayChain f a
pattern $bGather :: (a -> (b, c))
-> (b -> c -> a) -> f b -> DayChain f c -> DayChain f a
$mGather :: forall r a (f :: * -> *).
DayChain f a
-> (forall b c.
(a -> (b, c)) -> (b -> c -> a) -> f b -> DayChain f c -> r)
-> (Void# -> r)
-> r
Gather f g x xs = More (Day x xs f g)
pattern Knot :: a -> DayChain f a
pattern $bKnot :: a -> DayChain f a
$mKnot :: forall r a (f :: * -> *).
DayChain f a -> (a -> r) -> (Void# -> r) -> r
Knot x = Done (Identity x)
{-# COMPLETE Gather, Knot #-}
pattern DayChain1 :: Invariant f => (a -> (b, c)) -> (b -> c -> a) -> f b -> DayChain f c -> DayChain1 f a
pattern $bDayChain1 :: (a -> (b, c))
-> (b -> c -> a) -> f b -> DayChain f c -> DayChain1 f a
$mDayChain1 :: forall r (f :: * -> *) a.
Invariant f =>
DayChain1 f a
-> (forall b c.
(a -> (b, c)) -> (b -> c -> a) -> f b -> DayChain f c -> r)
-> (Void# -> r)
-> r
DayChain1 f g x xs <- (splitChain1->Day x xs f g)
where
DayChain1 f :: a -> (b, c)
f g :: b -> c -> a
g x :: f b
x xs :: DayChain f c
xs = Day f (ListBy Day f) a -> DayChain1 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 -> DayChain1 f a)
-> Day f (ListBy Day f) a -> DayChain1 f a
forall a b. (a -> b) -> a -> b
$ f b
-> DayChain f c
-> (a -> (b, c))
-> (b -> c -> a)
-> Day f (Chain Day Identity f) a
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day f b
x DayChain f c
xs a -> (b, c)
f b -> c -> a
g
{-# COMPLETE DayChain1 #-}
type DayChain1 = Chain1 Day
instance Invariant (Day f g) where
invmap :: (a -> b) -> (b -> a) -> Day f g a -> Day f g b
invmap f :: a -> b
f g :: b -> a
g (Day x :: f b
x y :: g c
y h :: a -> (b, c)
h j :: b -> c -> a
j) = f b -> g c -> (b -> (b, c)) -> (b -> c -> b) -> Day f g b
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day f b
x g c
y (a -> (b, c)
h (a -> (b, c)) -> (b -> a) -> b -> (b, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
g) (\q :: b
q -> a -> b
f (a -> b) -> (c -> a) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c -> a
j b
q)
instance HFunctor (Day f) where
hmap :: (f ~> g) -> Day f f ~> Day f g
hmap f :: f ~> g
f = (f ~> f) -> (f ~> g) -> Day f f ~> Day f g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(j :: k -> *) (g :: k -> *) (l :: k -> *).
HBifunctor t =>
(f ~> j) -> (g ~> l) -> t f g ~> t j l
hbimap forall a. a -> a
f ~> f
id f ~> g
f
instance HBifunctor Day where
hbimap :: (f ~> j) -> (g ~> l) -> Day f g ~> Day j l
hbimap f :: f ~> j
f g :: g ~> l
g (Day x :: f b
x y :: g c
y h :: x -> (b, c)
h j :: b -> c -> x
j) = j b -> l c -> (x -> (b, c)) -> (b -> c -> x) -> Day j l x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day (f b -> j b
f ~> j
f f b
x) (g c -> l c
g ~> l
g g c
y) x -> (b, c)
h b -> c -> x
j
instance Associative Day where
type NonEmptyBy Day = DayChain1
type FunctorBy Day = Invariant
associating :: Day f (Day g h) <~> Day (Day f g) h
associating = (Day f (Day g h) ~> Day (Day f g) h)
-> (Day (Day f g) h ~> Day f (Day g h))
-> Day f (Day g h) <~> Day (Day f g) h
forall k (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF Day f (Day g h) ~> Day (Day f g) h
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Day f (Day g h) ~> Day (Day f g) h
assoc Day (Day f g) h ~> Day f (Day g h)
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Day (Day f g) h ~> Day f (Day g h)
unassoc
appendNE :: Day (NonEmptyBy Day f) (NonEmptyBy Day f) x -> NonEmptyBy Day f x
appendNE (Day xs :: NonEmptyBy Day f b
xs ys :: NonEmptyBy Day f c
ys f :: x -> (b, c)
f g :: b -> c -> x
g) = case NonEmptyBy Day f b
xs of
Done1 x -> Day f (Chain1 Day f) x -> Chain1 Day f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 (f b
-> Chain1 Day f c
-> (x -> (b, c))
-> (b -> c -> x)
-> Day f (Chain1 Day f) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day f b
x NonEmptyBy Day f c
Chain1 Day f c
ys x -> (b, c)
f b -> c -> x
g)
More1 (Day z zs h j) -> Day f (Chain1 Day f) x -> NonEmptyBy Day f x
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) x -> NonEmptyBy Day f x)
-> Day f (Chain1 Day f) x -> NonEmptyBy Day f x
forall a b. (a -> b) -> a -> b
$
f b
-> Chain1 Day f (c, c)
-> (x -> (b, (c, c)))
-> (b -> (c, c) -> x)
-> Day f (Chain1 Day f) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day f b
z (Day (NonEmptyBy Day f) (NonEmptyBy Day f) (c, c)
-> NonEmptyBy Day f (c, c)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
Associative t =>
t (NonEmptyBy t f) (NonEmptyBy t f) ~> NonEmptyBy t f
appendNE (Chain1 Day f c
-> Chain1 Day f c
-> ((c, c) -> (c, c))
-> (c -> c -> (c, c))
-> Day (Chain1 Day f) (Chain1 Day f) (c, c)
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day Chain1 Day f c
zs NonEmptyBy Day f c
Chain1 Day f c
ys (c, c) -> (c, c)
forall a. a -> a
id (,)))
(((b, c), c) -> (b, (c, c))
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
B.assoc (((b, c), c) -> (b, (c, c)))
-> (x -> ((b, c), c)) -> x -> (b, (c, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> (b, c)) -> (b, c) -> ((b, c), c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> (b, c)
h ((b, c) -> ((b, c), c)) -> (x -> (b, c)) -> x -> ((b, c), c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f)
(\a :: b
a (b :: c
b, c :: c
c) -> b -> c -> x
g (b -> c -> b
j b
a c
b) c
c)
matchNE :: NonEmptyBy Day f ~> (f :+: Day f (NonEmptyBy Day f))
matchNE = NonEmptyBy Day f x -> (:+:) f (Day f (NonEmptyBy Day f)) x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *).
Chain1 t f ~> (f :+: t f (Chain1 t f))
matchChain1
consNE :: Day f (NonEmptyBy Day f) x -> NonEmptyBy Day f x
consNE = Day f (NonEmptyBy Day f) x -> NonEmptyBy Day f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1
toNonEmptyBy :: Day f f x -> NonEmptyBy Day f x
toNonEmptyBy = Day f f x -> NonEmptyBy Day f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *).
HBifunctor t =>
t f f ~> Chain1 t f
toChain1
instance Tensor Day Identity where
type ListBy Day = DayChain
intro1 :: f x -> Day f Identity x
intro1 = f x -> Day f Identity x
forall (f :: * -> *). f ~> Day f Identity
intro2
intro2 :: g x -> Day Identity g x
intro2 = g x -> Day Identity g x
forall (g :: * -> *). g ~> Day Identity g
intro1
elim1 :: Day f Identity ~> f
elim1 = Day f Identity x -> f x
forall (f :: * -> *). Invariant f => Day f Identity ~> f
elim2
elim2 :: Day Identity g ~> g
elim2 = Day Identity g x -> g x
forall (g :: * -> *). Invariant g => Day Identity g ~> g
elim1
appendLB :: Day (ListBy Day f) (ListBy Day f) x -> ListBy Day f x
appendLB = Day (ListBy Day f) (ListBy Day f) x -> ListBy Day f x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t (Chain t i f) (Chain t i f) ~> Chain t i f
appendChain
splitNE :: NonEmptyBy Day f x -> Day f (ListBy Day f) x
splitNE = NonEmptyBy Day f x -> Day f (ListBy Day f) x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
Chain1 t f ~> t f (Chain t i f)
splitChain1
splittingLB :: p ((:+:) Identity (Day f (ListBy Day f)) a)
((:+:) Identity (Day f (ListBy Day f)) a)
-> p (ListBy Day f a) (ListBy Day f a)
splittingLB = p ((:+:) Identity (Day f (ListBy Day f)) a)
((:+:) Identity (Day f (ListBy Day f)) a)
-> p (ListBy Day f a) (ListBy Day f a)
forall k1 k2 (t :: k1 -> (k2 -> *) -> k2 -> *) (i :: k2 -> *)
(f :: k1).
Chain t i f <~> (i :+: t f (Chain t i f))
splittingChain
toListBy :: Day f f x -> ListBy Day f x
toListBy = Day f f x -> ListBy Day f x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t f f ~> Chain t i f
toChain
instance Matchable Day Identity where
unsplitNE :: Day f (ListBy Day f) ~> NonEmptyBy Day f
unsplitNE (Day x :: f b
x xs :: ListBy Day f c
xs f :: x -> (b, c)
f g :: b -> c -> x
g) = case ListBy Day f c
xs of
Done (Identity r) -> f x -> NonEmptyBy Day f x
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
f a -> Chain1 t f a
Done1 (f x -> NonEmptyBy Day f x) -> f x -> NonEmptyBy Day f x
forall a b. (a -> b) -> a -> b
$ (b -> x) -> (x -> b) -> f b -> f x
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (b -> c -> x
`g` c
r) ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (x -> (b, c)) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) f b
x
More ys -> Day f (Chain1 Day f) x -> NonEmptyBy Day f x
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) x -> NonEmptyBy Day f x)
-> Day f (Chain1 Day f) x -> NonEmptyBy Day f x
forall a b. (a -> b) -> a -> b
$ f b
-> Chain1 Day f c
-> (x -> (b, c))
-> (b -> c -> x)
-> Day f (Chain1 Day f) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day f b
x (Day f (ListBy Day f) c -> NonEmptyBy Day f c
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE Day f (ListBy Day f) c
Day f (Chain Day Identity f) c
ys) x -> (b, c)
f b -> c -> x
g
matchLB :: ListBy Day f ~> (Identity :+: NonEmptyBy Day f)
matchLB = \case
Done x -> Identity x -> (:+:) Identity (Chain1 Day f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 Identity x
x
More xs -> Chain1 Day f x -> (:+:) Identity (NonEmptyBy Day f) x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (Chain1 Day f x -> (:+:) Identity (NonEmptyBy Day f) x)
-> Chain1 Day f x -> (:+:) Identity (NonEmptyBy Day f) x
forall a b. (a -> b) -> a -> b
$ Day f (ListBy Day f) x -> NonEmptyBy Day f x
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE Day f (ListBy Day f) x
Day f (Chain Day Identity f) x
xs
assembleDayChain
:: NP f as
-> DayChain f (NP I as)
assembleDayChain :: NP f as -> DayChain f (NP I as)
assembleDayChain = \case
Nil -> Identity (NP I '[]) -> DayChain f (NP I as)
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
i a -> Chain t i f a
Done (Identity (NP I '[]) -> DayChain f (NP I as))
-> Identity (NP I '[]) -> DayChain f (NP I as)
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
x :: f x
x :* xs :: NP f xs
xs -> Day f (Chain Day Identity f) (NP I (x : xs))
-> DayChain f (NP I as)
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))
-> DayChain f (NP I as))
-> Day f (Chain Day Identity f) (NP I (x : xs))
-> DayChain f (NP I as)
forall a b. (a -> b) -> a -> b
$ f x
-> Chain Day Identity f (NP I xs)
-> (NP I (x : xs) -> (x, NP I xs))
-> (x -> NP I xs -> NP I (x : xs))
-> Day f (Chain Day Identity f) (NP I (x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day
f x
x
(NP f xs -> Chain Day Identity f (NP I xs)
forall (f :: * -> *) (as :: [*]). NP f as -> DayChain f (NP I as)
assembleDayChain NP f xs
xs)
NP I (x : xs) -> (x, NP I xs)
forall a (as :: [*]). NP I (a : as) -> (a, NP I as)
unconsNPI
x -> NP I xs -> NP I (x : xs)
forall a (as :: [*]). a -> NP I as -> NP I (a : as)
consNPI
concatDayChain
:: NP (DayChain f) as
-> DayChain f (NP I as)
concatDayChain :: NP (DayChain f) as -> DayChain f (NP I as)
concatDayChain = \case
Nil -> Identity (NP I '[]) -> DayChain f (NP I as)
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
(a :: k).
i a -> Chain t i f a
Done (Identity (NP I '[]) -> DayChain f (NP I as))
-> Identity (NP I '[]) -> DayChain f (NP I as)
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
x :: DayChain f x
x :* xs :: NP (DayChain f) xs
xs -> Day (DayChain f) (DayChain f) (NP I (x : xs))
-> DayChain f (NP I as)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t (Chain t i f) (Chain t i f) ~> Chain t i f
appendChain (Day (DayChain f) (DayChain f) (NP I (x : xs))
-> DayChain f (NP I as))
-> Day (DayChain f) (DayChain f) (NP I (x : xs))
-> DayChain f (NP I as)
forall a b. (a -> b) -> a -> b
$ DayChain f x
-> Chain Day Identity f (NP I xs)
-> (NP I (x : xs) -> (x, NP I xs))
-> (x -> NP I xs -> NP I (x : xs))
-> Day (DayChain f) (DayChain f) (NP I (x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day
DayChain f x
x
(NP (DayChain f) xs -> Chain Day Identity f (NP I xs)
forall (f :: * -> *) (as :: [*]).
NP (DayChain f) as -> DayChain f (NP I as)
concatDayChain NP (DayChain f) xs
xs)
NP I (x : xs) -> (x, NP I xs)
forall a (as :: [*]). NP I (a : as) -> (a, NP I as)
unconsNPI
x -> NP I xs -> NP I (x : xs)
forall a (as :: [*]). a -> NP I as -> NP I (a : as)
consNPI
assembleDayChain1
:: Invariant f
=> NP f (a ': as)
-> DayChain1 f (NP I (a ': as))
assembleDayChain1 :: NP f (a : as) -> DayChain1 f (NP I (a : as))
assembleDayChain1 = \case
x :: f x
x :* xs :: NP f xs
xs -> case NP f xs
xs of
Nil -> f (NP I '[x]) -> DayChain1 f (NP I (a : as))
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
f a -> Chain1 t f a
Done1 (f (NP I '[x]) -> DayChain1 f (NP I (a : as)))
-> f (NP I '[x]) -> DayChain1 f (NP I (a : as))
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
_ :* _ -> Day f (Chain1 Day f) (NP I (x : x : xs))
-> DayChain1 f (NP I (a : as))
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))
-> DayChain1 f (NP I (a : as)))
-> Day f (Chain1 Day f) (NP I (x : x : xs))
-> DayChain1 f (NP I (a : as))
forall a b. (a -> b) -> a -> b
$ f x
-> Chain1 Day f (NP I (x : xs))
-> (NP I (x : x : xs) -> (x, NP I (x : xs)))
-> (x -> NP I (x : xs) -> NP I (x : x : xs))
-> Day f (Chain1 Day f) (NP I (x : x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day
f x
x
(NP f (x : xs) -> Chain1 Day f (NP I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP f (a : as) -> DayChain1 f (NP I (a : as))
assembleDayChain1 NP f xs
NP f (x : xs)
xs)
NP I (x : x : xs) -> (x, NP I (x : xs))
forall a (as :: [*]). NP I (a : as) -> (a, NP I as)
unconsNPI
x -> NP I (x : xs) -> NP I (x : x : xs)
forall a (as :: [*]). a -> NP I as -> NP I (a : as)
consNPI
concatDayChain1
:: Invariant f
=> NP (DayChain1 f) (a ': as)
-> DayChain1 f (NP I (a ': as))
concatDayChain1 :: NP (DayChain1 f) (a : as) -> DayChain1 f (NP I (a : as))
concatDayChain1 = \case
x :: DayChain1 f x
x :* xs :: NP (DayChain1 f) xs
xs -> case NP (DayChain1 f) xs
xs of
Nil -> (x -> NP I '[x])
-> (NP I '[x] -> x) -> DayChain1 f x -> Chain1 Day 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) DayChain1 f x
x
_ :* _ -> Day (DayChain1 f) (DayChain1 f) (NP I (x : x : xs))
-> DayChain1 f (NP I (a : as))
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
(Associative t, FunctorBy t f) =>
t (Chain1 t f) (Chain1 t f) ~> Chain1 t f
appendChain1 (Day (DayChain1 f) (DayChain1 f) (NP I (x : x : xs))
-> DayChain1 f (NP I (a : as)))
-> Day (DayChain1 f) (DayChain1 f) (NP I (x : x : xs))
-> DayChain1 f (NP I (a : as))
forall a b. (a -> b) -> a -> b
$ DayChain1 f x
-> Chain1 Day f (NP I (x : xs))
-> (NP I (x : x : xs) -> (x, NP I (x : xs)))
-> (x -> NP I (x : xs) -> NP I (x : x : xs))
-> Day (DayChain1 f) (DayChain1 f) (NP I (x : x : xs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day
DayChain1 f x
x
(NP (DayChain1 f) (x : xs) -> Chain1 Day f (NP I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP (DayChain1 f) (a : as) -> DayChain1 f (NP I (a : as))
concatDayChain1 NP (DayChain1 f) xs
NP (DayChain1 f) (x : xs)
xs)
NP I (x : x : xs) -> (x, NP I (x : xs))
forall a (as :: [*]). NP I (a : as) -> (a, NP I as)
unconsNPI
x -> NP I (x : xs) -> NP I (x : x : xs)
forall a (as :: [*]). a -> NP I as -> NP I (a : as)
consNPI
unconsNPI :: NP I (a ': as) -> (a, NP I as)
unconsNPI :: NP I (a : as) -> (a, NP I as)
unconsNPI (I y :: x
y :* ys :: NP I xs
ys) = (a
x
y, NP I as
NP I xs
ys)
consNPI :: a -> NP I as -> NP I (a ': as)
consNPI :: a -> NP I as -> NP I (a : as)
consNPI y :: a
y ys :: NP I as
ys = a -> I a
forall a. a -> I a
I a
y I a -> NP I as -> NP I (a : as)
forall k (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I as
ys
assembleDayChainRec
:: V.Rec f as
-> DayChain f (V.XRec V.Identity as)
assembleDayChainRec :: Rec f as -> DayChain f (XRec Identity as)
assembleDayChainRec = \case
V.RNil -> Identity (Rec (XData Identity) '[])
-> DayChain f (XRec Identity as)
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) '[])
-> DayChain f (XRec Identity as))
-> Identity (Rec (XData Identity) '[])
-> DayChain f (XRec Identity as)
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
x :: f r
x V.:& xs :: Rec f rs
xs -> Day f (Chain Day Identity f) (XRec Identity (r : rs))
-> DayChain f (XRec Identity as)
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))
-> DayChain f (XRec Identity as))
-> Day f (Chain Day Identity f) (XRec Identity (r : rs))
-> DayChain f (XRec Identity as)
forall a b. (a -> b) -> a -> b
$ f r
-> Chain Day Identity f (XRec Identity rs)
-> (XRec Identity (r : rs) -> (r, XRec Identity rs))
-> (r -> XRec Identity rs -> XRec Identity (r : rs))
-> Day f (Chain Day Identity f) (XRec Identity (r : rs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day
f r
x
(Rec f rs -> Chain Day Identity f (XRec Identity rs)
forall (f :: * -> *) (as :: [*]).
Rec f as -> DayChain f (XRec Identity as)
assembleDayChainRec Rec f rs
xs)
XRec Identity (r : rs) -> (r, XRec Identity rs)
forall a (as :: [*]).
XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec
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.::&)
concatDayChainRec
:: V.Rec (DayChain f) as
-> DayChain f (V.XRec V.Identity as)
concatDayChainRec :: Rec (DayChain f) as -> DayChain f (XRec Identity as)
concatDayChainRec = \case
V.RNil -> Identity (Rec (XData Identity) '[])
-> DayChain f (XRec Identity as)
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) '[])
-> DayChain f (XRec Identity as))
-> Identity (Rec (XData Identity) '[])
-> DayChain f (XRec Identity as)
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
x :: DayChain f r
x V.:& xs :: Rec (DayChain f) rs
xs -> Day (DayChain f) (DayChain f) (XRec Identity (r : rs))
-> DayChain f (XRec Identity as)
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
Tensor t i =>
t (Chain t i f) (Chain t i f) ~> Chain t i f
appendChain (Day (DayChain f) (DayChain f) (XRec Identity (r : rs))
-> DayChain f (XRec Identity as))
-> Day (DayChain f) (DayChain f) (XRec Identity (r : rs))
-> DayChain f (XRec Identity as)
forall a b. (a -> b) -> a -> b
$ DayChain f r
-> Chain Day Identity f (XRec Identity rs)
-> (XRec Identity (r : rs) -> (r, XRec Identity rs))
-> (r -> XRec Identity rs -> XRec Identity (r : rs))
-> Day (DayChain f) (DayChain f) (XRec Identity (r : rs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day
DayChain f r
x
(Rec (DayChain f) rs -> Chain Day Identity f (XRec Identity rs)
forall (f :: * -> *) (as :: [*]).
Rec (DayChain f) as -> DayChain f (XRec Identity as)
concatDayChainRec Rec (DayChain f) rs
xs)
XRec Identity (r : rs) -> (r, XRec Identity rs)
forall a (as :: [*]).
XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec
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.::&)
assembleDayChain1Rec
:: Invariant f
=> V.Rec f (a ': as)
-> DayChain1 f (V.XRec V.Identity (a ': as))
assembleDayChain1Rec :: Rec f (a : as) -> DayChain1 f (XRec Identity (a : as))
assembleDayChain1Rec = \case
x :: f r
x V.:& xs :: Rec f rs
xs -> case Rec f rs
xs of
V.RNil -> f (XRec Identity '[a]) -> DayChain1 f (XRec Identity (a : as))
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
f a -> Chain1 t f a
Done1 (f (XRec Identity '[a]) -> DayChain1 f (XRec Identity (a : as)))
-> f (XRec Identity '[a]) -> DayChain1 f (XRec Identity (a : as))
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 z :: HKD Identity a
z V.::& _ -> r
HKD Identity a
z) f r
x
_ V.:& _ -> Day f (Chain1 Day f) (XRec Identity (r : r : rs))
-> DayChain1 f (XRec Identity (a : as))
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))
-> DayChain1 f (XRec Identity (a : as)))
-> Day f (Chain1 Day f) (XRec Identity (r : r : rs))
-> DayChain1 f (XRec Identity (a : as))
forall a b. (a -> b) -> a -> b
$ f r
-> Chain1 Day f (XRec Identity (r : rs))
-> (XRec Identity (r : r : rs) -> (r, XRec Identity (r : rs)))
-> (r -> XRec Identity (r : rs) -> XRec Identity (r : r : rs))
-> Day f (Chain1 Day f) (XRec Identity (r : r : rs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day
f r
x
(Rec f (r : rs) -> Chain1 Day f (XRec Identity (r : rs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
Rec f (a : as) -> DayChain1 f (XRec Identity (a : as))
assembleDayChain1Rec Rec f rs
Rec f (r : rs)
xs)
XRec Identity (r : r : rs) -> (r, XRec Identity (r : rs))
forall a (as :: [*]).
XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec
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.::&)
concatDayChain1Rec
:: Invariant f
=> V.Rec (DayChain1 f) (a ': as)
-> DayChain1 f (V.XRec V.Identity (a ': as))
concatDayChain1Rec :: Rec (DayChain1 f) (a : as) -> DayChain1 f (XRec Identity (a : as))
concatDayChain1Rec = \case
x :: DayChain1 f r
x V.:& xs :: Rec (DayChain1 f) rs
xs -> case Rec (DayChain1 f) rs
xs of
V.RNil -> (r -> XRec Identity '[a])
-> (XRec Identity '[a] -> r)
-> DayChain1 f r
-> Chain1 Day 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 z :: HKD Identity a
z V.::& _ -> r
HKD Identity a
z) DayChain1 f r
x
_ V.:& _ -> Day (DayChain1 f) (DayChain1 f) (XRec Identity (r : r : rs))
-> DayChain1 f (XRec Identity (a : as))
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
(Associative t, FunctorBy t f) =>
t (Chain1 t f) (Chain1 t f) ~> Chain1 t f
appendChain1 (Day (DayChain1 f) (DayChain1 f) (XRec Identity (r : r : rs))
-> DayChain1 f (XRec Identity (a : as)))
-> Day (DayChain1 f) (DayChain1 f) (XRec Identity (r : r : rs))
-> DayChain1 f (XRec Identity (a : as))
forall a b. (a -> b) -> a -> b
$ DayChain1 f r
-> Chain1 Day f (XRec Identity (r : rs))
-> (XRec Identity (r : r : rs) -> (r, XRec Identity (r : rs)))
-> (r -> XRec Identity (r : rs) -> XRec Identity (r : r : rs))
-> Day (DayChain1 f) (DayChain1 f) (XRec Identity (r : r : rs))
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> (b, c)) -> (b -> c -> a) -> Day f g a
Day
DayChain1 f r
x
(Rec (DayChain1 f) (r : rs) -> Chain1 Day f (XRec Identity (r : rs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
Rec (DayChain1 f) (a : as) -> DayChain1 f (XRec Identity (a : as))
concatDayChain1Rec Rec (DayChain1 f) rs
Rec (DayChain1 f) (r : rs)
xs)
XRec Identity (r : r : rs) -> (r, XRec Identity (r : rs))
forall a (as :: [*]).
XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec
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.::&)
unconsRec :: V.XRec V.Identity (a ': as) -> (a, V.XRec V.Identity as)
unconsRec :: XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec (y :: HKD Identity a
y V.::& ys :: XRec Identity as
ys) = (a
HKD Identity a
y, XRec Identity as
ys)