{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Pandora.Paradigm.Structure.Some.Splay where

import Pandora.Core.Functor (type (~>), type (>), type (>>>))
import Pandora.Core.Interpreted (run, (<~))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Category ((<--), (<---), (<----), identity)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|---)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<), (==<<), (===<<)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Hoistable ((/|\))
import Pandora.Paradigm.Algebraic.Functor ((<-*-), extract, point, void)
import Pandora.Paradigm.Algebraic.Product (type (<:*:>), (<:*:>), attached)
import Pandora.Paradigm.Primary.Auxiliary (Horizontal (Left, Right))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Controlflow.Effect.Adaptable (adapt)
import Pandora.Paradigm.Controlflow.Effect.Transformer ((:>))
import Pandora.Paradigm.Inventory.Some.Optics (view, mutate)
import Pandora.Paradigm.Inventory.Some.State (State, change, current)
import Pandora.Paradigm.Inventory (zoom)
import Pandora.Paradigm.Schemes (TT (TT), type (<::>))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morphed, Morph (Rotate), premorph, rotate)
import Pandora.Paradigm.Structure.Modification.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Substructure (Segment (Root, Branch), sub)
import Pandora.Paradigm.Structure.Ability.Slidable (Slidable (Sliding, slide))
import Pandora.Paradigm.Structure.Ability.Monotonic (resolve)
import Pandora.Paradigm.Structure.Some.Binary (Binary)

data Splay a = Zig a | Zag a

