{-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Structure.Some.Stream where import Pandora.Core.Functor (type (:=), type (:=>), type (:::)) import Pandora.Pattern.Semigroupoid ((.)) import Pandora.Pattern.Category (($), (#)) import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-))) import Pandora.Pattern.Functor.Extendable (Extendable ((<<=))) import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)), twosome) import Pandora.Paradigm.Primary.Algebraic (extract) import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity)) import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right)) import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct, (.-+)) import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap)) import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Rotate), premorph, rotate) import Pandora.Paradigm.Structure.Ability.Zipper (Zipper) import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>)) import Pandora.Paradigm.Primary.Algebraic (point) type Stream = Construction Identity type instance Zipper (Construction Identity) (Left ::: Right) = Tap (Stream <:.:> Stream := (:*:)) instance Morphable (Rotate Left) (Tap (Stream <:.:> Stream := (:*:))) where type Morphing (Rotate Left) (Tap (Stream <:.:> Stream := (:*:))) = Tap (Stream <:.:> Stream := (:*:)) morphing :: (<:.>) (Tagged ('Rotate 'Left)) (Tap ((Stream <:.:> Stream) := (:*:))) a -> Morphing ('Rotate 'Left) (Tap ((Stream <:.:> Stream) := (:*:))) a morphing ((<:.>) (Tagged ('Rotate 'Left)) (Tap ((Stream <:.:> Stream) := (:*:))) a -> Tap ((Stream <:.:> Stream) := (:*:)) a forall k (mod :: k) (struct :: * -> *). Morphable mod struct => (Tagged mod <:.> struct) ~> struct premorph -> Tap a x (T_U (Stream a bs :*: Stream a fs))) = a -> T_U Covariant Covariant (:*:) Stream Stream a -> Tap ((Stream <:.:> Stream) := (:*:)) a forall (t :: * -> *) a. a -> t a -> Tap t a Tap (a -> T_U Covariant Covariant (:*:) Stream Stream a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> a -> T_U Covariant Covariant (:*:) Stream Stream a -> Tap ((Stream <:.:> Stream) := (:*:)) a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # Stream a -> a forall (t :: * -> *) a. Extractable_ t => t a -> a extract Stream a bs (T_U Covariant Covariant (:*:) Stream Stream a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> T_U Covariant Covariant (:*:) Stream Stream a -> Tap ((Stream <:.:> Stream) := (:*:)) a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ Stream a -> Stream a -> T_U Covariant Covariant (:*:) Stream Stream a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome (Stream a -> Stream a -> T_U Covariant Covariant (:*:) Stream Stream a) -> Stream a -> Stream a -> T_U Covariant Covariant (:*:) Stream Stream a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # Identity (Stream a) -> Stream a forall (t :: * -> *) a. Extractable_ t => t a -> a extract (Stream a -> Identity (Stream a) forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Stream a bs) (Stream a -> T_U Covariant Covariant (:*:) Stream Stream a) -> Stream a -> T_U Covariant Covariant (:*:) Stream Stream a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # a -> Identity (Stream a) -> Stream a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Stream a -> Identity (Stream a) forall (t :: * -> *) a. Monoidal (->) (->) (:*:) (:*:) t => a -> t a point Stream a fs) instance Morphable (Rotate Right) (Tap (Stream <:.:> Stream := (:*:))) where type Morphing (Rotate Right) (Tap (Stream <:.:> Stream := (:*:))) = Tap (Stream <:.:> Stream := (:*:)) morphing :: (<:.>) (Tagged ('Rotate 'Right)) (Tap ((Stream <:.:> Stream) := (:*:))) a -> Morphing ('Rotate 'Right) (Tap ((Stream <:.:> Stream) := (:*:))) a morphing ((<:.>) (Tagged ('Rotate 'Right)) (Tap ((Stream <:.:> Stream) := (:*:))) a -> Tap ((Stream <:.:> Stream) := (:*:)) a forall k (mod :: k) (struct :: * -> *). Morphable mod struct => (Tagged mod <:.> struct) ~> struct premorph -> Tap a x (T_U (Stream a bs :*: Stream a fs))) = a -> T_U Covariant Covariant (:*:) Stream Stream a -> Tap ((Stream <:.:> Stream) := (:*:)) a forall (t :: * -> *) a. a -> t a -> Tap t a Tap (a -> T_U Covariant Covariant (:*:) Stream Stream a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> a -> T_U Covariant Covariant (:*:) Stream Stream a -> Tap ((Stream <:.:> Stream) := (:*:)) a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # Stream a -> a forall (t :: * -> *) a. Extractable_ t => t a -> a extract Stream a fs (T_U Covariant Covariant (:*:) Stream Stream a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> T_U Covariant Covariant (:*:) Stream Stream a -> Tap ((Stream <:.:> Stream) := (:*:)) a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ Stream a -> Stream a -> T_U Covariant Covariant (:*:) Stream Stream a forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome (Stream a -> Stream a -> T_U Covariant Covariant (:*:) Stream Stream a) -> Stream a -> Stream a -> T_U Covariant Covariant (:*:) Stream Stream a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # a -> ((Identity :. Stream) := a) -> Stream a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Stream a -> (Identity :. Stream) := a forall (t :: * -> *) a. Monoidal (->) (->) (:*:) (:*:) t => a -> t a point Stream a bs) (Stream a -> T_U Covariant Covariant (:*:) Stream Stream a) -> Stream a -> T_U Covariant Covariant (:*:) Stream Stream a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # ((Identity :. Stream) := a) -> Stream a forall (t :: * -> *) a. Extractable_ t => t a -> a extract (Stream a -> (Identity :. Stream) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Stream a fs) instance {-# OVERLAPS #-} Extendable (->) (Tap (Stream <:.:> Stream := (:*:))) where Tap ((Stream <:.:> Stream) := (:*:)) a -> b f <<= :: (Tap ((Stream <:.:> Stream) := (:*:)) a -> b) -> Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) b <<= Tap ((Stream <:.:> Stream) := (:*:)) a z = let move :: (Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) move Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a rtt = Identity (Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a)) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (t :: * -> *) a. Extractable_ t => t a -> a extract (Identity (Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a)) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a)) -> (Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> Identity (Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a))) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> Identity (Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a)) forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct (Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a)) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ Tap ((Stream <:.:> Stream) := (:*:)) a -> Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (t :: * -> *) a. Monoidal (->) (->) (:*:) (:*:) t => a -> t a point (Tap ((Stream <:.:> Stream) := (:*:)) a -> Identity (Tap ((Stream <:.:> Stream) := (:*:)) a)) -> (Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> Tap ((Stream <:.:> Stream) := (:*:)) a -> Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a rtt (Tap ((Stream <:.:> Stream) := (:*:)) a -> Identity (Tap ((Stream <:.:> Stream) := (:*:)) a)) -> Tap ((Stream <:.:> Stream) := (:*:)) a :=> Stream forall (t :: * -> *) a. Covariant (->) (->) t => (a :=> t) -> a :=> Construction t .-+ Tap ((Stream <:.:> Stream) := (:*:)) a z in Tap ((Stream <:.:> Stream) := (:*:)) a -> b f (Tap ((Stream <:.:> Stream) := (:*:)) a -> b) -> Tap ((Stream <:.:> Stream) := (:*:)) (Tap ((Stream <:.:> Stream) := (:*:)) a) -> Tap ((Stream <:.:> Stream) := (:*:)) b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) -<$>- Tap ((Stream <:.:> Stream) := (:*:)) a -> (:=) (Stream <:.:> Stream) (:*:) (Tap ((Stream <:.:> Stream) := (:*:)) a) -> Tap ((Stream <:.:> Stream) := (:*:)) (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (t :: * -> *) a. a -> t a -> Tap t a Tap Tap ((Stream <:.:> Stream) := (:*:)) a z (Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> (:=) (Stream <:.:> Stream) (:*:) (Tap ((Stream <:.:> Stream) := (:*:)) a) forall k (t :: k -> *) (a :: k) (u :: k -> *). t a -> u a -> (<:.:>) t u (:*:) a twosome (Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> (:=) (Stream <:.:> Stream) (:*:) (Tap ((Stream <:.:> Stream) := (:*:)) a)) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> (:=) (Stream <:.:> Stream) (:*:) (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # ((Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) move ((Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a)) -> (Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ forall a (mod :: a) (struct :: * -> *). Morphable ('Rotate mod) struct => struct ~> Morphing ('Rotate mod) struct forall (struct :: * -> *). Morphable ('Rotate 'Left) struct => struct ~> Morphing ('Rotate 'Left) struct rotate @Left) (Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> (:=) (Stream <:.:> Stream) (:*:) (Tap ((Stream <:.:> Stream) := (:*:)) a)) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) -> (:=) (Stream <:.:> Stream) (:*:) (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) # ((Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) move ((Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a)) -> (Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ forall a (mod :: a) (struct :: * -> *). Morphable ('Rotate mod) struct => struct ~> Morphing ('Rotate mod) struct forall (struct :: * -> *). Morphable ('Rotate 'Right) struct => struct ~> Morphing ('Rotate 'Right) struct rotate @Right)) repeat :: a :=> Stream repeat :: a :=> Stream repeat a x = a -> ((Identity :. Stream) := a) -> Construction Identity a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (((Identity :. Stream) := a) -> Construction Identity a) -> (Construction Identity a -> (Identity :. Stream) := a) -> Construction Identity a -> Construction Identity a forall (m :: * -> * -> *) b c a. Semigroupoid m => m b c -> m a b -> m a c . Construction Identity a -> (Identity :. Stream) := a forall a. a -> Identity a Identity (Construction Identity a -> Construction Identity a) -> Construction Identity a -> Construction Identity a forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) $ a :=> Stream forall a. a :=> Stream repeat a x