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

{-# OPTIONS_HADDOCK show-extensions #-}

-- | 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 (..))
import           Data.Kind (Type)

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

-- | Opposite category 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 { forall k (f :: k -> k -> *) (a :: k) (b :: k). Op f a b -> f b a
runOp :: f b a }
  deriving Int -> Op f a b -> ShowS
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 k (f :: k -> k -> *) (g :: k -> k -> *) (a :: k) (b :: k).
(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) = forall k (f :: k -> k -> *) (a :: k) (b :: k). f b a -> Op f a b
Op (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 :: forall (a :: k). Op f a a
id = forall k (f :: k -> k -> *) (a :: k) (b :: k). f b a -> Op f a b
Op forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
    Op f c b
f . :: forall (b :: k) (c :: k) (a :: k). Op f b c -> Op f a b -> Op f a c
. Op f b a
g = forall k (f :: k -> k -> *) (a :: k) (b :: k). f b a -> Op f a b
Op (f b a
g 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
(<>) = 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 = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id


--
-- 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 :: forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
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 forall a. Num a => a -> a -> a
+ 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 :: forall k (f :: k -> k -> *) (x :: k) (y :: k) (z :: k).
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 = 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 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
ys
{-# INLINE [1] composeL #-}

liftL :: forall k (f :: k -> k -> Type) x y.
         f x y -> ListTr f x y
liftL :: forall k (f :: k -> k -> *) (x :: k) (y :: k).
f x y -> ListTr f x y
liftL f x y
f = 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 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 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 forall (x :: k) (y :: k). f x y -> c x y
_   ListTr f a b
NilTr     = 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) = forall (x :: k) (y :: k). f x y -> c x y
fun f b b
bc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. 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 {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 d
NilTr          = c a b
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) = forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z
nat f b d
xd (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 {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
bd ListTr f a b
NilTr          = 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 {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 (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 {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 = case (ListTr f a b
queueA, ListTr f a' b'
queueB) of
    (ListTr f a b
NilTr, ListTr f a' b'
NilTr) -> 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') -> forall {k} (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr (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')
`fn` f b b'
trB') (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 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) -> 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' forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
`fn` forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)   (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' 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')
                                 -> 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' 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 {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')

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 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show f b b
x forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListTr f a b
xs

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

  codom2 :: forall (f :: k -> k -> *).
AlgebraType0 ListTr f =>
Proof (AlgebraType ListTr (ListTr f)) (ListTr f)
codom2  = forall {l} (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: forall (f :: k -> k -> *).
AlgebraType ListTr f =>
Proof (AlgebraType0 ListTr f) (ListTr f)
forget2 = 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 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 = forall {k} (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr

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

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

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


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


-- | Type aligned real time queues; Based on `Purely Functional 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 :: forall {k} (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
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)
-> ((# #) -> r)
-> r
ConsQ a as <- (unconsQ -> a :< as) where
    ConsQ = 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 :: forall {k} (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
$mNilQ :: forall {r} {k} {a :: k} {b :: k} {f :: k -> k -> *}.
Queue f a b -> ((a ~ b) => r) -> ((# #) -> r) -> r
NilQ <- (unconsQ -> EmptyL) where
    NilQ = forall k (f :: k -> k -> *) (a :: k). Queue f a a
nilQ

{-# complete NilQ, ConsQ #-}

composeQ :: forall k (f :: k -> k -> Type) x y z.
            Queue f y z
         -> Queue f x y
         -> Queue f x z
composeQ :: forall k (f :: k -> k -> *) (x :: k) (y :: k) (z :: k).
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 = 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 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
q2
{-# INLINE [1] composeQ #-}

nilQ :: Queue (f :: k -> k -> Type) a a
nilQ :: forall k (f :: k -> k -> *) (a :: k). Queue f a a
nilQ = 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 forall {k} (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr forall {k} (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr 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 :: forall k (f :: k -> k -> *) (a :: k) (b :: k) (c :: k).
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) = 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 (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 (forall {k} (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr 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 :: forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
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
_)     = 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 forall {k} (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> Queue f a b -> ViewL 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 b
f ListTr (Op f) b a
r ListTr f b x
s
unconsQ Queue 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 :: forall k (f :: k -> k -> *) (a :: k) (b :: k) (c :: k).
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 = 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 (forall {k} (f :: k -> k -> *) (b :: k) (c :: k) (a :: k).
f b c -> ListTr f a b -> ListTr f a c
ConsTr (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 {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 d
NilQ          = c a b
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) = forall (x :: k) (y :: k) (z :: k). f y z -> c x y -> c x z
nat f b d
xd (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 :: forall k (f :: k -> k -> *) (a :: k) (b :: k). f a b -> Queue f a b
liftQ = \f a b
fab -> 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 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 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 forall (x :: k) (y :: k). f x y -> c x y
nat = 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 -> forall (x :: k) (y :: k). f x y -> c x y
nat f y z
f 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) 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 {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
bd Queue f a b
NilQ          = 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 {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 (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 {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 = case (Queue f a b
queueA, Queue f a' b'
queueB) of
    (Queue f a b
NilQ, Queue f a' b'
NilQ) -> 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') -> forall {k} (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
ConsQ (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')
`fn` f b b'
trB') (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 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) -> 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' forall (x :: k) (y :: k) (x' :: k) (y' :: k).
f x y -> f x' y' -> f (g x x') (g y y')
`fn` forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)   (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' 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')
                               -> 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' 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 {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 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 = case Queue f a b
q of
    Queue f a b
NilQ        -> 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' -> forall {k} (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
ConsQ (forall (x :: k) (y :: k). f x y -> g x y
nat f b b
tr) (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

#-}

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 ("
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListTr f b b
f
        forall a. [a] -> [a] -> [a]
++ String
") ("
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ListTr (Op f) b a
r
        forall a. [a] -> [a] -> [a]
++ String
") "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (f :: k -> k -> *) (a :: k) (b :: k).
ListTr f a b -> Int
lengthListTr ListTr f b x
s)

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

  codom2 :: forall (f :: k -> k -> *).
AlgebraType0 Queue f =>
Proof (AlgebraType Queue (Queue f)) (Queue f)
codom2  = forall {l} (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: forall (f :: k -> k -> *).
AlgebraType Queue f =>
Proof (AlgebraType0 Queue f) (Queue f)
forget2 = 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 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 = 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 :: forall b c. (b -> c) -> Queue f b c
arr b -> c
ab = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
ab forall {k} (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` 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) *** :: forall b c b' c'.
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 forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** f b c'
fyb)    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 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 forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) 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 forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, 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) = (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr 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')
*** f b c'
fxb) forall {k} (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` (forall {k} (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ 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            = forall {k} (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ

instance ArrowZero f => ArrowZero (Queue f) where
  zeroArrow :: forall b c. Queue f b c
zeroArrow = forall (a :: * -> * -> *) b c. ArrowZero a => a b c
zeroArrow forall {k} (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` 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) +++ :: forall b c b' c'.
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 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)    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 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 forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) 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 forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c 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) = (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr 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')
+++ f b c'
fxb) forall {k} (f :: k -> k -> *) (c :: k) (a :: k) (b :: k).
f b c -> Queue f a b -> Queue f a c
`ConsQ` (forall {k} (a :: k) (b :: k) (f :: k -> k -> *).
(a ~ b) =>
Queue f a b
NilQ 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            = 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 :: 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
xs ListTr (Op f) b a
ys (ConsTr f b x
_ ListTr f b b
t) = 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        = 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' forall {k} (f :: k -> k -> *) (a :: k). ListTr f a a
NilTr ListTr f a c
xs'
  where
    xs' :: ListTr f a c
xs' = 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 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 :: 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 d
NilTr         (ConsTr (Op f b b
f) ListTr (Op f) c b
NilTr) ListTr f a 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
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 = 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 (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 (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
_ = forall a. HasCallStack => String -> a
error String
"Queue.rotate: impossible happend"