{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.Functor.Invariant.Inplicative.Free (
DivAp(.., Gather, Knot)
, runCoDivAp
, runContraDivAp
, divApAp
, divApDiv
, foldDivAp
, assembleDivAp
, assembleDivApRec
, DivAp1(.., DivAp1)
, runCoDivAp1
, runContraDivAp1
, divApAp1
, divApDiv1
, foldDivAp1
, assembleDivAp1
, assembleDivAp1Rec
) 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.Functor.Invariant.Inplicative
import Data.HBifunctor.Tensor hiding (elim1, elim2, intro1, intro2)
import Data.HFunctor
import Data.HFunctor.Chain
import Data.HFunctor.Chain.Internal
import Data.HFunctor.Interpret
import Data.SOP hiding (hmap)
import qualified Data.Vinyl as V
import qualified Data.Vinyl.Functor as V
runCoDivAp1
:: forall f g. Apply g
=> f ~> g
-> DivAp1 f ~> g
runCoDivAp1 :: forall (f :: * -> *) (g :: * -> *).
Apply g =>
(f ~> g) -> DivAp1 f ~> g
runCoDivAp1 f ~> g
f = forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
foldDivAp1 f ~> g
f (forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Apply h =>
(f ~> h) -> (g ~> h) -> Day f g ~> h
runDayApply f ~> g
f forall a. a -> a
id)
runContraDivAp1
:: forall f g. Divise g
=> f ~> g
-> DivAp1 f ~> g
runContraDivAp1 :: forall (f :: * -> *) (g :: * -> *).
Divise g =>
(f ~> g) -> DivAp1 f ~> g
runContraDivAp1 f ~> g
f = forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
foldDivAp1 f ~> g
f (forall (f :: * -> *) (g :: * -> *) (h :: * -> *).
Divise h =>
(f ~> h) -> (g ~> h) -> Day f g ~> h
runDayDivise f ~> g
f forall a. a -> a
id)
runCoDivAp
:: forall f g. Applicative g
=> f ~> g
-> DivAp f ~> g
runCoDivAp :: forall (f :: * -> *) (g :: * -> *).
Applicative g =>
(f ~> g) -> DivAp f ~> g
runCoDivAp f ~> g
f = forall (g :: * -> *) (f :: * -> *).
(forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
foldDivAp forall (f :: * -> *) a. Applicative f => a -> f a
pure (\case Day f b
x g c
y b -> c -> x
h x -> (b, c)
_ -> forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 b -> c -> x
h (f ~> g
f f b
x) g c
y)
runContraDivAp
:: forall f g. Divisible g
=> f ~> g
-> DivAp f ~> g
runContraDivAp :: forall (f :: * -> *) (g :: * -> *).
Divisible g =>
(f ~> g) -> DivAp f ~> g
runContraDivAp f ~> g
f = forall (g :: * -> *) (f :: * -> *).
(forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
foldDivAp (forall a b. a -> b -> a
const forall (f :: * -> *) a. Divisible f => f a
conquer) (\case Day f b
x g c
y b -> c -> x
_ x -> (b, c)
g -> forall (f :: * -> *) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide x -> (b, c)
g (f ~> g
f f b
x) g c
y)
foldDivAp
:: (forall x. x -> g x)
-> (Day f g ~> g)
-> DivAp f ~> g
foldDivAp :: forall (g :: * -> *) (f :: * -> *).
(forall x. x -> g x) -> (Day f g ~> g) -> DivAp f ~> g
foldDivAp forall x. x -> g x
f Day f g ~> g
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 (forall x. x -> g x
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity) Day f g ~> g
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp
foldDivAp1
:: (f ~> g)
-> (Day f g ~> g)
-> DivAp1 f ~> g
foldDivAp1 :: forall (f :: * -> *) (g :: * -> *).
(f ~> g) -> (Day f g ~> g) -> DivAp1 f ~> g
foldDivAp1 f ~> g
f Day f g ~> g
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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. DivAp1 f a -> Chain1 Day f a
unDivAp1
divApAp :: DivAp f ~> Ap f
divApAp :: forall (f :: * -> *). DivAp f ~> Ap f
divApAp = forall (f :: * -> *) (g :: * -> *).
Applicative g =>
(f ~> g) -> DivAp f ~> g
runCoDivAp forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
divApAp1 :: DivAp1 f ~> Ap1 f
divApAp1 :: forall (f :: * -> *). DivAp1 f ~> Ap1 f
divApAp1 = forall (f :: * -> *) (g :: * -> *).
Apply g =>
(f ~> g) -> DivAp1 f ~> g
runCoDivAp1 forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
divApDiv :: DivAp f ~> Div f
divApDiv :: forall (f :: * -> *). DivAp f ~> Div f
divApDiv = forall (f :: * -> *) (g :: * -> *).
Divisible g =>
(f ~> g) -> DivAp f ~> g
runContraDivAp forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
divApDiv1 :: DivAp1 f ~> Div1 f
divApDiv1 :: forall (f :: * -> *). DivAp1 f ~> Div1 f
divApDiv1 = forall (f :: * -> *) (g :: * -> *).
Divise g =>
(f ~> g) -> DivAp1 f ~> g
runContraDivAp1 forall {k} (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
pattern Gather :: (b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> DivAp f a
pattern $bGather :: forall a (f :: * -> *) b c.
(b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> DivAp f a
$mGather :: forall {r} {a} {f :: * -> *}.
DivAp f a
-> (forall {b} {c}.
(b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> r)
-> ((# #) -> r)
-> r
Gather f g x xs <- (unGather_->MaybeF (Just (Day x xs f g)))
where
Gather b -> c -> a
f a -> (b, c)
g f b
x DivAp f c
xs = forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp forall a b. (a -> b) -> a -> b
$ forall {k} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
(f :: k) (a :: k1).
t f (Chain t i f) a -> Chain t i f a
More forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f b
x (forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp DivAp f c
xs) b -> c -> a
f a -> (b, c)
g
unGather_ :: DivAp f ~> MaybeF (Day f (DivAp f))
unGather_ :: forall (f :: * -> *). DivAp f ~> MaybeF (Day f (DivAp f))
unGather_ = \case
DivAp (More (Day f b
x Chain Day Identity f c
xs b -> c -> x
g x -> (b, c)
f)) -> forall {k} (f :: k -> *) (a :: k). Maybe (f a) -> MaybeF f a
MaybeF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day f b
x (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 Identity x
_ ) -> forall {k} (f :: k -> *) (a :: k). Maybe (f a) -> MaybeF f a
MaybeF forall a. Maybe a
Nothing
pattern Knot :: a -> DivAp f a
pattern $bKnot :: forall a (f :: * -> *). a -> DivAp f a
$mKnot :: forall {r} {a} {f :: * -> *}.
DivAp f a -> (a -> r) -> ((# #) -> r) -> r
Knot x = DivAp (Done (Identity x))
{-# COMPLETE Gather, Knot #-}
instance Inply (DivAp f) where
gather :: forall b c a.
(b -> c -> a)
-> (a -> (b, c)) -> DivAp f b -> DivAp f c -> DivAp f a
gather = coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: * -> *) b c a.
Inply f =>
(b -> c -> a) -> (a -> (b, c)) -> f b -> f c -> f a
gather @(Chain Day Identity _))
instance Inplicative (DivAp f) where
knot :: forall a. a -> DivAp f a
knot = coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: * -> *) a. Inplicative f => a -> f a
knot @(Chain Day Identity _))
pattern DivAp1 :: Invariant f => (b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> DivAp1 f a
pattern $bDivAp1 :: forall (f :: * -> *) a b c.
Invariant f =>
(b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> DivAp1 f a
$mDivAp1 :: forall {r} {f :: * -> *} {a}.
Invariant f =>
DivAp1 f a
-> (forall {b} {c}.
(b -> c -> a) -> (a -> (b, c)) -> f b -> DivAp f c -> r)
-> ((# #) -> r)
-> r
DivAp1 f g x xs <- (coerce splitChain1->Day x xs f g)
where
DivAp1 b -> c -> a
f a -> (b, c)
g f b
x DivAp f c
xs = forall (t :: (* -> *) -> (* -> *) -> * -> *) (i :: * -> *)
(f :: * -> *).
(Matchable t i, FunctorBy t f) =>
t f (ListBy t f) ~> NonEmptyBy t f
unsplitNE forall a b. (a -> b) -> a -> b
$ 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
f a -> (b, c)
g
{-# COMPLETE DivAp1 #-}
instance Invariant f => Inply (DivAp1 f) where
gather :: forall b c a.
(b -> c -> a)
-> (a -> (b, c)) -> DivAp1 f b -> DivAp1 f c -> DivAp1 f a
gather = coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: * -> *) b c a.
Inply f =>
(b -> c -> a) -> (a -> (b, c)) -> f b -> f c -> f a
gather @(Chain1 Day _))
assembleDivAp
:: NP f as
-> DivAp f (NP I as)
assembleDivAp :: forall (f :: * -> *) (as :: [*]). NP f as -> DivAp f (NP I as)
assembleDivAp = \case
NP f as
Nil -> forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp forall a b. (a -> b) -> a -> b
$ forall {k} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
(f :: k) (a :: k1).
i a -> Chain t i f a
Done forall a b. (a -> b) -> a -> b
$ forall a. a -> Identity a
Identity forall {k} (a :: k -> *). NP a '[]
Nil
f x
x :* NP f xs
xs -> forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp forall a b. (a -> b) -> a -> b
$ forall {k} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
(f :: k) (a :: k1).
t f (Chain t i f) a -> Chain t i f a
More forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day
f x
x
(forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp (forall (f :: * -> *) (as :: [*]). NP f as -> DivAp f (NP I as)
assembleDivAp NP f xs
xs))
(\x
y NP I xs
ys -> forall a. a -> I a
I x
y forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I xs
ys)
(\case I x
y :* NP I xs
ys -> (x
y, NP I xs
ys))
assembleDivAp1
:: Invariant f
=> NP f (a ': as)
-> DivAp1 f (NP I (a ': as))
assembleDivAp1 :: forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP f (a : as) -> DivAp1 f (NP I (a : as))
assembleDivAp1 (f x
x :* NP f xs
xs) = forall (f :: * -> *) a. Chain1 Day f a -> DivAp1 f a
DivAp1_ forall a b. (a -> b) -> a -> b
$ case NP f xs
xs of
NP f xs
Nil -> forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
f a -> Chain1 t f a
Done1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap ((forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {k} (a :: k -> *). NP a '[]
Nil) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> I a
I) (forall a. I a -> a
unI forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (f :: k -> *) (x :: k) (xs :: [k]). NP f (x : xs) -> f x
hd) f x
x
f x
_ :* NP f xs
_ -> forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day
f x
x
(forall (f :: * -> *) a. DivAp1 f a -> Chain1 Day f a
unDivAp1 (forall (f :: * -> *) a (as :: [*]).
Invariant f =>
NP f (a : as) -> DivAp1 f (NP I (a : as))
assembleDivAp1 NP f xs
xs))
(\x
y NP I (x : xs)
ys -> forall a. a -> I a
I x
y forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* NP I (x : xs)
ys)
(\case I x
y :* NP I xs
ys -> (x
y, NP I xs
ys))
assembleDivApRec
:: V.Rec f as
-> DivAp f (V.XRec V.Identity as)
assembleDivApRec :: forall (f :: * -> *) (as :: [*]).
Rec f as -> DivAp f (XRec Identity as)
assembleDivApRec = \case
Rec f as
V.RNil -> forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp forall a b. (a -> b) -> a -> b
$ forall {k} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
(f :: k) (a :: k1).
i a -> Chain t i f a
Done forall a b. (a -> b) -> a -> b
$ forall a. a -> Identity a
Identity forall {u} (a :: u -> *). Rec a '[]
V.RNil
f r
x V.:& Rec f rs
xs -> forall (f :: * -> *) a. Chain Day Identity f a -> DivAp f a
DivAp forall a b. (a -> b) -> a -> b
$ forall {k} {k1} (t :: k -> (k1 -> *) -> k1 -> *) (i :: k1 -> *)
(f :: k) (a :: k1).
t f (Chain t i f) a -> Chain t i f a
More forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day
f r
x
(forall (f :: * -> *) a. DivAp f a -> Chain Day Identity f a
unDivAp (forall (f :: * -> *) (as :: [*]).
Rec f as -> DivAp f (XRec Identity as)
assembleDivApRec Rec f rs
xs))
forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
HKD f r -> XRec f rs -> XRec f (r : rs)
(V.::&)
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 :: forall (f :: * -> *) a (as :: [*]).
Invariant f =>
Rec f (a : as) -> DivAp1 f (XRec Identity (a : as))
assembleDivAp1Rec (f r
x V.:& Rec f rs
xs) = case Rec f rs
xs of
Rec f rs
V.RNil -> forall (f :: * -> *) a. Chain1 Day f a -> DivAp1 f a
DivAp1_ forall a b. (a -> b) -> a -> b
$ forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
f a -> Chain1 t f a
Done1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap (forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
HKD f r -> XRec f rs -> XRec f (r : rs)
V.::& forall {u} (a :: u -> *). Rec a '[]
V.RNil) (\case HKD Identity a
z V.::& XRec Identity as
_ -> HKD Identity a
z) f r
x
f r
_ V.:& Rec f rs
_ -> forall (f :: * -> *) a. Chain1 Day f a -> DivAp1 f a
DivAp1_ forall a b. (a -> b) -> a -> b
$ forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(a :: k).
t f (Chain1 t f) a -> Chain1 t f a
More1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
Day
f r
x
(forall (f :: * -> *) a. DivAp1 f a -> Chain1 Day f a
unDivAp1 (forall (f :: * -> *) a (as :: [*]).
Invariant f =>
Rec f (a : as) -> DivAp1 f (XRec Identity (a : as))
assembleDivAp1Rec Rec f rs
xs))
forall {k} (f :: k -> *) (r :: k) (rs :: [k]).
HKD f r -> XRec f rs -> XRec f (r : rs)
(V.::&)
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 :: forall a (as :: [*]).
XRec Identity (a : as) -> (a, XRec Identity as)
unconsRec (HKD Identity a
y V.::& XRec Identity as
ys) = (HKD Identity a
y, XRec Identity as
ys)
instance Inply f => Interpret DivAp1 f where
interpret :: forall (g :: * -> *). (g ~> f) -> DivAp1 g ~> f
interpret g ~> f
f (DivAp1_ Chain1 Day g x
x) = forall {k} (t :: (k -> *) -> (k -> *) -> k -> *) (f :: k -> *)
(g :: k -> *).
HBifunctor t =>
(f ~> g) -> (t f g ~> g) -> Chain1 t f ~> g
foldChain1 g ~> f
f (forall (h :: * -> *) (f :: * -> *) (g :: * -> *).
Inply h =>
(f ~> h) -> (g ~> h) -> Day f g ~> h
runDay g ~> f
f forall a. a -> a
id) Chain1 Day g x
x
instance Inplicative f => Interpret DivAp f where
interpret :: forall (g :: * -> *). (g ~> f) -> DivAp g ~> f
interpret g ~> f
f (DivAp Chain Day Identity g x
x) = 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 (forall (f :: * -> *) a. Inplicative f => a -> f a
knot forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity) (forall (h :: * -> *) (f :: * -> *) (g :: * -> *).
Inply h =>
(f ~> h) -> (g ~> h) -> Day f g ~> h
runDay g ~> f
f forall a. a -> a
id) Chain Day Identity g x
x