{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure.Some.Stream where

import Pandora.Core.Impliable (imply)
import Pandora.Core.Interpreted (run)
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<-----), (-->))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|--)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<-/-)))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>), (<:*:>))
import Pandora.Paradigm.Algebraic.Functor (extract, empty, (-*))
import Pandora.Paradigm.Primary.Auxiliary (Horizontal (Left, Right))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct, constitute)
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse (Reverse))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Rotate), premorph, rotate)
import Pandora.Paradigm.Structure.Interface.Zipper (Zippable (Breadcrumbs, fasten))
import Pandora.Paradigm.Structure.Interface.Stack (Stack (Topping, push, pop, top))
import Pandora.Paradigm.Structure.Modification.Tape (Tape)
import Pandora.Paradigm.Inventory.Some.State (change, current)
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
import Pandora.Paradigm.Schemes.TT (TT (TT))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U))
import Pandora.Paradigm.Algebraic (point)

type Stream = Construction Exactly

instance Zippable (Construction Exactly) where
	type Breadcrumbs (Construction Exactly) = Reverse Stream <:*:> Stream
	-- TODO: It should not return Maybe since Stream is not empty, try to use Simplification (Fastenable structure) here
	fasten :: Construction Exactly e -> Maybe > Zipper (Construction Exactly) e
fasten (Construct e
x (Exactly :. Construction Exactly) >>> e
xs) = ((Exactly
  <:*:> T_U
          Covariant
          Covariant
          (:*:)
          (Reverse (Construction Exactly))
          (Construction Exactly))
 >>>>>> e)
-> Maybe
     ((Exactly
       <:*:> T_U
               Covariant
               Covariant
               (:*:)
               (Reverse (Construction Exactly))
               (Construction Exactly))
      >>>>>> e)
forall a. a -> Maybe a
Just (((Exactly
   <:*:> T_U
           Covariant
           Covariant
           (:*:)
           (Reverse (Construction Exactly))
           (Construction Exactly))
  >>>>>> e)
 -> Maybe
      ((Exactly
        <:*:> T_U
                Covariant
                Covariant
                (:*:)
                (Reverse (Construction Exactly))
                (Construction Exactly))
       >>>>>> e))
-> ((Exactly
     <:*:> T_U
             Covariant
             Covariant
             (:*:)
             (Reverse (Construction Exactly))
             (Construction Exactly))
    >>>>>> e)
-> Maybe
     ((Exactly
       <:*:> T_U
               Covariant
               Covariant
               (:*:)
               (Reverse (Construction Exactly))
               (Construction Exactly))
      >>>>>> e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- e -> Exactly e
forall a. a -> Exactly a
Exactly e
x Exactly e
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse (Construction Exactly))
     (Construction Exactly)
     e
-> (Exactly
    <:*:> T_U
            Covariant
            Covariant
            (:*:)
            (Reverse (Construction Exactly))
            (Construction Exactly))
   >>>>>> e
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> Construction Exactly e -> Reverse (Construction Exactly) e
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse (Construction Exactly e -> Reverse (Construction Exactly) e)
-> Construction Exactly e -> Reverse (Construction Exactly) e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Exactly :. Construction Exactly) >>> e) -> Construction Exactly e
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly :. Construction Exactly) >>> e
xs Reverse (Construction Exactly) e
-> Construction Exactly e
-> T_U
     Covariant
     Covariant
     (:*:)
     (Reverse (Construction Exactly))
     (Construction Exactly)
     e
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> ((Exactly :. Construction Exactly) >>> e) -> Construction Exactly e
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly :. Construction Exactly) >>> e
xs

-- TODO: Try to generalize to Extendable (Tape structure)
instance {-# OVERLAPS #-} Extendable (->) (Tape Stream) where
	Tape (Construction Exactly) a -> b
f <<= :: (Tape (Construction Exactly) a -> b)
-> Tape (Construction Exactly) a -> Tape (Construction Exactly) b
<<= Tape (Construction Exactly) a
z = let move :: (Tape (Construction Exactly) a -> Tape (Construction Exactly) a)
-> Construction Exactly (Tape (Construction Exactly) a)
move Tape (Construction Exactly) a -> Tape (Construction Exactly) a
rtt = Exactly (Construction Exactly (Tape (Construction Exactly) a))
-> Construction Exactly (Tape (Construction Exactly) a)
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly (Construction Exactly (Tape (Construction Exactly) a))
 -> Construction Exactly (Tape (Construction Exactly) a))
