-- |
-- Module      : Data.Functor.Invariant.Day
-- Copyright   : (c) Justin Le 2019
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Provide an invariant functor combinator sequencer, like a combination of
-- 'Ap' and 'Div'.
--
-- @since 0.3.5.0
module Data.Functor.Invariant.DivAp (
  -- * Chain
    DivAp(.., Gather, Knot)
  , runCoDivAp
  , runContraDivAp
  , divApAp
  , divApDiv
  , foldDivAp
  , gather, gathered
  , assembleDivAp
  , assembleDivApRec
  , concatDivAp
  , concatDivApRec
  -- * Nonempty Chain
  , DivAp1(.., DivAp1)
  , runCoDivAp1
  , runContraDivAp1
  , divApAp1
  , divApDiv1
  , foldDivAp1
  , gather1, gathered1
  , assembleDivAp1
  , assembleDivAp1Rec
  , concatDivAp1
  , concatDivAp1Rec
  -- * 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'.
runCoDivAp1
    :: forall f g. Apply g
    => f ~> g
    -> DivAp1 f ~> g
runCoDivAp1 :: (f ~> g) -> DivAp1 f ~> g
runCoDivAp1 f :: f ~> g
f = (f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
foldDivAp1 f ~> g
f ((f ~> g) -> (g ~> g) -> Day f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Apply h =>
(f ~> h) -> (g ~> h) -> Day f g ~> h
runDayApply f ~> g
f forall a. a -> a
g ~> g
id)

-- | In the contravariant direction, we can interpret out of a 'Chain1' of
-- 'Day' into any 'Divise'.
runContraDivAp1
    :: forall f g. Divise g
    => f ~> g
    -> DivAp1 f ~> g
runContraDivAp1 :: (f ~> g) -> DivAp1 f ~> g
runContraDivAp1 f :: f ~> g
f = (f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
foldDivAp1 f ~> g
f ((f ~> g) -> (g ~> g) -> Day f g ~> g
forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Divise h =>
(f ~> h) -> (g ~> h) -> Day f g ~> h
runDayDivise f ~> g
f forall a. a -> a
g ~> g
id)

-- | In the covariant direction, we can interpret out of a 'Chain' of 'Day'
-- into any 'Applicative'.
runCoDivAp
    :: forall f g. Applicative g
    => f ~> g
    -> DivAp f ~> g
runCoDivAp :: (f ~> g) -> DivAp f ~> g
runCoDivAp f :: f ~> g
f = (forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
forall (g :: * -> *) (f :: * -> *).
(forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
foldDivAp forall x. x -> g x
forall (f :: * -> *) a. Applicative f => a -> f a
pure (\case Day x :: f b
x y :: g c
y h :: b -> c -> x
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'.
runContraDivAp
    :: forall f g. Divisible g
    => f ~> g
    -> DivAp f ~> g
runContraDivAp :: (f ~> g) -> DivAp f ~> g
runContraDivAp f :: f ~> g
f = (forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
forall (g :: * -> *) (f :: * -> *).
(forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
foldDivAp (g x -> x -> g x
forall a b. a -> b -> a
const g x
forall (f :: * -> *) a. Divisible f => f a
conquer) (\case Day x :: f b
x y :: g c
y _ g :: x -> (b, c)
g -> (x -> (b, c)) -> g b -> g c -> g x
forall (f :: * -> *) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide x -> (b, c)
g (f b -> g b
f ~> g
f f b
x) g c
y)

-- | General-purpose folder of 'DivAp'.  Provide a way to handle the
-- identity ('pure'/'conquer'/'Knot') and a way to handle a cons
-- ('liftA2'/'divide'/'Gather').
--
-- @since 0.3.5.0
foldDivAp
    :: (forall x. x -> g x)
    -> (Day f g ~> g)
    -> DivAp f ~> g
foldDivAp :: (forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
foldDivAp f :: forall x. x -> g x
f g :: Day f g ~> g
g = (Identity ~> g) -> (Day f g ~> g) -> Chain Day Identity f ~> g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (i :: k -> *)
       (f :: k -> *) (g :: k -> *).
HBifunctor t =>
(i ~> g) -> (t f g ~> g) -> Chain t i f ~> g
foldChain (x -> g x
forall x. x -> g x
f (x -> g x) -> (Identity x -> x) -> Identity x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity x -> x
forall a. Identity a -> a
runIdentity) Day f g ~> g
g (Chain Day Identity f x -> g x)
-> (DivAp f x -> Chain Day Identity f x) -> DivAp f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DivAp f x -> Chain Day Identity f x
forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp

-- | General-purpose folder of 'DivAp1'.  Provide a way to handle the
-- individual leaves and a way to handle a cons ('liftF2/'divise'/'Gather').
--
-- @since 0.3.5.0
foldDivAp1
    :: (f ~> g)
    -> (Day f g ~> g)
    -> DivAp1 f ~> g
foldDivAp1 :: (f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
foldDivAp1 f :: f ~> g
f g :: Day f g ~> g
g = (f ~> g) -> (Day f g ~> g) -> Chain1 Day f ~> g
forall k (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
       (g :: k -> *).
HBifunctor t =>
(f ~> g) -> (t f g ~> g) -> Chain1 t f ~> g
foldChain1 f ~> g
f Day f g ~> g
g (Chain1 Day f x -> g x)
-> (DivAp1 f x -> Chain1 Day f x) -> DivAp1 f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DivAp1 f x -> Chain1 Day f x
forall (f :: * -> *) a. DivAp1 f a -> Chain1 Day f a
unDivAp1





-- | Extract the 'Ap' part out of a 'DivAp', shedding the
-- contravariant bits.
--
-- @since 0.3.2.0
divApAp :: DivAp f ~> Ap f
divApAp :: DivAp f x -> Ap f x
divApAp = (f ~> Ap f) -> DivAp f ~> Ap f
forall (f :: * -> *) (g :: * -> *).
Applicative g =>
(f ~> g) -> DivAp f ~> g
runCoDivAp f ~> Ap f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject

-- | Extract the 'Ap1' part out of a 'DivAp1', shedding the
-- contravariant bits.
--
-- @since 0.3.2.0
divApAp1 :: DivAp1 f ~> Ap1 f
divApAp1 :: DivAp1 f x -> Ap1 f x
divApAp1 = (f ~> Ap1 f) -> DivAp1 f ~> Ap1 f
forall (f :: * -> *) (g :: * -> *).
Apply g =>
(f ~> g) -> DivAp1 f ~> g
runCoDivAp1 f ~> Ap1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject

-- | Extract the 'Div' part out of a 'DivAp', shedding the
-- covariant bits.
--
-- @since 0.3.2.0
divApDiv :: DivAp f ~> Div f
divApDiv :: DivAp f x -> Div f x
divApDiv = (f ~> Div f) -> DivAp f ~> Div f
forall (f :: * -> *) (g :: * -> *).
Divisible g =>
(f ~> g) -> DivAp f ~> g
runContraDivAp f ~> Div f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject

-- | Extract the 'Div1' part out of a 'DivAp1', shedding the
-- covariant bits.
--
-- @since 0.3.2.0
divApDiv1 :: DivAp1 f ~> Div1 f
divApDiv1 :: DivAp1 f x -> Div1 f x
divApDiv1 = (f ~> Div1 f) -> DivAp1 f ~> Div1 f
forall (f :: * -> *) (g :: * -> *).
Divise g =>
(f ~> g) -> DivAp1 f ~> g
runContraDivAp1 f ~> Div1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject

-- | Match on a non-empty 'DivAp'; 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 -> DivAp f c -> DivAp f a
pattern $bGather :: (a -> (b, c)) -> (b -> c -> a) -> f b -> DivAp f c -> DivAp f a
$mGather :: forall r a (f :: * -> *).
DivAp f a
-> (forall b c.
    (a -> (b, c)) -> (b -> c -> a) -> f b -> DivAp 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 :: DivAp f c
xs = Chain Day Identity f a -> DivAp f a
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f a -> DivAp f a)
-> Chain Day Identity f a -> DivAp f a
forall a b. (a -> b) -> a -> b
$ Day f (Chain Day Identity f) a -> Chain Day Identity f a
forall k k (t :: k -> (k -> *) -> k -> *) (i :: k -> *) (f :: k)
       (a :: k).
t f (Chain t i f) a -> Chain t i f a
More (Day f (Chain Day Identity f) a -> Chain Day Identity f a)
-> Day f (Chain Day Identity f) a -> Chain Day Identity f a
forall a b. (a -> b) -> a -> b
$ f b
-> Chain Day Identity f c
-> (b -> c -> a)
-> (a -> (b, c))
-> Day f (Chain Day Identity f) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f b
x (DivAp f c -> Chain Day Identity f c
forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp DivAp f c
xs) b -> c -> a
g a -> (b, c)
f

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

-- | Match on an "empty" 'DivAp'; contains no @f@s, but only the
-- terminal value.  Analogous to 'Control.Applicative.Free.Pure'.
pattern Knot :: a -> DivAp f a
pattern $bKnot :: a -> DivAp f a
$mKnot :: forall r a (f :: * -> *).
DivAp f a -> (a -> r) -> (Void# -> r) -> r
Knot x = DivAp (Done (Identity x))
{-# COMPLETE Gather, Knot #-}

-- | Match on a 'DivAp1' to get the head and the rest of the items.
-- Analogous to the 'Data.Functor.Apply.Free.Ap1' constructor.
pattern DivAp1 :: Invariant f => (a -> (b, c)) -> (b -> c -> a) -> f b -> DivAp f c -> DivAp1 f a
pattern $bDivAp1 :: (a -> (b, c)) -> (b -> c -> a) -> f b -> DivAp f c -> DivAp1 f a
$mDivAp1 :: forall r (f :: * -> *) a.
Invariant f =>
DivAp1 f a
-> (forall b c.
    (a -> (b, c)) -> (b -> c -> a) -> f b -> DivAp f c -> r)
-> (Void# -> r)
-> r
DivAp1 f g x xs <- (coerce splitChain1->Day x xs g f)
  where
    DivAp1 f :: a -> (b, c)
f g :: b -> c -> a
g x :: f b
x xs :: DivAp f c
xs = Day f (ListBy Day f) a -> DivAp1 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 -> DivAp1 f a)
-> Day f (ListBy Day f) a -> DivAp1 f a
forall a b. (a -> b) -> a -> b
$ f b
-> DivAp f c -> (b -> c -> a) -> (a -> (b, c)) -> Day f (DivAp f) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f b
x DivAp f c
xs b -> c -> a
g a -> (b, c)
f
{-# COMPLETE DivAp1 #-}

-- | Invariantly combine two 'DivAp'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)
    -> DivAp f b
    -> DivAp f c
    -> DivAp f a
gather :: (a -> (b, c))
-> (b -> c -> a) -> DivAp f b -> DivAp f c -> DivAp f a
gather f :: a -> (b, c)
f g :: b -> c -> a
g x :: DivAp f b
x y :: DivAp f c
y = (Day (Chain Day Identity f) (Chain Day Identity f) a
 -> Chain Day Identity f a)
-> Day (DivAp f) (DivAp f) a -> DivAp 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 (DivAp f b
-> DivAp f c
-> (b -> c -> a)
-> (a -> (b, c))
-> Day (DivAp f) (DivAp f) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day DivAp f b
x DivAp 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
    :: DivAp f a
    -> DivAp f b
    -> DivAp f (a, b)
gathered :: DivAp f a -> DivAp f b -> DivAp f (a, b)
gathered = ((a, b) -> (a, b))
-> (a -> b -> (a, b)) -> DivAp f a -> DivAp f b -> DivAp f (a, b)
forall a b c (f :: * -> *).
(a -> (b, c))
-> (b -> c -> a) -> DivAp f b -> DivAp f c -> DivAp f a
gather (a, b) -> (a, b)
forall a. a -> a
id (,)

-- | Invariantly combine two 'DivAp1'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)
    -> DivAp1 f b
    -> DivAp1 f c
    -> DivAp1 f a
gather1 :: (a -> (b, c))
-> (b -> c -> a) -> DivAp1 f b -> DivAp1 f c -> DivAp1 f a
gather1 f :: a -> (b, c)
f g :: b -> c -> a
g x :: DivAp1 f b
x y :: DivAp1 f c
y = (Day (Chain1 Day f) (Chain1 Day f) a -> Chain1 Day f a)
-> Day (DivAp1 f) (DivAp1 f) a -> DivAp1 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 (DivAp1 f b
-> DivAp1 f c
-> (b -> c -> a)
-> (a -> (b, c))
-> Day (DivAp1 f) (DivAp1 f) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day DivAp1 f b
x DivAp1 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
    => DivAp1 f a
    -> DivAp1 f b
    -> DivAp1 f (a, b)
gathered1 :: DivAp1 f a -> DivAp1 f b -> DivAp1 f (a, b)
gathered1 = ((a, b) -> (a, b))
-> (a -> b -> (a, b))
-> DivAp1 f a
-> DivAp1 f b
-> DivAp1 f (a, b)
forall (f :: * -> *) a b c.
Invariant f =>
(a -> (b, c))
-> (b -> c -> a) -> DivAp1 f b -> DivAp1 f c -> DivAp1 f a
gather1 (a, b) -> (a, b)
forall a. a -> a
id (,)

-- | Convenient wrapper to build up a 'DivAp' 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) $
--   assembleDivAp $ 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.
assembleDivAp
    :: NP f as
    -> DivAp f (NP I as)
assembleDivAp :: NP f as -> DivAp f (NP I as)
assembleDivAp = \case
    Nil     -> Chain Day Identity f (NP I '[]) -> DivAp f (NP I as)
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f (NP I '[]) -> DivAp f (NP I as))
-> Chain Day Identity f (NP I '[]) -> DivAp 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)) -> DivAp f (NP I as)
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f (NP I (x : xs)) -> DivAp f (NP I as))
-> Chain Day Identity f (NP I (x : xs)) -> DivAp 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
      (DivAp f (NP I xs) -> Chain Day Identity f (NP I xs)
forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp (NP f xs -> DivAp f (NP I xs)
forall (f :: * -> *) (as :: [*]). NP f as -> DivAp f (NP I as)
assembleDivAp NP f xs
xs))
      x -> 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 'assembleDivAp' where each component is itself
-- a 'DivAp'.
--
-- @
-- assembleDivAp (x :* y :* z :* Nil)
--   = concatDivAp (injectChain x :* injectChain y :* injectChain z :* Nil)
-- @
concatDivAp
    :: NP (DivAp f) as
    -> DivAp f (NP I as)
concatDivAp :: NP (DivAp f) as -> DivAp f (NP I as)
concatDivAp = \case
    Nil     -> Chain Day Identity f (NP I '[]) -> DivAp f (NP I as)
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f (NP I '[]) -> DivAp f (NP I as))
-> Chain Day Identity f (NP I '[]) -> DivAp 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 :: DivAp f x
x :* xs :: NP (DivAp 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 (DivAp f) (DivAp f) (NP I (x : xs)) -> DivAp 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 (DivAp f) (DivAp f) (NP I (x : xs)) -> DivAp f (NP I as))
-> Day (DivAp f) (DivAp f) (NP I (x : xs)) -> DivAp f (NP I as)
forall a b. (a -> b) -> a -> b
$ DivAp f x
-> DivAp f (NP I xs)
-> (x -> NP I xs -> NP I (x : xs))
-> (NP I (x : xs) -> (x, NP I xs))
-> Day (DivAp f) (DivAp 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
      DivAp f x
x
      (NP (DivAp f) xs -> DivAp f (NP I xs)
forall (f :: * -> *) (as :: [*]).
NP (DivAp f) as -> DivAp f (NP I as)
concatDivAp NP (DivAp 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 'assembleDivAp' but for 'DivAp1' instead.  Can be
-- useful if you intend on interpreting it into something with only
-- a 'Divise' or 'Apply' instance, but no 'Divisible' or 'Applicative'.
assembleDivAp1
    :: Invariant f
    => NP f (a ': as)
    -> DivAp1 f (NP I (a ': as))
assembleDivAp1 :: NP f (a : as) -> DivAp1 f (NP I (a : as))
assembleDivAp1 = \case
    x :: f x
x :* xs :: NP f xs
xs -> Chain1 Day f (NP I (a : as)) -> DivAp1 f (NP I (a : as))
forall (f :: * -> *) a. Chain1 Day f a -> DivAp1 f a
DivAp1_ (Chain1 Day f (NP I (a : as)) -> DivAp1 f (NP I (a : as)))
-> Chain1 Day f (NP I (a : as)) -> DivAp1 f (NP I (a : as))
forall a b. (a -> b) -> a -> b
$ case NP f xs
xs of
      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
        (DivAp1 f (NP I (x : xs)) -> Chain1 Day f (NP I (x : xs))
forall (f :: * -> *) a. DivAp1 f a -> Chain1 Day f a
unDivAp1 (NP f (x : xs) -> DivAp1 f (NP I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP f (a : as) -> DivAp1 f (NP I (a : as))
assembleDivAp1 NP f xs
NP f (x : xs)
xs))
        x -> 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 'concatDivAp' but for 'DivAp1' instead.  Can be
-- useful if you intend on interpreting it into something with only
-- a 'Divise' or 'Apply' instance, but no 'Divisible' or 'Applicative'.
concatDivAp1
    :: Invariant f
    => NP (DivAp1 f) (a ': as)
    -> DivAp1 f (NP I (a ': as))
concatDivAp1 :: NP (DivAp1 f) (a : as) -> DivAp1 f (NP I (a : as))
concatDivAp1 = \case
    x :: DivAp1 f x
x :* xs :: NP (DivAp1 f) xs
xs -> case NP (DivAp1 f) xs
xs of
      Nil    -> (x -> NP I '[x])
-> (NP I '[x] -> x) -> DivAp1 f x -> DivAp1 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) DivAp1 f x
x
      _ :* _ -> (Day (Chain1 Day f) (Chain1 Day f) (NP I (a : x : xs))
 -> Chain1 Day f (NP I (a : x : xs)))
-> Day (DivAp1 f) (DivAp1 f) (NP I (x : x : xs))
-> DivAp1 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 (DivAp1 f) (DivAp1 f) (NP I (x : x : xs))
 -> DivAp1 f (NP I (a : as)))
-> Day (DivAp1 f) (DivAp1 f) (NP I (x : x : xs))
-> DivAp1 f (NP I (a : as))
forall a b. (a -> b) -> a -> b
$ DivAp1 f x
-> DivAp1 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 (DivAp1 f) (DivAp1 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
        DivAp1 f x
x
        (NP (DivAp1 f) (x : xs) -> DivAp1 f (NP I (x : xs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP (DivAp1 f) (a : as) -> DivAp1 f (NP I (a : as))
concatDivAp1 NP (DivAp1 f) xs
NP (DivAp1 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 'assembleDivAp' 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) $
--   assembleDivApRec $ intPrim
--                      :& boolPrim
--                      :& stringPrim
--                      :& Nil
-- @
assembleDivApRec
    :: V.Rec f as
    -> DivAp f (V.XRec V.Identity as)
assembleDivApRec :: Rec f as -> DivAp f (XRec Identity as)
assembleDivApRec = \case
    V.RNil    -> Chain Day Identity f (Rec (XData Identity) '[])
-> DivAp f (XRec Identity as)
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f (Rec (XData Identity) '[])
 -> DivAp f (XRec Identity as))
-> Chain Day Identity f (Rec (XData Identity) '[])
-> DivAp 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))
-> DivAp f (XRec Identity as)
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f (XRec Identity (r : rs))
 -> DivAp f (XRec Identity as))
-> Chain Day Identity f (XRec Identity (r : rs))
-> DivAp 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
      (DivAp f (XRec Identity rs)
-> Chain Day Identity f (XRec Identity rs)
forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp (Rec f rs -> DivAp f (XRec Identity rs)
forall (f :: * -> *) (as :: [*]).
Rec f as -> DivAp f (XRec Identity as)
assembleDivApRec Rec f rs
xs))
      r -> XRec Identity rs -> XRec Identity (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
HKD f r -> XRec f rs -> XRec f (r : rs)
(V.::&)
      XRec Identity (r : rs) -> (r, XRec Identity rs)
forall a (as :: [*]).
XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec

-- | A version of 'concatDivAp' 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.
concatDivApRec
    :: V.Rec (DivAp f) as
    -> DivAp f (V.XRec V.Identity as)
concatDivApRec :: Rec (DivAp f) as -> DivAp f (XRec Identity as)
concatDivApRec = \case
    V.RNil    -> Chain Day Identity f (Rec (XData Identity) '[])
-> DivAp f (XRec Identity as)
forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp (Chain Day Identity f (Rec (XData Identity) '[])
 -> DivAp f (XRec Identity as))
-> Chain Day Identity f (Rec (XData Identity) '[])
-> DivAp 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 :: DivAp f r
x V.:& xs :: Rec (DivAp 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 (DivAp f) (DivAp f) (XRec Identity (r : rs))
-> DivAp 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 (DivAp f) (DivAp f) (XRec Identity (r : rs))
 -> DivAp f (XRec Identity as))
-> Day (DivAp f) (DivAp f) (XRec Identity (r : rs))
-> DivAp f (XRec Identity as)
forall a b. (a -> b) -> a -> b
$ DivAp f r
-> DivAp f (XRec Identity rs)
-> (r -> XRec Identity rs -> XRec Identity (r : rs))
-> (XRec Identity (r : rs) -> (r, XRec Identity rs))
-> Day (DivAp f) (DivAp 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
      DivAp f r
x
      (Rec (DivAp f) rs -> DivAp f (XRec Identity rs)
forall (f :: * -> *) (as :: [*]).
Rec (DivAp f) as -> DivAp f (XRec Identity as)
concatDivApRec Rec (DivAp 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 'assembleDivAp1' 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.
assembleDivAp1Rec
    :: Invariant f
    => V.Rec f (a ': as)
    -> DivAp1 f (V.XRec V.Identity (a ': as))
assembleDivAp1Rec :: Rec f (a : as) -> DivAp1 f (XRec Identity (a : as))
assembleDivAp1Rec = \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])
-> DivAp1 f (XRec Identity (a : as))
forall (f :: * -> *) a. Chain1 Day f a -> DivAp1 f a
DivAp1_ (Chain1 Day f (XRec Identity '[a])
 -> DivAp1 f (XRec Identity (a : as)))
-> Chain1 Day f (XRec Identity '[a])
-> DivAp1 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))
-> DivAp1 f (XRec Identity (a : as))
forall (f :: * -> *) a. Chain1 Day f a -> DivAp1 f a
DivAp1_ (Chain1 Day f (XRec Identity (r : r : rs))
 -> DivAp1 f (XRec Identity (a : as)))
-> Chain1 Day f (XRec Identity (r : r : rs))
-> DivAp1 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
        (DivAp1 f (XRec Identity (r : rs))
-> Chain1 Day f (XRec Identity (r : rs))
forall (f :: * -> *) a. DivAp1 f a -> Chain1 Day f a
unDivAp1 (Rec f (r : rs) -> DivAp1 f (XRec Identity (r : rs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
Rec f (a : as) -> DivAp1 f (XRec Identity (a : as))
assembleDivAp1Rec Rec f rs
Rec f (r : rs)
xs))
        r -> XRec Identity (r : rs) -> XRec Identity (r : r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
HKD f r -> XRec f rs -> XRec f (r : rs)
(V.::&)
        XRec Identity (r : r : rs) -> (r, XRec Identity (r : rs))
forall a (as :: [*]).
XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec

-- | A version of 'concatDivAp1' 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.
concatDivAp1Rec
    :: Invariant f
    => V.Rec (DivAp1 f) (a ': as)
    -> DivAp1 f (V.XRec V.Identity (a ': as))
concatDivAp1Rec :: Rec (DivAp1 f) (a : as) -> DivAp1 f (XRec Identity (a : as))
concatDivAp1Rec = \case
    x :: DivAp1 f r
x V.:& xs :: Rec (DivAp1 f) rs
xs -> case Rec (DivAp1 f) rs
xs of
      V.RNil   -> (r -> XRec Identity '[a])
-> (XRec Identity '[a] -> r)
-> DivAp1 f r
-> DivAp1 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) DivAp1 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 (DivAp1 f) (DivAp1 f) (XRec Identity (r : r : rs))
-> DivAp1 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 (DivAp1 f) (DivAp1 f) (XRec Identity (r : r : rs))
 -> DivAp1 f (XRec Identity (a : as)))
-> Day (DivAp1 f) (DivAp1 f) (XRec Identity (r : r : rs))
-> DivAp1 f (XRec Identity (a : as))
forall a b. (a -> b) -> a -> b
$ DivAp1 f r
-> DivAp1 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 (DivAp1 f) (DivAp1 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
        DivAp1 f r
x
        (Rec (DivAp1 f) (r : rs) -> DivAp1 f (XRec Identity (r : rs))
forall (f :: * -> *) a (as :: [*]).
Invariant f =>
Rec (DivAp1 f) (a : as) -> DivAp1 f (XRec Identity (a : as))
concatDivAp1Rec Rec (DivAp1 f) rs
Rec (DivAp1 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)