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

import Pandora.Core.Impliable (imply)
import Pandora.Core.Functor (type (>), type (:=>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (-->))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|--)))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>))
import Pandora.Paradigm.Algebraic (extract)
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct, (.-+))
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))
import Pandora.Paradigm.Structure.Modification.Tape (Tape)
import Pandora.Paradigm.Schemes.T_U (T_U (T_U))
import Pandora.Paradigm.Algebraic (point)
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)

type Stream = Construction Exactly

instance Zippable (Construction Exactly) where
	type Breadcrumbs (Construction Exactly) = Reverse Stream <:*:> Stream

instance Morphable (Rotate Left) (Tape Stream) where
	type Morphing (Rotate Left) (Tape Stream) = Tape Stream
	morphing :: (<::>) (Tagged ('Rotate 'Left)) (Tape (Construction Exactly)) a
-> Morphing ('Rotate 'Left) (Tape (Construction Exactly)) a
morphing ((<:*:>)
  Exactly
  (Reverse (Construction Exactly) <:*:> 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 ((<:*:>)
   Exactly
   (Reverse (Construction Exactly) <:*:> Construction Exactly)
   a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse (Construction Exactly))
          (Construction Exactly)
          a)
-> ((<::>) (Tagged ('Rotate 'Left)) (Tape (Construction Exactly)) a
    -> (<:*:>)
         Exactly
         (Reverse (Construction Exactly) <:*:> Construction Exactly)
         a)
-> (<::>) (Tagged ('Rotate 'Left)) (Tape (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
. TU
  Covariant
  Covariant
  (Tagged (Zippable (Construction Exactly)))
  (Exactly
   <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
  a
-> (<:*:>)
     Exactly
     (Reverse (Construction Exactly) <:*:> Construction Exactly)
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable (Construction Exactly)))
   (Exactly
    <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
   a
 -> (<:*:>)
      Exactly
      (Reverse (Construction Exactly) <:*:> Construction Exactly)
      a)
-> ((<::>) (Tagged ('Rotate 'Left)) (Tape (Construction Exactly)) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable (Construction Exactly)))
         (Exactly
          <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
         a)
-> (<::>) (Tagged ('Rotate 'Left)) (Tape (Construction Exactly)) a
-> (<:*:>)
     Exactly
     (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)) (Tape (Construction Exactly)) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> 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
  (TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
     a) =>
Arguments
  (TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
     a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape Stream _) (a
 -> Construction Exactly a
 -> Construction Exactly a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Exactly)))
      (Exactly
       <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
      a)
-> a
-> Construction Exactly a
-> Construction Exactly a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> 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
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Exactly)))
      (Exactly
       <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
      a)
-> Construction Exactly a
-> Construction Exactly a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> 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
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Exactly)))
      (Exactly
       <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
      a)
-> Construction Exactly a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> 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)) (Tape (Construction Exactly)) a
-> Morphing ('Rotate 'Right) (Tape (Construction Exactly)) a
morphing ((<:*:>)
  Exactly
  (Reverse (Construction Exactly) <:*:> 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 ((<:*:>)
   Exactly
   (Reverse (Construction Exactly) <:*:> Construction Exactly)
   a
 -> Exactly a
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse (Construction Exactly))
          (Construction Exactly)
          a)
-> ((<::>)
      (Tagged ('Rotate 'Right)) (Tape (Construction Exactly)) a
    -> (<:*:>)
         Exactly
         (Reverse (Construction Exactly) <:*:> Construction Exactly)
         a)
-> (<::>) (Tagged ('Rotate 'Right)) (Tape (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
. TU
  Covariant
  Covariant
  (Tagged (Zippable (Construction Exactly)))
  (Exactly
   <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
  a
-> (<:*:>)
     Exactly
     (Reverse (Construction Exactly) <:*:> Construction Exactly)
     a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (TU
   Covariant
   Covariant
   (Tagged (Zippable (Construction Exactly)))
   (Exactly
    <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
   a
 -> (<:*:>)
      Exactly
      (Reverse (Construction Exactly) <:*:> Construction Exactly)
      a)
-> ((<::>)
      (Tagged ('Rotate 'Right)) (Tape (Construction Exactly)) a
    -> TU
         Covariant
         Covariant
         (Tagged (Zippable (Construction Exactly)))
         (Exactly
          <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
         a)
-> (<::>) (Tagged ('Rotate 'Right)) (Tape (Construction Exactly)) a
-> (<:*:>)
     Exactly
     (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)) (Tape (Construction Exactly)) a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> 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
  (TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
     a) =>
Arguments
  (TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
     a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape Stream _) (a
 -> Construction Exactly a
 -> Construction Exactly a
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Exactly)))
      (Exactly
       <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
      a)
-> a
-> Construction Exactly a
-> Construction Exactly a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> 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
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Exactly)))
      (Exactly
       <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
      a)
-> Construction Exactly a
-> Construction Exactly a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> 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
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Exactly)))
      (Exactly
       <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
      a)
-> Construction Exactly a
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> 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)

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)
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
 -> Exactly (Tape (Construction Exactly) a))
-> Tape (Construction Exactly) a :=> Construction Exactly
forall (t :: * -> *) a.
Covariant (->) (->) t =>
(a :=> t) -> a :=> Construction t
.-+ Tape (Construction Exactly) a
z in
		Tape (Construction Exactly) a -> b
f (Tape (Construction Exactly) a -> b)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (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
  (TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
     (Tape (Construction Exactly) a)) =>
Arguments
  (TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (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)
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Exactly)))
      (Exactly
       <:*:> (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)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (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)
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Exactly)))
      (Exactly
       <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
      (Tape (Construction Exactly) a))
-> Construction Exactly (Tape (Construction Exactly) a)
-> Construction Exactly (Tape (Construction Exactly) a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (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)
 -> TU
      Covariant
      Covariant
      (Tagged (Zippable (Construction Exactly)))
      (Exactly
       <:*:> (Reverse (Construction Exactly) <:*:> Construction Exactly))
      (Tape (Construction Exactly) a))
-> Construction Exactly (Tape (Construction Exactly) a)
-> TU
     Covariant
     Covariant
     (Tagged (Zippable (Construction Exactly)))
     (Exactly
      <:*:> (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)

repeat :: a :=> Stream
repeat :: a :=> Construction Exactly
repeat a
x = 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)
-> (Construction Exactly a
    -> (Exactly :. Construction Exactly) > a)
-> Construction Exactly a
-> Construction Exactly a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction Exactly a -> (Exactly :. Construction Exactly) > a
forall a. a -> Exactly a
Exactly (Construction Exactly a -> Construction Exactly a)
-> Construction Exactly a -> Construction Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a :=> Construction Exactly
forall a. a :=> Construction Exactly
repeat a
x