-- |
-- 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.Chain (
  -- * Chain
    DayChain(.., Gather, Knot)
  , runCoDayChain
  , runContraDayChain
  , chainAp
  , chainDiv
  , gather, gathered
  , assembleDayChain
  , assembleDayChainRec
  , concatDayChain
  , concatDayChainRec
  -- * Nonempty Chain
  , DayChain1(.., DayChain1)
  , runCoDayChain1
  , runContraDayChain1
  , chainAp1
  , chainDiv1
  , gather1, gathered1
  , assembleDayChain1
  , assembleDayChain1Rec
  , concatDayChain1
  , concatDayChain1Rec
  -- * Day Utility
  , runDayApply
  , runDayDivise
  ) 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.HBifunctor.Tensor hiding             (elim1, elim2, intro1, intro2)
import           Data.HFunctor
import           Data.HFunctor.Chain
import           Data.HFunctor.Chain.Internal
import           Data.SOP hiding                           (hmap)
import qualified Data.Vinyl                                as V
import qualified Data.Vinyl.Functor                        as V

-- | 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)

-- | 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) -> 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 ((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) (Chain1 Day f x -> g x)
-> (DayChain1 f x -> Chain1 Day f x) -> DayChain1 f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DayChain1 f x -> Chain1 Day f x
forall (f :: * -> *) a. DayChain1 f a -> Chain1 Day f a
unDayChain1

-- | 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) -> 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 ((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) (Chain1 Day f x -> g x)
-> (DayChain1 f x -> Chain1 Day f x) -> DayChain1 f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DayChain1 f x -> Chain1 Day f x
forall (f :: * -> *) a. DayChain1 f a -> Chain1 Day f a
unDayChain1

-- | 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) -> 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 (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) (\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)
                (Chain Day Identity f x -> g x)
-> (DayChain f x -> Chain Day Identity f x) -> DayChain f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DayChain f x -> Chain Day Identity f x
forall (f :: * -> *) a. DayChain f a -> Chain Day Identity f a
unDayChain

-- | 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) -> 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 (g x -> Identity x -> g x
forall a b. a -> b -> a
const g x
forall (f :: * -> *) a. Divisible f => f a
conquer) (\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)
                    (Chain Day Identity f x -> g x)
-> (DayChain f x -> Chain Day Identity f x) -> DayChain f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DayChain f x -> Chain Day Identity f x
forall (f :: * -> *) a. DayChain f a -> Chain Day Identity f a
unDayChain

-- | 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

-- | 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 <- (unGather_->MaybeF (Just (Day x xs g f)))
  where
    Gather f :: a -> (b, c)
f g :: b -> c -> a
g x :: f b
x xs :: DayChain f c
xs = Chain Day Identity f a -> DayChain f a
forall (f :: * -> *) a. Chain Day Identity f a -> DayChain f a
DayChain (Chain Day Identity f a -> DayChain f a)
-> Chain Day Identity f a -> DayChain 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 (DayChain f c -> Chain Day Identity f c
forall (f :: * -> *) a. DayChain f a -> Chain Day Identity f a
unDayChain DayChain f c
xs) b -> c -> a
g a -> (b, c)
f

