{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE CPP                   #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE ViewPatterns          #-}
{-# LANGUAGE QuantifiedConstraints #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module Control.Category.Free
    ( -- * Real time Queue
      Queue (ConsQ, NilQ)
    , consQ
    , snocQ
    , unconsQ
    , liftQ
    , foldNatQ
    , foldrQ
    , foldlQ
    , zipWithQ

      -- * Type aligned list
    , ListTr (..)
    , liftL
    , foldNatL
    , foldlL
    , foldrL
    , zipWithL

      -- * Free category (CPS style)
    , C (..)
    , liftC
    , consC
    , foldNatC
    , toC
    , fromC

      -- * Opposite category
    , Op (..)
    , hoistOp

      -- * Free interface re-exports
    , FreeAlgebra2 (..)
    , wrapFree2
    , foldFree2
    , hoistFree2
    , hoistFreeH2
    , joinFree2
    , bindFree2
    )
    where

import           Prelude hiding (id, concat, (.))
import           Control.Category (Category (..))
import           Control.Algebra.Free2
                  ( AlgebraType0
                  , AlgebraType
                  , FreeAlgebra2 (..)
                  , Proof (..)
                  , wrapFree2
                  , foldFree2
                  , hoistFree2
                  , hoistFreeH2
                  , joinFree2
                  , bindFree2
                  )
import           Control.Arrow (Arrow (..), ArrowZero (..), ArrowChoice (..))
import           Data.Kind (Type)

import           Control.Category.Free.Internal


--
-- CPS style free categories
--

-- | CPS style encoded free category; one can use @'FreeAlgebra2'@ class
-- instance:
--
-- > liftFree2    @C :: f a b -> C f a b
-- > foldNatFree2 @C :: Category d
-- >                 => (forall x y. f x y -> d x y)
-- >                 -> C f a b -> d a b
--
newtype C f a b
  = C { forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
C f a b
-> forall (r :: k -> k -> *).
   Category r =>
   (forall (x :: k) (y :: k). f x y -> r x y) -> r a b
runC :: forall r. Category r
             => (forall x y. f x y -> r x y)
             -> r a b
      }

composeC :: C f y z -> C f x y -> C f x z
composeC :: forall {k} (f :: k -> k -> *) (y :: k) (z :: k) (x :: k).
C f y z -> C f x y -> C f x z
composeC (C forall (r :: k -> k -> *).
Category r =>
(forall (x :: k) (y :: k). f x y -> r x y) -> r y z
g) (C forall (r :: k -> k -> *).
Category r =>
(forall (x :: k) (y :: k). f x y -> r x y) -> r x y
f) = forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(forall (r :: k -> k -> *).
 Category r =>
 (forall (x :: k) (y :: k). f x y -> r x y) -> r a b)
-> C f a b
C forall a b. (a -> b) -> a -> b
$ \forall (x :: k) (y :: k). f x y -> r x y
k -> forall (r :: k -> k -> *).
Category r =>
(forall (x :: k) (y :: k). f x y -> r x y) -> r y z
g forall (x :: k) (y :: k). f x y -> r x y
k forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (r :: k -> k -> *).
Category r =>
(forall (x :: k) (y :: k). f x y -> r x y) -> r x y
f forall (x :: k) (y :: k). f x y -> r x y
k
{-# INLINE [1] composeC #-}

-- | Isomorphism from @'ListTr'@ to @'C'@, which is a specialisation of
-- @'hoistFreeH2'@.
--
toC :: ListTr f a b -> C f a b
toC :: forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
ListTr f a b -> C f a b
toC = forall {k} (m :: (k -> k -> *) -> k -> k -> *)
       (n :: (k -> k -> *) -> k -> k -> *) (f :: k -> k -> *) (a :: k)
       (b :: k).
(FreeAlgebra2 m, FreeAlgebra2 n, AlgebraType0 m f,
 AlgebraType0 n f, AlgebraType m (n f)) =>
m f a b -> n f a b
hoistFreeH2
{-# INLINE toC #-}

-- | Inverse of @'fromC'@, which also is a specialisation of @'hoistFreeH2'@.
--
fromC :: C f a b -> ListTr f a b
fromC :: forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
C f a b -> ListTr f a b
fromC = forall {k} (m :: (k -> k -> *) -> k -> k -> *)
       (n :: (k -> k -> *) -> k -> k -> *) (f :: k -> k -> *) (a :: k)
       (b :: k).
(FreeAlgebra2 m, FreeAlgebra2 n, AlgebraType0 m f,
 AlgebraType0 n f, AlgebraType m (n f)) =>
m f a b -> n f a b
hoistFreeH2
{-# INLINE fromC #-}

liftC :: forall k (f :: k -> k -> Type) a b.
         f a b
      -> C f a b
liftC :: forall k (f :: k -> k -> *) (a :: k) (b :: k). f a b -> C f a b
liftC = \f a b
f -> forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(forall (r :: k -> k -> *).
 Category r =>
 (forall (x :: k) (y :: k). f x y -> r x y) -> r a b)
-> C f a b
C forall a b. (a -> b) -> a -> b
$ \forall (x :: k) (y :: k). f x y -> r x y
k -> forall (x :: k) (y :: k). f x y -> r x y
k f a b
f
{-# INLINE [1] liftC #-}

consC :: forall k (f :: k -> k -> Type) a b c.
         f b c
      -> C f a b
      -> C f a c
consC :: forall k (f :: k -> k -> *) (a :: k) (b :: k) (c :: k).
f b c -> C f a b -> C f a c
consC f b c
bc C f a b
ab = forall k (f :: k -> k -> *) (a :: k) (b :: k). f a b -> C f a b
liftC f b c
bc forall {k} (f :: k -> k -> *) (y :: k) (z :: k) (x :: k).
C f y z -> C f x y -> C f x z
`composeC` C f a b
ab
{-# INLINE [1] consC #-}

foldNatC :: forall k (f :: k -> k -> Type) c a b.
            Category c
         => (forall x y. f x y -> c x y)
         -> C f a b
         -> c a b
foldNatC :: forall k (f :: k -> k -> *) (c :: k -> k -> *) (a :: k) (b :: k).
Category c =>
(forall (x :: k) (y :: k). f x y -> c x y) -> C f a b -> c a b
foldNatC forall (x :: k) (y :: k). f x y -> c x y
nat (C forall (r :: k -> k -> *).
Category r =>
(forall (x :: k) (y :: k). f x y -> r x y) -> r a b
f) = forall (r :: k -> k -> *).
Category r =>
(forall (x :: k) (y :: k). f x y -> r x y) -> r a b
f forall (x :: k) (y :: k). f x y -> c x y
nat
{-# INLINE [1] foldNatC #-}

{-# RULES

"foldNatC/consC"
  forall (f :: f (v :: k) (w :: k))
         (q :: C f (u :: k) (v :: k))
         (nat :: forall (x :: k) (y :: k). f x y -> c x y).
  foldNatC nat (consC f q) = nat f . foldNatC nat q

"foldNatC/liftC"
  forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
         (g :: f v w)
         (h :: C f u v).
  foldNatC nat (liftC g `composeC` h) = nat g . foldNatC nat h

#-}

instance Category (C f) where
  id :: forall (a :: k). C f a a
id  = forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(forall (r :: k -> k -> *).
 Category r =>
 (forall (x :: k) (y :: k). f x y -> r x y) -> r a b)
-> C f a b
C (\forall (x :: k) (y :: k). f x y -> r x y
_ -> forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)
  . :: forall (b :: k) (c :: k) (a :: k). C f b c -> C f a b -> C f a c
(.) = forall {k} (f :: k -> k -> *) (y :: k) (z :: k) (x :: k).
C f y z -> C f x y -> C f x z
composeC

-- | Show instance via 'ListTr'
--
instance (forall x y. Show (f x y)) => Show (C f a b) where
    show :: C f a b -> String
show C f a b
c = forall a. Show a => a -> String
show (forall {k} (m :: (k -> k -> *) -> k -> k -> *)
       (n :: (k -> k -> *) -> k -> k -> *) (f :: k -> k -> *) (a :: k)
       (b :: k).
(FreeAlgebra2 m, FreeAlgebra2 n, AlgebraType0 m f,
 AlgebraType0 n f, AlgebraType m (n f)) =>
m f a b -> n f a b
hoistFreeH2 C f a b
c :: ListTr f a b)

type instance AlgebraType0 C f = ()
type instance AlgebraType  C c = Category c

instance FreeAlgebra2 C where
  liftFree2 :: forall (f :: k -> k -> *) (a :: k) (b :: k).
AlgebraType0 C f =>
f a b -> C f a b
liftFree2    = forall k (f :: k -> k -> *) (a :: k) (b :: k). f a b -> C f a b
liftC
  {-# INLINE liftFree2 #-}
  foldNatFree2 :: forall (d :: k -> k -> *) (f :: k -> k -> *) (a :: k) (b :: k).
(AlgebraType C d, AlgebraType0 C f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> C f a b -> d a b
foldNatFree2 = forall k (f :: k -> k -> *) (c :: k -> k -> *) (a :: k) (b :: k).
Category c =>
(forall (x :: k) (y :: k). f x y -> c x y) -> C f a b -> c a b
foldNatC
  {-# INLINE foldNatFree2 #-}

  codom2 :: forall (f :: k -> k -> *).
AlgebraType0 C f =>
Proof (AlgebraType C (C f)) (C f)
codom2  = forall {l} (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: forall (f :: k -> k -> *).
AlgebraType C f =>
Proof (AlgebraType0 C f) (C f)
forget2 = forall {l} (c :: Constraint) (a :: l). c => Proof c a
Proof

instance Arrow f => Arrow (C f) where
  arr :: forall b c. (b -> c) -> C f b c
arr b -> c
ab = forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(forall (r :: k -> k -> *).
 Category r =>
 (forall (x :: k) (y :: k). f x y -> r x y) -> r a b)
-> C f a b
C forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> forall x y. f x y -> r x y
k (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
ab)
  {-# INLINE arr #-}

  C forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b c
c1 *** :: forall b c b' c'. C f b c -> C f b' c' -> C f (b, b') (c, c')
*** C forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b' c'
c2  = forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(forall (r :: k -> k -> *).
 Category r =>
 (forall (x :: k) (y :: k). f x y -> r x y) -> r a b)
-> C f a b
C forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> forall x y. f x y -> r x y
k (forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b c
c1 forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b' c'
c2 forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)
  {-# INLINE (***) #-}

instance ArrowZero f => ArrowZero (C f) where
  zeroArrow :: forall b c. C f b c
zeroArrow = forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(forall (r :: k -> k -> *).
 Category r =>
 (forall (x :: k) (y :: k). f x y -> r x y) -> r a b)
-> C f a b
C forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> forall x y. f x y -> r x y
k forall (a :: * -> * -> *) b c. ArrowZero a => a b c
zeroArrow

instance ArrowChoice f => ArrowChoice (C f) where
  C forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b c
c1 +++ :: forall b c b' c'.
C f b c -> C f b' c' -> C f (Either b b') (Either c c')
+++ C forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b' c'
c2  = forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
(forall (r :: k -> k -> *).
 Category r =>
 (forall (x :: k) (y :: k). f x y -> r x y) -> r a b)
-> C f a b
C forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> forall x y. f x y -> r x y
k (forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b c
c1 forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b' c'
c2 forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)
  {-# INLINE (+++) #-}

instance Semigroup (C f o o) where
  C f o o
f <> :: C f o o -> C f o o -> C f o o
<> C f o o
g = C f o o
f forall {k} (f :: k -> k -> *) (y :: k) (z :: k) (x :: k).
C f y z -> C f x y -> C f x z
`composeC` C f o o
g

instance Monoid (C f o o) where
  mempty :: C f o o
mempty = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id