{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

module Control.Invertible.BiArrow.Free where

import Prelude hiding ((.), id, fst, snd, curry)
-- import qualified Prelude as P
import Control.Invertible.BiArrow
import Control.Category
import Data.Groupoid
import Data.Invertible.Bijection
import Data.Invertible.Profunctor
import Data.Invertible.Strong
import Data.Semigroupoid

infixr :-

data FreeA p a b = PureP (a <-> b)
                 | forall x. p a x :- FreeA p x b

nil :: IsoProfunctor p => FreeA p a a
nil = PureP id

instance IsoProfunctor b => IsoProfunctor (FreeA b) where
  lmap f (PureP g) = PureP (g . f)
  lmap f (g :- h)  = (lmap f g) :- h
  rmap f (PureP g) = PureP (f . g)
  rmap f (g :- h)  = g :- (rmap f h)

instance IsoStrong p => IsoStrong (FreeA p) where
  first' (PureP f) = PureP (first' f)
  first' (g :- h)  = (first' g) :- (first' h)

instance IsoProfunctor p => Semigroupoid (FreeA p) where
  o g (PureP f) = lmap f g
  o k (g :- h)  = g :- (k `o` h)

instance IsoProfunctor p => Category (FreeA p) where
  id = PureP id
  (.) = o

revinv :: (IsoProfunctor p, Groupoid p)
       => (forall x y. p x y -> p y x)
       -> FreeA p a b
       -> FreeA p b a
revinv _ (PureP f) = PureP $ inv f
revinv i (g :- h)  = go i h (i g :- nil)

go :: IsoProfunctor p => (forall x y. p x y -> p y x) -> FreeA p x d -> FreeA p x c -> FreeA p d c
go _ (PureP f) acc = lmap (inv f) acc
go i (g :- h)  acc = go i h (i g :- acc)

instance (IsoProfunctor p, Groupoid p) => Groupoid (FreeA p) where
  inv = revinv inv

instance (IsoProfunctor p, Groupoid p) => BiArrow (FreeA p) where
  (<->) f g = PureP $ f :<->: g

-- instance (IsoProfunctor p, IsoStrong p, Groupoid p) => BiArrow' (FreeA p) where