{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}

module Data.PTraversable.Internal.Day
  (ptraverseDay, ptraverseDayWith) where

import Prelude hiding (Enum)

import Data.Profunctor
import Data.Profunctor.Cartesian

import Data.Functor.Day ( Day(..), trans1, trans2 )

import Data.Finitary.PolyRep
import Data.Type.Equality

import Data.PTraversable.Internal.ClassOnly

-- * Auxiliary definitions

data EncoderF t where
  EncoderF :: !(SPoly r) -> (forall a. t a -> Eval r a) -> (forall b. Eval r b -> t b) -> EncoderF t

unsafeGeneralizeEncoder :: forall t. (forall a b. Encoder a b (t a) (t b)) -> EncoderF t
unsafeGeneralizeEncoder :: forall (t :: * -> *).
(forall a b. Encoder a b (t a) (t b)) -> EncoderF t
unsafeGeneralizeEncoder forall a b. Encoder a b (t a) (t b)
polyEncoder = case Encoder (ZonkAny 3) (ZonkAny 2) (t (ZonkAny 3)) (t (ZonkAny 2))
forall a b. Encoder a b (t a) (t b)
polyEncoder of
  Encoder SPoly r
sr t (ZonkAny 3) -> Eval r (ZonkAny 3)
_ Eval r (ZonkAny 2) -> t (ZonkAny 2)
_ -> SPoly r
-> (forall a. t a -> Eval r a)
-> (forall b. Eval r b -> t b)
-> EncoderF t
forall (r :: Poly) (t :: * -> *).
SPoly r
-> (forall a. t a -> Eval r a)
-> (forall b. Eval r b -> t b)
-> EncoderF t
EncoderF SPoly r
sr (SPoly r -> t a -> Eval r a
forall (r :: Poly) a. SPoly r -> t a -> Eval r a
from SPoly r
sr) (SPoly r -> Eval r b -> t b
forall (r :: Poly) a. SPoly r -> Eval r a -> t a
to SPoly r
sr)
  where
    from :: forall r a. SPoly r -> t a -> Eval r a 
    from :: forall (r :: Poly) a. SPoly r -> t a -> Eval r a
from SPoly r
sr = case Encoder a (ZonkAny 1) (t a) (t (ZonkAny 1))
forall a b. Encoder a b (t a) (t b)
polyEncoder of
      Encoder SPoly r
sr' t a -> Eval r a
from' Eval r (ZonkAny 1) -> t (ZonkAny 1)
_ -> case SPoly r -> SPoly r -> Maybe (r :~: r)
forall (a :: Poly) (b :: Poly).
SPoly a -> SPoly b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SPoly r
sr SPoly r
sr' of
        Maybe (r :~: r)
Nothing -> [Char] -> t a -> Eval r a
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen (parametricity)"
        Just r :~: r
Refl -> t a -> Eval r a
t a -> Eval r a
from'
    
    to :: forall r a. SPoly r -> Eval r a -> t a
    to :: forall (r :: Poly) a. SPoly r -> Eval r a -> t a
to SPoly r
sr = case Encoder (ZonkAny 0) a (t (ZonkAny 0)) (t a)
forall a b. Encoder a b (t a) (t b)
polyEncoder of
      Encoder SPoly r
sr' t (ZonkAny 0) -> Eval r (ZonkAny 0)
_ Eval r a -> t a
to' -> case SPoly r -> SPoly r -> Maybe (r :~: r)
forall (a :: Poly) (b :: Poly).
SPoly a -> SPoly b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SPoly r
sr SPoly r
sr' of
        Maybe (r :~: r)
Nothing -> [Char] -> Eval r a -> t a
forall a. HasCallStack => [Char] -> a
error [Char]
"should not happen (parametricity)"
        Just r :~: r
Refl -> Eval r a -> t a
Eval r a -> t a
to'

dayEncoderF :: EncoderF t -> EncoderF u -> EncoderF (Day t u)
dayEncoderF :: forall (t :: * -> *) (u :: * -> *).
EncoderF t -> EncoderF u -> EncoderF (Day t u)
dayEncoderF @t @u (EncoderF @r1 SPoly r
sr1 forall a. t a -> Eval r a
fromT forall b. Eval r b -> t b
toT) (EncoderF @r2 SPoly r
sr2 forall a. u a -> Eval r a
fromU forall b. Eval r b -> u b
toU) =
  SPoly (DayPoly r r)
