{-# LANGUAGE RankNTypes #-}
module Unbound.Generics.LocallyNameless.Internal.Iso where

import Data.Profunctor (Profunctor(..))
import Data.Functor.Identity (Identity(..))

data Exchange a b s t = Exchange (s -> a) (b -> t)

instance Functor (Exchange a b s) where
  fmap :: forall a b. (a -> b) -> Exchange a b s a -> Exchange a b s b
fmap a -> b
f (Exchange s -> a
p b -> a
q) = (s -> a) -> (b -> b) -> Exchange a b s b
forall a b s t. (s -> a) -> (b -> t) -> Exchange a b s t
Exchange s -> a
p (a -> b
f (a -> b) -> (b -> a) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
q)

instance Profunctor (Exchange a b) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Exchange a b b c -> Exchange a b a d
dimap a -> b
f c -> d
g (Exchange b -> a
h b -> c
k) = (a -> a) -> (b -> d) -> Exchange a b a d
forall a b s t. (s -> a) -> (b -> t) -> Exchange a b s t
Exchange (b -> a
h (b -> a) -> (a -> b) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f ) (c -> d
g (c -> d) -> (b -> c) -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c
k)

type Iso s t a b = forall p f . (Profunctor p, Functor f) => p a (f b) -> p s (f t)

type AnIso s t a b = Exchange a b a (Identity b) -> Exchange a b s (Identity t)

iso :: (s -> a) -> (b -> t) -> Iso s t a b
iso :: forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso s -> a
sa b -> t
bt = (s -> a) -> (f b -> f t) -> p a (f b) -> p s (f t)
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 s -> a
sa ((b -> t) -> f b -> f t
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> t
bt)
{-# INLINE iso #-}

from :: AnIso s t a b -> Iso b a t s
from :: forall s t a b. AnIso s t a b -> Iso b a t s
from AnIso s t a b
l = AnIso s t a b
-> ((s -> a) -> (b -> t) -> p t (f s) -> p b (f a))
-> p t (f s)
-> p b (f a)
forall s t a b r. AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
withIso AnIso s t a b
l (((s -> a) -> (b -> t) -> p t (f s) -> p b (f a))
 -> p t (f s) -> p b (f a))
-> ((s -> a) -> (b -> t) -> p t (f s) -> p b (f a))
-> p t (f s)
-> p b (f a)
forall a b. (a -> b) -> a -> b
$  \ s -> a
sa b -> t
bt -> (b -> t) -> (s -> a) -> Iso b a t s
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso b -> t
bt s -> a
sa
{-# INLINE from #-}

withIso :: AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
withIso :: forall s t a b r. AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
withIso AnIso s t a b
ai (s -> a) -> (b -> t) -> r
k =
  case AnIso s t a b
ai ((a -> a) -> (b -> Identity b) -> Exchange a b a (Identity b)
forall a b s t. (s -> a) -> (b -> t) -> Exchange a b s t
Exchange a -> a
forall a. a -> a
id b -> Identity b
forall a. a -> Identity a
Identity) of
   Exchange s -> a
sa b -> Identity t
bt -> (s -> a) -> (b -> t) -> r
k s -> a
sa (Identity t -> t
forall a. Identity a -> a
runIdentity (Identity t -> t) -> (b -> Identity t) -> b -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Identity t
bt)
{-# INLINE withIso #-}