{-# LANGUAGE CPP                   #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE ViewPatterns          #-}

#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE QuantifiedConstraints #-}
#endif

{-# OPTIONS_HADDOCK show-extensions #-}

#if __GLASGOW_HASKELL__ <= 802
-- ghc802 does not infer that 'consQ' 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


-- | Internal module, contains implementation of type aligned real time queues
-- (C.Okasaki 'Purely Functional Data Structures').
--
module Control.Category.Free.Internal
  ( Op (..)
  , hoistOp

  , ListTr (..)
  , liftL
  , foldNatL
  , lengthListTr
  , foldrL
  , foldlL
  , zipWithL

  , Queue (NilQ, ConsQ)
  , liftQ
  , nilQ
  , consQ
  , ViewL (..)
  , unconsQ
  , snocQ
  , foldNatQ
  , foldrQ
  , foldlQ
  , hoistQ
  , zipWithQ
  ) where


import           Prelude hiding (id, (.))
import           Control.Arrow
import           Control.Category (Category (..))
#if __GLASGOW_HASKELL__ < 804
import           Data.Monoid (Monoid (..))
import           Data.Semigroup (Semigroup (..))
#endif
import           Data.Kind (Type)

import           Control.Algebra.Free2 ( AlgebraType0
                                       , AlgebraType
                                       , FreeAlgebra2 (..)
                                       , Proof (..)
                                       )

-- | Oposite categoy in which arrows from @a@ to @b@ are represented by arrows
-- from @b@ to @a@ in the original category.
--
newtype Op (f :: k -> k -> Type) (a :: k) (b :: k) = Op { Op f a b -> f b a
runOp :: f b a }
  deriving Int -> Op f a b -> ShowS
[Op f a b] -> ShowS
Op f a b -> String
(Int -> Op f a b -> ShowS)
-> (Op f a b -> String) -> ([Op f a b] -> ShowS) -> Show (Op f a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (f :: k -> k -> *) (a :: k) (b :: k).
Show (f b a) =>
Int -> Op f a b -> ShowS
forall k (f :: k -> k -> *) (a :: k) (b :: k).
Show (f b a) =>
[Op f a b] -> ShowS
forall k (f :: k -> k -> *) (a :: k) (b :: k).
Show (f b a) =>
Op f a b -> String
showList :: [Op f a b] -> ShowS
$cshowList :: forall k (f :: k -> k -> *) (a :: k) (b :: k).
Show (f b a) =>
[Op f a b] -> ShowS
show :: Op f a b -> String
$cshow :: forall k (f :: k -> k -> *) (a :: k) (b :: k).
Show (f b a) =>
Op f a b -> String
showsPrec :: Int -> Op f a b -> ShowS
$cshowsPrec :: forall k (f :: k -> k -> *) (a :: k) (b :: k).
Show (f b a) =>
Int -> Op f a b -> ShowS
Show

-- | 'Op' is an endo-functor of the category of categories.
--
hoistOp :: forall k
                  (f :: k -> k -> Type)
                  (g :: k -> k -> Type)
                  a b.
           (forall x y. f x y -> g x y)
        -> Op f a b
        -> Op g a b
hoistOp :: (forall (x :: k) (y :: k). f x y -> g x y) -> Op f a b -> Op g a b
hoistOp forall (x :: k) (y :: k). f x y -> g x y
nat (Op f b a
ba) = g b a -> Op g a b
forall k (f :: k -> k -> *) (a :: k) (b :: k). f b a -> Op f a b
Op (f b a -> g b a
forall (x :: k) (y :: k). f x y -> g x y
nat f b a
ba)
{-# INLINE hoistOp #-}

instance Category f => Category (Op f) where
    id :: Op f a a
id = f a a -> Op f a a
forall k (f :: k -> k -> *) (a :: k) (b :: k). f b a -> Op f a b
Op f a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
    Op f c b
f . :: Op f b c -> Op f a b -> Op f a c
. Op f b a
g = f c a -> Op f a c
forall k (f :: k -> k -> *) (a :: k) (b :: k). f b a -> Op f a b
Op (f b a
g f b a -> f c b -> f c a
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f c b
f)

instance Category f => Semigroup (Op f o o) where
    <> :: Op f o o -> Op f o o -> Op f o o
(<>) = Op f o o -> Op f o o -> Op f o o
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
(.)

instance Category f => Monoid (Op f o o) where
    mempty :: Op f o o
mempty = Op f o o
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
#if __GLASGOW_HASKELL__ < 804
    mappend = (<>)
#endif


--
-- Type aligned list 'ListTr'
--


-- | Simple representation of a free category by using type aligned
-- lists.  This is not a surprise as free monoids can be represented by
-- lists (up to laziness)
--
-- 'ListTr' has @'FreeAlgebra2'@ class instance:
--
-- > liftFree2    @ListTr :: f a b -> ListTr f ab
-- > foldNatFree2 @ListTr :: Category d
-- >                      => (forall x y. f x y -> d x y)
-- >                      -> ListTr f a b
-- >                      -> d a b
--
-- The same performance concerns that apply to @'Control.Monad.Free.Free'@
-- apply to this encoding of a free category.
--
-- Note that even though this is a naive version, it behaves quite well in
-- simple benchmarks and quite stable regardless of the level of optimisations.
--
data ListTr :: (k -> k -> Type) -> k -> k -> Type where
  NilTr  :: ListTr f a a
  ConsTr :: f b c -> ListTr f a b -> ListTr f a c

lengthListTr :: ListTr f a b -> Int
lengthListTr :: ListTr f a b -> Int
lengthListTr ListTr f a b
NilTr = Int
0
lengthListTr (ConsTr f b b
_ ListTr f a b
xs) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ListTr f a b -> Int
forall k (f :: k -> k -> *) (a :: k) (b :: k). ListTr f a b -> Int
lengthListTr ListTr f a b
xs

composeL :: forall k (f :: k -> k -> Type) x y z.
            ListTr f y z
         -> ListTr f x y
         -> ListTr f x z
composeL :: ListTr f y z -> ListTr f x y -> ListTr f x z
composeL (ConsTr f b z
x ListTr f y b
xs) ListTr f x y
ys = f b z -> ListTr f x b -> ListTr f x z
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr f b z
x (ListTr f y b
xs ListTr f y b -> ListTr f x y -> ListTr f x b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ListTr f x y
ys)
composeL ListTr f y z
NilTr         ListTr f x y
ys = ListTr f x y
ListTr f x z
ys
{-# INLINE [1] composeL #-}

liftL :: forall k (f :: k -> k -> Type) x y.
         f x y -> ListTr f x y
liftL :: f x y -> ListTr f x y
liftL f x y
f = f x y -> ListTr f x x -> ListTr f x y
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr f x y
f ListTr f x x
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr
{-# INLINE [1] liftL #-}

foldNatL :: forall k (f :: k -> k -> Type) c a b.
            Category c
         => (forall x y. f x y -> c x y)
         -> ListTr f a b
         -> c a b
foldNatL :: (forall (x :: k) (y :: k). f x y -> c x y) -> ListTr f a b -> c a b
foldNatL forall (x :: k) (y :: k). f x y -> c x y
_   ListTr f a b
NilTr     = c a b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
foldNatL forall (x :: k) (y :: k). f x y -> c x y
fun (ConsTr f b b
bc ListTr f a b
ab) = f b b -> c b b
forall (x :: k) (y :: k). f x y -> c x y
fun f b b
bc c b b -> c a b -> c a b
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 -> c x y) -> ListTr f a b -> c a b
forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall (x :: k) (y :: k). f x y -> c x y
fun ListTr f a b
ab
{-# INLINE [1] foldNatL #-}

{-# RULES

"foldNatL/ConsTr"
  forall (f :: f (v :: k) (w :: k))
         (q :: ListTr f (u :: k) (v :: k))
         (nat :: forall (x :: k) (y :: k). f x y -> c x y).
  foldNatL nat (ConsTr f q) = nat f . foldNatL nat q

"foldNatL/NilTr"  forall (nat :: forall (x :: k) (y :: k). f x y -> c x y).
                  foldNatL nat NilTr = id

"foldNatL/liftL"
  forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
         (g :: f v w)
         (h :: ListTr f u v).
    foldNatL nat (liftL g `composeL` h) = nat g . foldNatL nat h

#-}

-- | 'foldr' of a 'ListTr'
--
foldrL :: forall k (f :: k -> k -> Type) c a b d.
          (forall x y z. f y z -> c x y -> c x z)
       -> c a b
       -> ListTr f b d
       -> c a d
foldrL :: (forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
-> c a b -> ListTr f b d -> c a d
foldrL forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z
_nat c a b
ab ListTr f b d
NilTr          = c a b
c a d
ab
foldrL  forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z
nat c a b
ab (ConsTr f b d
xd ListTr f b b
bx) = f b d -> c a b -> c a d
forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z
nat f b d
xd ((forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
-> c a b -> ListTr f b b -> c a b
forall k k (f :: k -> k -> *) (c :: k -> k -> *) (a :: k) (b :: k)
       (d :: k).
(forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
-> c a b -> ListTr f b d -> c a d
foldrL forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z
nat c a b
ab ListTr f b b
bx)
{-# INLINE [1] foldrL #-}

-- | 'foldl' of a 'ListTr'
--
-- TODO: make it strict, like 'foldl''.
--
foldlL :: forall k (f :: k -> k -> Type) c a b d.
          (forall x y z. c y z -> f x y -> c x z)
       -> c b d
       -> ListTr f a b
       -> c a d
foldlL :: (forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z)
-> c b d -> ListTr f a b -> c a d
foldlL forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z
_nat c b d
bd ListTr f a b
NilTr          = c a d
c b d
bd
foldlL  forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z
nat c b d
bd (ConsTr f b b
xb ListTr f a b
ax) = (forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z)
-> c b d -> ListTr f a b -> c a d
forall k k (f :: k -> k -> *) (c :: k -> k -> *) (a :: k) (b :: k)
       (d :: k).
(forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z)
-> c b d -> ListTr f a b -> c a d
foldlL forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z
nat (c b d -> f b b -> c b d
forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z
nat c b d
bd f b b
xb) ListTr f a b
ax

zipWithL :: forall f g a b a' b'.
        Category f
     => (forall x y x' y'. f x y -> f x' y' -> f (g x x') (g y y'))
     -> ListTr f a  b
     -> ListTr f a' b'
     -> ListTr f (g a a') (g b b')
zipWithL :: (forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> ListTr f a b -> ListTr f a' b' -> ListTr f (g a a') (g b b')
zipWithL forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
fn ListTr f a b
queueA ListTr f a' b'
queueB = case (ListTr f a b
queueA, ListTr f a' b'
queueB) of
    (ListTr f a b
NilTr, ListTr f a' b'
NilTr) -> ListTr f (g a a') (g b b')
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr
    (ListTr f a b
NilTr, ConsTr f b b'
trB' ListTr f a' b
queueB') -> f (g a b) (g a b')
-> ListTr f (g a a') (g a b) -> ListTr f (g a a') (g a b')
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr (f a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id   f a a -> f b b' -> f (g a b) (g a b')
forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
`fn` f b b'
trB') ((forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> ListTr f a a -> ListTr f a' b -> ListTr f (g a a') (g a b)
forall k (f :: k -> k -> *) (g :: k -> k -> k) (a :: k) (b :: k)
       (a' :: k) (b' :: k).
Category f =>
(forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> ListTr f a b -> ListTr f a' b' -> ListTr f (g a a') (g b b')
zipWithL forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
fn ListTr f a a
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr    ListTr f a' b
queueB')
    (ConsTr f b b
trA' ListTr f a b
queueA', ListTr f a' b'
NilTr) -> f (g b a') (g b a')
-> ListTr f (g a a') (g b a') -> ListTr f (g a a') (g b a')
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr (f b b
trA' f b b -> f a' a' -> f (g b a') (g b a')
forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
`fn` f a' a'
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)   ((forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> ListTr f a b -> ListTr f a' a' -> ListTr f (g a a') (g b a')
forall k (f :: k -> k -> *) (g :: k -> k -> k) (a :: k) (b :: k)
       (a' :: k) (b' :: k).
Category f =>
(forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> ListTr f a b -> ListTr f a' b' -> ListTr f (g a a') (g b b')
zipWithL forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
fn ListTr f a b
queueA' ListTr f a' a'
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr)
    (ConsTr f b b
trA' ListTr f a b
queueA', ConsTr f b b'
trB' ListTr f a' b
queueB')
                                 -> f (g b b) (g b b')
-> ListTr f (g a a') (g b b) -> ListTr f (g a a') (g b b')
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr (f b b
trA' f b b -> f b b' -> f (g b b) (g b b')
forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
`fn` f b b'
trB') ((forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> ListTr f a b -> ListTr f a' b -> ListTr f (g a a') (g b b)
forall k (f :: k -> k -> *) (g :: k -> k -> k) (a :: k) (b :: k)
       (a' :: k) (b' :: k).
Category f =>
(forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> ListTr f a b -> ListTr f a' b' -> ListTr f (g a a') (g b b')
zipWithL forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
fn ListTr f a b
queueA' ListTr f a' b
queueB')

#if __GLASGOW_HASKELL__ >= 806
instance (forall (x :: k) (y :: k). Show (f x y)) => Show (ListTr f a b) where
    show :: ListTr f a b -> String
show ListTr f a b
NilTr         = String
"NilTr"
    show (ConsTr f b b
x ListTr f a b
xs) = String
"ConsTr " String -> ShowS
forall a. [a] -> [a] -> [a]
++ f b b -> String
forall a. Show a => a -> String
show f b b
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ListTr f a b -> String
forall a. Show a => a -> String
show ListTr f a b
xs
#else
instance Show (ListTr f a b) where
    show NilTr         = "NilTr"
    show (ConsTr _ xs) = "ConsTr _ " ++ show xs
#endif

instance Category (ListTr f) where
  id :: ListTr f a a
id  = ListTr f a a
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr
  . :: ListTr f b c -> ListTr f a b -> ListTr f a c
(.) = ListTr f b c -> ListTr f a b -> ListTr f a c
forall k (f :: k -> k -> *) (x :: k) (y :: k) (z :: k).
ListTr f y z -> ListTr f x y -> ListTr f x z
composeL

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

instance FreeAlgebra2 ListTr where
  liftFree2 :: f a b -> ListTr f a b
liftFree2    = f a b -> ListTr f a b
forall k (f :: k -> k -> *) (x :: k) (y :: k).
f x y -> ListTr f x y
liftL
  {-# INLINE liftFree2 #-}
  foldNatFree2 :: (forall (x :: k) (y :: k). f x y -> d x y) -> ListTr f a b -> d a b
foldNatFree2 = (forall (x :: k) (y :: k). f x y -> d x y) -> ListTr 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) -> ListTr f a b -> c a b
foldNatL
  {-# INLINE foldNatFree2 #-}

  codom2 :: Proof (AlgebraType ListTr (ListTr f)) (ListTr f)
codom2  = Proof (AlgebraType ListTr (ListTr f)) (ListTr f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: Proof (AlgebraType0 ListTr f) (ListTr f)
forget2 = Proof (AlgebraType0 ListTr f) (ListTr f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof

instance Semigroup (ListTr f o o) where
  ListTr f o o
f <> :: ListTr f o o -> ListTr f o o -> ListTr f o o
<> ListTr f o o
g = ListTr f o o
g ListTr f o o -> ListTr f o o -> ListTr f o o
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ListTr f o o
f

instance Monoid (ListTr f o o) where
  mempty :: ListTr f o o
mempty = ListTr f o o
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr
#if __GLASGOW_HASKELL__ < 804
  mappend = (<>)
#endif

instance Arrow f => Arrow (ListTr f) where
  arr :: (b -> c) -> ListTr f b c
arr b -> c
ab                          = (b -> c) -> f b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
ab f b c -> ListTr f b b -> ListTr f b c
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
`ConsTr` ListTr f b b
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr

  (ConsTr f b c
fxb ListTr f b b
cax) *** :: ListTr f b c -> ListTr f b' c' -> ListTr f (b, b') (c, c')
*** (ConsTr f b c'
fyb ListTr f b' b
cay)
                             = (f b c
fxb 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')
*** f b c'
fyb)    f (b, b) (c, c')
-> ListTr f (b, b') (b, b) -> ListTr f (b, b') (c, c')
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
`ConsTr` (ListTr f b b
cax ListTr f b b -> ListTr f b' b -> ListTr f (b, b') (b, b)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** ListTr f b' b
cay)
  (ConsTr f b c
fxb ListTr f b b
cax) *** ListTr f b' c'
NilTr = (f b c
fxb 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')
*** (b' -> c') -> f b' c'
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b' -> c'
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) f (b, b') (c, c')
-> ListTr f (b, b') (b, b') -> ListTr f (b, b') (c, c')
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
`ConsTr` (ListTr f b b
cax ListTr f b b -> ListTr f b' b' -> ListTr f (b, b') (b, b')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** ListTr f b' b'
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr)
  ListTr f b c
NilTr *** (ConsTr f b c'
fxb ListTr f b' b
cax) = ((b -> c) -> f b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
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')
*** f b c'
fxb) f (b, b) (c, c')
-> ListTr f (b, b') (b, b) -> ListTr f (b, b') (c, c')
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
`ConsTr` (ListTr f b b
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr ListTr f b b -> ListTr f b' b -> ListTr f (b, b') (b, b)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** ListTr f b' b
cax)
  ListTr f b c
NilTr *** ListTr f b' c'
NilTr            = ListTr f (b, b') (c, c')
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr

instance ArrowZero f => ArrowZero (ListTr f) where
  zeroArrow :: ListTr f b c
zeroArrow = f b c
forall (a :: * -> * -> *) b c. ArrowZero a => a b c
zeroArrow f b c -> ListTr f b b -> ListTr f b c
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
`ConsTr` ListTr f b b
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr

instance ArrowChoice f => ArrowChoice (ListTr f) where
  (ConsTr f b c
fxb ListTr f b b
cax) +++ :: ListTr f b c
-> ListTr f b' c' -> ListTr f (Either b b') (Either c c')
+++ (ConsTr f b c'
fyb ListTr f b' b
cay)
                             = (f b c
fxb 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')
+++ f b c'
fyb)    f (Either b b) (Either c c')
-> ListTr f (Either b b') (Either b b)
-> ListTr f (Either b b') (Either c c')
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
`ConsTr` (ListTr f b b
cax ListTr f b b
-> ListTr f b' b -> ListTr f (Either b b') (Either b b)
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ ListTr f b' b
cay)
  (ConsTr f b c
fxb ListTr f b b
cax) +++ ListTr f b' c'
NilTr = (f b c
fxb 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')
+++ (b' -> c') -> f b' c'
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b' -> c'
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) f (Either b b') (Either c c')
-> ListTr f (Either b b') (Either b b')
-> ListTr f (Either b b') (Either c c')
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
`ConsTr` (ListTr f b b
cax ListTr f b b
-> ListTr f b' b' -> ListTr f (Either b b') (Either b b')
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ ListTr f b' b'
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr)
  ListTr f b c
NilTr +++ (ConsTr f b c'
fxb ListTr f b' b
cax) = ((b -> c) -> f b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
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')
+++ f b c'
fxb) f (Either b b) (Either c c')
-> ListTr f (Either b b') (Either b b)
-> ListTr f (Either b b') (Either c c')
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
`ConsTr` (ListTr f b b
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr ListTr f b b
-> ListTr f b' b -> ListTr f (Either b b') (Either b b)
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ ListTr f b' b
cax)
  ListTr f b c
NilTr +++ ListTr f b' c'
NilTr            = ListTr f (Either b b') (Either c c')
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr


--
-- Type aligned real time 'Queue'
--


-- | Type alligned real time queues; Based on `Purely Functinal Data Structures`
-- C.Okasaki.  This the most reliably behaved implementation of free categories
-- in this package.
--
-- Upper bounds of `consQ`, `snocQ`, `unconsQ` are @O\(1\)@ (worst case).
--
-- Internal invariant: sum of lengths of two last least is equal the length of
-- the first one.
--
data Queue (f :: k -> k -> Type) (a :: k) (b :: k) where
    Queue :: forall f a c b x.
               ListTr f      b c
          -> !(ListTr (Op f) b a)
          ->   ListTr f      b x
          -> Queue f a c

pattern ConsQ :: f b c -> Queue f a b -> Queue f a c
pattern $bConsQ :: f b c -> Queue f a b -> Queue f a c
$mConsQ :: forall r k (f :: k -> k -> *) (c :: k) (a :: k).
Queue f a c
-> (forall (b :: k). f b c -> Queue f a b -> r)
-> (Void# -> r)
-> r
ConsQ a as <- (unconsQ -> a :< as) where
    ConsQ = f b c -> Queue f a b -> Queue f a c
forall k (f :: k -> k -> *) (a :: k) (b :: k) (c :: k).
f b c -> Queue f a b -> Queue f a c
consQ

pattern NilQ :: () => a ~ b => Queue f a b
pattern $bNilQ :: Queue f a b
$mNilQ :: forall r k (a :: k) (b :: k) (f :: k -> k -> *).
Queue f a b -> ((a ~ b) => r) -> (Void# -> r) -> r
NilQ <- (unconsQ -> EmptyL) where
    NilQ = Queue f a b
forall k (f :: k -> k -> *) (a :: k). Queue f a a
nilQ

#if __GLASGOW_HASKELL__ > 802
{-# complete NilQ, ConsQ #-}
#endif

composeQ :: forall k (f :: k -> k -> Type) x y z.
            Queue f y z
         -> Queue f x y
         -> Queue f x z
composeQ :: Queue f y z -> Queue f x y -> Queue f x z
composeQ (ConsQ f b z
f Queue f y b
q1) Queue f x y
q2 = f b z -> Queue f x b -> Queue f x z
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
ConsQ f b z
f (Queue f y b
q1 Queue f y b -> Queue f x y -> Queue f x b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Queue f x y
q2)
composeQ Queue f y z
NilQ         Queue f x y
q2 = Queue f x y
Queue f x z
q2
{-# INLINE [1] composeQ #-}

nilQ :: Queue (f :: k -> k -> Type) a a
nilQ :: Queue f a a
nilQ = ListTr f a a -> ListTr (Op f) a a -> ListTr f a a -> Queue f a a
forall k (f :: k -> k -> *) (a :: k) (c :: k) (b :: k) (x :: k).
ListTr f b c -> ListTr (Op f) b a -> ListTr f b x -> Queue f a c
Queue ListTr f a a
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr ListTr (Op f) a a
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr ListTr f a a
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr
{-# INLINE [1] nilQ #-}

consQ :: forall k (f :: k -> k -> Type) a b c.
         f b c
      -> Queue f a b
      -> Queue f a c
consQ :: f b c -> Queue f a b -> Queue f a c
consQ f b c
bc (Queue ListTr f b b
f ListTr (Op f) b a
r ListTr f b x
s) = ListTr f b c -> ListTr (Op f) b a -> ListTr f b Any -> Queue f a c
forall k (f :: k -> k -> *) (a :: k) (c :: k) (b :: k) (x :: k).
ListTr f b c -> ListTr (Op f) b a -> ListTr f b x -> Queue f a c
Queue (f b c -> ListTr f b b -> ListTr f b c
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr f b c
bc ListTr f b b
f) ListTr (Op f) b a
r (f x Any -> ListTr f b x -> ListTr f b Any
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr f x Any
forall a. HasCallStack => a
undefined ListTr f b x
s)
{-# INLINE [1] consQ #-}

data ViewL f a b where
    EmptyL :: ViewL f a a
    (:<)   :: f b c -> Queue f a b -> ViewL f a c

-- | 'uncons' a 'Queue', complexity: @O\(1\)@
--
unconsQ :: Queue f a b
        -> ViewL f a b
unconsQ :: Queue f a b -> ViewL f a b
unconsQ (Queue ListTr f b b
NilTr ListTr (Op f) b a
NilTr ListTr f b x
_)     = ViewL f a b
forall k (f :: k -> k -> *) (a :: k). ViewL f a a
EmptyL
unconsQ (Queue (ConsTr f b b
tr ListTr f b b
f) ListTr (Op f) b a
r ListTr f b x
s) = f b b
tr f b b -> Queue f a b -> ViewL f a b
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> Queue f a b -> ViewL f a c
:< ListTr f b b -> ListTr (Op f) b a -> ListTr f b x -> Queue f a b
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k) (x :: k).
ListTr f b c -> ListTr (Op f) b a -> ListTr f b x -> Queue f a c
exec ListTr f b b
f ListTr (Op f) b a
r ListTr f b x
s
unconsQ Queue f a b
_                         = String -> ViewL f a b
forall a. HasCallStack => String -> a
error String
"Queue.uncons: invariant violation"
{-# INLINE unconsQ #-}

snocQ :: forall k (f :: k -> k -> Type) a b c.
         Queue f b c
      -> f a b
      -> Queue f a c
snocQ :: Queue f b c -> f a b -> Queue f a c
snocQ (Queue ListTr f b c
f ListTr (Op f) b b
r ListTr f b x
s) f a b
g = ListTr f b c -> ListTr (Op f) b a -> ListTr f b x -> Queue f a c
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k) (x :: k).
ListTr f b c -> ListTr (Op f) b a -> ListTr f b x -> Queue f a c
exec ListTr f b c
f (Op f b a -> ListTr (Op f) b b -> ListTr (Op f) b a
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr (f a b -> Op f b a
forall k (f :: k -> k -> *) (a :: k) (b :: k). f b a -> Op f a b
Op f a b
g) ListTr (Op f) b b
r) ListTr f b x
s
{-# INLINE snocQ #-}

-- | 'foldr' of a 'Queue'
--
foldrQ :: forall k (f :: k -> k -> Type) c a b d.
          (forall x y z. f y z -> c x y -> c x z)
       -> c a b
       -> Queue f b d
       -> c a d
foldrQ :: (forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
-> c a b -> Queue f b d -> c a d
foldrQ forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z
_nat c a b
ab Queue f b d
NilQ          = c a b
c a d
ab
foldrQ  forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z
nat c a b
ab (ConsQ f b d
xd Queue f b b
bx) = f b d -> c a b -> c a d
forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z
nat f b d
xd ((forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
-> c a b -> Queue f b b -> c a b
forall k k (f :: k -> k -> *) (c :: k -> k -> *) (a :: k) (b :: k)
       (d :: k).
(forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
-> c a b -> Queue f b d -> c a d
foldrQ forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z
nat c a b
ab Queue f b b
bx)
{-# INLINE [1] foldrQ #-}

{-# RULES

"foldrQ/consQ/nilQ"
  foldrQ consQ nilQ = id

"foldrQ/single"
  forall (nat :: forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
         (t :: f (v :: k) (w :: k))
         (nil :: c (u :: k) (v :: k)).
  foldrQ nat nil (consQ t nilQ) = nat t nil

"foldrQ/nilQ"
  forall (nat :: forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
         (nil :: c (u :: k) (v :: k)).
  foldrQ nat nil nilQ = nil

"foldrQ/consQ"
  forall (f :: Queue f (x :: k) (y :: k))
         (g :: Queue f (y :: k) (z :: k)).
  foldrQ consQ f g = g . f

#-}

liftQ :: forall k (f :: k -> k -> Type) a b.
         f a b -> Queue f a b
liftQ :: f a b -> Queue f a b
liftQ = \f a b
fab -> f a b -> Queue f a a -> Queue f a b
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
ConsQ f a b
fab Queue f a a
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ
{-# INLINE [1] liftQ #-}

-- | Efficient fold of a queue into a category, analogous to 'foldM'.
--
-- /complexity/ @O\(n\)@
--
foldNatQ :: forall k (f :: k -> k -> Type) c a b.
            Category c
         => (forall x y. f x y -> c x y)
         -> Queue f a b
         -> c a b
foldNatQ :: (forall (x :: k) (y :: k). f x y -> c x y) -> Queue f a b -> c a b
foldNatQ forall (x :: k) (y :: k). f x y -> c x y
nat = (forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
-> c a a -> Queue f a b -> c a b
forall k k (f :: k -> k -> *) (c :: k -> k -> *) (a :: k) (b :: k)
       (d :: k).
(forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z)
-> c a b -> Queue f b d -> c a d
foldrQ (\f y z
f c x y
c -> f y z -> c y z
forall (x :: k) (y :: k). f x y -> c x y
nat f y z
f c y z -> c x y -> c x z
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. c x y
c) c a a
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
{-# INLINE [1] foldNatQ #-}

{-# RULES

"foldNatQ/consQ" forall (f :: f (v :: k) (w :: k))
                        (q :: Queue f (u :: k) (v :: k))
                        (nat :: forall (x :: k) (y :: k). f x y -> c x y).
                 foldNatQ nat (consQ f q) = nat f . foldNatQ nat q

"foldNatQ/nilQ"  forall (nat :: forall (x :: k) (y :: k). f x y -> c x y).
                 foldNatQ nat nilQ = id


"foldNatC/liftQ"
  forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
         (g :: f v w)
         (h :: Queue f u v).
  foldNatQ nat (liftQ g `composeQ` h) = nat g . foldNatQ nat h

#-}

-- | 'foldl' of a 'Queue'
--
-- TODO: make it strict, like 'foldl''.
--
foldlQ :: forall k (f :: k -> k -> Type) c a b d.
          (forall x y z. c y z -> f x y -> c x z)
       -> c b d
       -> Queue f a b
       -> c a d
foldlQ :: (forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z)
-> c b d -> Queue f a b -> c a d
foldlQ forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z
_nat c b d
bd Queue f a b
NilQ          = c a d
c b d
bd
foldlQ  forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z
nat c b d
bd (ConsQ f b b
xb Queue f a b
ax) = (forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z)
-> c b d -> Queue f a b -> c a d
forall k k (f :: k -> k -> *) (c :: k -> k -> *) (a :: k) (b :: k)
       (d :: k).
(forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z)
-> c b d -> Queue f a b -> c a d
foldlQ forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z
nat (c b d -> f b b -> c b d
forall (x :: k) (y :: k) (z :: k). c y z -> f x y -> c x z
nat c b d
bd f b b
xb) Queue f a b
ax

zipWithQ :: forall f g a b a' b'.
        Category f
     => (forall x y x' y'. f x y -> f x' y' -> f (g x x') (g y y'))
     -> Queue f a  b
     -> Queue f a' b'
     -> Queue f (g a a') (g b b')
zipWithQ :: (forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> Queue f a b -> Queue f a' b' -> Queue f (g a a') (g b b')
zipWithQ forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
fn Queue f a b
queueA Queue f a' b'
queueB = case (Queue f a b
queueA, Queue f a' b'
queueB) of
    (Queue f a b
NilQ, Queue f a' b'
NilQ) -> Queue f (g a a') (g b b')
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ
    (Queue f a b
NilQ, ConsQ f b b'
trB' Queue f a' b
queueB') -> f (g b b) (g b b')
-> Queue f (g a a') (g b b) -> Queue f (g a a') (g b b')
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
ConsQ (f b b
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id   f b b -> f b b' -> f (g b b) (g b b')
forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
`fn` f b b'
trB') ((forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> Queue f a b -> Queue f a' b -> Queue f (g a a') (g b b)
forall k (f :: k -> k -> *) (g :: k -> k -> k) (a :: k) (b :: k)
       (a' :: k) (b' :: k).
Category f =>
(forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> Queue f a b -> Queue f a' b' -> Queue f (g a a') (g b b')
zipWithQ forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
fn Queue f a b
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ    Queue f a' b
queueB')
    (ConsQ f b b
trA' Queue f a b
queueA', Queue f a' b'
NilQ) -> f (g b b') (g b b')
-> Queue f (g a a') (g b b') -> Queue f (g a a') (g b b')
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
ConsQ (f b b
trA' f b b -> f b' b' -> f (g b b') (g b b')
forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
`fn` f b' b'
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)   ((forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> Queue f a b -> Queue f a' b' -> Queue f (g a a') (g b b')
forall k (f :: k -> k -> *) (g :: k -> k -> k) (a :: k) (b :: k)
       (a' :: k) (b' :: k).
Category f =>
(forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> Queue f a b -> Queue f a' b' -> Queue f (g a a') (g b b')
zipWithQ forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
fn Queue f a b
queueA' Queue f a' b'
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ)
    (ConsQ f b b
trA' Queue f a b
queueA', ConsQ f b b'
trB' Queue f a' b
queueB')
                               -> f (g b b) (g b b')
-> Queue f (g a a') (g b b) -> Queue f (g a a') (g b b')
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
ConsQ (f b b
trA' f b b -> f b b' -> f (g b b) (g b b')
forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
`fn` f b b'
trB') ((forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> Queue f a b -> Queue f a' b -> Queue f (g a a') (g b b)
forall k (f :: k -> k -> *) (g :: k -> k -> k) (a :: k) (b :: k)
       (a' :: k) (b' :: k).
Category f =>
(forall (x :: k) (y :: k) (x' :: k) (y' :: k).
 f x y -> f x' y' -> f (g x x') (g y y'))
-> Queue f a b -> Queue f a' b' -> Queue f (g a a') (g b b')
zipWithQ forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
fn Queue f a b
queueA' Queue f a' b
queueB')


-- | 'Queue' is an endo-functor on the category of graphs (or category of
-- categories), thus one can hoist the transitions using a natural
-- transformation.  This in analogy to @'map' :: (a -> b) -> [a] -> [b]@.
--
hoistQ :: forall k
                 (f :: k -> k -> Type)
                 (g :: k -> k -> Type)
                 a  b.
          (forall x y. f x y -> g x y)
       -> Queue f a b
       -> Queue g a b
hoistQ :: (forall (x :: k) (y :: k). f x y -> g x y)
-> Queue f a b -> Queue g a b
hoistQ forall (x :: k) (y :: k). f x y -> g x y
nat Queue f a b
q = case Queue f a b
q of
    Queue f a b
NilQ        -> Queue g a b
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ
    ConsQ f b b
tr Queue f a b
q' -> g b b -> Queue g a b -> Queue g a b
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
ConsQ (f b b -> g b b
forall (x :: k) (y :: k). f x y -> g x y
nat f b b
tr) ((forall (x :: k) (y :: k). f x y -> g x y)
-> Queue f a b -> Queue g a b
forall k (f :: k -> k -> *) (g :: k -> k -> *) (a :: k) (b :: k).
(forall (x :: k) (y :: k). f x y -> g x y)
-> Queue f a b -> Queue g a b
hoistQ forall (x :: k) (y :: k). f x y -> g x y
nat Queue f a b
q')
{-# INLINE [1] hoistQ #-}

{-# RULES

"hoistQ/foldNatQ"
  forall (nat1 :: forall (x :: k) (y :: k). f x y -> g x y)
         (nat  :: forall (x :: k) (y :: k). g x y -> h x y)
         (q    :: Queue f x y).
  foldNatQ nat (hoistQ nat1 q) = foldNatQ (nat . nat1) q

"hoistQ/hoistQ"
  forall (nat1 :: forall (x :: k) (y :: k). f x y -> g x y)
         (nat  :: forall (x :: k) (y :: k). g x y -> h x y)
         (q    :: Queue f x y).
    hoistQ nat (hoistQ nat1 q) = hoistQ (nat . nat1) q

#-}

#if __GLASGOW_HASKELL__ >= 806
instance (forall (x :: k) (y :: k). Show (f x y))
      => Show (Queue f a b) where
    show :: Queue f a b -> String
show (Queue ListTr f b b
f ListTr (Op f) b a
r ListTr f b x
s) =
        String
"Queue ("
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ ListTr f b b -> String
forall a. Show a => a -> String
show ListTr f b b
f
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") ("
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ ListTr (Op f) b a -> String
forall a. Show a => a -> String
show ListTr (Op f) b a
r
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (ListTr f b x -> Int
forall k (f :: k -> k -> *) (a :: k) (b :: k). ListTr f a b -> Int
lengthListTr ListTr f b x
s)
#else
instance Show (Queue f r s) where
    show (Queue f r s) =
        "Queue "
      ++ show (lengthListTr f)
      ++ " "
      ++ show (lengthListTr r)
      ++ " "
      ++ show (lengthListTr s)
#endif

instance Category (Queue f) where
    id :: Queue f a a
id  = Queue f a a
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ
    . :: Queue f b c -> Queue f a b -> Queue f a c
(.) = Queue f b c -> Queue f a b -> Queue f a c
forall k (f :: k -> k -> *) (x :: k) (y :: k) (z :: k).
Queue f y z -> Queue f x y -> Queue f x z
composeQ

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

instance FreeAlgebra2 Queue where
  liftFree2 :: f a b -> Queue f a b
liftFree2    = f a b -> Queue f a b
forall k (f :: k -> k -> *) (a :: k) (b :: k). f a b -> Queue f a b
liftQ
  {-# INLINE liftFree2 #-}
  foldNatFree2 :: (forall (x :: k) (y :: k). f x y -> d x y) -> Queue f a b -> d a b
foldNatFree2 = (forall (x :: k) (y :: k). f x y -> d x y) -> Queue 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) -> Queue f a b -> c a b
foldNatQ
  {-# INLINE foldNatFree2 #-}

  codom2 :: Proof (AlgebraType Queue (Queue f)) (Queue f)
codom2  = Proof (AlgebraType Queue (Queue f)) (Queue f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: Proof (AlgebraType0 Queue f) (Queue f)
forget2 = Proof (AlgebraType0 Queue f) (Queue f)
forall l (c :: Constraint) (a :: l). c => Proof c a
Proof

instance Semigroup (Queue f o o) where
  Queue f o o
f <> :: Queue f o o -> Queue f o o -> Queue f o o
<> Queue f o o
g = Queue f o o
g Queue f o o -> Queue f o o -> Queue f o o
forall k (f :: k -> k -> *) (x :: k) (y :: k) (z :: k).
Queue f y z -> Queue f x y -> Queue f x z
`composeQ` Queue f o o
f

instance Monoid (Queue f o o) where
  mempty :: Queue f o o
mempty = Queue f o o
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ
#if __GLASGOW_HASKELL__ < 804
  mappend = (<>)
#endif

instance Arrow f => Arrow (Queue f) where
  arr :: (b -> c) -> Queue f b c
arr b -> c
ab = (b -> c) -> f b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
ab f b c -> Queue f b b -> Queue f b c
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` Queue f b b
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ

  (ConsQ f b c
fxb Queue f b b
cax) *** :: Queue f b c -> Queue f b' c' -> Queue f (b, b') (c, c')
*** (ConsQ f b c'
fyb Queue f b' b
cay)
                           = (f b c
fxb 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')
*** f b c'
fyb)    f (b, b) (c, c')
-> Queue f (b, b') (b, b) -> Queue f (b, b') (c, c')
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` (Queue f b b
cax Queue f b b -> Queue f b' b -> Queue f (b, b') (b, b)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Queue f b' b
cay)
  (ConsQ f b c
fxb Queue f b b
cax) *** Queue f b' c'
NilQ = (f b c
fxb f b c -> f c' c' -> f (b, c') (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (c' -> c') -> f c' c'
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr c' -> c'
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) f (b, c') (c, c')
-> Queue f (b, b') (b, c') -> Queue f (b, b') (c, c')
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` (Queue f b b
cax Queue f b b -> Queue f b' c' -> Queue f (b, b') (b, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Queue f b' c'
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ)
  Queue f b c
NilQ *** (ConsQ f b c'
fxb Queue f b' b
cax) = ((c -> c) -> f c c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr c -> c
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id f c c -> f b c' -> f (c, b) (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** f b c'
fxb) f (c, b) (c, c')
-> Queue f (b, b') (c, b) -> Queue f (b, b') (c, c')
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` (Queue f b c
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ Queue f b c -> Queue f b' b -> Queue f (b, b') (c, b)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Queue f b' b
cax)
  Queue f b c
NilQ *** Queue f b' c'
NilQ            = Queue f (b, b') (c, c')
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ

instance ArrowZero f => ArrowZero (Queue f) where
  zeroArrow :: Queue f b c
zeroArrow = f b c
forall (a :: * -> * -> *) b c. ArrowZero a => a b c
zeroArrow f b c -> Queue f b b -> Queue f b c
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` Queue f b b
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ

instance ArrowChoice f => ArrowChoice (Queue f) where
  (ConsQ f b c
fxb Queue f b b
cax) +++ :: Queue f b c -> Queue f b' c' -> Queue f (Either b b') (Either c c')
+++ (ConsQ f b c'
fyb Queue f b' b
cay)
                           = (f b c
fxb 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')
+++ f b c'
fyb)    f (Either b b) (Either c c')
-> Queue f (Either b b') (Either b b)
-> Queue f (Either b b') (Either c c')
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` (Queue f b b
cax Queue f b b -> Queue f b' b -> Queue f (Either b b') (Either b b)
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ Queue f b' b
cay)
  (ConsQ f b c
fxb Queue f b b
cax) +++ Queue f b' c'
NilQ = (f b c
fxb f b c -> f c' c' -> f (Either b c') (Either c c')
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ (c' -> c') -> f c' c'
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr c' -> c'
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) f (Either b c') (Either c c')
-> Queue f (Either b b') (Either b c')
-> Queue f (Either b b') (Either c c')
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` (Queue f b b
cax Queue f b b -> Queue f b' c' -> Queue f (Either b b') (Either b c')
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ Queue f b' c'
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ)
  Queue f b c
NilQ +++ (ConsQ f b c'
fxb Queue f b' b
cax) = ((c -> c) -> f c c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr c -> c
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id f c c -> f b c' -> f (Either c 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')
+++ f b c'
fxb) f (Either c b) (Either c c')
-> Queue f (Either b b') (Either c b)
-> Queue f (Either b b') (Either c c')
forall k (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` (Queue f b c
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ Queue f b c -> Queue f b' b -> Queue f (Either b b') (Either c b)
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ Queue f b' b
cax)
  Queue f b c
NilQ +++ Queue f b' c'
NilQ            = Queue f (Either b b') (Either c c')
forall k (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ

--
-- Internal API
--

exec :: ListTr f b c -> ListTr (Op f) b a -> ListTr f b x -> Queue f a c
exec :: ListTr f b c -> ListTr (Op f) b a -> ListTr f b x -> Queue f a c
exec ListTr f b c
xs ListTr (Op f) b a
ys (ConsTr f b x
_ ListTr f b b
t) = ListTr f b c -> ListTr (Op f) b a -> ListTr f b b -> Queue f a c
forall k (f :: k -> k -> *) (a :: k) (c :: k) (b :: k) (x :: k).
ListTr f b c -> ListTr (Op f) b a -> ListTr f b x -> Queue f a c
Queue ListTr f b c
xs ListTr (Op f) b a
ys ListTr f b b
t
exec ListTr f b c
xs ListTr (Op f) b a
ys ListTr f b x
NilTr        = ListTr f a c -> ListTr (Op f) a a -> ListTr f a c -> Queue f a c
forall k (f :: k -> k -> *) (a :: k) (c :: k) (b :: k) (x :: k).
ListTr f b c -> ListTr (Op f) b a -> ListTr f b x -> Queue f a c
Queue ListTr f a c
xs' ListTr (Op f) a a
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr ListTr f a c
xs'
  where
    xs' :: ListTr f a c
xs' = ListTr f b c -> ListTr (Op f) b a -> ListTr f a a -> ListTr f a c
forall k (f :: k -> k -> *) (c :: k) (d :: k) (b :: k) (a :: k).
ListTr f c d -> ListTr (Op f) c b -> ListTr f a b -> ListTr f a d
rotate ListTr f b c
xs ListTr (Op f) b a
ys ListTr f a a
forall k (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr
{-# INLINABLE exec #-}

rotate :: ListTr f c d -> ListTr (Op f) c b -> ListTr f a b -> ListTr f a d
rotate :: ListTr f c d -> ListTr (Op f) c b -> ListTr f a b -> ListTr f a d
rotate ListTr f c d
NilTr         (ConsTr (Op f b b
f) ListTr (Op f) c b
NilTr) ListTr f a b
a = f b b -> ListTr f a b -> ListTr f a b
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr f b b
f ListTr f a b
a
rotate (ConsTr f b d
f ListTr f c b
fs) (ConsTr (Op f b b
g) ListTr (Op f) c b
gs)    ListTr f a b
a = f b d -> ListTr f a b -> ListTr f a d
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr f b d
f (ListTr f c b -> ListTr (Op f) c b -> ListTr f a b -> ListTr f a b
forall k (f :: k -> k -> *) (c :: k) (d :: k) (b :: k) (a :: k).
ListTr f c d -> ListTr (Op f) c b -> ListTr f a b -> ListTr f a d
rotate ListTr f c b
fs ListTr (Op f) c b
gs (f b b -> ListTr f a b -> ListTr f a b
forall k (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr f b b
g ListTr f a b
a))
rotate ListTr f c d
_             ListTr (Op f) c b
_                     ListTr f a b
_ = String -> ListTr f a d
forall a. HasCallStack => String -> a
error String
"Queue.rotate: impossible happend"