-> (forall a. Day t u a -> Eval (DayPoly r r) a)
-> (forall b. Eval (DayPoly r r) b -> Day t u b)
-> EncoderF (Day t u)
forall (r :: Poly) (t :: * -> *).
SPoly r
-> (forall a. t a -> Eval r a)
-> (forall b. Eval r b -> t b)
-> EncoderF t
EncoderF (SPoly r -> SPoly r -> SPoly (DayPoly r r)
forall (r1 :: Poly) (r2 :: Poly).
SPoly r1 -> SPoly r2 -> SPoly (DayPoly r1 r2)
sDayPoly SPoly r
sr1 SPoly r
sr2) Day t u a -> Eval (DayPoly r r) a
forall a. Day t u a -> Eval (DayPoly r r) a
from Eval (DayPoly r r) b -> Day t u b
forall b. Eval (DayPoly r r) b -> Day t u b
to
  where
    from :: forall x. Day t u x -> Eval (DayPoly r1 r2) x
    from :: forall a. Day t u a -> Eval (DayPoly r r) a
from = SPoly r
-> SPoly r -> Day (Eval r) (Eval r) x -> Eval (DayPoly r r) x
forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Day (Eval r1) (Eval r2) x -> Eval (DayPoly r1 r2) x
fromDay SPoly r
sr1 SPoly r
sr2 (Day (Eval r) (Eval r) x -> Eval (DayPoly r r) x)
-> (Day t u x -> Day (Eval r) (Eval r) x)
-> Day t u x
-> Eval (DayPoly r r) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. t a -> Eval r a)
-> Day t (Eval r) x -> Day (Eval r) (Eval r) x
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
(forall x. f x -> g x) -> Day f h a -> Day g h a
trans1 t x -> Eval r x
forall a. t a -> Eval r a
fromT (Day t (Eval r) x -> Day (Eval r) (Eval r) x)
-> (Day t u x -> Day t (Eval r) x)
-> Day t u x
-> Day (Eval r) (Eval r) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. u a -> Eval r a) -> Day t u x -> Day t (Eval r) x
forall (g :: * -> *) (h :: * -> *) (f :: * -> *) a.
(forall x. g x -> h x) -> Day f g a -> Day f h a
trans2 u x -> Eval r x
forall a. u a -> Eval r a
fromU 

    to :: forall x. Eval (DayPoly r1 r2) x -> Day t u x
    to :: forall b. Eval (DayPoly r r) b -> Day t u b
to = (forall b. Eval r b -> u b) -> Day t (Eval r) x -> Day t u x
forall (g :: * -> *) (h :: * -> *) (f :: * -> *) a.
(forall x. g x -> h x) -> Day f g a -> Day f h a
trans2 Eval r x -> u x
forall b. Eval r b -> u b
toU (Day t (Eval r) x -> Day t u x)
-> (Eval (DayPoly r r) x -> Day t (Eval r) x)
-> Eval (DayPoly r r) x
-> Day t u x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall b. Eval r b -> t b)
-> Day (Eval r) (Eval r) x -> Day t (Eval r) x
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
(forall x. f x -> g x) -> Day f h a -> Day g h a
trans1 Eval r x -> t x
forall b. Eval r b -> t b
toT (Day (Eval r) (Eval r) x -> Day t (Eval r) x)
-> (Eval (DayPoly r r) x -> Day (Eval r) (Eval r) x)
-> Eval (DayPoly r r) x
-> Day t (Eval r) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPoly r
-> SPoly r -> Eval (DayPoly r r) x -> Day (Eval r) (Eval r) x
forall (r1 :: Poly) (r2 :: Poly) x.
SPoly r1
-> SPoly r2 -> Eval (DayPoly r1 r2) x -> Day (Eval r1) (Eval r2) x
toDay SPoly r
sr1 SPoly r
sr2

-----------

-- | 'Day' lacks various instances required to be a 'PTraversable'
ptraverseDayWith :: forall t u.
     (PTraversable t, PTraversable u)
  => forall p a b as bs. (Cartesian p, Cocartesian p)
  => (as -> Day t u a) -> (Day t u b -> bs) -> p a b -> p as bs
ptraverseDayWith :: forall (t :: * -> *) (u :: * -> *) (p :: * -> * -> *) a b as bs.
(PTraversable t, PTraversable u, Cartesian p, Cocartesian p) =>
(as -> Day t u a) -> (Day t u b -> bs) -> p a b -> p as bs
ptraverseDayWith = (as -> Day t u a) -> (Day t u b -> bs) -> p a b -> p as bs
forall (p :: * -> * -> *) a b as bs.
(Cartesian p, Cocartesian p) =>
(as -> Day t u a) -> (Day t u b -> bs) -> p a b -> p as bs
travDayTU
  where
    encT :: EncoderF t
    encT :: EncoderF t