-> (Construction Exactly (Tape (Construction Exactly) a)
    -> Exactly (Construction Exactly (Tape (Construction Exactly) a)))
-> Construction Exactly (Tape (Construction Exactly) a)
-> Construction Exactly (Tape (Construction Exactly) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Exactly (Tape (Construction Exactly) a)
-> Exactly (Construction Exactly (Tape (Construction Exactly) a))
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct (Construction Exactly (Tape (Construction Exactly) a)
 -> Construction Exactly (Tape (Construction Exactly) a))
-> Construction Exactly (Tape (Construction Exactly) a)
-> Construction Exactly (Tape (Construction Exactly) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (Tape (Construction Exactly) a
 -> Exactly (Tape (Construction Exactly) a))
-> Tape (Construction Exactly) a
-> Construction Exactly (Tape (Construction Exactly) a)
forall (t :: * -> *) a.
Covariant (->) (->) t =>
(a -> t a) -> a -> Construction t a
constitute ((Tape (Construction Exactly) a
  -> Exactly (Tape (Construction Exactly) a))
 -> Tape (Construction Exactly) a
 -> Construction Exactly (Tape (Construction Exactly) a))
-> (Tape (Construction Exactly) a
    -> Exactly (Tape (Construction Exactly) a))
-> Tape (Construction Exactly) a
-> Construction Exactly (Tape (Construction Exactly) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Tape (Construction Exactly) a
-> Exactly (Tape (Construction Exactly) a)
forall (t :: * -> *) a. Pointable t => a -> t a
point (Tape (Construction Exactly) a
 -> Exactly (Tape (Construction Exactly) a))
-> (Tape (Construction Exactly) a -> Tape (Construction Exactly) a)
-> Tape (Construction Exactly) a
-> Exactly (Tape (Construction Exactly) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Tape (Construction Exactly) a -> Tape (Construction Exactly) a
rtt (Tape (Construction Exactly) a
 -> Construction Exactly (Tape (Construction Exactly) a))
-> Tape (Construction Exactly) a
-> Construction Exactly (Tape (Construction Exactly) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Tape (Construction Exactly) a
z in
		Tape (Construction Exactly) a -> b
f (Tape (Construction Exactly) a -> b)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Exactly))
        (Construction Exactly))
     (Tape (Construction Exactly) a)
-> Tape (Construction Exactly) b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- Impliable
  (T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Exactly))
        (Construction Exactly))
     (Tape (Construction Exactly) a)) =>
Arguments
  (T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Exactly))
        (Construction Exactly))
     (Tape (Construction Exactly) a))
forall k (result :: k). Impliable result => Arguments result
imply @(Tape Stream _) (Tape (Construction Exactly) a
 -> Construction Exactly (Tape (Construction Exactly) a)
 -> Construction Exactly (Tape (Construction Exactly) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Exactly))
         (Construction Exactly))
      (Tape (Construction Exactly) a))
-> Tape (Construction Exactly) a
-> Construction Exactly (Tape (Construction Exactly) a)
-> Construction Exactly (Tape (Construction Exactly) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Exactly))
        (Construction Exactly))
     (Tape (Construction Exactly) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Tape (Construction Exactly) a
z (Construction Exactly (Tape (Construction Exactly) a)
 -> Construction Exactly (Tape (Construction Exactly) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Exactly))
         (Construction Exactly))
      (Tape (Construction Exactly) a))
