{-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Structure.Some.Stream where import Pandora.Core.Functor (type (:=), type (:=>)) import Pandora.Pattern.Category ((.), ($), (/)) import Pandora.Pattern.Functor.Covariant (Covariant ((<$>))) import Pandora.Pattern.Functor.Pointable (point) import Pandora.Pattern.Functor.Extractable (extract) import Pandora.Pattern.Functor.Extendable (Extendable ((=>>))) import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), twosome) 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 (<:.:>)) type Stream = Construction Identity type instance Zipper Stream = 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 (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t 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 <:= Stream forall (t :: * -> *) a. Extractable t => a <:= t 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 :: * -> * -> *). Category m => m ~~> m $ 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 :: * -> * -> *). Category m => m ~~> m / 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 -> T_U Covariant Covariant (:*:) Stream Stream a) -> Stream a -> T_U Covariant Covariant (:*:) Stream Stream a forall (m :: * -> * -> *). Category m => m ~~> m / 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 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 (f :: k) (t :: * -> *). Morphable f t => (Tagged f <:.> t) ~> t 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 :: * -> * -> *). Category m => m ~~> m / a <:= Stream forall (t :: * -> *) a. Extractable t => a <:= t 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 :: * -> * -> *). Category m => m ~~> m $ 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 :: * -> * -> *). Category m => m ~~> m / 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 -> T_U Covariant Covariant (:*:) Stream Stream a) -> Stream a -> T_U Covariant Covariant (:*:) Stream Stream a forall (m :: * -> * -> *). Category m => m ~~> m / ((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) instance {-# OVERLAPS #-} Extendable (Tap (Stream <:.:> Stream := (:*:))) where Tap ((Stream <:.:> Stream) := (:*:)) a z =>> :: Tap ((Stream <:.:> Stream) := (:*:)) a -> (Tap ((Stream <:.:> Stream) := (:*:)) a -> b) -> Tap ((Stream <:.:> Stream) := (:*:)) b =>> Tap ((Stream <:.:> Stream) := (:*:)) a -> b f = 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 = Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) <:= Identity forall (t :: * -> *) a. Extractable t => a <:= t extract (Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) <:= Identity) -> (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. Category 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 :: * -> * -> *). Category m => m ~~> m $ Tap ((Stream <:.:> Stream) := (:*:)) a -> Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) forall (t :: * -> *) a. Pointable t => a :=> t 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. Category 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 (t :: * -> *) a b. Covariant t => (a -> b) -> 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 :: * -> * -> *). Category m => m ~~> m / (Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) move (forall a (f :: a) (t :: * -> *). Morphable ('Rotate f) t => t ~> Morphing ('Rotate f) t forall (t :: * -> *). Morphable ('Rotate 'Left) t => t ~> Morphing ('Rotate 'Left) t 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 :: * -> * -> *). Category m => m ~~> m / (Tap ((Stream <:.:> Stream) := (:*:)) a -> Tap ((Stream <:.:> Stream) := (:*:)) a) -> Construction Identity (Tap ((Stream <:.:> Stream) := (:*:)) a) move (forall a (f :: a) (t :: * -> *). Morphable ('Rotate f) t => t ~> Morphing ('Rotate f) t forall (t :: * -> *). Morphable ('Rotate 'Right) t => t ~> Morphing ('Rotate 'Right) t 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. Category 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 :: * -> * -> *). Category m => m ~~> m $ a :=> Stream forall a. a :=> Stream repeat a x