encT = (forall a b. Encoder a b (t a) (t b)) -> EncoderF t
forall (t :: * -> *).
(forall a b. Encoder a b (t a) (t b)) -> EncoderF t
unsafeGeneralizeEncoder (Encoder a b a b -> Encoder a b (t a) (t b)
forall (t :: * -> *) (p :: * -> * -> *) a b.
(PTraversable t, Cartesian p, Cocartesian p) =>
p a b -> p (t a) (t b)
ptraverse Encoder a b a b
forall a b. Encoder a b a b
idEncoder)

    encU :: EncoderF u
    encU :: EncoderF u
encU = (forall a b. Encoder a b (u a) (u b)) -> EncoderF u
forall (t :: * -> *).
(forall a b. Encoder a b (t a) (t b)) -> EncoderF t
unsafeGeneralizeEncoder (Encoder a b a b -> Encoder a b (u a) (u b)
forall (t :: * -> *) (p :: * -> * -> *) a b.
(PTraversable t, Cartesian p, Cocartesian p) =>
p a b -> p (t a) (t b)
ptraverse Encoder a b a b
forall a b. Encoder a b a b
idEncoder)

    encDayTU :: EncoderF (Day t u)
    encDayTU :: EncoderF (Day t u)
encDayTU = EncoderF t -> EncoderF u -> EncoderF (Day t u)
forall (t :: * -> *) (u :: * -> *).
EncoderF t -> EncoderF u -> EncoderF (Day t u)
dayEncoderF EncoderF t
encT EncoderF u
encU

    travDayTU :: forall p a b as bs. (Cartesian p, Cocartesian p)
      => (as -> Day t u a) -> (Day t u b -> bs) -> p a b -> p as bs
    travDayTU :: forall (p :: * -> * -> *) a b as bs.
(Cartesian p, Cocartesian p) =>
(as -> Day t u a) -> (Day t u b -> bs) -> p a b -> p as bs
travDayTU as -> Day t u a
pre Day t u b -> bs
post = case EncoderF (Day t u)
encDayTU of
      EncoderF SPoly r
sr forall a. Day t u a -> Eval r a
from forall b. Eval r b -> Day t u b
to -> (as -> Eval r a)
-> (Eval r b -> bs) -> p (Eval r a) (Eval r b) -> p as bs
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (Day t u a -> Eval r a
forall a. Day t u a -> Eval r a
from (Day t u a -> Eval r a) -> (as -> Day t u a) -> as -> Eval r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. as -> Day t u a
pre) (Day t u b -> bs
post (Day t u b -> bs) -> (Eval r b -> Day t u b) -> Eval r b -> bs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Eval r b -> Day t u b
forall b. Eval r b -> Day t u b
to) (p (Eval r a) (Eval r b) -> p as bs)
-> (p a b -> p (Eval r a) (Eval r b)) -> p a b -> p as bs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPoly r -> p a b -> p (Eval r a) (Eval r b)
forall (p :: * -> * -> *) (r :: Poly) a b.
(Cartesian p, Cocartesian p) =>
SPoly r -> p a b -> p (Eval r a) (Eval r b)
ptraverseEval SPoly r
sr

ptraverseDay :: forall t u.
     (PTraversable t, PTraversable u)
  => forall p a b. (Cartesian p, Cocartesian p)
  => p a b -> p (Day t u a) (Day t u b)
ptraverseDay :: forall (t :: * -> *) (u :: * -> *) (p :: * -> * -> *) a b.
(PTraversable t, PTraversable u, Cartesian p, Cocartesian p) =>
p a b -> p (Day t u a) (Day t u b)
ptraverseDay = (Day t u a -> Day t u a)
-> (Day t u b -> Day t u b) -> p a b -> p (Day t u a) (Day t u b)
forall (t :: * -> *) (u :: * -> *) (p :: * -> * -> *) a b as bs.
(PTraversable t, PTraversable u, Cartesian p, Cocartesian p) =>
(as -> Day t u a) -> (Day t u b -> bs) -> p a b -> p as bs
forall (p :: * -> * -> *) a b as bs.
(Cartesian p, Cocartesian p) =>
(as -> Day t u a) -> (Day t u b -> bs) -> p a b -> p as bs
ptraverseDayWith Day t u a -> Day t u a
forall a. a -> a
id Day t u b -> Day t u b
forall a. a -> a
id