{-# 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          #-}
#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE QuantifiedConstraints #-}
#endif

{-# OPTIONS_HADDOCK show-extensions #-}

#if __GLASGOW_HASKELL__ <= 802
-- ghc802 does not infer that 'cons' is used when using a bidirectional
-- pattern
{-# OPTIONS_GHC -Wno-unused-top-binds    #-}
-- the 'complete' pragma was introduced in ghc804
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
#endif

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

      -- * Type alligned 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 (..))
#if __GLASGOW_HASKELL__ < 804
import           Data.Monoid (Monoid (..))
import           Data.Semigroup (Semigroup (..))
#endif
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 { 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 :: 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 (r :: k -> k -> *).
 Category r =>
 (forall (x :: k) (y :: k). f x y -> r x y) -> r x z)
-> C f x z
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 (r :: k -> k -> *).
  Category r =>
  (forall (x :: k) (y :: k). f x y -> r x y) -> r x z)
 -> C f x z)
-> (forall (r :: k -> k -> *).
    Category r =>
    (forall (x :: k) (y :: k). f x y -> r x y) -> r x z)
-> C f x z
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) -> r y z
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 r y z -> r x y -> r x z
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (forall (x :: k) (y :: k). f x y -> r x y) -> r x y
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 :: ListTr f a b -> C f a b
toC = ListTr f a b -> C f a b
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 :: C f a b -> ListTr f a b
fromC = C f a b -> ListTr f a b
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 :: f a b -> C f a b
liftC = \f a b
f -> (forall (r :: k -> k -> *).
 Category r =>
 (forall (x :: k) (y :: k). f x y -> r x y) -> r a b)
-> C f a b
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 (r :: k -> k -> *).
  Category r =>
  (forall (x :: k) (y :: k). f x y -> r x y) -> r a b)
 -> C f a b)
-> (forall (r :: k -> k -> *).
    Category r =>
    (forall (x :: k) (y :: k). f x y -> r x y) -> r a b)
-> C f a b
forall a b. (a -> b) -> a -> b
$ \forall (x :: k) (y :: k). f x y -> r x y
k -> f a b -> r a b
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 :: f b c -> C f a b -> C f a c
consC f b c
bc C f a b
ab = f b c -> C f b c
forall k (f :: k -> k -> *) (a :: k) (b :: k). f a b -> C f a b
liftC f b c
bc 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` 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 (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 (x :: k) (y :: k). f x y -> c x y) -> c a b
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 :: C f a a
id  = (forall (r :: k -> k -> *).
 Category r =>
 (forall (x :: k) (y :: k). f x y -> r x y) -> r a a)
-> C f a a
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
_ -> r a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)
  . :: C f b c -> C f a b -> C f a c
(.) = 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

#if __GLASGOW_HASKELL__ >= 806
-- | 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 = ListTr f a b -> String
forall a. Show a => a -> String
show (C f a b -> ListTr f a b
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)
#else
-- | Blind show instance via 'ListTr'
--
instance Show (C f a b) where
    show c = show (hoistFreeH2 c :: ListTr f a b)
#endif

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

instance FreeAlgebra2 C where
  liftFree2 :: f a b -> C f a b
liftFree2    = f a b -> C f a b
forall k (f :: k -> k -> *) (a :: k) (b :: k). f a b -> C f a b
liftC
  {-# INLINE liftFree2 #-}
  foldNatFree2 :: (forall (x :: k) (y :: k). f x y -> d x y) -> C f a b -> d a b
foldNatFree2 = (forall (x :: k) (y :: k). f x y -> d x y) -> C f a b -> d a b
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 :: Proof (AlgebraType C (C f)) (C f)
codom2  = Proof (AlgebraType C (C f)) (C f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: Proof (AlgebraType0 C f) (C f)
forget2 = Proof (AlgebraType0 C f) (C f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof

instance Arrow f => Arrow (C f) where
  arr :: (b -> c) -> C f b c
arr b -> c
ab = (forall (r :: * -> * -> *).
 Category r =>
 (forall x y. f x y -> r x y) -> r b c)
-> C f b c
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 (r :: * -> * -> *).
  Category r =>
  (forall x y. f x y -> r x y) -> r b c)
 -> C f b c)
-> (forall (r :: * -> * -> *).
    Category r =>
    (forall x y. f x y -> r x y) -> r b c)
-> C f b c
forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> f b c -> r b c
forall x y. f x y -> r x y
k ((b -> c) -> f b c
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 *** :: 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 (r :: * -> * -> *).
 Category r =>
 (forall x y. f x y -> r x y) -> r (b, b') (c, c'))
-> C f (b, b') (c, c')
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 (r :: * -> * -> *).
  Category r =>
  (forall x y. f x y -> r x y) -> r (b, b') (c, c'))
 -> C f (b, b') (c, c'))
-> (forall (r :: * -> * -> *).
    Category r =>
    (forall x y. f x y -> r x y) -> r (b, b') (c, c'))
-> C f (b, b') (c, c')
forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> f (b, b') (c, c') -> r (b, b') (c, c')
forall x y. f x y -> r x y
k ((forall x y. f x y -> f x y) -> f b c
forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b c
c1 forall x y. f x y -> f x y
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id f b c -> f b' c' -> f (b, b') (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (forall x y. f x y -> f x y) -> f b' c'
forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b' c'
c2 forall x y. f x y -> f x y
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)
  {-# INLINE (***) #-}

instance ArrowZero f => ArrowZero (C f) where
  zeroArrow :: C f b c
zeroArrow = (forall (r :: * -> * -> *).
 Category r =>
 (forall x y. f x y -> r x y) -> r b c)
-> C f b c
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 (r :: * -> * -> *).
  Category r =>
  (forall x y. f x y -> r x y) -> r b c)
 -> C f b c)
-> (forall (r :: * -> * -> *).
    Category r =>
    (forall x y. f x y -> r x y) -> r b c)
-> C f b c
forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> f b c -> r b c
forall x y. f x y -> r x y
k f b c
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 +++ :: 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 (r :: * -> * -> *).
 Category r =>
 (forall x y. f x y -> r x y) -> r (Either b b') (Either c c'))
-> C f (Either b b') (Either c c')
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 (r :: * -> * -> *).
  Category r =>
  (forall x y. f x y -> r x y) -> r (Either b b') (Either c c'))
 -> C f (Either b b') (Either c c'))
-> (forall (r :: * -> * -> *).
    Category r =>
    (forall x y. f x y -> r x y) -> r (Either b b') (Either c c'))
-> C f (Either b b') (Either c c')
forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> f (Either b b') (Either c c') -> r (Either b b') (Either c c')
forall x y. f x y -> r x y
k ((forall x y. f x y -> f x y) -> f b c
forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b c
c1 forall x y. f x y -> f x y
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id f b c -> f b' c' -> f (Either b b') (Either c c')
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ (forall x y. f x y -> f x y) -> f b' c'
forall (r :: * -> * -> *).
Category r =>
(forall x y. f x y -> r x y) -> r b' c'
c2 forall x y. f x y -> f x y
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 C f o o -> C f o o -> C f o o
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 = C f o o
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
#if __GLASGOW_HASKELL__ < 804
  mappend = (<>)
#endif