module Data.Functor.Invariant.Day.Chain (
DayChain(.., Gather, Knot)
, runCoDayChain
, runContraDayChain
, chainAp
, chainDiv
, gather, gathered
, assembleDayChain
, assembleDayChainRec
, concatDayChain
, concatDayChainRec
, DayChain1(.., DayChain1)
, runCoDayChain1
, runContraDayChain1
, chainAp1
, chainDiv1
, gather1, gathered1
, assembleDayChain1
, assembleDayChain1Rec
, concatDayChain1
, concatDayChain1Rec
, 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)
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
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
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
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
chainAp :: DayChain f ~> Ap f
chainAp :: DayChain f x -> Ap f x
chainAp = (f ~> Ap f) -> DayChain f ~> Ap f
forall (f :: * -> *) (g :: * -> *).
Applicative g =>
(f ~> g) -> DayChain f ~> g
runCoDayChain f ~> Ap f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
chainAp1 :: DayChain1 f ~> Ap1 f
chainAp1 :: DayChain1 f x -> Ap1 f x
chainAp1 = (f ~> Ap1 f) -> DayChain1 f ~> Ap1 f
forall (f :: * -> *) (g :: * -> *).
Apply g =>
(f ~> g) -> DayChain1 f ~> g
runCoDayChain1 f ~> Ap1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
chainDiv :: DayChain f ~> Div f
chainDiv :: DayChain f x -> Div f x
chainDiv = (f ~> Div f) -> DayChain f ~> Div f
forall (f :: * -> *) (g :: * -> *).
Divisible g =>
(f ~> g) -> DayChain f ~> g
runContraDayChain f ~> Div f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
chainDiv1 :: DayChain1 f ~> Div1 f
chainDiv1 :: DayChain1 f x -> Div1 f x
chainDiv1 = (f ~> Div1 f) -> DayChain1 f ~> Div1 f
forall (f :: * -> *) (g :: * -> *).
Divise g =>
(f ~> g) -> DayChain1 f ~> g
runContraDayChain1 f ~> Div1 f
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
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
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 #-}
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 #-}
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)
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 (,)
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)
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 (,)
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
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
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
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
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
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
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
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)