-> Construction Exactly (Tape (Construction Exactly) a)
-> Construction Exactly (Tape (Construction Exactly) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Exactly))
        (Construction Exactly))
     (Tape (Construction Exactly) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (Tape (Construction Exactly) a -> Tape (Construction Exactly) a)
-> Construction Exactly (Tape (Construction Exactly) a)
move (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 Exactly (Tape (Construction Exactly) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Exactly))
         (Construction Exactly))
      (Tape (Construction Exactly) a))
-> Construction Exactly (Tape (Construction Exactly) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (T_U
        Covariant
        Covariant
        (:*:)
        (Reverse (Construction Exactly))
        (Construction Exactly))
     (Tape (Construction Exactly) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (Tape (Construction Exactly) a -> Tape (Construction Exactly) a)
-> Construction Exactly (Tape (Construction Exactly) a)
move (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)

instance Stack (Construction Exactly) where
	type Topping (Construction Exactly) = Exactly
	top :: ((Lens < Topping (Construction Exactly)) < Construction Exactly e)
< e
top = (Construction Exactly e
 -> Store (Exactly e) (Construction Exactly e))
-> P_Q_T (->) Store Exactly (Construction Exactly e) e
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T ((Construction Exactly e
  -> Store (Exactly e) (Construction Exactly e))
 -> P_Q_T (->) Store Exactly (Construction Exactly e) e)
-> (Construction Exactly e
    -> Store (Exactly e) (Construction Exactly e))
-> P_Q_T (->) Store Exactly (Construction Exactly e) e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \Construction Exactly e
xs -> (((:*:) (Exactly e) :. (->) (Exactly e))
 >>> Construction Exactly e)
-> Store (Exactly e) (Construction Exactly e)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Exactly e) :. (->) (Exactly e))
  >>> Construction Exactly e)
 -> Store (Exactly e) (Construction Exactly e))
-> (((:*:) (Exactly e) :. (->) (Exactly e))
    >>> Construction Exactly e)