unGather_ :: DayChain f ~> MaybeF (Day f (DayChain f))
unGather_ :: DayChain f x -> MaybeF (Day f (DayChain f)) x
unGather_ = \case
  DayChain (More (Day x :: f b
x xs :: Chain Day Identity f c
xs g :: b -> c -> x
g f :: x -> (b, c)
f)) -> Maybe (Day f (DayChain f) x) -> MaybeF (Day f (DayChain f)) x
forall k (f :: k -> *) (a :: k). Maybe (f a) -> MaybeF f a
MaybeF (Maybe (Day f (DayChain f) x) -> MaybeF (Day f (DayChain f)) x)
-> (Day f (DayChain f) x -> Maybe (Day f (DayChain f) x))
-> Day f (DayChain f) x
-> MaybeF (Day f (DayChain f)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Day f (DayChain f) x -> Maybe (Day f (DayChain f) x)
forall a. a -> Maybe a
Just (Day f (DayChain f) x -> MaybeF (Day f (DayChain f)) x)
-> Day f (DayChain f) x -> MaybeF (Day f (DayChain f)) x
forall a b. (a -> b) -> a -> b
$ f b
-> DayChain f c
-> (b -> c -> x)
-> (x -> (b, c))
-> Day f (DayChain 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 -> DayChain f c
forall (f :: * -> *) a. Chain Day Identity f a -> DayChain f a
DayChain Chain Day Identity f c
xs) b -> c -> x
g x -> (b, c)
f
  DayChain (Done _             ) -> Maybe (Day f (DayChain f) x) -> MaybeF (Day f (DayChain f)) x
forall k (f :: k -> *) (a :: k). Maybe (f a) -> MaybeF f a
MaybeF Maybe (Day f (DayChain f) x)
forall a. Maybe a
Nothing

-- | 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 = DayChain (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 <- (coerce splitChain1->Day x xs g f)
  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
-> (b -> c -> a)
-> (a -> (b, c))
-> Day f (DayChain 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 DayChain f c
xs b -> c -> a
g a -> (b, c)
f
{-# COMPLETE DayChain1 #-}

-- | Invariantly combine two 'DayChain's.
--
-- Analogous to 'liftA2' and 'divise'.  If there was some typeclass that
-- represented semigroups on invariant 'Day', this would be the method of
-- that typeclass.
--
-- The identity of this is 'Knot'.
--
-- @since 0.3.4.0
gather
    :: (a -> (b, c))
    -> (b -> c -> a)
    -> DayChain f b
    -> DayChain f c
    -> DayChain f a
gather :: (a -> (b, c))
-> (b -> c -> a) -> DayChain f b -> DayChain f c -> DayChain f a
gather f :: a -> (b, c)
f g :: b -> c -> a
g x :: DayChain f b
x y :: DayChain f c
y = (Day (Chain Day Identity f) (Chain Day Identity f) a
 -> Chain Day Identity f a)
-> Day (DayChain f) (DayChain f) a -> DayChain f a
forall a b. Coercible a b => a -> b
coerce Day (Chain Day Identity f) (Chain Day Identity f) a
-> Chain Day Identity f a
forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
       (f :: * -> *).
Tensor t i =>
t (Chain t i f) (Chain t i f) ~> Chain t i f
appendChain (DayChain f b
-> DayChain f c
-> (b -> c -> a)
-> (a -> (b, c))
-> Day (DayChain f) (DayChain f) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day DayChain f b
x DayChain f c
y b -> c -> a
g a -> (b, c)
f)

-- | Convenient wrapper over 'gather' that simply combines the two options
-- in a tuple.  Analogous to 'divised'.
--
-- @since 0.3.4.0
gathered
    :: DayChain f a
    -> DayChain f b
    -> DayChain f (a, b)
gathered :: DayChain f a -> DayChain f b -> DayChain f (a, b)
gathered = ((a, b) -> (a, b))
-> (a -> b -> (a, b))
-> DayChain f a
-> DayChain f b
-> DayChain f (a, b)
forall a b c (f :: * -> *).
(a -> (b, c))
-> (b -> c -> a) -> DayChain f b -> DayChain f c -> DayChain f a
gather (a, b) -> (a, b)
forall a. a -> a
id (,)

-- | Invariantly combine two 'DayChain1's.
--
-- Analogous to 'liftA2' and 'divise'.  If there was some typeclass that
-- represented semigroups on invariant 'Day', this would be the method of
-- that typeclass.
--
-- @since 0.3.4.0
gather1
    :: Invariant f
    => (a -> (b, c))
    -> (b -> c -> a)
    -> DayChain1 f b
    -> DayChain1 f c
    -> DayChain1 f a
gather1 :: (a -> (b, c))
-> (b -> c -> a) -> DayChain1 f b -> DayChain1 f c -> DayChain1 f a
gather1 f :: a -> (b, c)
f g :: b -> c -> a
g x :: DayChain1 f b
x y :: DayChain1 f c
y = (Day (Chain1 Day f) (Chain1 Day f) a -> Chain1 Day f a)
-> Day (DayChain1 f) (DayChain1 f) a -> DayChain1 f a
forall a b. Coercible a b => a -> b
coerce Day (Chain1 Day f) (Chain1 Day f) a -> Chain1 Day f a
forall (t :: (* -> *) -> (* -> *) -> * -> *) (f :: * -> *).
(Associative t, FunctorBy t f) =>
t (Chain1 t f) (Chain1 t f) ~> Chain1 t f
appendChain1 (DayChain1 f b
-> DayChain1 f c
-> (b -> c -> a)
-> (a -> (b, c))
-> Day (DayChain1 f) (DayChain1 f) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day DayChain1 f b
x DayChain1 f c
y b -> c -> a
g a -> (b, c)
f)

-- | Convenient wrapper over 'gather1' that simply combines the two options
-- in a tuple.  Analogous to 'divised'.
--
-- @since 0.3.4.0
gathered1
    :: Invariant f
    => DayChain1 f a
    -> DayChain1 f b
    -> DayChain1 f (a, b)
gathered1 :: DayChain1 f a -> DayChain1 f b -> DayChain1 f (a, b)
gathered1 = ((a, b) -> (a, b))
-> (a -> b -> (a, b))
-> DayChain1 f a
-> DayChain1 f b
-> DayChain1 f (a, b)
forall (f :: * -> *) a b c.
Invariant f =>
(a -> (b, c))
-> (b -> c -> a) -> DayChain1 f b -> DayChain1 f c -> DayChain1 f a
gather1 (a, b) -> (a, b)
forall a. a -> a
id (,)

-- | 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     -> Chain Day Identity f (NP I '[]) -> DayChain f (NP I as)
forall (f :: * -> *) a. Chain Day Identity f a -> DayChain f a
DayChain (Chain Day Identity f (NP I '[]) -> DayChain f (NP I as))
-> Chain Day Identity f (NP I '[]) -> DayChain f (NP I as)
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
    x :: f x
x :* xs :: NP f xs
xs -> Chain Day Identity f (NP I (x : xs)) -> DayChain f (NP I as)
forall (f :: * -> *) a. Chain Day Identity f a -> DayChain f a
DayChain (Chain Day Identity f (NP I (x : xs)) -> DayChain f (NP I as))
-> Chain Day Identity f (NP I (x : xs)) -> DayChain f (NP I as)
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
      (DayChain f (NP I xs) -> Chain Day Identity f (NP I xs)
forall (f :: * -> *) a. DayChain f a -> Chain Day Identity f a
unDayChain (NP f xs -> DayChain f (NP I xs)
forall (f :: * -> *) (as :: [*]). NP f as -> DayChain f (NP I as)
assembleDayChain NP f xs
xs))
      x -> NP I xs -> NP I (x : xs)
forall a (as :: [*]). a -> NP I as -> NP I (a : as)
consNPI
      NP I (x : xs) -> (x, NP I xs)
forall a (as :: [*]). NP I (a : as) -> (a, NP I as)
unconsNPI

-- | 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     -> Chain Day Identity f (NP I '[]) -> DayChain f (NP I as)
forall (f :: * -> *) a. Chain Day Identity f a -> DayChain f a
DayChain (Chain Day Identity f (NP I '[]) -> DayChain f (NP I as))
-> Chain Day Identity f (NP I '[]) -> DayChain f (NP I as)
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
    x :: DayChain f x
x :* xs :: NP (DayChain f) xs
xs -> (Day (Chain Day Identity f) (Chain Day Identity f) (NP I (x : xs))
 -> Chain Day Identity f (NP I (x : xs)))
-> Day (DayChain f) (DayChain f) (NP I (x : xs))
-> DayChain f (NP I as)
forall a b. Coercible a b => a -> b
coerce Day (Chain Day Identity f) (Chain Day Identity f) (NP I (x : xs))
-> Chain Day Identity f (NP I (x : xs))
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
-> DayChain f (NP I xs)
-> (x -> NP I xs -> NP I (x : xs))
-> (NP I (x : xs) -> (x, NP I xs))
-> Day (DayChain f) (DayChain 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
      DayChain f x
x
      (NP (DayChain f) xs -> DayChain f (NP I xs)
forall (f :: * -> *) (as :: [*]).
NP (DayChain f) as -> DayChain f (NP I as)
concatDayChain NP (DayChain f) xs
xs)
      x -> NP I xs -> NP I (x : xs)
forall a (as :: [*]). a -> NP I as -> NP I (a : as)
consNPI
      NP I (x : xs) -> (x, NP I xs)
forall a (as :: [*]). NP I (a : as) -> (a, NP I as)
unconsNPI

-- | 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 -> Chain1 Day f (NP I (a : as)) -> DayChain1 f (NP I (a : as))
forall (f :: * -> *) a. Chain1 Day f a -> DayChain1 f a
DayChain1_ (Chain1 Day f (NP I (a : as)) -> DayChain1 f (NP I (a : as)))
-> Chain1 Day f (NP I (a : as)) -> DayChain1 f (NP I (a : as))
forall a b. (a -> b) -> a -> b
$ case NP f xs
xs of
      Nil    -> f (NP I '[x]) -> Chain1 Day 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]) -> Chain1 Day f (NP I (a : as)))
-> f (NP I '[x]) -> Chain1 Day 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))
-> Chain1 Day 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))
 -> Chain1 Day f (NP I (a : as)))
-> Day f (Chain1 Day f) (NP I (x : x : xs))
-> Chain1 Day f (NP I (a : as))
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
        (DayChain1 f (NP I (x : xs)) -> Chain1 Day f (NP I (x : xs))
forall (f :: * -> *) a. DayChain1 f a -> Chain1 Day f a
unDayChain1 (NP f (x : xs) -> DayChain1 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))
        x -> NP I (x : xs) -> NP I (x : x : xs)
forall a (as :: [*]). a -> NP I as -> NP I (a : as)
consNPI
        NP I (x : x : xs) -> (x, NP I (x : xs))
forall a (as :: [*]). NP I (a : as) -> (a, NP I as)
unconsNPI

-- | 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 -> DayChain1 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 (Chain1 Day f) (Chain1 Day f) (NP I (a : x : xs))
 -> Chain1 Day f (NP I (a : x : xs)))
-> Day (DayChain1 f) (DayChain1 f) (NP I (x : x : xs))
-> DayChain1 f (NP I (a : as))
forall a b. Coercible a b => a -> b
coerce Day (Chain1 Day f) (Chain1 Day f) (NP I (a : x : xs))
-> Chain1 Day f (NP I (a : x : xs))
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
-> DayChain1 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 (DayChain1 f) (DayChain1 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
        DayChain1 f x
x
        (NP (DayChain1 f) (x : xs) -> DayChain1 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)
        x -> NP I (x : xs) -> NP I (x : x : xs)
forall a (as :: [*]). a -> NP I as -> NP I (a : as)
consNPI
        NP I (x : x : xs) -> (x, NP I (x : xs))
forall a (as :: [*]). NP I (a : as) -> (a, NP I as)
unconsNPI

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    -> Chain Day Identity f (Rec (XData Identity) '[])
-> DayChain f (XRec Identity as)
forall (f :: * -> *) a. Chain Day Identity f a -> DayChain f a
DayChain (Chain Day Identity f (Rec (XData Identity) '[])
 -> DayChain f (XRec Identity as))
-> Chain Day Identity f (Rec (XData Identity) '[])
-> DayChain f (XRec Identity as)
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
    x :: f r
x V.:& xs :: Rec f rs
xs -> Chain Day Identity f (XRec Identity (r : rs))
-> DayChain f (XRec Identity as)
forall (f :: * -> *) a. Chain Day Identity f a -> DayChain f a
DayChain (Chain Day Identity f (XRec Identity (r : rs))
 -> DayChain f (XRec Identity as))
-> Chain Day Identity f (XRec Identity (r : rs))
-> DayChain f (XRec Identity as)
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
      (DayChain f (XRec Identity rs)
-> Chain Day Identity f (XRec Identity rs)
forall (f :: * -> *) a. DayChain f a -> Chain Day Identity f a
unDayChain (Rec f rs -> DayChain f (XRec Identity rs)
forall (f :: * -> *) (as :: [*]).
Rec f as -> DayChain f (XRec Identity as)
assembleDayChainRec 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

-- | 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    -> Chain Day Identity f (Rec (XData Identity) '[])
-> DayChain f (XRec Identity as)
forall (f :: * -> *) a. Chain Day Identity f a -> DayChain f a
DayChain (Chain Day Identity f (Rec (XData Identity) '[])
 -> DayChain f (XRec Identity as))
-> Chain Day Identity f (Rec (XData Identity) '[])
-> DayChain f (XRec Identity as)
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
    x :: DayChain f r
x V.:& xs :: Rec (DayChain f) rs
xs -> (Day
   (Chain Day Identity f)
   (Chain Day Identity f)
   (XRec Identity (r : rs))
 -> Chain Day Identity f (XRec Identity (r : rs)))
-> Day (DayChain f) (DayChain f) (XRec Identity (r : rs))
-> DayChain f (XRec Identity as)
forall a b. Coercible a b => a -> b
coerce Day
  (Chain Day Identity f)
  (Chain Day Identity f)
  (XRec Identity (r : rs))
-> Chain Day Identity f (XRec Identity (r : rs))
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
-> DayChain f (XRec Identity rs)
-> (r -> XRec Identity rs -> XRec Identity (r : rs))
-> (XRec Identity (r : rs) -> (r, XRec Identity rs))
-> Day (DayChain f) (DayChain 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
      DayChain f r
x
      (Rec (DayChain f) rs -> DayChain f (XRec Identity rs)
forall (f :: * -> *) (as :: [*]).
Rec (DayChain f) as -> DayChain f (XRec Identity as)
concatDayChainRec Rec (DayChain 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

-- | 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   -> Chain1 Day f (XRec Identity '[a])
-> DayChain1 f (XRec Identity (a : as))
forall (f :: * -> *) a. Chain1 Day f a -> DayChain1 f a
DayChain1_ (Chain1 Day f (XRec Identity '[a])
 -> DayChain1 f (XRec Identity (a : as)))
-> Chain1 Day f (XRec Identity '[a])
-> DayChain1 f (XRec Identity (a : as))
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 z :: HKD Identity a
z V.::& _ -> r
HKD Identity a
z) f r
x
      _ V.:& _ -> Chain1 Day f (XRec Identity (r : r : rs))
-> DayChain1 f (XRec Identity (a : as))
forall (f :: * -> *) a. Chain1 Day f a -> DayChain1 f a
DayChain1_ (Chain1 Day f (XRec Identity (r : r : rs))
 -> DayChain1 f (XRec Identity (a : as)))
-> Chain1 Day f (XRec Identity (r : r : rs))
-> DayChain1 f (XRec Identity (a : as))
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
        (DayChain1 f (XRec Identity (r : rs))
-> Chain1 Day f (XRec Identity (r : rs))
forall (f :: * -> *) a. DayChain1 f a -> Chain1 Day f a
unDayChain1 (Rec f (r : rs) -> DayChain1 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))
        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

-- | 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
-> DayChain1 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 (Chain1 Day f) (Chain1 Day f) (XRec Identity (a : r : rs))
 -> Chain1 Day f (XRec Identity (a : r : rs)))
-> Day (DayChain1 f) (DayChain1 f) (XRec Identity (r : r : rs))
-> DayChain1 f (XRec Identity (a : as))
forall a b. Coercible a b => a -> b
coerce Day (Chain1 Day f) (Chain1 Day f) (XRec Identity (a : r : rs))
-> Chain1 Day f (XRec Identity (a : r : rs))
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
-> DayChain1 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 (DayChain1 f) (DayChain1 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
        DayChain1 f r
x
        (Rec (DayChain1 f) (r : rs) -> DayChain1 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)
        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 (y :: HKD Identity a
y V.::& ys :: XRec Identity as
ys) = (a
HKD Identity a
y, XRec Identity as
ys)