{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Structure.Modification.Tape where

import Pandora.Core.Functor (type (>), type (>>>))
import Pandora.Core.Impliable (Impliable (Arguments, 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.Bindable (Bindable ((====<<)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal)
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Paradigm.Algebraic.Exponential (type (-->), (%))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>), (<:*:>))
import Pandora.Paradigm.Algebraic.Functor ((<-*--), extract, point, void)
import Pandora.Paradigm.Schemes.TT (TT (TT), type (<::>))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U))
import Pandora.Paradigm.Schemes.P_Q_T (P_Q_T (P_Q_T))
import Pandora.Paradigm.Primary.Auxiliary (Vertical (Up, Down), Horizontal (Left, Right))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse (Reverse))
import Pandora.Paradigm.Controlflow.Effect.Adaptable (adapt)
import Pandora.Paradigm.Controlflow.Effect.Transformer ((:>), wrap)
import Pandora.Paradigm.Structure.Ability.Morphable (Occurrence (All))
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure), Segment (Root, Branch, Rest), sub)
import Pandora.Paradigm.Structure.Ability.Slidable (Slidable (Sliding, slide))
import Pandora.Paradigm.Structure.Interface.Stack (Stack (Topping, push, pop))
import Pandora.Paradigm.Inventory.Some.State (State, change)
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (view, replace, mutate, transwrap)
import Pandora.Paradigm.Inventory (zoom, overlook)

type Tape structure = Exactly <:*:> Reverse structure <:*:> structure

-- TODO: No overlapping, let's use wrappers instead
-- instance {-# OVERLAPS #-} Traversable (->) (->) t => Traversable (->) (->) (Tape t) where
-- 	f <-/- z = (\ls x rs -> lift <------ x <:*:> ls <:*:> rs)
-- 		<-|--- f <-/--- view <-- sub @Left <-- z
-- 		<-*--- f <-/--- view <-- sub @Root <-- z
-- 		<-*--- f <-/--- view <-- sub @Right <-- z

instance Covariant (->) (->) t => Impliable (Tape t a) where
	type Arguments (Tape t a) = a -> t a -> t a -> Tape t a
	imply :: Arguments (Tape t a)
imply a
focused t a
left t a
right = a -> Exactly a
forall a. a -> Exactly a
Exactly a
focused Exactly a
-> T_U Covariant Covariant (:*:) (Reverse t) t a -> Tape t a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> t a -> Reverse t a
forall k (t :: k -> *) (a :: k). t a -> Reverse t a
Reverse t a
left Reverse t a -> t a -> T_U Covariant Covariant (:*:) (Reverse t) t a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> t a
right

instance Covariant (->) (->) t => Substructure Up (Tape t <::> Tape t) where
	type Substance Up (Tape t <::> Tape t) = t <::> Tape t
	substructure :: Lens
  (Substance 'Up (Tape t <::> Tape t))
  ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
  a
substructure = ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
 -> Store
      (TT Covariant Covariant t (Tape t) a)
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (TT Covariant Covariant t (Tape t))
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
     a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
  -> Store
       (TT Covariant Covariant t (Tape t) a)
       ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      (TT Covariant Covariant t (Tape t))
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
      a)
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> Store
         (TT Covariant Covariant t (Tape t) a)
         ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (TT Covariant Covariant t (Tape t))
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
x -> case T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Reverse t <:*:> t)
  (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> Exactly
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Reverse t <:*:> t)
   (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
 -> Exactly
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Reverse t <:*:> t)
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Exactly
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant (Tape t) (Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant (Tape t) (Tape t) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Reverse t <:*:> t)
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> TT Covariant Covariant (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
 -> Exactly
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
-> Exactly
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
x of
		Exactly T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
focused :*: T_U (Reverse t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
d :*: t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
u) ->
			(((:*:) (TT Covariant Covariant t (Tape t) a)
  :. (->) (TT Covariant Covariant t (Tape t) a))
 >>> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> Store
     (TT Covariant Covariant t (Tape t) a)
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (TT Covariant Covariant t (Tape t) a)
   :. (->) (TT Covariant Covariant t (Tape t) a))
  >>> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
 -> Store
      (TT Covariant Covariant t (Tape t) a)
      ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a))