-> Store (Exactly e) (Construction Exactly e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- e -> Exactly e
forall a. a -> Exactly a
Exactly (Construction Exactly e -> e
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Exactly e
xs) Exactly e
-> (Exactly e -> Construction Exactly e)
-> ((:*:) (Exactly e) :. (->) (Exactly e))
   >>> Construction Exactly e
forall s a. s -> a -> s :*: a
:*: \(Exactly e
new) -> e
-> ((Exactly :. Construction Exactly) >>> e)
-> Construction Exactly e
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct e
new (((Exactly :. Construction Exactly) >>> e)
 -> Construction Exactly e)
-> ((Exactly :. Construction Exactly) >>> e)
-> Construction Exactly e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Construction Exactly e -> (Exactly :. Construction Exactly) >>> e
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Construction Exactly e
xs
	pop :: (State < Construction Exactly e) < Topping (Construction Exactly) e
pop = (\(Construct e
x (Exactly :. Construction Exactly) >>> e
xs) -> Exactly e -> ((Exactly :. Construction Exactly) >>> e) -> Exactly e
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (Exactly e
 -> ((Exactly :. Construction Exactly) >>> e) -> Exactly e)
-> Exactly e
-> ((Exactly :. Construction Exactly) >>> e)
-> Exactly e
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- e -> Exactly e
forall a. a -> Exactly a
Exactly e
x (((Exactly :. Construction Exactly) >>> e) -> Exactly e)
-> State
     (Construction Exactly e) ((Exactly :. Construction Exactly) >>> e)
-> State (Construction Exactly e) (Exactly e)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
forall (t :: * -> *).
Stateful (Construction Exactly e) t =>
(Construction Exactly e -> Construction Exactly e)
-> t (Construction Exactly e)
change @(Stream _) ((Construction Exactly e -> Construction Exactly e)
 -> State (Construction Exactly e) (Construction Exactly e))
-> (Construction Exactly e
    -> Construction Exactly e -> Construction Exactly e)
-> Construction Exactly e
-> State (Construction Exactly e) (Construction Exactly e)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Exactly e
-> Construction Exactly e -> Construction Exactly e
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (Construction Exactly e
 -> State (Construction Exactly e) (Construction Exactly e))
-> ((Exactly :. Construction Exactly) >>> e)
-> State
     (Construction Exactly e) ((Exactly :. Construction Exactly) >>> e)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
 Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<-/- (Exactly :. Construction Exactly) >>> e
xs) (Construction Exactly e
 -> State (Construction Exactly e) (Exactly e))
-> State (Construction Exactly e) (Construction Exactly e)
-> State (Construction Exactly e) (Exactly e)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< State (Construction Exactly e) (Construction Exactly e)
forall s (t :: * -> *). Stateful s t => t s
current
	push :: e -> (State < Construction Exactly e) < e
push e
x = ((Construction Exactly e -> Construction Exactly e)
-> State (Construction Exactly e) (Construction Exactly e)
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
change ((Construction Exactly e -> Construction Exactly e)
 -> State (Construction Exactly e) (Construction Exactly e))
-> (Construction Exactly e -> Construction Exactly e)
-> State (Construction Exactly e) (Construction Exactly e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- e
-> ((Exactly :. Construction Exactly) >>> e)
-> Construction Exactly e
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct e
x (((Exactly :. Construction Exactly) >>> e)
 -> Construction Exactly e)
-> (Construction Exactly e
    -> (Exactly :. Construction Exactly) >>> e)
-> Construction Exactly e
-> Construction Exactly e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Exactly e -> (Exactly :. Construction Exactly) >>> e
forall a. a -> Exactly a
Exactly) State (Construction Exactly e) (Construction Exactly e)
-> ((State < Construction Exactly e) < e)
-> (State < Construction Exactly e) < e
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t a -> t b -> t b
-* e -> (State < Construction Exactly e) < e
forall (t :: * -> *) a. Pointable t => a -> t a
point e
x

instance Morphable (Rotate Left) (Tape Stream) where
	type Morphing (Rotate Left) (Tape Stream) = Tape Stream
	morphing :: (<::>)
  (Tagged ('Rotate 'Left))
  (Exactly
   <:*:> T_U
           Covariant
           Covariant
           (:*:)
           (Reverse (Construction Exactly))
           (Construction Exactly))
  a
-> Morphing
     ('Rotate 'Left)
     (Exactly
      <:*:> T_U
              Covariant
              Covariant
              (:*:)
              (Reverse (Construction Exactly))
              (Construction Exactly))
     a
morphing (Tape (Construction Exactly) a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Exactly))
         (Construction Exactly)
         a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Tape (Construction Exactly) a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse (Construction Exactly))
          (Construction Exactly)
          a)
-> ((<::>)
      (Tagged ('Rotate 'Left))
      (Exactly
       <:*:> T_U
               Covariant
               Covariant
               (:*:)
               (Reverse (Construction Exactly))
               (Construction Exactly))
      a
    -> Tape (Construction Exactly) a)
-> (<::>)
     (Tagged ('Rotate 'Left))
     (Exactly
      <:*:> T_U
              Covariant
              Covariant
              (:*:)
              (Reverse (Construction Exactly))
              (Construction Exactly))
     a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Exactly))
         (Construction Exactly)
         a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>)
  (Tagged ('Rotate 'Left))
  (Exactly
   <:*:> T_U
           Covariant
           Covariant
           (:*:)
           (Reverse (Construction Exactly))
           (Construction Exactly))
  a
-> Tape (Construction Exactly) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Exactly a
x :*: T_U (Reverse Construction Exactly a
ls :*: Construction Exactly a
rs)) =
		Impliable (Tape (Construction Exactly) a) =>
Arguments (Tape (Construction Exactly) a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape Stream _) (a
 -> Construction Exactly a
 -> Construction Exactly a
 -> Tape (Construction Exactly) a)
-> a
-> Construction Exactly a
-> Construction Exactly a
-> Tape (Construction Exactly) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Construction Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Exactly a
ls (Construction Exactly a
 -> Construction Exactly a -> Tape (Construction Exactly) a)
