{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Structure.Some.Rose where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Category ((.), ($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((<$>)))
import Pandora.Pattern.Functor.Contravariant ((>$<))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
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.Paradigm.Primary.Object.Boolean (Boolean (True, False), (?))
import Pandora.Paradigm.Primary.Functor.Function ((!.), (%))
import Pandora.Paradigm.Primary.Functor.Identity (Identity (Identity))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate), equate)
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached)
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct)
import Pandora.Paradigm.Schemes (TU (TU), T_U (T_U), P_Q_T (P_Q_T), type (<:.>), type (<:.:>))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, (=||$>))
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Structure.Ability.Morphable (Morphable (Morphing, morphing)
	, Morph (Lookup, Vary, Element, Key), premorph, find, vary)
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Available, Substance, substructure), Segment (Root, Tail))
import Pandora.Paradigm.Structure.Modification.Prefixed (Prefixed (Prefixed))
import Pandora.Paradigm.Structure.Some.List (List)

type Rose = Maybe <:.> Construction List

instance Nullable Rose where
	null :: (Predicate :. Rose) := a
null = (Rose a -> Boolean) -> (Predicate :. Rose) := a
forall a. (a -> Boolean) -> Predicate a
Predicate ((Rose a -> Boolean) -> (Predicate :. Rose) := a)
-> (Rose a -> Boolean) -> (Predicate :. Rose) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \case { TU Maybe (Construction List a)
Nothing -> Boolean
True ; Rose a
_ -> Boolean
False }

