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