-> Construction Exactly a
-> Construction Exactly a
-> Tape (Construction Exactly) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Exactly (Construction Exactly a) -> Construction Exactly a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Construction Exactly a -> Exactly (Construction Exactly a)
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Construction Exactly a
ls) (Construction Exactly a -> Tape (Construction Exactly) a)
-> Construction Exactly a -> Tape (Construction Exactly) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a -> Exactly (Construction Exactly a) -> Construction Exactly a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct a
x (Exactly (Construction Exactly a) -> Construction Exactly a)
-> Exactly (Construction Exactly a) -> Construction Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
--> Construction Exactly a -> Exactly (Construction Exactly a)
forall (t :: * -> *) a. Pointable t => a -> t a
point Construction Exactly a
rs

instance Morphable (Rotate Right) (Tape Stream) where
	type Morphing (Rotate Right) (Tape Stream) = Tape Stream
	morphing :: (<::>)
  (Tagged ('Rotate 'Right))
  (Exactly
   <:*:> T_U
           Covariant
           Covariant
           (:*:)
           (Reverse (Construction Exactly))
           (Construction Exactly))
  a
-> Morphing
     ('Rotate 'Right)
     (Exactly
      <:*:> T_U
              Covariant
              Covariant
              (:*:)
              (Reverse (Construction Exactly))
              (Construction Exactly))
     a
morphing (Tape (Construction Exactly) a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Exactly))
         (Construction Exactly)
         a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Tape (Construction Exactly) a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse (Construction Exactly))
          (Construction Exactly)
          a)
-> ((<::>)
      (Tagged ('Rotate 'Right))
      (Exactly
       <:*:> T_U
               Covariant
               Covariant
               (:*:)
               (Reverse (Construction Exactly))
               (Construction Exactly))
      a
    -> Tape (Construction Exactly) a)
-> (<::>)
     (Tagged ('Rotate 'Right))
     (Exactly
      <:*:> T_U
              Covariant
              Covariant
              (:*:)
              (Reverse (Construction Exactly))
              (Construction Exactly))
     a
-> Exactly a
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse (Construction Exactly))
         (Construction Exactly)
         a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<::>)
  (Tagged ('Rotate 'Right))
  (Exactly
   <:*:> T_U
           Covariant
           Covariant
           (:*:)
           (Reverse (Construction Exactly))
           (Construction Exactly))
  a
-> Tape (Construction Exactly) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Exactly a
x :*: T_U (Reverse Construction Exactly a
ls :*: Construction Exactly a
rs)) =
		Impliable (Tape (Construction Exactly) a) =>
Arguments (Tape (Construction Exactly) a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape Stream _) (a
 -> Construction Exactly a
 -> Construction Exactly a
 -> Tape (Construction Exactly) a)
-> a
-> Construction Exactly a
-> Construction Exactly a
-> Tape (Construction Exactly) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Construction Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Construction Exactly a
rs (Construction Exactly a
 -> Construction Exactly a -> Tape (Construction Exactly) a)
-> Construction Exactly a
-> Construction Exactly a
-> Tape (Construction Exactly) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a
-> ((Exactly :. Construction Exactly) >>> a)
-> Construction Exactly a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct a
x (Construction Exactly a -> (Exactly :. Construction Exactly) >>> a
forall (t :: * -> *) a. Pointable t => a -> t a
point Construction Exactly a
ls) (Construction Exactly a -> Tape (Construction Exactly) a)
-> Construction Exactly a -> Tape (Construction Exactly) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- ((Exactly :. Construction Exactly) >>> a) -> Construction Exactly a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Construction Exactly a -> (Exactly :. Construction Exactly) >>> a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Construction Exactly a
rs)

repeat :: a -> Stream a
repeat :: a -> Stream a
repeat a
x = a -> ((Exactly :. Construction Exactly) >>> a) -> Stream a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct a
x (((Exactly :. Construction Exactly) >>> a) -> Stream a)
-> (Stream a -> (Exactly :. Construction Exactly) >>> a)
-> Stream a
-> Stream a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Stream a -> (Exactly :. Construction Exactly) >>> a
forall a. a -> Exactly a
Exactly (Stream a -> Stream a) -> Stream a -> Stream a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> Stream a
forall a. a -> Stream a
repeat a
x