-> (((:*:) (TT Covariant Covariant t (Tape t) a)
     :. (->) (TT Covariant Covariant t (Tape t) a))
    >>> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> Store
     (TT Covariant Covariant t (Tape t) a)
     ((<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> TT Covariant Covariant t (Tape t) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') >>> a) -> TT ct ct' t t' a
TT t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
u TT Covariant Covariant t (Tape t) a
-> (TT Covariant Covariant t (Tape t) a
    -> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> ((:*:) (TT Covariant Covariant t (Tape t) a)
    :. (->) (TT Covariant Covariant t (Tape t) a))
   >>> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
forall s a. s -> a -> s :*: a
:*: TT Covariant Covariant (Tape t) (Tape t) a
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant (Tape t) (Tape t) a
 -> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a)
-> (TT Covariant Covariant t (Tape t) a
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> TT Covariant Covariant t (Tape t) a
-> (<:.>) (Tagged 'Up) (Tape t <::> Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Reverse t <:*:> t)
  (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> TT Covariant Covariant (Tape t) (Tape t) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') >>> a) -> TT ct ct' t t' a
TT (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Reverse t <:*:> t)
   (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
 -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (TT Covariant Covariant t (Tape t) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Reverse t <:*:> t)
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> TT Covariant Covariant t (Tape t) a
-> TT Covariant Covariant (Tape t) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
focused t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
d (t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Reverse t <:*:> t)
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> (TT Covariant Covariant t (Tape t) a
    -> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> TT Covariant Covariant t (Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant t (Tape t) a
-> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

instance Covariant (->) (->) t => Substructure Down (Tape t <::> Tape t) where
	type Substance Down (Tape t <::> Tape t) = Reverse t <::> Tape t
	substructure :: Lens
  (Substance 'Down (Tape t <::> Tape t))
  ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
  a
substructure = ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
 -> Store
      (TT Covariant Covariant (Reverse t) (Tape t) a)
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (TT Covariant Covariant (Reverse t) (Tape t))
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
     a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
  -> Store
       (TT Covariant Covariant (Reverse t) (Tape t) a)
       ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      (TT Covariant Covariant (Reverse t) (Tape t))
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
      a)
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> Store
         (TT Covariant Covariant (Reverse t) (Tape t) a)
         ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (TT Covariant Covariant (Reverse t) (Tape t))
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
ii -> case T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Reverse t <:*:> t)
  (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> Exactly
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Reverse t <:*:> t)
   (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
 -> Exactly
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Reverse t <:*:> t)
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Exactly
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant (Tape t) (Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant (Tape t) (Tape t) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Reverse t <:*:> t)
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> TT Covariant Covariant (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
 -> Exactly
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
    :*: T_U
          Covariant
          Covariant
          (:*:)
          (Reverse t)
          t
          (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
-> Exactly
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
   :*: T_U
         Covariant
         Covariant
         (:*:)
         (Reverse t)
         t
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
ii of
		Exactly T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
focused :*: T_U (Reverse
  t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
d :*: t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
u) ->
			(((:*:) (TT Covariant Covariant (Reverse t) (Tape t) a)
  :. (->) (TT Covariant Covariant (Reverse t) (Tape t) a))
 >>> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> Store
     (TT Covariant Covariant (Reverse t) (Tape t) a)
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (TT Covariant Covariant (Reverse t) (Tape t) a)
   :. (->) (TT Covariant Covariant (Reverse t) (Tape t) a))
  >>> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
 -> Store
      (TT Covariant Covariant (Reverse t) (Tape t) a)
      ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a))
-> (((:*:) (TT Covariant Covariant (Reverse t) (Tape t) a)
     :. (->) (TT Covariant Covariant (Reverse t) (Tape t) a))
    >>> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> Store
     (TT Covariant Covariant (Reverse t) (Tape t) a)
     ((<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Reverse
  t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> TT Covariant Covariant (Reverse t) (Tape t) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') >>> a) -> TT ct ct' t t' a
TT Reverse
  t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
d TT Covariant Covariant (Reverse t) (Tape t) a
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> ((:*:) (TT Covariant Covariant (Reverse t) (Tape t) a)
    :. (->) (TT Covariant Covariant (Reverse t) (Tape t) a))
   >>> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
forall s a. s -> a -> s :*: a
:*: TT Covariant Covariant (Tape t) (Tape t) a
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (TT Covariant Covariant (Tape t) (Tape t) a
 -> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a)
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> TT Covariant Covariant (Tape t) (Tape t) a)
-> TT Covariant Covariant (Reverse t) (Tape t) a
-> (<:.>) (Tagged 'Down) (Tape t <::> Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Reverse t <:*:> t)
  (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> TT Covariant Covariant (Tape t) (Tape t) a
forall k k k k (ct :: k) (ct' :: k) (t :: k -> *) (t' :: k -> k)
       (a :: k).
((t :. t') >>> a) -> TT ct ct' t t' a
TT (T_U
   Covariant
   Covariant
   (:*:)
   Exactly
   (Reverse t <:*:> t)
   (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
 -> TT Covariant Covariant (Tape t) (Tape t) a)
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> T_U
         Covariant
         Covariant
         (:*:)
         Exactly
         (Reverse t <:*:> t)
         (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> TT Covariant Covariant (Reverse t) (Tape t) a
-> TT Covariant Covariant (Tape t) (Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall k (result :: k). Impliable result => Arguments result
imply @(Tape t _) T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
focused (t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
 -> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Reverse t <:*:> t)
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall a b c. (a -> b -> c) -> b -> a -> c
% t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
u) (t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Reverse t <:*:> t)
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> TT Covariant Covariant (Reverse t) (Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Reverse
  t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Reverse
   t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
 -> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> (TT Covariant Covariant (Reverse t) (Tape t) a
    -> Reverse
         t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> TT Covariant Covariant (Reverse t) (Tape t) a
-> t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. TT Covariant Covariant (Reverse t) (Tape t) a
-> Reverse
     t (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => Substructure (All Left) (Tape t <::> Tape t) where
	type Substance (All Left) (Tape t <::> Tape t) = Tape t <::> Reverse t
	substructure :: Lens
  (Substance ('All 'Left) (Tape t <::> Tape t))
  ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
  a
substructure = ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
 -> Store
      ((<::>) (Tape t) (Reverse t) a)
      ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (Tape t <::> Reverse t)
     ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
     a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
  -> Store
       ((<::>) (Tape t) (Reverse t) a)
       ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      (Tape t <::> Reverse t)
      ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
      a)
-> ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
    -> Store
         ((<::>) (Tape t) (Reverse t) a)
         ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (Tape t <::> Reverse t)
     ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
source ->
		let target :: (<::>) (Tape t) (Reverse t) a
target = (Lens (Reverse t) (T_U Covariant Covariant (:*:) (Reverse t) t a) a
-> T_U Covariant Covariant (:*:) (Reverse t) t a -> Reverse t a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left) (T_U Covariant Covariant (:*:) (Reverse t) t a -> Reverse t a)
-> (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
    -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> Reverse t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens
  (Reverse t <:*:> t)
  (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
  a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest) (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
 -> Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (Reverse t a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Primary (Tape t <::> Tape t) a
 -> Primary (Tape t <::> Reverse t) a)
-> ((->) < (<::>) (Tape t) (Tape t) a)
   < (<::>) (Tape t) (Reverse t) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#- (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
-> (<::>) (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
source in
		let updated :: T_U
  Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
updated T_U
  Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (Reverse t a)
new = (\Reverse t a
trg T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
src -> (T_U Covariant Covariant (:*:) (Reverse t) t a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Lens
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
     a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
forall (i :: * -> *) target source.
(i target -> i target) -> Lens i source target -> source -> source
mutate (Reverse t a
-> Lens
     (Reverse t) (T_U Covariant Covariant (:*:) (Reverse t) t a) a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
forall (i :: * -> *) source target.
i target -> Lens i source target -> source -> source
replace (Reverse t a
 -> Lens
      (Reverse t) (T_U Covariant Covariant (:*:) (Reverse t) t a) a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Reverse t a
-> Lens
     (Reverse t) (T_U Covariant Covariant (:*:) (Reverse t) t a) a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Reverse t a
trg (Lens (Reverse t) (T_U Covariant Covariant (:*:) (Reverse t) t a) a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Lens
     (Reverse t) (T_U Covariant Covariant (:*:) (Reverse t) t a) a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left) (Lens
   (Reverse t <:*:> t)
   (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
   a
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> Lens
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
     a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
src) (Reverse t a
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U
     Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
      -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- T_U
  Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (Reverse t a)
new T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Reverse t <:*:> t)
  (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
   -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*-- (<::>) (Tape t) (Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<::>) (Tape t) (Tape t) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Reverse t <:*:> t)
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> (<::>) (Tape t) (Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
-> (<::>) (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
source in
		(((:*:) ((<::>) (Tape t) (Reverse t) a)
  :. (->) ((<::>) (Tape t) (Reverse t) a))
 >>> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
-> Store
     ((<::>) (Tape t) (Reverse t) a)
     ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) ((<::>) (Tape t) (Reverse t) a)
   :. (->) ((<::>) (Tape t) (Reverse t) a))
  >>> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
 -> Store
      ((<::>) (Tape t) (Reverse t) a)
      ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a))
-> (((:*:) ((<::>) (Tape t) (Reverse t) a)
     :. (->) ((<::>) (Tape t) (Reverse t) a))
    >>> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
-> Store
     ((<::>) (Tape t) (Reverse t) a)
     ((<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (<::>) (Tape t) (Reverse t) a
target (<::>) (Tape t) (Reverse t) a
-> ((<::>) (Tape t) (Reverse t) a
    -> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
-> ((:*:) ((<::>) (Tape t) (Reverse t) a)
    :. (->) ((<::>) (Tape t) (Reverse t) a))
   >>> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
forall s a. s -> a -> s :*: a
:*: (<::>) (Tape t) (Tape t) a
-> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((<::>) (Tape t) (Tape t) a
 -> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a)
-> ((<::>) (Tape t) (Reverse t) a -> (<::>) (Tape t) (Tape t) a)
-> (<::>) (Tape t) (Reverse t) a
-> (<:.>) (Tagged ('All 'Left)) (Tape t <::> Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Primary (Tape t <::> Reverse t) a -> Primary (Tape t <::> Tape t) a
T_U
  Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (Reverse t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
updated (Primary (Tape t <::> Reverse t) a
 -> Primary (Tape t <::> Tape t) a)
-> (<::>) (Tape t) (Reverse t) a -> (<::>) (Tape t) (Tape t) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#-)

instance (Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) => Substructure (All Right) (Tape t <::> Tape t) where
	type Substance (All Right) (Tape t <::> Tape t) = Tape t <::> t
	substructure :: Lens
  (Substance ('All 'Right) (Tape t <::> Tape t))
  ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
  a
substructure = ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
 -> Store
      ((<::>) (Tape t) t a)
      ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (Tape t <::> t)
     ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
     a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
  -> Store
       ((<::>) (Tape t) t a)
       ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a))
 -> P_Q_T
      (->)
      Store
      (Tape t <::> t)
      ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
      a)
-> ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
    -> Store
         ((<::>) (Tape t) t a)
         ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a))
-> P_Q_T
     (->)
     Store
     (Tape t <::> t)
     ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
source ->
		let target :: (<::>) (Tape t) t a
target = (Lens t (T_U Covariant Covariant (:*:) (Reverse t) t a) a
-> T_U Covariant Covariant (:*:) (Reverse t) t a -> t a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right) (T_U Covariant Covariant (:*:) (Reverse t) t a -> t a)
-> (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
    -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> t a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens
  (Reverse t <:*:> t)
  (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
  a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest) (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
 -> t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (t a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-) (Primary (Tape t <::> Tape t) a -> Primary (Tape t <::> t) a)
-> ((->) < (<::>) (Tape t) (Tape t) a) < (<::>) (Tape t) t a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#- (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
-> (<::>) (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
source in
		let updated :: T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
updated T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (t a)
new = (\t a
trg T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
src -> (T_U Covariant Covariant (:*:) (Reverse t) t a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Lens
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
     a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
forall (i :: * -> *) target source.
(i target -> i target) -> Lens i source target -> source -> source
mutate (t a
-> Lens t (T_U Covariant Covariant (:*:) (Reverse t) t a) a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
forall (i :: * -> *) source target.
i target -> Lens i source target -> source -> source
replace (t a
 -> Lens t (T_U Covariant Covariant (:*:) (Reverse t) t a) a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> t a
-> Lens t (T_U Covariant Covariant (:*:) (Reverse t) t a) a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- t a
trg (Lens t (T_U Covariant Covariant (:*:) (Reverse t) t a) a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a
 -> T_U Covariant Covariant (:*:) (Reverse t) t a)
-> Lens t (T_U Covariant Covariant (:*:) (Reverse t) t a) a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
-> T_U Covariant Covariant (:*:) (Reverse t) t a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right) (Lens
   (Reverse t <:*:> t)
   (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
   a
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> Lens
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
     a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
src) (t a
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
 -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
      -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-- T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (t a)
new T_U
  Covariant
  Covariant
  (:*:)
  Exactly
  (Reverse t <:*:> t)
  (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a
   -> T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*-- (<::>) (Tape t) (Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run ((<::>) (Tape t) (Tape t) a
 -> T_U
      Covariant
      Covariant
      (:*:)
      Exactly
      (Reverse t <:*:> t)
      (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a))
-> (<::>) (Tape t) (Tape t) a
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
-> (<::>) (Tape t) (Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
source in
		(((:*:) ((<::>) (Tape t) t a) :. (->) ((<::>) (Tape t) t a))
 >>> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
-> Store
     ((<::>) (Tape t) t a)
     ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) ((<::>) (Tape t) t a) :. (->) ((<::>) (Tape t) t a))
  >>> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
 -> Store
      ((<::>) (Tape t) t a)
      ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a))
-> (((:*:) ((<::>) (Tape t) t a) :. (->) ((<::>) (Tape t) t a))
    >>> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
-> Store
     ((<::>) (Tape t) t a)
     ((<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (<::>) (Tape t) t a
target (<::>) (Tape t) t a
-> ((<::>) (Tape t) t a
    -> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
-> ((:*:) ((<::>) (Tape t) t a) :. (->) ((<::>) (Tape t) t a))
   >>> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
forall s a. s -> a -> s :*: a
:*: (<::>) (Tape t) (Tape t) a
-> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift ((<::>) (Tape t) (Tape t) a
 -> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a)
-> ((<::>) (Tape t) t a -> (<::>) (Tape t) (Tape t) a)
-> (<::>) (Tape t) t a
-> (<:.>) (Tagged ('All 'Right)) (Tape t <::> Tape t) a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Primary (Tape t <::> t) a -> Primary (Tape t <::> Tape t) a
T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) (t a)
-> T_U
     Covariant
     Covariant
     (:*:)
     Exactly
     (Reverse t <:*:> t)
     (T_U Covariant Covariant (:*:) Exactly (Reverse t <:*:> t) a)
updated (Primary (Tape t <::> t) a -> Primary (Tape t <::> Tape t) a)
-> (<::>) (Tape t) t a -> (<::>) (Tape t) (Tape t) a
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b.
(Interpreted m t, Semigroupoid m, Interpreted m u) =>
((m < Primary t a) < Primary u b) -> (m < t a) < u b
=#-)

instance (Covariant (->) (->) structure, Bindable (->) (Topping structure), Monoidal (-->) (-->) (:*:) (:*:) (Topping structure), Stack structure) => Slidable Right (Tape structure) where
	type Sliding Right (Tape structure) = Topping structure
	slide :: forall e . State > Tape structure e :> Topping structure >>> ()
	slide :: ((State > Tape structure e) :> Topping structure) >>> ()
slide = (:>) (State > Tape structure e) (Topping structure) e
-> ((State > Tape structure e) :> Topping structure) >>> ()
forall (t :: * -> *) a. Covariant (->) (->) t => t a -> t ()
void ((:>) (State > Tape structure e) (Topping structure) e
 -> ((State > Tape structure e) :> Topping structure) >>> ())
-> (Exactly e
    -> (:>) (State > Tape structure e) (Topping structure) e)
-> Exactly e
-> ((State > Tape structure e) :> Topping structure) >>> ()
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((->) < State (Tape structure e) e)
< (:>) (State > Tape structure e) (Topping structure) e
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a.
(Monadic m t, Pointable u) =>
(m < t a) < (:>) t u a
wrap (((->) < State (Tape structure e) e)
 < (:>) (State > Tape structure e) (Topping structure) e)
-> (Exactly e -> State (Tape structure e) e)
-> Exactly e
-> (:>) (State > Tape structure e) (Topping structure) e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens
  (T_U Covariant Covariant (:*:) (Reverse structure) structure)
  (Tape structure e)
  e
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e
-> State (Tape structure e) e
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom @(Tape structure e) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest)
		(State
   (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e
 -> State (Tape structure e) e)
-> (Exactly e
    -> State
         (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e)
-> Exactly e
-> State (Tape structure e) e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens
  (Reverse structure)
  (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
  e
-> State (Reverse structure e) e
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left) (State (Reverse structure e) e
 -> State
      (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e)
-> (Exactly e -> State (Reverse structure e) e)
-> Exactly e
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens structure (Reverse structure e) e
-> State (structure e) e -> State (Reverse structure e) e
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom Lens structure (Reverse structure e) e
forall (u :: * -> *) (t :: (* -> *) -> * -> *) e.
(Covariant (->) (->) u, Liftable (->) t, Lowerable (->) t) =>
(Lens u < t u e) < e
transwrap (State (structure e) e -> State (Reverse structure e) e)
-> (Exactly e -> State (structure e) e)
-> Exactly e
-> State (Reverse structure e) e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall e. Stack structure => e -> (State < structure e) < e
forall (structure :: * -> *) e.
Stack structure =>
e -> (State < structure e) < e
push @structure (e -> State (structure e) e)
-> (Exactly e -> e) -> Exactly e -> State (structure e) e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly e -> e
forall (t :: * -> *) a. Extractable t => t a -> a
extract
			(Exactly e
 -> ((State > Tape structure e) :> Topping structure) >>> ())
-> (:>) (State > Tape structure e) (Topping structure) (Exactly e)
-> ((State > Tape structure e) :> Topping structure) >>> ()
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
====<< ((->) < State (Tape structure e) (Exactly e))
< (:>) (State > Tape structure e) (Topping structure) (Exactly e)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a.
(Monadic m t, Pointable u) =>
(m < t a) < (:>) t u a
wrap (((->) < State (Tape structure e) (Exactly e))
 < (:>) (State > Tape structure e) (Topping structure) (Exactly e))
-> (e -> State (Tape structure e) (Exactly e))
-> e
-> (:>) (State > Tape structure e) (Topping structure) (Exactly e)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens Exactly (Tape structure e) e
-> State (Exactly e) (Exactly e)
-> State (Tape structure e) (Exactly e)
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom @(Tape structure e) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Root structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Root structure
sub @Root) (State (Exactly e) (Exactly e)
 -> State (Tape structure e) (Exactly e))
-> (e -> State (Exactly e) (Exactly e))
-> e
-> State (Tape structure e) (Exactly e)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. State e e -> State (Exactly e) (Exactly e)
forall (t :: * -> *) s result.
(Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t) =>
State s result -> State (t s) (t result)
overlook (State e e -> State (Exactly e) (Exactly e))
-> (e -> State e e) -> e -> State (Exactly e) (Exactly e)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (e -> e) -> State e e
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
change ((e -> e) -> State e e) -> (e -> e -> e) -> e -> State e e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. e -> e -> e
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant
				(e
 -> (:>) (State > Tape structure e) (Topping structure) (Exactly e))
-> (:>) (State > Tape structure e) (Topping structure) e
-> (:>) (State > Tape structure e) (Topping structure) (Exactly e)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
====<< Topping structure e
-> (:>) (State > Tape structure e) (Topping structure) e
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Topping structure e
 -> (:>) (State > Tape structure e) (Topping structure) e)
-> (:>)
     (State > Tape structure e)
     (Topping structure)
     (Topping structure e)
-> (:>) (State > Tape structure e) (Topping structure) e
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
====<< ((->) < State (Tape structure e) (Topping structure e))
< (:>)
    (State > Tape structure e)
    (Topping structure)
    (Topping structure e)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a.
(Monadic m t, Pointable u) =>
(m < t a) < (:>) t u a
wrap (((->) < State (Tape structure e) (Topping structure e))
 < (:>)
     (State > Tape structure e)
     (Topping structure)
     (Topping structure e))
-> ((->) < State (Tape structure e) (Topping structure e))
   < (:>)
       (State > Tape structure e)
       (Topping structure)
       (Topping structure e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
forall ls (u :: * -> *) result.
Lens u (Tape structure e) ls
-> State (u ls) result -> State (Tape structure e) result
zoom @(Tape structure e) (Lens
   (T_U Covariant Covariant (:*:) (Reverse structure) structure)
   (Tape structure e)
   e
 -> State
      (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
      (Topping structure e)
 -> State (Tape structure e) (Topping structure e))
-> Lens
     (T_U Covariant Covariant (:*:) (Reverse structure) structure)
     (Tape structure e)
     e
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     (Topping structure e)
-> State (Tape structure e) (Topping structure e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest
					(State
   (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
   (Topping structure e)
 -> State (Tape structure e) (Topping structure e))
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     (Topping structure e)
-> State (Tape structure e) (Topping structure e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
  structure
  (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
  e
-> State (structure e) (Topping structure e)
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     (Topping structure e)
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom (Lens
   structure
   (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
   e
 -> State (structure e) (Topping structure e)
 -> State
      (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
      (Topping structure e))
-> Lens
     structure
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     e
-> State (structure e) (Topping structure e)
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     (Topping structure e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right (State (structure e) (Topping structure e)
 -> State
      (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
      (Topping structure e))
-> State (structure e) (Topping structure e)
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     (Topping structure e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall e.
Stack structure =>
(State < structure e) < Topping structure e
forall (structure :: * -> *) e.
Stack structure =>
(State < structure e) < Topping structure e
pop @structure

instance (Covariant (->) (->) structure, Stack structure, Bindable (->) (Topping structure), Monoidal (-->) (-->) (:*:) (:*:) (Topping structure)) => Slidable Left (Tape structure) where
	type Sliding Left (Tape structure) = Topping structure
	slide :: forall e . State > Tape structure e :> Topping structure >>> ()
	slide :: ((State > Tape structure e) :> Topping structure) >>> ()
slide = (:>) (State > Tape structure e) (Topping structure) e
-> ((State > Tape structure e) :> Topping structure) >>> ()
forall (t :: * -> *) a. Covariant (->) (->) t => t a -> t ()
void ((:>) (State > Tape structure e) (Topping structure) e
 -> ((State > Tape structure e) :> Topping structure) >>> ())
-> (Exactly e
    -> (:>) (State > Tape structure e) (Topping structure) e)
-> Exactly e
-> ((State > Tape structure e) :> Topping structure) >>> ()
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((->) < State (Tape structure e) e)
< (:>) (State > Tape structure e) (Topping structure) e
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a.
(Monadic m t, Pointable u) =>
(m < t a) < (:>) t u a
wrap (((->) < State (Tape structure e) e)
 < (:>) (State > Tape structure e) (Topping structure) e)
-> (Exactly e -> State (Tape structure e) e)
-> Exactly e
-> (:>) (State > Tape structure e) (Topping structure) e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens
  (T_U Covariant Covariant (:*:) (Reverse structure) structure)
  (Tape structure e)
  e
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e
-> State (Tape structure e) e
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom @(Tape structure e) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest)
		(State
   (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e
 -> State (Tape structure e) e)
-> (Exactly e
    -> State
         (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e)
-> Exactly e
-> State (Tape structure e) e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens
  structure
  (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
  e
-> State (structure e) e
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right) (State (structure e) e
 -> State
      (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e)
-> (Exactly e -> State (structure e) e)
-> Exactly e
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e) e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. e -> State (structure e) e
forall (structure :: * -> *) e.
Stack structure =>
e -> (State < structure e) < e
push (e -> State (structure e) e)
-> (Exactly e -> e) -> Exactly e -> State (structure e) e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly e -> e
forall (t :: * -> *) a. Extractable t => t a -> a
extract
			(Exactly e
 -> ((State > Tape structure e) :> Topping structure) >>> ())
-> (:>) (State > Tape structure e) (Topping structure) (Exactly e)
-> ((State > Tape structure e) :> Topping structure) >>> ()
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
====<< ((->) < State (Tape structure e) (Exactly e))
< (:>) (State > Tape structure e) (Topping structure) (Exactly e)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a.
(Monadic m t, Pointable u) =>
(m < t a) < (:>) t u a
wrap (((->) < State (Tape structure e) (Exactly e))
 < (:>) (State > Tape structure e) (Topping structure) (Exactly e))
-> (e -> State (Tape structure e) (Exactly e))
-> e
-> (:>) (State > Tape structure e) (Topping structure) (Exactly e)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens Exactly (Tape structure e) e
-> State (Exactly e) (Exactly e)
-> State (Tape structure e) (Exactly e)
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom @(Tape structure e) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Root structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Root structure
sub @Root) (State (Exactly e) (Exactly e)
 -> State (Tape structure e) (Exactly e))
-> (e -> State (Exactly e) (Exactly e))
-> e
-> State (Tape structure e) (Exactly e)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. State e e -> State (Exactly e) (Exactly e)
forall (t :: * -> *) s result.
(Covariant (->) (->) t, Semimonoidal (<--) (:*:) (:*:) t) =>
State s result -> State (t s) (t result)
overlook (State e e -> State (Exactly e) (Exactly e))
-> (e -> State e e) -> e -> State (Exactly e) (Exactly e)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (e -> e) -> State e e
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
change ((e -> e) -> State e e) -> (e -> e -> e) -> e -> State e e
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. e -> e -> e
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant
				(e
 -> (:>) (State > Tape structure e) (Topping structure) (Exactly e))
-> (:>) (State > Tape structure e) (Topping structure) e
-> (:>) (State > Tape structure e) (Topping structure) (Exactly e)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
====<< Topping structure e
-> (:>) (State > Tape structure e) (Topping structure) e
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Topping structure e
 -> (:>) (State > Tape structure e) (Topping structure) e)
-> (:>)
     (State > Tape structure e)
     (Topping structure)
     (Topping structure e)
-> (:>) (State > Tape structure e) (Topping structure) e
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
====<< ((->) < State (Tape structure e) (Topping structure e))
< (:>)
    (State > Tape structure e)
    (Topping structure)
    (Topping structure e)
forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a.
(Monadic m t, Pointable u) =>
(m < t a) < (:>) t u a
wrap (((->) < State (Tape structure e) (Topping structure e))
 < (:>)
     (State > Tape structure e)
     (Topping structure)
     (Topping structure e))
-> ((->) < State (Tape structure e) (Topping structure e))
   < (:>)
       (State > Tape structure e)
       (Topping structure)
       (Topping structure e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
forall ls (u :: * -> *) result.
Lens u (Tape structure e) ls
-> State (u ls) result -> State (Tape structure e) result
zoom @(Tape structure e) (Lens
   (T_U Covariant Covariant (:*:) (Reverse structure) structure)
   (Tape structure e)
   e
 -> State
      (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
      (Topping structure e)
 -> State (Tape structure e) (Topping structure e))
-> Lens
     (T_U Covariant Covariant (:*:) (Reverse structure) structure)
     (Tape structure e)
     e
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     (Topping structure e)
-> State (Tape structure e) (Topping structure e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest
					(State
   (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
   (Topping structure e)
 -> State (Tape structure e) (Topping structure e))
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     (Topping structure e)
-> State (Tape structure e) (Topping structure e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
  (Reverse structure)
  (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
  e
-> State (Reverse structure e) (Topping structure e)
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     (Topping structure e)
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom (Lens
   (Reverse structure)
   (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
   e
 -> State (Reverse structure e) (Topping structure e)
 -> State
      (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
      (Topping structure e))
-> Lens
     (Reverse structure)
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     e
-> State (Reverse structure e) (Topping structure e)
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     (Topping structure e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left (State (Reverse structure e) (Topping structure e)
 -> State
      (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
      (Topping structure e))
-> State (Reverse structure e) (Topping structure e)
-> State
     (T_U Covariant Covariant (:*:) (Reverse structure) structure e)
     (Topping structure e)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Lens structure (Reverse structure e) e
-> State (structure e) (Topping structure e)
-> State (Reverse structure e) (Topping structure e)
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom Lens structure (Reverse structure e) e
forall (u :: * -> *) (t :: (* -> *) -> * -> *) e.
(Covariant (->) (->) u, Liftable (->) t, Lowerable (->) t) =>
(Lens u < t u e) < e
transwrap State (structure e) (Topping structure e)
forall (structure :: * -> *) e.
Stack structure =>
(State < structure e) < Topping structure e
pop