{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Structure.Some.Rose where
import Pandora.Core.Functor (type (:.), type (>>>))
import Pandora.Core.Interpreted (run, unite, (<~))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----), (<-----), identity)
import Pandora.Pattern.Kernel (constant)
import Pandora.Pattern.Functor.Covariant ((<-|-))
import Pandora.Pattern.Functor.Contravariant ((>-|-))
import Pandora.Pattern.Functor.Traversable ((<<-))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Pattern.Transformer.Lowerable (lower)
import Pandora.Pattern.Object.Setoid (Setoid ((?=)))
import Pandora.Pattern.Object.Semigroup ((+))
import Pandora.Paradigm.Algebraic.Exponential ((%))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)), type (<:*:>), (<:*:>), attached)
import Pandora.Paradigm.Algebraic.Functor (extract, point, empty)
import Pandora.Paradigm.Primary.Auxiliary (Vertical (Up, Down), Horizontal (Left, Right))
import Pandora.Paradigm.Primary.Functor.Exactly (Exactly (Exactly))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (equate)
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct)
import Pandora.Paradigm.Primary.Transformer.Reverse (Reverse)
import Pandora.Paradigm.Schemes (TU (TU), TT (TT), T_U (T_U), P_Q_T (P_Q_T), type (<::>), type (<:.>))
import Pandora.Paradigm.Inventory.Some.Store (Store (Store))
import Pandora.Paradigm.Inventory.Some.Optics (view)
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing), Morph (Into, Rotate, Lookup, Element, Key), premorph, find)
import Pandora.Paradigm.Structure.Modification.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure), Segment (Root, Rest, Forest), sub)
import Pandora.Paradigm.Structure.Interface.Zipper (Zippable (Breadcrumbs))
import Pandora.Paradigm.Structure.Interface.Stack (Stack (pop))
import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed)
import Pandora.Paradigm.Structure.Modification.Tape (Tape)
import Pandora.Paradigm.Structure.Some.List (List)
type Rose = Maybe <:.> Construction List
type instance Nonempty Rose = Construction List
instance Setoid k => Morphable (Lookup Key) (Prefixed Rose k) where
type Morphing (Lookup Key) (Prefixed Rose k) = (->) (Nonempty List k) <:.> Maybe
morphing :: (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
-> Morphing ('Lookup 'Key) (Prefixed Rose k) a
morphing (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
prefixed_rose_tree = case TT Covariant Covariant Rose ((:*:) k) a -> (Rose :. (:*:) k) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (TT Covariant Covariant Rose ((:*:) k) a
-> (Rose :. (:*:) k) >>> a)
-> TT Covariant Covariant Rose ((:*:) k) a
-> (Rose :. (:*:) k) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
-> TT Covariant Covariant Rose ((:*:) k) a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
prefixed_rose_tree of
TU Maybe (Construction List (k :*: a))
Nothing -> (((->) (Construction Maybe k) :. Maybe) >>> a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) >>> a) -> TU ct cu t u a
TU ((((->) (Construction Maybe k) :. Maybe) >>> a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a)
-> (((->) (Construction Maybe k) :. Maybe) >>> a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Maybe a -> ((->) (Construction Maybe k) :. Maybe) >>> a
forall (m :: * -> * -> *) a i. Kernel m => m a (m i a)
constant Maybe a
forall a. Maybe a
Nothing
TU (Just Construction List (k :*: a)
tree) -> (((->) (Construction Maybe k) :. Maybe) >>> a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a
forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k)
(a :: k).
((t :. u) >>> a) -> TU ct cu t u a
TU ((((->) (Construction Maybe k) :. Maybe) >>> a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a)
-> (((->) (Construction Maybe k) :. Maybe) >>> a)
-> TU Covariant Covariant ((->) (Construction Maybe k)) Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe k -> Construction List (k :*: a) -> Maybe a
forall k a.
Setoid k =>
Nonempty List k -> (Nonempty Rose >>> (k :*: a)) -> Maybe a
find_rose_sub_tree (Construction Maybe k -> Construction List (k :*: a) -> Maybe a)
-> Construction List (k :*: a)
-> ((->) (Construction Maybe k) :. Maybe) >>> a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction List (k :*: a)
tree
find_rose_sub_tree :: forall k a . Setoid k => Nonempty List k -> Nonempty Rose >>> k :*: a -> Maybe a
find_rose_sub_tree :: Nonempty List k -> (Nonempty Rose >>> (k :*: a)) -> Maybe a
find_rose_sub_tree (Construct k ks) Nonempty Rose >>> (k :*: a)
tree = k
k k -> k -> Maybe a -> Maybe a -> Maybe a
forall a r. Setoid a => a -> a -> r -> r -> r
?= (k :*: a) -> k
forall a b. (a :*: b) -> a
attached (Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Nonempty Rose >>> (k :*: a)
Construction List (k :*: a)
tree)
(Maybe a -> Maybe a -> Maybe a) -> Maybe a -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- case (Maybe :. Construction Maybe) >>> k
ks of
Just Construction Maybe k
keys -> Nonempty List k -> (Nonempty Rose >>> (k :*: a)) -> Maybe a
forall k a.
Setoid k =>
Nonempty List k -> (Nonempty Rose >>> (k :*: a)) -> Maybe a
find_rose_sub_tree Nonempty List k
Construction Maybe k
keys (Construction List (k :*: a) -> Maybe a)
-> Maybe (Construction List (k :*: a)) -> Maybe a
forall (source :: * -> * -> *) (t :: * -> *) a b.
Bindable source t =>
source a (t b) -> source (t a) (t b)
=<< Nonempty List k -> (Maybe :. Nonempty Rose) >>> (k :*: a)
subtree Nonempty List k
Construction Maybe k
keys
(Maybe :. Construction Maybe) >>> k
Nothing -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (k :*: a) -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract ((k :*: a) -> a) -> (k :*: a) -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract Nonempty Rose >>> (k :*: a)
Construction List (k :*: a)
tree
(Maybe a -> Maybe a) -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<----- Maybe a
forall a. Maybe a
Nothing where
subtree :: Nonempty List k -> Maybe :. Nonempty Rose >>> k :*: a
subtree :: Nonempty List k -> (Maybe :. Nonempty Rose) >>> (k :*: a)
subtree Nonempty List k
keys = forall a1 (mod :: a1) (struct :: * -> *) (result :: * -> *) a2.
Morphed
('Find mod) struct ((Predicate <:.:> result) >>>>>> (->)) =>
Predicate a2 -> struct a2 -> result a2
forall (struct :: * -> *) (result :: * -> *) a2.
Morphed
('Find 'Element) struct ((Predicate <:.:> result) >>>>>> (->)) =>
Predicate a2 -> struct a2 -> result a2
find @Element
(Predicate (Construction List (k :*: a))
-> List (Construction List (k :*: a))
-> Maybe (Construction List (k :*: a)))
-> Predicate (Construction List (k :*: a))
-> List (Construction List (k :*: a))
-> Maybe (Construction List (k :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (k :*: a) -> k
forall a b. (a :*: b) -> a
attached ((k :*: a) -> k)
-> (Construction List (k :*: a) -> k :*: a)
-> Construction List (k :*: a)
-> k
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) a. Extractable t => t a -> a
extract
(Construction List (k :*: a) -> k)
-> Predicate k -> Predicate (Construction List (k :*: a))
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Contravariant source target t =>
source a b -> target (t b) (t a)
>-|- k :=> Predicate
forall a. Setoid a => a :=> Predicate
equate (k :=> Predicate) -> k :=> Predicate
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Construction Maybe k -> k
forall (t :: * -> *) a. Extractable t => t a -> a
extract Nonempty List k
Construction Maybe k
keys
(List (Construction List (k :*: a))
-> Maybe (Construction List (k :*: a)))
-> List (Construction List (k :*: a))
-> Maybe (Construction List (k :*: a))
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- Construction List (k :*: a) -> List (Construction List (k :*: a))
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) >>> a
deconstruct Nonempty Rose >>> (k :*: a)
Construction List (k :*: a)
tree
type Roses = List <::> Construction List
instance Zippable (Construction List) where
type Breadcrumbs (Construction List) = Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)
instance Substructure (Up Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
type Substance (Up Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = List <::> Tape Roses
substructure :: Lens
(Substance
('Up 'Forest)
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
substructure = ((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
((<::>) List (Tape Roses) a)
((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
(List <::> Tape Roses)
((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
((<::>) List (Tape Roses) a)
((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
(List <::> Tape Roses)
((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a)
-> ((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
((<::>) List (Tape Roses) a)
((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
(List <::> Tape Roses)
((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
zipper -> case T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
zipper of
Exactly a
x :*: T_U (Roses a
down :*: T_U (Reverse Roses a
left :*: T_U (Roses a
right :*: (<::>) List (Tape Roses) a
up))) ->
(((:*:) ((<::>) List (Tape Roses) a)
:. (->) ((<::>) List (Tape Roses) a))
>>> (<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
((<::>) List (Tape Roses) a)
((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) ((<::>) List (Tape Roses) a)
:. (->) ((<::>) List (Tape Roses) a))
>>> (<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
((<::>) List (Tape Roses) a)
((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> (((:*:) ((<::>) List (Tape Roses) a)
:. (->) ((<::>) List (Tape Roses) a))
>>> (<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
((<::>) List (Tape Roses) a)
((<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (<::>) List (Tape Roses) a
up (<::>) List (Tape Roses) a
-> ((<::>) List (Tape Roses) a
-> (<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> ((:*:) ((<::>) List (Tape Roses) a)
:. (->) ((<::>) List (Tape Roses) a))
>>> (<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall s a. s -> a -> s :*: a
:*: T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> ((<::>) List (Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
-> (<::>) List (Tape Roses) a
-> (<:.>)
(Tagged ('Up 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
-> ((<::>) List (Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> (<::>) List (Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
down Roses a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> ((<::>) List (Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a)
-> (<::>) List (Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Reverse Roses a
left Reverse Roses a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a)
-> ((<::>) List (Tape Roses) a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a)
-> (<::>) List (Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
right Roses a
-> (<::>) List (Tape Roses) a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>)
instance Substructure (Down Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
type Substance (Down Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = Roses
substructure :: Lens
(Substance
('Down 'Forest)
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
substructure = ((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
(Roses a)
((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
Roses
((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
(Roses a)
((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
Roses
((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a)
-> ((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
(Roses a)
((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
Roses
((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
zipper -> case T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
zipper of
Exactly a
x :*: T_U (Roses a
down :*: (<:*:>) (Reverse Roses) (Roses <:*:> (List <::> Tape Roses)) a
rest) ->
(((:*:) (Roses a) :. (->) (Roses a))
>>> (<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
(Roses a)
((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Roses a) :. (->) (Roses a))
>>> (<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
(Roses a)
((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> (((:*:) (Roses a) :. (->) (Roses a))
>>> (<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
(Roses a)
((<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Roses a
down Roses a
-> (Roses a
-> (<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> ((:*:) (Roses a) :. (->) (Roses a))
>>> (<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall s a. s -> a -> s :*: a
:*: T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> (Roses a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
-> Roses a
-> (<:.>)
(Tagged ('Down 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
-> (Roses a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> Roses a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
-> (<:*:>) (Reverse Roses) (Roses <:*:> (List <::> Tape Roses)) a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> (<:*:>) (Reverse Roses) (Roses <:*:> (List <::> Tape Roses)) a
rest)
instance Substructure (Left Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
type Substance (Left Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = Reverse Roses
substructure :: Lens
(Substance
('Left 'Forest)
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
substructure = ((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
(Reverse Roses a)
((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
(Reverse Roses)
((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
(Reverse Roses a)
((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
(Reverse Roses)
((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a)
-> ((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
(Reverse Roses a)
((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
(Reverse Roses)
((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
zipper -> case T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
zipper of
Exactly a
x :*: T_U (Roses a
down :*: T_U (Reverse Roses a
left :*: (<:*:>) Roses (List <::> Tape Roses) a
rest)) ->
(((:*:) (Reverse Roses a) :. (->) (Reverse Roses a))
>>> (<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
(Reverse Roses a)
((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Reverse Roses a) :. (->) (Reverse Roses a))
>>> (<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
(Reverse Roses a)
((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> (((:*:) (Reverse Roses a) :. (->) (Reverse Roses a))
>>> (<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
(Reverse Roses a)
((<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Reverse Roses a
left Reverse Roses a
-> (Reverse Roses a
-> (<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> ((:*:) (Reverse Roses a) :. (->) (Reverse Roses a))
>>> (<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall s a. s -> a -> s :*: a
:*: T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> (Reverse Roses a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
-> Reverse Roses a
-> (<:.>)
(Tagged ('Left 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
-> (Reverse Roses a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> Reverse Roses a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
down Roses a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> (Reverse Roses a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a)
-> Reverse Roses a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Reverse Roses a
-> (<:*:>) Roses (List <::> Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> (<:*:>) Roses (List <::> Tape Roses) a
rest)
instance Substructure (Right Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
type Substance (Right Forest) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) = Roses
substructure :: Lens
(Substance
('Right 'Forest)
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
substructure = ((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
(Roses a)
((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
Roses
((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
forall (p :: * -> * -> *) (q :: * -> * -> *) (t :: * -> *) a b.
p a (q (t b) a) -> P_Q_T p q t a b
P_Q_T (((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
(Roses a)
((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
Roses
((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a)
-> ((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Store
(Roses a)
((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> P_Q_T
(->)
Store
Roses
((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
zipper -> case T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
:*: T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
lower (<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
zipper of
Exactly a
x :*: T_U (Roses a
down :*: T_U (Reverse Roses a
left :*: T_U (Roses a
right :*: (<::>) List (Tape Roses) a
rest))) ->
(((:*:) (Roses a) :. (->) (Roses a))
>>> (<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
(Roses a)
((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
forall s a. (((:*:) s :. (->) s) >>> a) -> Store s a
Store ((((:*:) (Roses a) :. (->) (Roses a))
>>> (<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
(Roses a)
((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a))
-> (((:*:) (Roses a) :. (->) (Roses a))
>>> (<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> Store
(Roses a)
((<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Roses a
right Roses a
-> (Roses a
-> (<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> ((:*:) (Roses a) :. (->) (Roses a))
>>> (<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall s a. s -> a -> s :*: a
:*: T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
lift (T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> (Roses a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
-> Roses a
-> (<:.>)
(Tagged ('Right 'Forest))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
-> (Roses a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> Roses a
-> T_U
Covariant
Covariant
(:*:)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
down Roses a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a)
-> (Roses a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a)
-> Roses a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Reverse Roses a
left Reverse Roses a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:>) (T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a)
-> (Roses a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a)
-> Roses a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Roses a
-> (<::>) List (Tape Roses) a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> (<::>) List (Tape Roses) a
rest)
instance Morphable (Into (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses))) (Construction List) where
type Morphing (Into (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses))) (Construction List) =
Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)
morphing :: (<::>)
(Tagged
('Into
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses
<:*:> (Roses <:*:> (List <::> Tape Roses)))))))
(Construction List)
a
-> Morphing
('Into
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
(Construction List)
a
morphing (<::>)
(Tagged
('Into
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses
<:*:> (Roses <:*:> (List <::> Tape Roses)))))))
(Construction List)
a
nonempty_rose_tree = case (<::>)
(Tagged
('Into
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses
<:*:> (Roses <:*:> (List <::> Tape Roses)))))))
(Construction List)
a
-> Construction List a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph (<::>)
(Tagged
('Into
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses
<:*:> (Roses <:*:> (List <::> Tape Roses)))))))
(Construction List)
a
nonempty_rose_tree of
Construct a
x (List :. Construction List) >>> a
xs -> a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
-> (Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
>>>>>> a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> ((List :. Construction List) >>> a) -> Roses a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < Primary t a) < t a
unite (List :. Construction List) >>> a
xs Roses a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> Reverse Roses a
forall (t :: * -> *) a. Emptiable t => t a
empty Reverse Roses a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> Roses a
forall (t :: * -> *) a. Emptiable t => t a
empty Roses a
-> (<::>) List (Tape Roses) a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> (<::>) List (Tape Roses) a
forall (t :: * -> *) a. Emptiable t => t a
empty
instance Morphable (Rotate Up) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) where
type Morphing (Rotate Up) (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses)) =
Maybe <::> (Exactly <:*:> Roses <:*:> Reverse Roses <:*:> Roses <:*:> (List <::> Tape Roses))
morphing :: (<::>)
(Tagged ('Rotate 'Up))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> Morphing
('Rotate 'Up)
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
morphing ((<::>)
(Tagged ('Rotate 'Up))
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <::> struct) ~> struct
premorph -> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
z) = ((Maybe
:. (Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
>>> a)
-> TT
Covariant
Covariant
Maybe
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
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
:. (Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
>>> a)
-> TT
Covariant
Covariant
Maybe
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a)
-> ((Maybe
:. (Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
>>> a)
-> TT
Covariant
Covariant
Maybe
(Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))))
a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- (TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
:*: T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
restruct ((TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
:*: T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
-> Maybe
(TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
:*: T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
-> (Maybe
:. (Exactly
<:*:> (Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))))
>>> a
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- forall a. Category (->) => a -> a
forall (m :: * -> * -> *) a. Category m => m a a
identity @(->) (Maybe
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
-> Maybe
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a))
-> (TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
:*: Maybe
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a))
-> Maybe
(TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
:*: T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
forall (source :: * -> * -> *) (target :: * -> * -> *)
(t :: * -> *) (u :: * -> *) a b.
(Traversable source target t, Covariant source target u,
Monoidal (Straight source) (Straight target) (:*:) (:*:) u) =>
source a (u b) -> target (t a) (u (t b))
<<- forall e. Stack List => (State < List e) < Topping List e
forall (structure :: * -> *) e.
Stack structure =>
(State < structure e) < Topping structure e
pop @List State
(TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a))
(Maybe
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a))
-> ((->)
(TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a))
:. (:*:)
(TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)))
>>> Maybe
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ (<::>) List (Tape Roses) a
-> TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Lens
(List <::> Tape Roses)
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<::>) List (Tape Roses) a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
(List <::> Tape Roses)
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<::>) List (Tape Roses) a)
-> Lens
(List <::> Tape Roses)
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<::>) List (Tape Roses) 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 ('Up 'Forest) structure,
Covariant (->) (->) structure) =>
structure @>>> Substance ('Up 'Forest) structure
sub @(Up Forest) ((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<::>) List (Tape Roses) a)
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> (<::>) List (Tape Roses) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
z) where
restruct :: (TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
:*: T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
restruct (TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
parents :*: T_U Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
parent) =
let child_node :: a
child_node = 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
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
Exactly
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a)
-> Lens
Exactly
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
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 ((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a)
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
z in
let central_children :: (List :. Construction List) >>> a
central_children = Roses a -> (List :. Construction List) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Roses a -> (List :. Construction List) >>> a)
-> Roses a -> (List :. Construction List) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
Roses
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
Roses
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Roses a)
-> Lens
Roses
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Roses 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 ('Down 'Forest) structure,
Covariant (->) (->) structure) =>
structure @>>> Substance ('Down 'Forest) structure
sub @(Down Forest) ((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Roses a)
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
z in
let left_children :: (List :. Construction List) >>> a
left_children = forall (t :: * -> *) a.
Interpreted (->) t =>
((->) < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) (Roses a -> (List :. Construction List) >>> a)
-> Roses a -> (List :. Construction List) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- Reverse Roses a -> Roses a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Reverse Roses a -> Roses a) -> Reverse Roses a -> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
(Reverse Roses)
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Reverse Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
(Reverse Roses)
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Reverse Roses a)
-> Lens
(Reverse Roses)
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Reverse Roses 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 'Forest) structure,
Covariant (->) (->) structure) =>
structure @>>> Substance ('Left 'Forest) structure
sub @(Left Forest) ((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Reverse Roses a)
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Reverse Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
z in
let right_children :: (List :. Construction List) >>> a
right_children = Roses a -> (List :. Construction List) >>> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run (Roses a -> (List :. Construction List) >>> a)
-> Roses a -> (List :. Construction List) >>> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
Roses
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
Roses
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Roses a)
-> Lens
Roses
((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a)
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Roses 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 'Forest) structure,
Covariant (->) (->) structure) =>
structure @>>> Substance ('Right 'Forest) structure
sub @(Right Forest) ((<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Roses a)
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
z in
Lens
Exactly
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
a
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> Exactly a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
Exactly
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
a
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> Exactly a)
-> Lens
Exactly
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
a
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) 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 (T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> Exactly a)
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- T_U Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
parent
Exactly a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
-> (<:*:>)
Exactly
(Roses
<:*:> (Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses))))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> ((List :. Construction List) >>> a) -> Roses a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < Primary t a) < t a
unite (((List :. Construction List) >>> a) -> Roses a)
-> ((List :. Construction List) >>> a) -> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (List :. Construction List) >>> a
left_children ((List :. Construction List) >>> a)
-> ((List :. Construction List) >>> a)
-> (List :. Construction List) >>> a
forall a. Semigroup a => a -> a -> a
+ Construction List a -> (List :. Construction List) >>> a
forall (t :: * -> *) a. Pointable t => a -> t a
point (a -> ((List :. Construction List) >>> a) -> Construction List a
forall (t :: * -> *) a.
a -> ((t :. Construction t) >>> a) -> Construction t a
Construct a
child_node (List :. Construction List) >>> a
central_children) ((List :. Construction List) >>> a)
-> ((List :. Construction List) >>> a)
-> (List :. Construction List) >>> a
forall a. Semigroup a => a -> a -> a
+ (List :. Construction List) >>> a
right_children
Roses a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
-> T_U
Covariant
Covariant
(:*:)
Roses
(Reverse Roses <:*:> (Roses <:*:> (List <::> Tape Roses)))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> Lens
(Reverse Roses)
(T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Reverse Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
(Reverse Roses)
(T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Reverse Roses a)
-> Lens
(Reverse Roses)
(T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Reverse Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Left structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Left structure
sub @Left (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Reverse Roses a)
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Reverse Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
(Reverse Roses <:*:> Roses)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
a
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
(Reverse Roses <:*:> Roses)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
a
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
-> Lens
(Reverse Roses <:*:> Roses)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
a
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest (T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- T_U Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
parent
Reverse Roses a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
-> T_U
Covariant
Covariant
(:*:)
(Reverse Roses)
(Roses <:*:> (List <::> Tape Roses))
a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> Lens
Roses (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a -> Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
Roses (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Roses a)
-> Lens
Roses (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
-> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Right structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Right structure
sub @Right (T_U Covariant Covariant (:*:) (Reverse Roses) Roses a -> Roses a)
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a -> Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- Lens
(Reverse Roses <:*:> Roses)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
a
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (i :: * -> *) source target.
Lens i source target -> source -> i target
view (Lens
(Reverse Roses <:*:> Roses)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
a
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
-> Lens
(Reverse Roses <:*:> Roses)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
a
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- forall k (segment :: k) (structure :: * -> *).
(Substructure segment structure, Covariant (->) (->) structure) =>
structure @>>> Substance segment structure
forall (structure :: * -> *).
(Substructure 'Rest structure, Covariant (->) (->) structure) =>
structure @>>> Substance 'Rest structure
sub @Rest (T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a)
-> T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
-> T_U Covariant Covariant (:*:) (Reverse Roses) Roses a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- T_U Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a
parent
Roses a
-> (<::>) List (Tape Roses) a
-> T_U Covariant Covariant (:*:) Roses (List <::> Tape Roses) a
forall k (t :: k -> *) (a :: k) (u :: k -> *).
t a -> u a -> (t <:*:> u) >>>>>> a
<:*:> TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
-> (<::>) List (Tape Roses) a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < Primary t a) < t a
unite TT
Covariant
Covariant
Maybe
(Construction Maybe)
(T_U
Covariant Covariant (:*:) Exactly (Reverse Roses <:*:> Roses) a)
parents