{-# 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
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