-- |
-- Module      : Data.Functor.Invariant.Day
-- Copyright   : (c) Justin Le 2019
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Provides an 'Invariant' version of the typical Haskell Day convolution
-- over tuples.
--
-- @since 0.3.0.0
module Data.Functor.Invariant.Day (
    Day(..)
  , day
  , runDayApply
  , runDayDivise
  , toCoDay
  , toContraDay
  , assoc, unassoc
  , intro1, intro2
  , elim1, elim2
  , swapped
  , trans1, trans2
  -- * Chain
  , DayChain
  , pattern Gather, pattern Knot
  , runCoDayChain
  , runContraDayChain
  , chainAp
  , chainDiv
  , assembleDayChain
  , assembleDayChainRec
  , concatDayChain
  , concatDayChainRec
  -- * Nonempty Chain
  , 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

-- | A pairing of invariant functors to create a new invariant functor that
-- represents the "combination" between the two.
--
-- A @'Day' f g a@ is a invariant "consumer" and "producer" of @a@, and
-- it does this by taking the @a@ and feeding it to both @f@ and @g@, and
-- aggregating back the results.
--
-- For example, if we have @x :: f a@ and @y :: g b@, then @'day' x y ::
-- 'Day' f g (a, b)@.  This is a consumer/producer of @(a, b)@s, and it
-- feeds the @a@ to @x@ and the @b@ to @y@, and tuples the results back
-- together.
--
-- Mathematically, this is a invariant day convolution along a tuple.
data Day :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
    Day :: f b
        -> g c
        -> (a -> (b, c))
        -> (b -> c -> a)
        -> Day f g a

-- | Pair two invariant actions together in a way that tuples together
-- their input/outputs.  The first one will take the 'fst' part of the
-- tuple, and the second one will take the 'snd' part of the tuple.
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 (,)

-- | Interpret the covariant part of a 'Day' into a target context @h@,
-- as long as the context is an instance of 'Apply'.  The 'Apply' is used to
-- combine results back together using '<*>'.
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)

-- | Interpret the contravariant part of a 'Day' into a target context
-- @h@, as long as the context is an instance of 'Divise'.  The 'Divise' is
-- used to split up the input to pass to each of the actions.
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)

-- | Convert an invariant 'Day' into the covariant version, dropping the
-- contravariant part.
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

-- | Convert an invariant 'Day' into the contravariant version, dropping
-- the covariant part.
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

-- | 'Day' is associative.
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))

-- | 'Day' is associative.
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)

-- | The left identity of 'Day' is 'Identity'; this is one side of that
-- isomorphism.
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)

-- | The right identity of 'Day' is 'Identity'; this is one side of that
-- isomorphism.
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

-- | The left identity of 'Day' is 'Identity'; this is one side of that
-- isomorphism.
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

-- | The right identity of 'Day' is 'Identity'; this is one side of that
-- isomorphism.
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

-- | The two sides of a 'Day' can be swapped.
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)

-- | Hoist a function over the left side of a 'Day'.
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

-- | Hoist a function over the right side of a 'Day'.
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

-- | In the covariant direction, we can interpret out of a 'Chain1' of 'Day'
-- into any 'Apply'.
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)

-- | In the contravariant direction, we can interpret out of a 'Chain1' of
-- 'Day' into any 'Divise'.
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)

-- | In the covariant direction, we can interpret out of a 'Chain' of 'Day'
-- into any 'Applicative'.
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

-- | In the contravariant direction, we can interpret out of a 'Chain' of
-- 'Day' into any 'Divisible'.
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

-- | Extract the 'Ap' part out of a 'DayChain', shedding the
-- contravariant bits.
--
-- @since 0.3.2.0
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

-- | Extract the 'Ap1' part out of a 'DayChain1', shedding the
-- contravariant bits.
--
-- @since 0.3.2.0
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

-- | Extract the 'Div' part out of a 'DayChain', shedding the
-- covariant bits.
--
-- @since 0.3.2.0
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

-- | Extract the 'Div1' part out of a 'DayChain1', shedding the
-- covariant bits.
--
-- @since 0.3.2.0
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

-- | Instead of defining yet another separate free monoid like
-- 'Control.Applicative.Free.Ap',
-- 'Data.Functor.Contravariant.Divisible.Free.Div', or
-- 'Data.Functor.Contravariant.Divisible.Free.Dec', we re-use 'Chain'.
--
-- You can assemble values using the combinators in "Data.HFunctor.Chain",
-- and then tear them down/interpret them using 'runCoDayChain' and
-- 'runContraDayChain'.  There is no general invariant interpreter (and so no
-- 'MonoidIn' instance for 'Day') because the typeclasses used to express
-- the target contexts are probably not worth defining given how little the
-- Haskell ecosystem uses invariant functors as an abstraction.
type DayChain  = Chain Day Identity