-- FIXME: If we want to remove root node, we ruin the whole tree
instance Substructure Root Rose where
	type Available Root Rose = Maybe
	type Substance Root Rose = Identity
	substructure :: Lens
  (Available 'Root Rose)
  ((<:.>) (Tagged 'Root) Rose a)
  (Substance 'Root Rose a)
substructure = ((<:.>) (Tagged 'Root) Rose a
 -> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) Rose a))
-> P_Q_T
     (->) Store Maybe ((<:.>) (Tagged 'Root) Rose a) (Identity 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 'Root) Rose a
  -> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) Rose a))
 -> P_Q_T
      (->) Store Maybe ((<:.>) (Tagged 'Root) Rose a) (Identity a))
-> ((<:.>) (Tagged 'Root) Rose a
    -> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) Rose a))
-> P_Q_T
     (->) Store Maybe ((<:.>) (Tagged 'Root) Rose a) (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Root) Rose a
rose -> case TU Covariant Covariant Maybe (Construction List) a
-> (Maybe :. Construction List) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction List) a
 -> (Maybe :. Construction List) := a)
-> TU Covariant Covariant Maybe (Construction List) a
-> (Maybe :. Construction List) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Root) Rose a
-> TU Covariant Covariant Maybe (Construction List) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant_ u (->) (->)) =>
t u ~> u
lower (<:.>) (Tagged 'Root) Rose a
rose of
		(Maybe :. Construction List) := a
Nothing -> (((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
 := (<:.>) (Tagged 'Root) Rose a)
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) Rose a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
  := (<:.>) (Tagged 'Root) Rose a)
 -> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) Rose a))
-> (((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
    := (<:.>) (Tagged 'Root) Rose a)
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) Rose a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Maybe (Identity a)
forall a. Maybe a
Nothing Maybe (Identity a)
-> (Maybe (Identity a) -> (<:.>) (Tagged 'Root) Rose a)
-> ((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
   := (<:.>) (Tagged 'Root) Rose a
forall s a. s -> a -> Product s a
:*: ((Tagged 'Root :. Rose) := a) -> (<:.>) (Tagged 'Root) Rose 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 (((Tagged 'Root :. Rose) := a) -> (<:.>) (Tagged 'Root) Rose a)
-> (Maybe (Identity a) -> (Tagged 'Root :. Rose) := a)
-> Maybe (Identity a)
-> (<:.>) (Tagged 'Root) Rose a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant Maybe (Construction List) a
-> (Tagged 'Root :. Rose) := a
forall k (tag :: k) a. a -> Tagged tag a
Tag (TU Covariant Covariant Maybe (Construction List) a
 -> (Tagged 'Root :. Rose) := a)
-> (Maybe (Identity a)
    -> TU Covariant Covariant Maybe (Construction List) a)
-> Maybe (Identity a)
-> (Tagged 'Root :. Rose) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Maybe :. Construction List) := a)
-> TU Covariant Covariant Maybe (Construction List) 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 (((Maybe :. Construction List) := a)
 -> TU Covariant Covariant Maybe (Construction List) a)
-> (Maybe (Identity a) -> (Maybe :. Construction List) := a)
-> Maybe (Identity a)
-> TU Covariant Covariant Maybe (Construction List) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((a -> ((List :. Construction List) := a) -> Construction List a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((List :. Construction List) := a) -> Construction List a)
-> ((List :. Construction List) := a) -> a -> Construction List a
forall a b c. (a -> b -> c) -> b -> a -> c
% (List :. Construction List) := a
forall (t :: * -> *) a. Avoidable t => t a
empty) (a -> Construction List a)
-> (Identity a -> a) -> Identity a -> Construction List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Identity a -> Construction List a)
-> Maybe (Identity a) -> (Maybe :. Construction List) := a
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
<$>)
		Just Construction List a
nonempty_rose -> (((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
 := (<:.>) (Tagged 'Root) Rose a)
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) Rose a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
  := (<:.>) (Tagged 'Root) Rose a)
 -> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) Rose a))
-> (((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
    := (<:.>) (Tagged 'Root) Rose a)
-> Store (Maybe (Identity a)) ((<:.>) (Tagged 'Root) Rose a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Identity a -> Maybe (Identity a)
forall a. a -> Maybe a
Just (a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a) -> a -> Identity a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction List a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Construction List a
nonempty_rose) Maybe (Identity a)
-> (Maybe (Identity a) -> (<:.>) (Tagged 'Root) Rose a)
-> ((:*:) (Maybe (Identity a)) :. (->) (Maybe (Identity a)))
   := (<:.>) (Tagged 'Root) Rose a
forall s a. s -> a -> Product s a
:*: \case
			Just (Identity a
new) -> TU Covariant Covariant Maybe (Construction List) a
-> (<:.>) (Tagged 'Root) Rose a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction List) a
 -> (<:.>) (Tagged 'Root) Rose a)
-> (((List :. Construction List) := a)
    -> TU Covariant Covariant Maybe (Construction List) a)
-> ((List :. Construction List) := a)
-> (<:.>) (Tagged 'Root) Rose a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. ((Maybe :. Construction List) := a)
-> TU Covariant Covariant Maybe (Construction List) 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 (((Maybe :. Construction List) := a)
 -> TU Covariant Covariant Maybe (Construction List) a)
-> (((List :. Construction List) := a)
    -> (Maybe :. Construction List) := a)
-> ((List :. Construction List) := a)
-> TU Covariant Covariant Maybe (Construction List) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction List a -> (Maybe :. Construction List) := a
forall a. a -> Maybe a
Just (Construction List a -> (Maybe :. Construction List) := a)
-> (((List :. Construction List) := a) -> Construction List a)
-> ((List :. Construction List) := a)
-> (Maybe :. Construction List) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((List :. Construction List) := a) -> Construction List a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
new (((List :. Construction List) := a)
 -> (<:.>) (Tagged 'Root) Rose a)
-> ((List :. Construction List) := a)
-> (<:.>) (Tagged 'Root) Rose a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction List a -> (List :. Construction List) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction List a
nonempty_rose
			Maybe (Identity a)
Nothing -> TU Covariant Covariant Maybe (Construction List) a
-> (<:.>) (Tagged 'Root) Rose a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift TU Covariant Covariant Maybe (Construction List) a
forall (t :: * -> *) a. Avoidable t => t a
empty

instance Substructure Just Rose where
	type Available Just Rose = Identity
	type Substance Just Rose = List <:.> Construction List
	substructure :: Lens
  (Available 'Just Rose)
  ((<:.>) (Tagged 'Just) Rose a)
  (Substance 'Just Rose a)
substructure = ((<:.>) (Tagged 'Just) Rose a
 -> Store
      (Identity (TU Covariant Covariant List (Construction List) a))
      ((<:.>) (Tagged 'Just) Rose a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Just) Rose a)
     (TU Covariant Covariant List (Construction List) 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 'Just) Rose a
  -> Store
       (Identity (TU Covariant Covariant List (Construction List) a))
       ((<:.>) (Tagged 'Just) Rose a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Just) Rose a)
      (TU Covariant Covariant List (Construction List) a))
-> ((<:.>) (Tagged 'Just) Rose a
    -> Store
         (Identity (TU Covariant Covariant List (Construction List) a))
         ((<:.>) (Tagged 'Just) Rose a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Just) Rose a)
     (TU Covariant Covariant List (Construction List) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Just) Rose a
rose -> case TU Covariant Covariant Maybe (Construction List) a
-> (Maybe :. Construction List) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction List) a
 -> (Maybe :. Construction List) := a)
-> ((<:.>) (Tagged 'Just) Rose a
    -> TU Covariant Covariant Maybe (Construction List) a)
-> (<:.>) (Tagged 'Just) Rose a
-> (Maybe :. Construction List) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Just (TU Covariant Covariant Maybe (Construction List) a)
-> TU Covariant Covariant Maybe (Construction List) a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Tagged 'Just (TU Covariant Covariant Maybe (Construction List) a)
 -> TU Covariant Covariant Maybe (Construction List) a)
-> ((<:.>) (Tagged 'Just) Rose a
    -> Tagged
         'Just (TU Covariant Covariant Maybe (Construction List) a))
-> (<:.>) (Tagged 'Just) Rose a
-> TU Covariant Covariant Maybe (Construction List) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Just) Rose a
-> Tagged
     'Just (TU Covariant Covariant Maybe (Construction List) a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run ((<:.>) (Tagged 'Just) Rose a -> (Maybe :. Construction List) := a)
-> (<:.>) (Tagged 'Just) Rose a
-> (Maybe :. Construction List) := a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Just) Rose a
rose of
		(Maybe :. Construction List) := a
Nothing -> (((:*:)
    (Identity (TU Covariant Covariant List (Construction List) a))
  :. (->)
       (Identity (TU Covariant Covariant List (Construction List) a)))
 := (<:.>) (Tagged 'Just) Rose a)
-> Store
     (Identity (TU Covariant Covariant List (Construction List) a))
     ((<:.>) (Tagged 'Just) Rose a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:)
     (Identity (TU Covariant Covariant List (Construction List) a))
   :. (->)
        (Identity (TU Covariant Covariant List (Construction List) a)))
  := (<:.>) (Tagged 'Just) Rose a)
 -> Store
      (Identity (TU Covariant Covariant List (Construction List) a))
      ((<:.>) (Tagged 'Just) Rose a))
-> (((:*:)
       (Identity (TU Covariant Covariant List (Construction List) a))
     :. (->)
          (Identity (TU Covariant Covariant List (Construction List) a)))
    := (<:.>) (Tagged 'Just) Rose a)
-> Store
     (Identity (TU Covariant Covariant List (Construction List) a))
     ((<:.>) (Tagged 'Just) Rose a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant List (Construction List) a
-> Identity (TU Covariant Covariant List (Construction List) a)
forall a. a -> Identity a
Identity TU Covariant Covariant List (Construction List) a
forall (t :: * -> *) a. Avoidable t => t a
empty Identity (TU Covariant Covariant List (Construction List) a)
-> (Identity (TU Covariant Covariant List (Construction List) a)
    -> (<:.>) (Tagged 'Just) Rose a)
-> ((:*:)
      (Identity (TU Covariant Covariant List (Construction List) a))
    :. (->)
         (Identity (TU Covariant Covariant List (Construction List) a)))
   := (<:.>) (Tagged 'Just) Rose a
forall s a. s -> a -> Product s a
:*: (TU Covariant Covariant Maybe (Construction List) a
-> (<:.>) (Tagged 'Just) Rose a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift TU Covariant Covariant Maybe (Construction List) a
forall (t :: * -> *) a. Avoidable t => t a
empty (<:.>) (Tagged 'Just) Rose a
-> Identity (TU Covariant Covariant List (Construction List) a)
-> (<:.>) (Tagged 'Just) Rose a
forall a b. a -> b -> a
!.)
		Just (Construct a
x (List :. Construction List) := a
xs) -> (((:*:)
    (Identity (TU Covariant Covariant List (Construction List) a))
  :. (->)
       (Identity (TU Covariant Covariant List (Construction List) a)))
 := (<:.>) (Tagged 'Just) Rose a)
-> Store
     (Identity (TU Covariant Covariant List (Construction List) a))
     ((<:.>) (Tagged 'Just) Rose a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:)
     (Identity (TU Covariant Covariant List (Construction List) a))
   :. (->)
        (Identity (TU Covariant Covariant List (Construction List) a)))
  := (<:.>) (Tagged 'Just) Rose a)
 -> Store
      (Identity (TU Covariant Covariant List (Construction List) a))
      ((<:.>) (Tagged 'Just) Rose a))
-> (((:*:)
       (Identity (TU Covariant Covariant List (Construction List) a))
     :. (->)
          (Identity (TU Covariant Covariant List (Construction List) a)))
    := (<:.>) (Tagged 'Just) Rose a)
-> Store
     (Identity (TU Covariant Covariant List (Construction List) a))
     ((<:.>) (Tagged 'Just) Rose a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant List (Construction List) a
-> Identity (TU Covariant Covariant List (Construction List) a)
forall a. a -> Identity a
Identity (((List :. Construction List) := a)
-> TU Covariant Covariant List (Construction List) 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 (List :. Construction List) := a
xs) Identity (TU Covariant Covariant List (Construction List) a)
-> (Identity (TU Covariant Covariant List (Construction List) a)
    -> (<:.>) (Tagged 'Just) Rose a)
-> ((:*:)
      (Identity (TU Covariant Covariant List (Construction List) a))
    :. (->)
         (Identity (TU Covariant Covariant List (Construction List) a)))
   := (<:.>) (Tagged 'Just) Rose a
forall s a. s -> a -> Product s a
:*: TU Covariant Covariant Maybe (Construction List) a
-> (<:.>) (Tagged 'Just) Rose a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (TU Covariant Covariant Maybe (Construction List) a
 -> (<:.>) (Tagged 'Just) Rose a)
-> (Identity (TU Covariant Covariant List (Construction List) a)
    -> TU Covariant Covariant Maybe (Construction List) a)
-> Identity (TU Covariant Covariant List (Construction List) a)
-> (<:.>) (Tagged 'Just) Rose a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction List a
-> TU Covariant Covariant Maybe (Construction List) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Construction List a
 -> TU Covariant Covariant Maybe (Construction List) a)
-> (Identity (TU Covariant Covariant List (Construction List) a)
    -> Construction List a)
-> Identity (TU Covariant Covariant List (Construction List) a)
-> TU Covariant Covariant Maybe (Construction List) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((List :. Construction List) := a) -> Construction List a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((List :. Construction List) := a) -> Construction List a)
-> (Identity (TU Covariant Covariant List (Construction List) a)
    -> (List :. Construction List) := a)
-> Identity (TU Covariant Covariant List (Construction List) a)
-> Construction List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant List (Construction List) a
-> (List :. Construction List) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant List (Construction List) a
 -> (List :. Construction List) := a)
-> (Identity (TU Covariant Covariant List (Construction List) a)
    -> TU Covariant Covariant List (Construction List) a)
-> Identity (TU Covariant Covariant List (Construction List) a)
-> (List :. Construction List) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (TU Covariant Covariant List (Construction List) a)
-> TU Covariant Covariant List (Construction List) a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

--------------------------------------- Non-empty rose tree ----------------------------------------

type instance Nonempty Rose = Construction List

instance Substructure Root (Construction List) where
	type Available Root (Construction List) = Identity
	type Substance Root (Construction List) = Identity
	substructure :: Lens
  (Available 'Root (Construction List))
  ((<:.>) (Tagged 'Root) (Construction List) a)
  (Substance 'Root (Construction List) a)
substructure = ((<:.>) (Tagged 'Root) (Construction List) a
 -> Store
      (Identity (Identity a))
      ((<:.>) (Tagged 'Root) (Construction List) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Root) (Construction List) a)
     (Identity 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 'Root) (Construction List) a
  -> Store
       (Identity (Identity a))
       ((<:.>) (Tagged 'Root) (Construction List) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Root) (Construction List) a)
      (Identity a))
-> ((<:.>) (Tagged 'Root) (Construction List) a
    -> Store
         (Identity (Identity a))
         ((<:.>) (Tagged 'Root) (Construction List) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Root) (Construction List) a)
     (Identity a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Root) (Construction List) a
rose -> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
 := (<:.>) (Tagged 'Root) (Construction List) a)
-> Store
     (Identity (Identity a))
     ((<:.>) (Tagged 'Root) (Construction List) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
  := (<:.>) (Tagged 'Root) (Construction List) a)
 -> Store
      (Identity (Identity a))
      ((<:.>) (Tagged 'Root) (Construction List) a))
-> (((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
    := (<:.>) (Tagged 'Root) (Construction List) a)
-> Store
     (Identity (Identity a))
     ((<:.>) (Tagged 'Root) (Construction List) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Identity a -> Identity (Identity a)
forall a. a -> Identity a
Identity (a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a) -> a -> Identity a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction List a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract ((<:.>) (Tagged 'Root) (Construction List) a -> Construction List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant_ u (->) (->)) =>
t u ~> u
lower (<:.>) (Tagged 'Root) (Construction List) a
rose)) Identity (Identity a)
-> (Identity (Identity a)
    -> (<:.>) (Tagged 'Root) (Construction List) a)
-> ((:*:) (Identity (Identity a)) :. (->) (Identity (Identity a)))
   := (<:.>) (Tagged 'Root) (Construction List) a
forall s a. s -> a -> Product s a
:*: Construction List a -> (<:.>) (Tagged 'Root) (Construction List) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Construction List a
 -> (<:.>) (Tagged 'Root) (Construction List) a)
-> (Identity (Identity a) -> Construction List a)
-> Identity (Identity a)
-> (<:.>) (Tagged 'Root) (Construction List) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> ((List :. Construction List) := a) -> Construction List a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((List :. Construction List) := a) -> Construction List a)
-> ((List :. Construction List) := a) -> a -> Construction List a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction List a -> (List :. Construction List) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct ((<:.>) (Tagged 'Root) (Construction List) a -> Construction List a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Lowerable t, Covariant_ u (->) (->)) =>
t u ~> u
lower (<:.>) (Tagged 'Root) (Construction List) a
rose)) (a -> Construction List a)
-> (Identity (Identity a) -> a)
-> Identity (Identity a)
-> Construction List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

instance Substructure Tail (Construction List) where
	type Available Tail (Construction List) = Identity
	type Substance Tail (Construction List) = List <:.> Construction List
	substructure :: Lens
  (Available 'Tail (Construction List))
  ((<:.>) (Tagged 'Tail) (Construction List) a)
  (Substance 'Tail (Construction List) a)
substructure = ((<:.>) (Tagged 'Tail) (Construction List) a
 -> Store
      (Identity (TU Covariant Covariant List (Construction List) a))
      ((<:.>) (Tagged 'Tail) (Construction List) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Tail) (Construction List) a)
     (TU Covariant Covariant List (Construction List) 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 'Tail) (Construction List) a
  -> Store
       (Identity (TU Covariant Covariant List (Construction List) a))
       ((<:.>) (Tagged 'Tail) (Construction List) a))
 -> P_Q_T
      (->)
      Store
      Identity
      ((<:.>) (Tagged 'Tail) (Construction List) a)
      (TU Covariant Covariant List (Construction List) a))
-> ((<:.>) (Tagged 'Tail) (Construction List) a
    -> Store
         (Identity (TU Covariant Covariant List (Construction List) a))
         ((<:.>) (Tagged 'Tail) (Construction List) a))
-> P_Q_T
     (->)
     Store
     Identity
     ((<:.>) (Tagged 'Tail) (Construction List) a)
     (TU Covariant Covariant List (Construction List) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(<:.>) (Tagged 'Tail) (Construction List) a
rose -> case Tagged 'Tail (Construction List a) -> Construction List a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Tagged 'Tail (Construction List a) -> Construction List a)
-> Tagged 'Tail (Construction List a) -> Construction List a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (<:.>) (Tagged 'Tail) (Construction List) a
-> Primary (Tagged 'Tail <:.> Construction List) a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (<:.>) (Tagged 'Tail) (Construction List) a
rose of
		Construct a
x (List :. Construction List) := a
xs -> (((:*:)
    (Identity (TU Covariant Covariant List (Construction List) a))
  :. (->)
       (Identity (TU Covariant Covariant List (Construction List) a)))
 := (<:.>) (Tagged 'Tail) (Construction List) a)
-> Store
     (Identity (TU Covariant Covariant List (Construction List) a))
     ((<:.>) (Tagged 'Tail) (Construction List) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:)
     (Identity (TU Covariant Covariant List (Construction List) a))
   :. (->)
        (Identity (TU Covariant Covariant List (Construction List) a)))
  := (<:.>) (Tagged 'Tail) (Construction List) a)
 -> Store
      (Identity (TU Covariant Covariant List (Construction List) a))
      ((<:.>) (Tagged 'Tail) (Construction List) a))
-> (((:*:)
       (Identity (TU Covariant Covariant List (Construction List) a))
     :. (->)
          (Identity (TU Covariant Covariant List (Construction List) a)))
    := (<:.>) (Tagged 'Tail) (Construction List) a)
-> Store
     (Identity (TU Covariant Covariant List (Construction List) a))
     ((<:.>) (Tagged 'Tail) (Construction List) a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ TU Covariant Covariant List (Construction List) a
-> Identity (TU Covariant Covariant List (Construction List) a)
forall a. a -> Identity a
Identity (((List :. Construction List) := a)
-> TU Covariant Covariant List (Construction List) 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 (List :. Construction List) := a
xs) Identity (TU Covariant Covariant List (Construction List) a)
-> (Identity (TU Covariant Covariant List (Construction List) a)
    -> (<:.>) (Tagged 'Tail) (Construction List) a)
-> ((:*:)
      (Identity (TU Covariant Covariant List (Construction List) a))
    :. (->)
         (Identity (TU Covariant Covariant List (Construction List) a)))
   := (<:.>) (Tagged 'Tail) (Construction List) a
forall s a. s -> a -> Product s a
:*: Construction List a -> (<:.>) (Tagged 'Tail) (Construction List) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Construction List a
 -> (<:.>) (Tagged 'Tail) (Construction List) a)
-> (Identity (TU Covariant Covariant List (Construction List) a)
    -> Construction List a)
-> Identity (TU Covariant Covariant List (Construction List) a)
-> (<:.>) (Tagged 'Tail) (Construction List) a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((List :. Construction List) := a) -> Construction List a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct a
x (((List :. Construction List) := a) -> Construction List a)
-> (Identity (TU Covariant Covariant List (Construction List) a)
    -> (List :. Construction List) := a)
-> Identity (TU Covariant Covariant List (Construction List) a)
-> Construction List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. TU Covariant Covariant List (Construction List) a
-> (List :. Construction List) := a
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant List (Construction List) a
 -> (List :. Construction List) := a)
-> (Identity (TU Covariant Covariant List (Construction List) a)
    -> TU Covariant Covariant List (Construction List) a)
-> Identity (TU Covariant Covariant List (Construction List) a)
-> (List :. Construction List) := a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Identity (TU Covariant Covariant List (Construction List) a)
-> TU Covariant Covariant List (Construction List) a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract

--------------------------------------- Prefixed rose tree -----------------------------------------

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 (Prefixed Rose k a
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed Rose k a
 -> TU Covariant Covariant Maybe (Construction List) (Product k a))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
    -> Prefixed Rose k a)
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
-> Prefixed Rose k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> TU Maybe (Construction List (Product 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)
$ \Construction Maybe k
_ -> Maybe a
forall a. Maybe a
Nothing
	morphing (Prefixed Rose k a
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed Rose k a
 -> TU Covariant Covariant Maybe (Construction List) (Product k a))
-> ((<:.>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
    -> Prefixed Rose k a)
-> (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
-> Prefixed Rose k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> TU (Just Construction List (Product 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 (Product 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 (Product k a) -> Maybe a)
-> Construction List (Product k a)
-> ((->) (Construction Maybe k) :. Maybe) := a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction List (Product k a)
tree

-- TODO: Ineffiecient - we iterate over all branches in subtree, but we need to short-circuit on the first matching part of
instance Setoid k => Morphable (Vary Element) (Prefixed Rose k) where
	type Morphing (Vary Element) (Prefixed Rose k) = (Product (Nonempty List k) <:.> Identity) <:.:> Prefixed Rose k := (->)
	morphing :: (<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
-> Morphing ('Vary 'Element) (Prefixed Rose k) a
morphing (TU Covariant Covariant Maybe (Construction List) (Product k a)
-> Maybe (Construction List (Product k a))
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction List) (Product k a)
 -> Maybe (Construction List (Product k a)))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
    -> TU Covariant Covariant Maybe (Construction List) (Product k a))
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
-> Maybe (Construction List (Product k a))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Prefixed Rose k a
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed Rose k a
 -> TU Covariant Covariant Maybe (Construction List) (Product k a))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
    -> Prefixed Rose k a)
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
-> Prefixed Rose k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Maybe (Construction List (Product k a))
Nothing) = (TU Covariant Covariant (Product (Construction Maybe k)) Identity a
 -> Prefixed Rose k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
     (Prefixed Rose k)
     a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((TU
    Covariant Covariant (Product (Construction Maybe k)) Identity a
  -> Prefixed Rose k a)
 -> T_U
      Covariant
      Covariant
      (->)
      (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
      (Prefixed Rose k)
      a)
-> (TU
      Covariant Covariant (Product (Construction Maybe k)) Identity a
    -> Prefixed Rose k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
     (Prefixed Rose k)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(TU (Construct k
key (Maybe :. Construction Maybe) := k
_ :*: Identity a
value)) -> TU Covariant Covariant Maybe (Construction List) (Product k a)
-> Prefixed Rose k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (TU Covariant Covariant Maybe (Construction List) (Product k a)
 -> Prefixed Rose k a)
-> (Construction List (Product k a)
    -> TU Covariant Covariant Maybe (Construction List) (Product k a))
-> Construction List (Product k a)
-> Prefixed Rose k a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction List (Product k a)
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Construction List (Product k a) -> Prefixed Rose k a)
-> Construction List (Product k a) -> Prefixed Rose k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Product k a
-> ((List :. Construction List) := Product k a)
-> Construction List (Product k a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (k
key k -> a -> Product k a
forall s a. s -> a -> Product s a
:*: a
value) (List :. Construction List) := Product k a
forall (t :: * -> *) a. Avoidable t => t a
empty
	morphing (TU Covariant Covariant Maybe (Construction List) (Product k a)
-> Maybe (Construction List (Product k a))
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (TU Covariant Covariant Maybe (Construction List) (Product k a)
 -> Maybe (Construction List (Product k a)))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
    -> TU Covariant Covariant Maybe (Construction List) (Product k a))
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
-> Maybe (Construction List (Product k a))
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Prefixed Rose k a
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed Rose k a
 -> TU Covariant Covariant Maybe (Construction List) (Product k a))
-> ((<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
    -> Prefixed Rose k a)
-> (<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Vary 'Element)) (Prefixed Rose k) a
-> Prefixed Rose k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Just (Construct Product k a
focused (List :. Construction List) := Product k a
subtree)) = (TU Covariant Covariant (Product (Construction Maybe k)) Identity a
 -> Prefixed Rose k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
     (Prefixed Rose k)
     a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((TU
    Covariant Covariant (Product (Construction Maybe k)) Identity a
  -> Prefixed Rose k a)
 -> T_U
      Covariant
      Covariant
      (->)
      (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
      (Prefixed Rose k)
      a)
-> (TU
      Covariant Covariant (Product (Construction Maybe k)) Identity a
    -> Prefixed Rose k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
     (Prefixed Rose k)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(TU (Construction Maybe k
breadcrumbs :*: Identity a
value)) -> case Construction Maybe k
breadcrumbs of
		Construct k
key (Maybe :. Construction Maybe) := k
Nothing -> TU Covariant Covariant Maybe (Construction List) (Product k a)
-> Prefixed Rose k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (TU Covariant Covariant Maybe (Construction List) (Product k a)
 -> Prefixed Rose k a)
-> (Construction List (Product k a)
    -> TU Covariant Covariant Maybe (Construction List) (Product k a))
-> Construction List (Product k a)
-> Prefixed Rose k a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction List (Product k a)
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Construction List (Product k a) -> Prefixed Rose k a)
-> Construction List (Product k a) -> Prefixed Rose k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Product k a -> k
forall a b. (a :*: b) -> a
attached Product k a
focused k -> k -> Boolean
forall a. Setoid a => a -> a -> Boolean
== k
key Boolean
-> Construction List (Product k a)
-> Construction List (Product k a)
-> Construction List (Product k a)
forall a. Boolean -> a -> a -> a
? Product k a
-> ((List :. Construction List) := Product k a)
-> Construction List (Product k a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (k
key k -> a -> Product k a
forall s a. s -> a -> Product s a
:*: a
value) (List :. Construction List) := Product k a
subtree (Construction List (Product k a)
 -> Construction List (Product k a))
-> Construction List (Product k a)
-> Construction List (Product k a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Product k a
-> ((List :. Construction List) := Product k a)
-> Construction List (Product k a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct Product k a
focused (List :. Construction List) := Product k a
subtree
		Construct k
key (Just Construction Maybe k
keys) -> TU Covariant Covariant Maybe (Construction List) (Product k a)
-> Prefixed Rose k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (TU Covariant Covariant Maybe (Construction List) (Product k a)
 -> Prefixed Rose k a)
-> (Construction List (Product k a)
    -> TU Covariant Covariant Maybe (Construction List) (Product k a))
-> Construction List (Product k a)
-> Prefixed Rose k a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction List (Product k a)
-> TU Covariant Covariant Maybe (Construction List) (Product k a)
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Construction List (Product k a) -> Prefixed Rose k a)
-> Construction List (Product k a) -> Prefixed Rose k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Product k a -> k
forall a b. (a :*: b) -> a
attached Product k a
focused k -> k -> Boolean
forall a. Setoid a => a -> a -> Boolean
!= k
key Boolean
-> Construction List (Product k a)
-> Construction List (Product k a)
-> Construction List (Product k a)
forall a. Boolean -> a -> a -> a
? Product k a
-> ((List :. Construction List) := Product k a)
-> Construction List (Product k a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct Product k a
focused (List :. Construction List) := Product k a
subtree
			(Construction List (Product k a)
 -> Construction List (Product k a))
-> Construction List (Product k a)
-> Construction List (Product k a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Product k a
-> ((List :. Construction List) := Product k a)
-> Construction List (Product k a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct Product k a
focused (((List :. Construction List) := Product k a)
 -> Construction List (Product k a))
-> ((List :. Construction List) := Product k a)
-> Construction List (Product k a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Maybe k
-> a
-> Nonempty (Prefixed Rose k) a
-> Nonempty (Prefixed Rose k) a
forall a (mod :: a) key value (struct :: * -> *).
Morphed
  ('Vary mod)
  struct
  (((Product key <:.> Identity) <:.:> struct) := (->)) =>
key -> value -> struct value -> struct value
vary @Element @_ @_ @(Nonempty (Prefixed Rose k)) Construction Maybe k
keys a
value (Prefixed (Construction List) k a
 -> Prefixed (Construction List) k a)
-> (List := Primary (Prefixed (Construction List) k) a)
-> List := Primary (Prefixed (Construction List) k) a
forall (t :: * -> *) (j :: * -> *) (u :: * -> *) a b.
(Interpreted t, Covariant j, Interpreted u) =>
(t a -> u b) -> (j := Primary t a) -> j := Primary u b
=||$> List := Primary (Prefixed (Construction List) k) a
(List :. Construction List) := Product k a
subtree

---------------------------------- Non-empty prefixed rose tree ------------------------------------

-- TODO: Ineffiecient - we iterate over all branches in subtree, but we need to short-circuit on the first matching part of
instance Setoid k => Morphable (Vary Element) (Prefixed (Construction List) k) where
	type Morphing (Vary Element) (Prefixed (Construction List) k) =
		(Product (Nonempty List k) <:.> Identity) <:.:> Prefixed (Construction List) k := (->)
	morphing :: (<:.>) (Tagged ('Vary 'Element)) (Prefixed (Construction List) k) a
-> Morphing ('Vary 'Element) (Prefixed (Construction List) k) a
morphing (Prefixed (Construction List) k a -> Construction List (k :*: a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed (Construction List) k a -> Construction List (k :*: a))
-> ((<:.>)
      (Tagged ('Vary 'Element)) (Prefixed (Construction List) k) a
    -> Prefixed (Construction List) k a)
-> (<:.>)
     (Tagged ('Vary 'Element)) (Prefixed (Construction List) k) a
-> Construction List (k :*: a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Vary 'Element)) (Prefixed (Construction List) k) a
-> Prefixed (Construction List) k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct k :*: a
x (TU Maybe (Construction Maybe (Construction List (k :*: a)))
Nothing)) = (TU Covariant Covariant (Product (Construction Maybe k)) Identity a
 -> Prefixed (Construction List) k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
     (Prefixed (Construction List) k)
     a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((TU
    Covariant Covariant (Product (Construction Maybe k)) Identity a
  -> Prefixed (Construction List) k a)
 -> T_U
      Covariant
      Covariant
      (->)
      (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
      (Prefixed (Construction List) k)
      a)
-> (TU
      Covariant Covariant (Product (Construction Maybe k)) Identity a
    -> Prefixed (Construction List) k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
     (Prefixed (Construction List) k)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(TU (Construction Maybe k
breadcrumbs :*: Identity a
value)) -> case Construction Maybe k
breadcrumbs of
		Construct k
key Maybe (Construction Maybe k)
Nothing -> Construction List (k :*: a) -> Prefixed (Construction List) k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (Construction List (k :*: a) -> Prefixed (Construction List) k a)
-> Construction List (k :*: a) -> Prefixed (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
x k -> k -> Boolean
forall a. Setoid a => a -> a -> Boolean
== k
key Boolean
-> Construction List (k :*: a)
-> Construction List (k :*: a)
-> Construction List (k :*: a)
forall a. Boolean -> a -> a -> a
? (k :*: a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (k
key k -> a -> k :*: a
forall s a. s -> a -> Product s a
:*: a
value) TU
  Covariant
  Covariant
  Maybe
  (Construction Maybe)
  (Construction List (k :*: a))
forall (t :: * -> *) a. Avoidable t => t a
empty (Construction List (k :*: a) -> Construction List (k :*: a))
-> Construction List (k :*: a) -> Construction List (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (k :*: a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct k :*: a
x TU
  Covariant
  Covariant
  Maybe
  (Construction Maybe)
  (Construction List (k :*: a))
forall (t :: * -> *) a. Avoidable t => t a
empty
		Construct k
_ (Just Construction Maybe k
_) -> Construction List (k :*: a) -> Prefixed (Construction List) k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (Construction List (k :*: a) -> Prefixed (Construction List) k a)
-> Construction List (k :*: a) -> Prefixed (Construction List) k a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (k :*: a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct k :*: a
x (Maybe (Construction Maybe (Construction List (k :*: a)))
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: 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 Maybe (Construction Maybe (Construction List (k :*: a)))
forall a. Maybe a
Nothing)
	morphing (Prefixed (Construction List) k a -> Construction List (k :*: a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Prefixed (Construction List) k a -> Construction List (k :*: a))
-> ((<:.>)
      (Tagged ('Vary 'Element)) (Prefixed (Construction List) k) a
    -> Prefixed (Construction List) k a)
-> (<:.>)
     (Tagged ('Vary 'Element)) (Prefixed (Construction List) k) a
-> Construction List (k :*: a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged ('Vary 'Element)) (Prefixed (Construction List) k) a
-> Prefixed (Construction List) k a
forall k (mod :: k) (struct :: * -> *).
Morphable mod struct =>
(Tagged mod <:.> struct) ~> struct
premorph -> Construct k :*: a
x (TU (Just Construction Maybe (Construction List (k :*: a))
subtree))) = (TU Covariant Covariant (Product (Construction Maybe k)) Identity a
 -> Prefixed (Construction List) k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
     (Prefixed (Construction List) k)
     a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((TU
    Covariant Covariant (Product (Construction Maybe k)) Identity a
  -> Prefixed (Construction List) k a)
 -> T_U
      Covariant
      Covariant
      (->)
      (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
      (Prefixed (Construction List) k)
      a)
-> (TU
      Covariant Covariant (Product (Construction Maybe k)) Identity a
    -> Prefixed (Construction List) k a)
-> T_U
     Covariant
     Covariant
     (->)
     (TU Covariant Covariant (Product (Construction Maybe k)) Identity)
     (Prefixed (Construction List) k)
     a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ \(TU (Construction Maybe k
breadcrumbs :*: Identity a
value)) -> case Construction Maybe k
breadcrumbs of
		Construct k
key Maybe (Construction Maybe k)
Nothing -> Construction List (k :*: a) -> Prefixed (Construction List) k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (Construction List (k :*: a) -> Prefixed (Construction List) k a)
-> Construction List (k :*: a) -> Prefixed (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
x k -> k -> Boolean
forall a. Setoid a => a -> a -> Boolean
!= k
key Boolean
-> Construction List (k :*: a)
-> Construction List (k :*: a)
-> Construction List (k :*: a)
forall a. Boolean -> a -> a -> a
? (k :*: a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct k :*: a
x (TU
   Covariant
   Covariant
   Maybe
   (Construction Maybe)
   (Construction List (k :*: a))
 -> Construction List (k :*: a))
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Maybe (Construction List (k :*: a))
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift Construction Maybe (Construction List (k :*: a))
subtree
			(Construction List (k :*: a) -> Construction List (k :*: a))
-> Construction List (k :*: a) -> Construction List (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (k :*: a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (k
key k -> a -> k :*: a
forall s a. s -> a -> Product s a
:*: a
value) (Construction Maybe (Construction List (k :*: a))
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift Construction Maybe (Construction List (k :*: a))
subtree)
		Construct k
key (Just Construction Maybe k
keys) -> Construction List (k :*: a) -> Prefixed (Construction List) k a
forall (t :: * -> *) k a. ((t :. Product k) := a) -> Prefixed t k a
Prefixed (Construction List (k :*: a) -> Prefixed (Construction List) k a)
-> Construction List (k :*: a) -> Prefixed (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
x k -> k -> Boolean
forall a. Setoid a => a -> a -> Boolean
!= k
key Boolean
-> Construction List (k :*: a)
-> Construction List (k :*: a)
-> Construction List (k :*: a)
forall a. Boolean -> a -> a -> a
? (k :*: a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct k :*: a
x (TU
   Covariant
   Covariant
   Maybe
   (Construction Maybe)
   (Construction List (k :*: a))
 -> Construction List (k :*: a))
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# Construction Maybe (Construction List (k :*: a))
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift Construction Maybe (Construction List (k :*: a))
subtree
			(Construction List (k :*: a) -> Construction List (k :*: a))
-> Construction List (k :*: a) -> Construction List (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (k :*: a)
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (k
key k -> a -> k :*: a
forall s a. s -> a -> Product s a
:*: a
value) (TU
   Covariant
   Covariant
   Maybe
   (Construction Maybe)
   (Construction List (k :*: a))
 -> Construction List (k :*: a))
-> (Construction Maybe (Construction List (k :*: a))
    -> TU
         Covariant
         Covariant
         Maybe
         (Construction Maybe)
         (Construction List (k :*: a)))
-> Construction Maybe (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Construction Maybe (Construction List (k :*: a))
-> TU
     Covariant
     Covariant
     Maybe
     (Construction Maybe)
     (Construction List (k :*: a))
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant_ u (->) (->)) =>
u ~> t u
lift (Construction Maybe (Construction List (k :*: a))
 -> Construction List (k :*: a))
-> Construction Maybe (Construction List (k :*: a))
-> Construction List (k :*: a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ Construction Maybe k
-> a
-> Nonempty (Prefixed Rose k) a
-> Nonempty (Prefixed Rose k) a
forall a (mod :: a) key value (struct :: * -> *).
Morphed
  ('Vary mod)
  struct
  (((Product key <:.> Identity) <:.:> struct) := (->)) =>
key -> value -> struct value -> struct value
vary @Element @_ @_ @(Nonempty (Prefixed Rose k)) Construction Maybe k
keys a
value (Prefixed (Construction List) k a
 -> Prefixed (Construction List) k a)
-> (Construction Maybe
    := Primary (Prefixed (Construction List) k) a)
-> Construction Maybe := Primary (Prefixed (Construction List) k) a
forall (t :: * -> *) (j :: * -> *) (u :: * -> *) a b.
(Interpreted t, Covariant j, Interpreted u) =>
(t a -> u b) -> (j := Primary t a) -> j := Primary u b
=||$> Construction Maybe := Primary (Prefixed (Construction List) k) a
Construction Maybe (Construction List (k :*: a))
subtree

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 Nothing) Nonempty Rose := (k :*: a)
tree = k
k k -> k -> Boolean
forall a. Setoid a => a -> a -> Boolean
== (k :*: a) -> k
forall a b. (a :*: b) -> a
attached (Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Nonempty Rose := (k :*: a)
Construction List (k :*: a)
tree) Boolean -> Maybe a -> Maybe a -> Maybe a
forall a. Boolean -> a -> a -> a
? a -> Maybe a
forall a. a -> Maybe a
Just ((k :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (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 :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (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
find_rose_sub_tree (Construct k (Just ks)) Nonempty Rose := (k :*: a)
tree = k
k k -> k -> Boolean
forall a. Setoid a => a -> a -> Boolean
!= (k :*: a) -> k
forall a b. (a :*: b) -> a
attached (Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Nonempty Rose := (k :*: a)
Construction List (k :*: a)
tree) Boolean -> Maybe a -> Maybe a -> Maybe a
forall a. Boolean -> a -> a -> a
? Maybe a
forall a. Maybe a
Nothing (Maybe a -> Maybe a) -> Maybe a -> Maybe a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (Maybe :. Nonempty Rose) := (k :*: a)
Maybe (Construction List (k :*: a))
subtree Maybe (Construction List (k :*: a))
-> (Construction List (k :*: a) -> Maybe a) -> Maybe a
forall (t :: * -> *) a b. Bindable t => t a -> (a -> t b) -> t b
>>= 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
ks where

	subtree :: Maybe :. Nonempty Rose := k :*: a
	subtree :: (Maybe :. Nonempty Rose) := (k :*: a)
subtree = 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.
Category m =>
m b c -> m a b -> m a c
. Construction List (k :*: a) -> k :*: a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract (Construction List (k :*: a) -> k)
-> Predicate k -> Predicate (Construction List (k :*: a))
forall (t :: * -> *) a b. Contravariant t => (a -> b) -> t b -> t a
>$< k :=> Predicate
forall a. Setoid a => a :=> Predicate
equate (Construction Maybe k -> k
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract Construction Maybe k
ks) (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