module Data.Functor.Invariant.DivAp (
DivAp(.., Gather, Knot)
, runCoDivAp
, runContraDivAp
, divApAp
, divApDiv
, foldDivAp
, gather, gathered
, assembleDivAp
, assembleDivApRec
, concatDivAp
, concatDivApRec
, DivAp1(.., DivAp1)
, runCoDivAp1
, runContraDivAp1
, divApAp1
, divApDiv1
, foldDivAp1
, gather1, gathered1
, assembleDivAp1
, assembleDivAp1Rec
, concatDivAp1
, concatDivAp1Rec
, 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
runDayApply
:: forall f g h. Apply h
=> f ~> h
-> g ~> h
-> Day f g ~> h
runDayApply :: (f ~> h) -> (g ~> h) -> Day f g ~> h
runDayApply f :: f ~> h
f g :: g ~> h
g (Day x :: f b
x y :: g c
y j :: b -> c -> x
j _) = (b -> c -> x) -> h b -> h c -> h x
forall (f :: * -> *) a b c.
Apply f =>
(a -> b -> c) -> f a -> f b -> f c
liftF2 b -> c -> x
j (f b -> h b
f ~> h
f f b
x) (g c -> h c
g ~> h
g g c
y)
runDayDivise
:: forall f g h. Divise h
=> f ~> h
-> g ~> h
-> Day f g ~> h
runDayDivise :: (f ~> h) -> (g ~> h) -> Day f g ~> h
runDayDivise f :: f ~> h
f g :: g ~> h
g (Day x :: f b
x y :: g c
y _ h :: x -> (b, c)
h) = (x -> (b, c)) -> h b -> h c -> h x
forall (f :: * -> *) a b c.
Divise f =>
(a -> (b, c)) -> f b -> f c -> f a
divise x -> (b, c)
h (f b -> h b
f ~> h
f f b
x) (g c -> h c
g ~> h
g g c
y)
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)
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)
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)
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)
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
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
divApAp :: DivAp f ~> Ap f
divApAp :: DivAp f x -> Ap f x
divApAp = (f ~> Ap f) -> DivAp f ~> Ap f
forall (f :: * -> *) (g :: * -> *).
Applicative g =>
(f ~> g) -> DivAp f ~> g
runCoDivAp f ~> Ap f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
divApAp1 :: DivAp1 f ~> Ap1 f
divApAp1 :: DivAp1 f x -> Ap1 f x
divApAp1 = (f ~> Ap1 f) -> DivAp1 f ~> Ap1 f
forall (f :: * -> *) (g :: * -> *).
Apply g =>
(f ~> g) -> DivAp1 f ~> g
runCoDivAp1 f ~> Ap1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
divApDiv :: DivAp f ~> Div f
divApDiv :: DivAp f x -> Div f x
divApDiv = (f ~> Div f) -> DivAp f ~> Div f
forall (f :: * -> *) (g :: * -> *).
Divisible g =>
(f ~> g) -> DivAp f ~> g
runContraDivAp f ~> Div f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
divApDiv1 :: DivAp1 f ~> Div1 f
divApDiv1 :: DivAp1 f x -> Div1 f x
divApDiv1 = (f ~> Div1 f) -> DivAp1 f ~> Div1 f
forall (f :: * -> *) (g :: * -> *).
Divise g =>
(f ~> g) -> DivAp1 f ~> g
runContraDivAp1 f ~> Div1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
pattern Gather :: (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
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 #-}
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 #-}
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)
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 (,)
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)
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 (,)
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
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
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
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
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
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
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
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)