-- | Match on a non-empty 'DayChain'; contains no @f@s, but only the
-- terminal value.  Analogous to the 'Control.Applicative.Free.Ap'
-- constructor.
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)

-- | Match on an "empty" 'DayChain'; contains no @f@s, but only the
-- terminal value.  Analogous to 'Control.Applicative.Free.Pure'.
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 #-}

-- | Match on a 'DayChain1' to get the head and the rest of the items.
-- Analogous to the 'Data.Functor.Apply.Free.Ap1' constructor.
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 #-}

-- | Instead of defining yet another separate free semigroup like
-- 'Data.Functor.Apply.Free.Ap1',
-- 'Data.Functor.Contravariant.Divisible.Free.Div1', or
-- 'Data.Functor.Contravariant.Divisible.Free.Dec1', we re-use 'Chain1'.
--
-- You can assemble values using the combinators in "Data.HFunctor.Chain",
-- and then tear them down/interpret them using 'runCoDayChain1' and
-- 'runContraDayChain1'.  There is no general invariant interpreter (and so no
-- 'SemigroupIn' instance for 'Day') because the typeclasses used to
-- express the target contexts are probably not worth defining given how
-- little the Haskell ecosystem uses invariant functors as an abstraction.
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

-- | Convenient wrapper to build up a 'DayChain' by providing each
-- component of it.  This makes it much easier to build up longer chains
-- because you would only need to write the splitting/joining functions in
-- one place.
--
-- For example, if you had a data type
--
-- @
-- data MyType = MT Int Bool String
-- @
--
-- and an invariant functor @Prim@ (representing, say, a bidirectional
-- parser, where @Prim Int@ is a bidirectional parser for an 'Int'@),
-- then you could assemble a bidirectional parser for a @MyType@ using:
--
-- @
-- invmap (\(MyType x y z) -> I x :* I y :* I z :* Nil)
--        (\(I x :* I y :* I z :* Nil) -> MyType x y z) $
--   assembleDayChain $ intPrim
--                   :* boolPrim
--                   :* stringPrim
--                   :* Nil
-- @
--
-- Some notes on usefulness depending on how many components you have:
--
-- *    If you have 0 components, use 'Knot' directly.
-- *    If you have 1 component, use 'inject' or 'injectChain' directly.
-- *    If you have 2 components, use 'toListBy' or 'toChain'.
-- *    If you have 3 or more components, these combinators may be useful;
--      otherwise you'd need to manually peel off tuples one-by-one.
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

-- | A version of 'assembleDayChain' where each component is itself
-- a 'DayChain'.
--
-- @
-- assembleDayChain (x :* y :* z :* Nil)
--   = concatDayChain (injectChain x :* injectChain y :* injectChain z :* Nil)
-- @
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

-- | A version of 'assembleDayChain' but for 'DayChain1' instead.  Can be
-- useful if you intend on interpreting it into something with only
-- a 'Divise' or 'Apply' instance, but no 'Divisible' or 'Applicative'.
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

-- | A version of 'concatDayChain' but for 'DayChain1' instead.  Can be
-- useful if you intend on interpreting it into something with only
-- a 'Divise' or 'Apply' instance, but no 'Divisible' or 'Applicative'.
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

-- | A version of 'assembleDayChain' using 'V.XRec' from /vinyl/ instead of
-- 'NP' from /sop-core/.  This can be more convenient because it doesn't
-- require manual unwrapping/wrapping of components.
--
-- @
-- data MyType = MT Int Bool String
--
-- invmap (\(MyType x y z) -> x ::& y ::& z ::& RNil)
--        (\(x ::& y ::& z ::& RNil) -> MyType x y z) $
--   assembleDayChainRec $ intPrim
--                      :& boolPrim
--                      :& stringPrim
--                      :& Nil
-- @
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.::&)

-- | A version of 'concatDayChain' using 'V.XRec' from /vinyl/ instead of
-- 'NP' from /sop-core/.  This can be more convenient because it doesn't
-- require manual unwrapping/wrapping of components.
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.::&)

-- | A version of 'assembleDayChain1' using 'V.XRec' from /vinyl/ instead of
-- 'NP' from /sop-core/.  This can be more convenient because it doesn't
-- require manual unwrapping/wrapping of components.
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.::&)

-- | A version of 'concatDayChain1' using 'V.XRec' from /vinyl/ instead of
-- 'NP' from /sop-core/.  This can be more convenient because it doesn't
-- require manual unwrapping/wrapping of components.
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)