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

import Pandora.Core.Functor (type (~>), type (>))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), identity)
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-), (<-|---)))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<), (==<<), (===<<)))
import Pandora.Pattern.Transformer.Hoistable ((/|\))
import Pandora.Paradigm.Algebraic ((<-*-), extract)
import Pandora.Paradigm.Algebraic.Product (type (<:*:>), (<:*:>))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just))
import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Inventory.Some.Optics (view, mutate)
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.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Substructure (Segment (Root, Branch), sub)
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: 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 Nonempty Binary a
Construction (Maybe <:*:> Maybe) 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 Nonempty Binary a
Construction (Maybe <:*:> Maybe) a
tree