instance Morphable (Rotate > Left Zig) Binary where
	type Morphing (Rotate > Left Zig) Binary = Binary
	morphing :: (<::>) (Tagged ('Rotate > 'Left 'Zig)) Binary a
-> Morphing ('Rotate > 'Left 'Zig) Binary a
morphing ((<::>) (Tagged ('Rotate > 'Left 'Zig)) Binary a -> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Binary a
binary) = ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary 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 (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a -> Binary a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate ('Left 'Zig)) struct =>
struct ~> Morphing ('Rotate ('Left 'Zig)) struct
rotate @(Left Zig) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Binary a
binary

instance Morphable (Rotate > Right Zig) Binary where
	type Morphing (Rotate > Right Zig) Binary = Binary
	morphing :: (<::>) (Tagged ('Rotate > 'Right 'Zig)) Binary a
-> Morphing ('Rotate > 'Right 'Zig) Binary a
morphing ((<::>) (Tagged ('Rotate > 'Right 'Zig)) Binary a -> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Binary a
binary) = ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary 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 (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a -> Binary a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate ('Right 'Zig)) struct =>
struct ~> Morphing ('Rotate ('Right 'Zig)) struct
rotate @(Right Zig) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Binary a
binary

instance Morphable (Rotate > Left > Zig Zig) Binary where
	type Morphing (Rotate > Left > Zig Zig) Binary = Binary
	morphing :: (<::>) (Tagged ('Rotate > ('Left > 'Zig 'Zig))) Binary a
-> Morphing ('Rotate > ('Left > 'Zig 'Zig)) Binary a
morphing ((<::>) (Tagged ('Rotate > ('Left > 'Zig 'Zig))) Binary a
-> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Binary a
binary) = ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary 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 (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a -> Binary a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate ('Left > 'Zig 'Zig)) struct =>
struct ~> Morphing ('Rotate ('Left > 'Zig 'Zig)) struct
rotate @(Left > Zig Zig) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Binary a
binary

instance Morphable (Rotate > Right > Zig Zig) Binary where
	type Morphing (Rotate > Right > Zig Zig) Binary = Binary
	morphing :: (<::>) (Tagged ('Rotate > ('Right > 'Zig 'Zig))) Binary a
-> Morphing ('Rotate > ('Right > 'Zig 'Zig)) Binary a
morphing ((<::>) (Tagged ('Rotate > ('Right > 'Zig 'Zig))) Binary a
-> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Binary a
binary) = ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary 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 (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a -> Binary a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate ('Right > 'Zig 'Zig)) struct =>
struct ~> Morphing ('Rotate ('Right > 'Zig 'Zig)) struct
rotate @(Right > Zig Zig) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Binary a
binary

instance Morphable (Rotate > Left > Zig Zag) Binary where
	type Morphing (Rotate > Left > Zig Zag) Binary = Binary
	morphing :: (<::>) (Tagged ('Rotate > ('Left > 'Zig 'Zag))) Binary a
-> Morphing ('Rotate > ('Left > 'Zig 'Zag)) Binary a
morphing ((<::>) (Tagged ('Rotate > ('Left > 'Zig 'Zag))) Binary a
-> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Binary a
binary) = ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary 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 (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a -> Binary a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate ('Left > 'Zig 'Zag)) struct =>
struct ~> Morphing ('Rotate ('Left > 'Zig 'Zag)) struct
rotate @(Left > Zig Zag) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Binary a
binary

instance Morphable (Rotate > Right > Zig Zag) Binary where
	type Morphing (Rotate > Right > Zig Zag) Binary = Binary
	morphing :: (<::>) (Tagged ('Rotate > ('Right > 'Zig 'Zag))) Binary a
-> Morphing ('Rotate > ('Right > 'Zig 'Zag)) Binary a
morphing ((<::>) (Tagged ('Rotate > ('Right > 'Zig 'Zag))) Binary a
-> Binary a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Binary a
binary) = ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary 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 (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a -> Binary a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate ('Right > 'Zig 'Zag)) struct =>
struct ~> Morphing ('Rotate ('Right > 'Zig 'Zag)) struct
rotate @(Right > Zig Zag) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Binary a -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Binary a
binary

-------------------------------------- Non-empty Splay tree ----------------------------------------

instance Morphable (Rotate > Left Zig) (Construction (Maybe <:*:> Maybe)) where
	type Morphing (Rotate > Left Zig) (Construction (Maybe <:*:> Maybe)) = Binary
	morphing :: (<::>)
  (Tagged ('Rotate > 'Left 'Zig))
  (Construction (Maybe <:*:> Maybe))
  a
-> Morphing
     ('Rotate > 'Left 'Zig) (Construction (Maybe <:*:> Maybe)) a
morphing ((<::>)
  (Tagged ('Rotate > 'Left 'Zig))
  (Construction (Maybe <:*:> Maybe))
  a
-> Construction (Maybe <:*:> Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construction (Maybe <:*:> Maybe) a
tree) = ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    >>> a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct
		(a
 -> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
     >>> a)
 -> Construction (Maybe <:*:> Maybe) a)
-> Maybe a
-> Maybe
     ((((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
      -> Construction (Maybe <:*:> Maybe) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (Construction (Maybe <:*:> Maybe) a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Construction (Maybe <:*:> Maybe) a -> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|--- TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Right 'Branch) structure
sub @(Right Branch) (Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
tree)
		Maybe
  ((((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
   -> Construction (Maybe <:*:> Maybe) a)
-> Maybe
     (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
-> Maybe
     (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
forall a. a -> Maybe a
Just (
			((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
(<:*:>)
				(TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Branch) structure
sub @(Left Branch) (Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
tree)
				(Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall a. a -> Maybe a
Just (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
     >>> a)
    -> Construction (Maybe <:*:> Maybe) a)
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    >>> a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct (Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly a -> a) -> Exactly a -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens Exactly (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a -> Exactly a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Exactly (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a -> Exactly a)
-> Lens Exactly (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> Exactly 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 'Root structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Root structure
sub @Root (Construction (Maybe <:*:> Maybe) a -> Exactly a)
-> Construction (Maybe <:*:> Maybe) a -> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
tree) ((((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
(<:*:>)
					(TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a
    -> TT
         Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Branch) structure
sub @(Left Branch)) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Right 'Branch) structure
sub @(Right Branch) (Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
tree)
					(TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a
    -> TT
         Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Right 'Branch) structure
sub @(Right Branch)) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Right 'Branch) structure
sub @(Right Branch) (Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
tree)
				)
			)

instance Morphable (Rotate > Right Zig) (Construction (Maybe <:*:> Maybe)) where
	type Morphing (Rotate > Right Zig) (Construction (Maybe <:*:> Maybe)) = Binary
	morphing :: (<::>)
  (Tagged ('Rotate > 'Right 'Zig))
  (Construction (Maybe <:*:> Maybe))
  a
-> Morphing
     ('Rotate > 'Right 'Zig) (Construction (Maybe <:*:> Maybe)) a
morphing ((<::>)
  (Tagged ('Rotate > 'Right 'Zig))
  (Construction (Maybe <:*:> Maybe))
  a
-> Construction (Maybe <:*:> Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construction (Maybe <:*:> Maybe) a
tree) = ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    >>> a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct
		(a
 -> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
     >>> a)
 -> Construction (Maybe <:*:> Maybe) a)
-> Maybe a
-> Maybe
     ((((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
      -> Construction (Maybe <:*:> Maybe) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- (Construction (Maybe <:*:> Maybe) a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Construction (Maybe <:*:> Maybe) a -> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a) -> Maybe a
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|--- TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Branch) structure
sub @(Left Branch) (Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
tree)
		Maybe
  ((((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
   -> Construction (Maybe <:*:> Maybe) a)
-> Maybe
     (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (t :: * -> *) a b.
(Covariant (->) (->) t, Semimonoidal (-->) (:*:) (:*:) t) =>
t (a -> b) -> t a -> t b
<-*- (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
-> Maybe
     (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
forall a. a -> Maybe a
Just (
			((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
(<:*:>)
				(TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a
    -> TT
         Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Branch) structure
sub @(Left Branch)) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Branch) structure
sub @(Left Branch) (Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
tree)
				(Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall a. a -> Maybe a
Just (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
     >>> a)
    -> Construction (Maybe <:*:> Maybe) a)
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    >>> a)
-> Construction (Maybe <:*:> Maybe) a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct (Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly a -> a) -> Exactly a -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens Exactly (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a -> Exactly a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Exactly (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a -> Exactly a)
-> Lens Exactly (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> Exactly 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 'Root structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Root structure
sub @Root (Construction (Maybe <:*:> Maybe) a -> Exactly a)
-> Construction (Maybe <:*:> Maybe) a -> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
tree) ((((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a)
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe))
    >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe <:*:> Maybe) :. Construction (Maybe <:*:> Maybe)) >>> a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
(<:*:>)
					(TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a
    -> TT
         Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Branch) structure
sub @(Left Branch)) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Branch) structure
sub @(Left Branch) (Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
tree)
					(TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Right 'Branch) structure
sub @(Right Branch) (Construction (Maybe <:*:> Maybe) a
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
tree)
				)
			)

-- TODO: Slidable (Left > Zig) (Construction (Maybe <:*:> Maybe))
-- TODO: Slidable (Left > Zig Zig) (Construction (Maybe <:*:> Maybe))
-- TODO: Slidable (Right > Zig Zig) (Construction (Maybe <:*:> Maybe))
-- TODO: Slidable (Left > Zig Zag) (Construction (Maybe <:*:> Maybe))
-- TODO: Slidable (Right > Zig Zag) (Construction (Maybe <:*:> Maybe))
-- TODO: Slidable (Left > Zig) Binary
-- TODO: Slidable (Left > Zig Zig) Binary
-- TODO: Slidable (Right > Zig Zig) Binary
-- TODO: Slidable (Left > Zig Zag) Binary
-- TODO: Slidable (Right > Zig Zag) Binary

instance Slidable (Right Zig) (Construction (Maybe <:*:> Maybe)) where
	type Sliding (Right Zig) (Construction (Maybe <:*:> Maybe)) = Maybe
	slide :: forall element . State > Nonempty Binary element :> Maybe >>> ()
	slide :: ((State > Nonempty Binary element) :> Maybe) >>> ()
slide = (:>)
  (State > Construction (Maybe <:*:> Maybe) element)
  Maybe
  (Binary element)
-> (:>) (State > Construction (Maybe <:*:> Maybe) element) Maybe ()
forall (t :: * -> *) a. Covariant (->) (->) t => t a -> t ()
void ((:>)
   (State > Construction (Maybe <:*:> Maybe) element)
   Maybe
   (Binary element)
 -> (:>)
      (State > Construction (Maybe <:*:> Maybe) element) Maybe ())
-> (Binary element
    -> (:>)
         (State > Construction (Maybe <:*:> Maybe) element)
         Maybe
         (Binary element))
-> Binary element
-> (:>) (State > Construction (Maybe <:*:> Maybe) element) Maybe ()
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Binary element
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element)
forall (t :: * -> *) a. Pointable t => a -> t a
point
		(Binary element
 -> (:>)
      (State > Construction (Maybe <:*:> Maybe) element) Maybe ())
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element)
-> (:>) (State > Construction (Maybe <:*:> Maybe) element) Maybe ()
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< ((->)
 < State
     (Construction (Maybe <:*:> Maybe) element) (Binary element))
< (:>)
    (State > Construction (Maybe <:*:> Maybe) element)
    Maybe
    (Binary element)
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->)
  < State
      (Construction (Maybe <:*:> Maybe) element) (Binary element))
 < (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element))
-> (Binary element
    -> State
         (Construction (Maybe <:*:> Maybe) element) (Binary element))
-> Binary element
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens Binary (Nonempty Binary element) element
-> State (Binary element) (Binary element)
-> State (Nonempty Binary element) (Binary element)
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom @(Nonempty Binary element) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure ('Right 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Right 'Branch) structure
sub @(Right Branch)) (State (Binary element) (Binary element)
 -> State
      (Construction (Maybe <:*:> Maybe) element) (Binary element))
-> (Binary element -> State (Binary element) (Binary element))
-> Binary element
-> State
     (Construction (Maybe <:*:> Maybe) element) (Binary element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
.
			Lens Binary (Binary element) element
-> State (Binary element) (Binary element)
-> State (Binary element) (Binary element)
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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Branch) structure
sub @(Left Branch)) (State (Binary element) (Binary element)
 -> State (Binary element) (Binary element))
-> (Binary element -> State (Binary element) (Binary element))
-> Binary element
-> State (Binary element) (Binary element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Binary element -> Binary element)
-> State (Binary element) (Binary element)
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
change ((Binary element -> Binary element)
 -> State (Binary element) (Binary element))
-> (Binary element -> Binary element -> Binary element)
-> Binary element
-> State (Binary element) (Binary element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Binary element -> Binary element -> Binary element
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant
		(Binary element
 -> (:>)
      (State > Construction (Maybe <:*:> Maybe) element)
      Maybe
      (Binary element))
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element)
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< ((->)
 < State
     (Construction (Maybe <:*:> Maybe) element) (Binary element))
< (:>)
    (State > Construction (Maybe <:*:> Maybe) element)
    Maybe
    (Binary element)
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->)
  < State
      (Construction (Maybe <:*:> Maybe) element) (Binary element))
 < (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element))
-> (Construction (Maybe <:*:> Maybe) element
    -> State
         (Construction (Maybe <:*:> Maybe) element) (Binary element))
-> Construction (Maybe <:*:> Maybe) element
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Lens Binary (Nonempty Binary element) element
-> State (Binary element) (Binary element)
-> State (Nonempty Binary element) (Binary element)
forall bg ls (u :: * -> *) result.
Lens u bg ls -> State (u ls) result -> State bg result
zoom @(Nonempty Binary element) (forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure ('Right 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Right 'Branch) structure
sub @(Right Branch))
			(State (Binary element) (Binary element)
 -> State
      (Construction (Maybe <:*:> Maybe) element) (Binary element))
-> (Construction (Maybe <:*:> Maybe) element
    -> State (Binary element) (Binary element))
-> Construction (Maybe <:*:> Maybe) element
-> State
     (Construction (Maybe <:*:> Maybe) element) (Binary element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
forall (t :: * -> *).
Stateful (Binary element) t =>
(Binary element -> Binary element) -> t (Binary element)
change @(Binary element) ((Binary element -> Binary element)
 -> State (Binary element) (Binary element))
-> (Construction (Maybe <:*:> Maybe) element
    -> Binary element -> Binary element)
-> Construction (Maybe <:*:> Maybe) element
-> State (Binary element) (Binary element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Binary element -> Binary element -> Binary element
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (Binary element -> Binary element -> Binary element)
-> (Construction (Maybe <:*:> Maybe) element -> Binary element)
-> Construction (Maybe <:*:> Maybe) element
-> Binary element
-> Binary element
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction (Maybe <:*:> Maybe) element -> Binary element
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift
		(Construction (Maybe <:*:> Maybe) element
 -> (:>)
      (State > Construction (Maybe <:*:> Maybe) element)
      Maybe
      (Binary element))
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element)
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< (Construction (Maybe <:*:> Maybe) element
 -> Construction (Maybe <:*:> Maybe) element)
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element)
forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
change ((Construction (Maybe <:*:> Maybe) element
  -> Construction (Maybe <:*:> Maybe) element)
 -> (:>)
      (State > Construction (Maybe <:*:> Maybe) element)
      Maybe
      (Construction (Maybe <:*:> Maybe) element))
-> (Construction (Maybe <:*:> Maybe) element
    -> Construction (Maybe <:*:> Maybe) element
    -> Construction (Maybe <:*:> Maybe) element)
-> Construction (Maybe <:*:> Maybe) element
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction (Maybe <:*:> Maybe) element
-> Construction (Maybe <:*:> Maybe) element
-> Construction (Maybe <:*:> Maybe) element
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (Construction (Maybe <:*:> Maybe) element
 -> (:>)
      (State > Construction (Maybe <:*:> Maybe) element)
      Maybe
      (Construction (Maybe <:*:> Maybe) element))
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element)
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< ((->) < Maybe (Construction (Maybe <:*:> Maybe) element))
< (:>)
    (State > Construction (Maybe <:*:> Maybe) element)
    Maybe
    (Construction (Maybe <:*:> Maybe) element)
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->) < Maybe (Construction (Maybe <:*:> Maybe) element))
 < (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element))
-> (Binary element
    -> Maybe (Construction (Maybe <:*:> Maybe) element))
-> Binary element
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Binary element -> Maybe (Construction (Maybe <:*:> Maybe) element)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run
		(Binary element
 -> (:>)
      (State > Construction (Maybe <:*:> Maybe) element)
      Maybe
      (Construction (Maybe <:*:> Maybe) element))
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element)
-> (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
===<< ((->)
 < State
     (Construction (Maybe <:*:> Maybe) element) (Binary element))
< (:>)
    (State > Construction (Maybe <:*:> Maybe) element)
    Maybe
    (Binary element)
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->)
  < State
      (Construction (Maybe <:*:> Maybe) element) (Binary element))
 < (:>)
     (State > Construction (Maybe <:*:> Maybe) element)
     Maybe
     (Binary element))
-> ((->)
    < State
        (Construction (Maybe <:*:> Maybe) element) (Binary element))
   < (:>)
       (State > Construction (Maybe <:*:> Maybe) element)
       Maybe
       (Binary element)
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 (Nonempty Binary element) ls
-> State (u ls) result -> State (Nonempty Binary element) result
zoom @(Nonempty Binary element)
			(P_Q_T
   (->)
   Store
   Binary
   (Construction (Maybe <:*:> Maybe) element)
   element
 -> State (Binary element) (Binary element)
 -> State
      (Construction (Maybe <:*:> Maybe) element) (Binary element))
-> P_Q_T
     (->)
     Store
     Binary
     (Construction (Maybe <:*:> Maybe) element)
     element
-> State (Binary element) (Binary element)
-> State
     (Construction (Maybe <:*:> Maybe) element) (Binary element)
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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Branch) structure
sub @(Left Branch)
			(State (Binary element) (Binary element)
 -> State
      (Construction (Maybe <:*:> Maybe) element) (Binary element))
-> State (Binary element) (Binary element)
-> State
     (Construction (Maybe <:*:> Maybe) element) (Binary element)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall s (t :: * -> *). Stateful s t => t s
forall (t :: * -> *).
Stateful (Binary element) t =>
t (Binary element)
current @(Binary element)

instance Slidable (Right > Zig) Binary where
	type Sliding (Right Zig) Binary = Maybe
	slide :: forall element . State > Binary element :> Maybe >>> ()
	slide :: ((State > Binary element) :> Maybe) >>> ()
slide = (:>) (State > Binary element) Maybe (Binary element)
-> ((State > Binary element) :> Maybe) >>> ()
forall (t :: * -> *) a. Covariant (->) (->) t => t a -> t ()
void ((:>) (State > Binary element) Maybe (Binary element)
 -> ((State > Binary element) :> Maybe) >>> ())
-> ((Construction (Maybe <:*:> Maybe) element :*: ())
    -> (:>) (State > Binary element) Maybe (Binary element))
-> (Construction (Maybe <:*:> Maybe) element :*: ())
-> ((State > Binary element) :> Maybe) >>> ()
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall s (t :: * -> *). Stateful s t => (s -> s) -> t s
forall (t :: * -> *).
Stateful (Binary element) t =>
(Binary element -> Binary element) -> t (Binary element)
change @(Binary element) ((Binary element -> Binary element)
 -> (:>) (State > Binary element) Maybe (Binary element))
-> ((Construction (Maybe <:*:> Maybe) element :*: ())
    -> Binary element -> Binary element)
-> (Construction (Maybe <:*:> Maybe) element :*: ())
-> (:>) (State > Binary element) Maybe (Binary element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Binary element -> Binary element -> Binary element
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant (Binary element -> Binary element -> Binary element)
-> ((Construction (Maybe <:*:> Maybe) element :*: ())
    -> Binary element)
-> (Construction (Maybe <:*:> Maybe) element :*: ())
-> Binary element
-> Binary element
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction (Maybe <:*:> Maybe) element -> Binary element
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (Construction (Maybe <:*:> Maybe) element -> Binary element)
-> ((Construction (Maybe <:*:> Maybe) element :*: ())
    -> Construction (Maybe <:*:> Maybe) element)
-> (Construction (Maybe <:*:> Maybe) element :*: ())
-> Binary element
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Construction (Maybe <:*:> Maybe) element :*: ())
-> Construction (Maybe <:*:> Maybe) element
forall a b. (a :*: b) -> a
attached
		((Construction (Maybe <:*:> Maybe) element :*: ())
 -> ((State > Binary element) :> Maybe) >>> ())
-> (:>)
     (State > Binary element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element :*: ())
-> ((State > Binary element) :> Maybe) >>> ()
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< ((->) < Maybe (Construction (Maybe <:*:> Maybe) element :*: ()))
< (:>)
    (State > Binary element)
    Maybe
    (Construction (Maybe <:*:> Maybe) element :*: ())
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->) < Maybe (Construction (Maybe <:*:> Maybe) element :*: ()))
 < (:>)
     (State > Binary element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element :*: ()))
-> (Construction (Maybe <:*:> Maybe) element
    -> Maybe (Construction (Maybe <:*:> Maybe) element :*: ()))
-> Construction (Maybe <:*:> Maybe) element
-> (:>)
     (State > Binary element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element :*: ())
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (forall e.
Slidable ('Right 'Zig) (Nonempty Binary) =>
((State < Nonempty Binary e)
 :> Sliding ('Right 'Zig) (Nonempty Binary))
>>> ()
forall k (d :: k) (s :: * -> *) e.
Slidable d s =>
((State < s e) :> Sliding d s) >>> ()
slide @(Right > Zig) @(Nonempty Binary) (:>) (State (Construction (Maybe <:*:> Maybe) element)) Maybe ()
-> Construction (Maybe <:*:> Maybe) element
-> Maybe (Construction (Maybe <:*:> Maybe) element :*: ())
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~)
		(Construction (Maybe <:*:> Maybe) element
 -> (:>)
      (State > Binary element)
      Maybe
      (Construction (Maybe <:*:> Maybe) element :*: ()))
-> (:>)
     (State > Binary element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element)
-> (:>)
     (State > Binary element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element :*: ())
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< ((->) < Maybe (Construction (Maybe <:*:> Maybe) element))
< (:>)
    (State > Binary element)
    Maybe
    (Construction (Maybe <:*:> Maybe) element)
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->) < Maybe (Construction (Maybe <:*:> Maybe) element))
 < (:>)
     (State > Binary element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element))
-> (Binary element
    -> Maybe (Construction (Maybe <:*:> Maybe) element))
-> Binary element
-> (:>)
     (State > Binary element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Binary element -> Maybe (Construction (Maybe <:*:> Maybe) element)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Binary element
 -> (:>)
      (State > Binary element)
      Maybe
      (Construction (Maybe <:*:> Maybe) element))
-> (:>) (State > Binary element) Maybe (Binary element)
-> (:>)
     (State > Binary element)
     Maybe
     (Construction (Maybe <:*:> Maybe) element)
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< forall s (t :: * -> *). Stateful s t => t s
forall (t :: * -> *).
Stateful (Binary element) t =>
t (Binary element)
current @(Binary element)

-- TODO: Morphing ... = Conclussion Error <::> Nonempty Binary
instance Morphable (Rotate > Left > Zig Zig) (Construction (Maybe <:*:> Maybe)) where
	type Morphing (Rotate > Left > Zig Zig) (Construction (Maybe <:*:> Maybe)) = Maybe <::> Construction (Maybe <:*:> Maybe)
	morphing :: (<::>)
  (Tagged ('Rotate > ('Left > 'Zig 'Zig)))
  (Construction (Maybe <:*:> Maybe))
  a
-> Morphing
     ('Rotate > ('Left > 'Zig 'Zig))
     (Construction (Maybe <:*:> Maybe))
     a
morphing ((<::>)
  (Tagged ('Rotate > ('Left > 'Zig 'Zig)))
  (Construction (Maybe <:*:> Maybe))
  a
-> Construction (Maybe <:*:> Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construction (Maybe <:*:> Maybe) a
tree) = ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a
    -> TT
         Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate ('Left 'Zig)) struct =>
struct ~> Morphing ('Rotate ('Left 'Zig)) struct
rotate @(Left Zig) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
==<< TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
-> Morphing
     ('Rotate ('Left 'Zig)) (Construction (Maybe <:*:> Maybe)) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
rotate @(Left Zig) Construction (Maybe <:*:> Maybe) a
tree

-- TODO: Morphing ... = Conclussion Error <::> Nonempty Binary
instance Morphable (Rotate > Right > Zig Zig) (Construction (Maybe <:*:> Maybe)) where
	type Morphing (Rotate > Right > Zig Zig) (Construction (Maybe <:*:> Maybe)) = Maybe <::> Construction (Maybe <:*:> Maybe)
	morphing :: (<::>)
  (Tagged ('Rotate > ('Right > 'Zig 'Zig)))
  (Construction (Maybe <:*:> Maybe))
  a
-> Morphing
     ('Rotate > ('Right > 'Zig 'Zig))
     (Construction (Maybe <:*:> Maybe))
     a
morphing ((<::>)
  (Tagged ('Rotate > ('Right > 'Zig 'Zig)))
  (Construction (Maybe <:*:> Maybe))
  a
-> Construction (Maybe <:*:> Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construction (Maybe <:*:> Maybe) a
tree) = ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) 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 (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
 -> TT
      Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Construction (Maybe <:*:> Maybe) a
    -> TT
         Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a)
-> Construction (Maybe <:*:> Maybe) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate ('Right 'Zig)) struct =>
struct ~> Morphing ('Rotate ('Right 'Zig)) struct
rotate @(Right Zig) (Construction (Maybe <:*:> Maybe) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
==<< TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
-> Morphing
     ('Rotate ('Right 'Zig)) (Construction (Maybe <:*:> Maybe)) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
rotate @(Right Zig) Construction (Maybe <:*:> Maybe) a
tree

-- TODO: Morphing ... = Conclussion Error <::> Nonempty Binary
instance Morphable (Rotate > Left > Zig Zag) (Construction (Maybe <:*:> Maybe)) where
	type Morphing (Rotate > Left > Zig Zag) (Construction (Maybe <:*:> Maybe)) = Maybe <::> Construction (Maybe <:*:> Maybe)
	morphing :: (<::>)
  (Tagged ('Rotate > ('Left > 'Zig 'Zag)))
  (Construction (Maybe <:*:> Maybe))
  a
-> Morphing
     ('Rotate > ('Left > 'Zig 'Zag))
     (Construction (Maybe <:*:> Maybe))
     a
morphing ((<::>)
  (Tagged ('Rotate > ('Left > 'Zig 'Zag)))
  (Construction (Maybe <:*:> Maybe))
  a
-> Construction (Maybe <:*:> Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construction (Maybe <:*:> Maybe) a
struct) = forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate ('Left 'Zig)) struct =>
struct ~> Morphing ('Rotate ('Left 'Zig)) struct
rotate @(Left Zig) (Construction (Maybe <:*:> Maybe) a -> Binary a)
-> Construction (Maybe <:*:> Maybe) a -> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (Binary a -> Binary a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
forall (i :: * -> *) target source.
(i target -> i target) -> Lens i source target -> source -> source
mutate ((Binary a -> Binary a)
 -> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a)
-> (Binary a -> Binary a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (Morphed ('Rotate ('Right 'Zig)) (Nonempty Binary) Binary =>
Nonempty Binary ~> Nonempty Binary
forall a (direction :: a).
Morphed ('Rotate direction) (Nonempty Binary) Binary =>
Nonempty Binary ~> Nonempty Binary
try_to_rotate @(Right Zig) (forall a.
 Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a)
-> Binary a -> Binary a
forall k (m :: * -> * -> *) (t :: (* -> *) -> k -> *) (u :: * -> *)
       (v :: * -> *).
(Hoistable m t, Covariant m m u) =>
(forall a. m (u a) (v a)) -> forall (a :: k). m (t u a) (t v a)
/|\) (Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Branch) structure
sub @(Left Branch) (Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
struct

-- TODO: Morphing ... = Conclussion Error <::> Nonempty Binary
instance Morphable (Rotate > Right > Zig Zag) (Construction (Maybe <:*:> Maybe)) where
	type Morphing (Rotate > Right > Zig Zag) (Construction (Maybe <:*:> Maybe)) = Maybe <::> Construction (Maybe <:*:> Maybe)
	morphing :: (<::>)
  (Tagged ('Rotate > ('Right > 'Zig 'Zag)))
  (Construction (Maybe <:*:> Maybe))
  a
-> Morphing
     ('Rotate > ('Right > 'Zig 'Zag))
     (Construction (Maybe <:*:> Maybe))
     a
morphing ((<::>)
  (Tagged ('Rotate > ('Right > 'Zig 'Zag)))
  (Construction (Maybe <:*:> Maybe))
  a
-> Construction (Maybe <:*:> Maybe) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> Construction (Maybe <:*:> Maybe) a
struct) = forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
forall (struct :: * -> *).
Morphable ('Rotate ('Right 'Zig)) struct =>
struct ~> Morphing ('Rotate ('Right 'Zig)) struct
rotate @(Right Zig) (Construction (Maybe <:*:> Maybe) a -> Binary a)
-> Construction (Maybe <:*:> Maybe) a -> Binary a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (Binary a -> Binary a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
forall (i :: * -> *) target source.
(i target -> i target) -> Lens i source target -> source -> source
mutate ((Binary a -> Binary a)
 -> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a)
-> (Binary a -> Binary a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (Morphed ('Rotate ('Left 'Zig)) (Nonempty Binary) Binary =>
Nonempty Binary ~> Nonempty Binary
forall a (direction :: a).
Morphed ('Rotate direction) (Nonempty Binary) Binary =>
Nonempty Binary ~> Nonempty Binary
try_to_rotate @(Left Zig) (forall a.
 Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a)
-> Binary a -> Binary a
forall k (m :: * -> * -> *) (t :: (* -> *) -> k -> *) (u :: * -> *)
       (v :: * -> *).
(Hoistable m t, Covariant m m u) =>
(forall a. m (u a) (v a)) -> forall (a :: k). m (t u a) (t v a)
/|\) (Lens Binary (Construction (Maybe <:*:> Maybe) a) a
 -> Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a)
-> Lens Binary (Construction (Maybe <:*:> Maybe) a) a
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) 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 'Branch) structure,
 Covariant (->) (->) structure) =>
structure @>>> Substance ('Right 'Branch) structure
sub @(Right Branch) (Construction (Maybe <:*:> Maybe) a
 -> Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
struct

-- TODO: Include error instead of returning empty tree
try_to_rotate :: forall direction . Morphed (Rotate direction) (Nonempty Binary) Binary => Nonempty Binary ~> Nonempty Binary
try_to_rotate :: Nonempty Binary ~> Nonempty Binary
try_to_rotate Nonempty Binary a
tree = (Nonempty Binary a -> Construction (Maybe <:*:> Maybe) a)
-> Construction (Maybe <:*:> Maybe) a
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> Construction (Maybe <:*:> Maybe) a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve @(Nonempty Binary _) Nonempty Binary a -> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) a. Category m => m a a
identity Construction (Maybe <:*:> Maybe) a
Nonempty Binary a
tree (((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
 -> Construction (Maybe <:*:> Maybe) a)
-> ((Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> Construction (Maybe <:*:> Maybe) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
 -> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a)
-> TT
     Covariant Covariant Maybe (Construction (Maybe <:*:> Maybe)) a
-> (Maybe :. Construction (Maybe <:*:> Maybe)) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction (Maybe <:*:> Maybe) a
-> Morphing
     ('Rotate direction) (Construction (Maybe <:*:> Maybe)) a
forall a (mod :: a) (struct :: * -> *).
Morphable ('Rotate mod) struct =>
struct ~> Morphing ('Rotate mod) struct
rotate @direction Construction (Maybe <:*:> Maybe) a
Nonempty Binary a
tree