{-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Structure.Stream where import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Pointable (point) import Pandora.Pattern.Functor.Extractable (extract) import Pandora.Paradigm.Primary.Functor.Delta (Delta ((:^:))) 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.Rotatable (Rotatable (Rotational, rotation)) import Pandora.Paradigm.Structure.Ability.Zipper (Zipper) import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>)) type Stream = Construction Identity type instance Zipper Stream = Tap (Delta <:.> Stream) instance Rotatable Left (Tap (Delta <:.> Stream)) where type Rotational Left (Tap (Delta <:.> Stream)) a = Tap (Delta <:.> Stream) a rotation :: Tagged 'Left (Tap (Delta <:.> Stream) a) -> Rotational 'Left (Tap (Delta <:.> Stream)) a rotation (Tap (Delta <:.> Stream) a <-| Tagged 'Left forall (t :: * -> *) a. Extractable t => a <-| t extract -> Tap a x (TU (Stream a bs :^: Stream a fs))) = a -> TU Covariant Covariant Delta Stream a -> Tap (Delta <:.> Stream) a forall (t :: * -> *) a. a -> t a -> Tap t a Tap (a <-| Stream forall (t :: * -> *) a. Extractable t => a <-| t extract Stream a bs) (TU Covariant Covariant Delta Stream a -> Tap (Delta <:.> Stream) a) -> (Delta (Stream a) -> TU Covariant Covariant Delta Stream a) -> Delta (Stream a) -> Tap (Delta <:.> Stream) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Delta (Stream a) -> TU Covariant Covariant Delta Stream a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Delta (Stream a) -> Tap (Delta <:.> Stream) a) -> Delta (Stream a) -> Tap (Delta <:.> Stream) a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ Stream a <-| Identity forall (t :: * -> *) a. Extractable t => a <-| t extract (Stream a -> (:.) Identity Stream a forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Stream a bs) Stream a -> Stream a -> Delta (Stream a) forall a. a -> a -> Delta a :^: a -> Stream a <-| Identity forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (Stream a -> (:.) Identity Stream a forall (t :: * -> *) a. Pointable t => a |-> t point Stream a fs) instance Rotatable Right (Tap (Delta <:.> Stream)) where type Rotational Right (Tap (Delta <:.> Stream)) a = Tap (Delta <:.> Stream) a rotation :: Tagged 'Right (Tap (Delta <:.> Stream) a) -> Rotational 'Right (Tap (Delta <:.> Stream)) a rotation (Tap (Delta <:.> Stream) a <-| Tagged 'Right forall (t :: * -> *) a. Extractable t => a <-| t extract -> Tap a x (TU (Stream a bs :^: Stream a fs))) = a -> TU Covariant Covariant Delta Stream a -> Tap (Delta <:.> Stream) a forall (t :: * -> *) a. a -> t a -> Tap t a Tap (a <-| Stream forall (t :: * -> *) a. Extractable t => a <-| t extract Stream a fs) (TU Covariant Covariant Delta Stream a -> Tap (Delta <:.> Stream) a) -> (Delta (Stream a) -> TU Covariant Covariant Delta Stream a) -> Delta (Stream a) -> Tap (Delta <:.> Stream) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Delta (Stream a) -> TU Covariant Covariant Delta Stream a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (Delta (Stream a) -> Tap (Delta <:.> Stream) a) -> Delta (Stream a) -> Tap (Delta <:.> Stream) a forall (m :: * -> * -> *) a b. Category 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 forall (t :: * -> *) a. Pointable t => a |-> t point Stream a bs) Stream a -> Stream a -> Delta (Stream a) forall a. a -> a -> Delta a :^: ((Identity :. Stream) := a) -> Stream a forall (t :: * -> *) a. Extractable t => a <-| t extract (Stream a |-> Identity forall (t :: * -> *) a. Construction t a -> (:.) t (Construction t) a deconstruct Stream a fs) repeat :: a -> Stream a repeat :: a -> Stream a repeat a x = a -> ((Identity :. Stream) := a) -> Stream a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (((Identity :. Stream) := a) -> Stream a) -> (Stream a -> (Identity :. Stream) := a) -> Stream a -> Stream a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Stream a -> (Identity :. Stream) := a forall a. a -> Identity a Identity (Stream a -> Stream a) -> Stream a -> Stream a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a -> Stream a forall a. a -> Stream a repeat a x