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

module Pandora.Paradigm.Structure.Some.Rose where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category (($), (#))
import Pandora.Pattern.Functor.Contravariant ((>-|-))
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.Algebraic.Product ((:*:) ((:*:)), attached)
import Pandora.Paradigm.Primary.Algebraic.Exponential ((%))
import Pandora.Paradigm.Primary.Algebraic (extract)
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.Transformer.Construction (Construction (Construct), deconstruct)
import Pandora.Paradigm.Schemes (TU (TU), P_Q_T (P_Q_T), 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, Element, Key), premorph, find)
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)
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 = P_Q_T $ \rose -> case run # lower rose of
--		Nothing -> Store $ Nothing :*: TU . Tag . TU . ((Construct % empty) . extract <-|-)
--		Just nonempty_rose -> Store $ Just (Identity # extract nonempty_rose) :*: \case
--			Just (Identity new) -> lift . TU . Just . Construct new $ deconstruct nonempty_rose
--			Nothing -> lift empty

--instance Substructure Just Rose where
--	type Available Just Rose = Identity
--	type Substance Just Rose = List <:.> Construction List
--	substructure = P_Q_T $ \rose -> case run . extract . run # rose of
--		Nothing -> Store $ Identity empty :*: (lift empty !.)
--		Just (Construct x xs) -> Store $ Identity (TU xs) :*: lift . lift . Construct x . run . 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 :: * -> *) a. Extractable t => t a -> a
extract ((<:.>) (Tagged 'Root) (Construction List) a -> Construction List a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
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 -> s :*: a
:*: Construction List a -> (<:.>) (Tagged 'Root) (Construction List) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
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.
Semigroupoid 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 (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Lowerable cat t, Covariant cat cat u) =>
cat (t u a) (u a)
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.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Identity a -> a)
-> (Identity (Identity a) -> Identity a)
-> Identity (Identity a)
-> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Identity (Identity a) -> Identity a
forall (t :: * -> *) a. Extractable t => 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 :: * -> *) a. Extractable t => 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
-> Tagged 'Tail (Construction List a)
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (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 -> s :*: a
:*: Construction List a -> (<:.>) (Tagged 'Tail) (Construction List) a
forall (cat :: * -> * -> *) (t :: (* -> *) -> * -> *) (u :: * -> *)
       a.
(Liftable cat t, Covariant cat cat u) =>
cat (u a) (t u a)
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.
Semigroupoid 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.
Semigroupoid m =>
m b c -> m a b -> m a c
. TU Covariant Covariant List (Construction List) a
-> (List :. Construction List) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (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.
Semigroupoid 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 :: * -> *) a. Extractable t => 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 (<:.>) (Tagged ('Lookup 'Key)) (Prefixed Rose k) a
prefixed_rose_tree = case Prefixed Rose k a -> (Rose :. (:*:) k) := a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
run (Prefixed Rose k a -> (Rose :. (:*:) k) := a)
-> Prefixed 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
-> Prefixed 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)
$ \Construction Maybe k
_ -> 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

-- 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) = ((:*:) (Nonempty List k) <:.> Identity) <:.:> Prefixed Rose k := (->)
--	morphing (run . run . premorph -> Nothing) = T_U $ \(TU (Construct key _ :*: Identity value)) -> Prefixed . lift $ Construct (key :*: value) empty
--	morphing (run . run . premorph -> Just (Construct focused subtree)) = T_U $ \(TU (breadcrumbs :*: Identity value)) -> case breadcrumbs of
--		Construct key Nothing -> Prefixed . lift $ attached focused == key ? Construct (key :*: value) subtree $ Construct focused subtree
--		Construct key (Just keys) -> Prefixed . lift $ attached focused != key ? Construct focused subtree
--			$ Construct focused $ vary @Element @_ @_ @(Nonempty (Prefixed Rose k)) keys value =||$> 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) =
--		((:*:) (Nonempty List k) <:.> Identity) <:.:> Prefixed (Construction List) k := (->)
--	morphing (run . premorph -> Construct x (TU Nothing)) = T_U $ \(TU (breadcrumbs :*: Identity value)) -> case breadcrumbs of
--		Construct key Nothing -> Prefixed $ attached x == key ? Construct (key :*: value) empty $ Construct x empty
--		Construct _ (Just _) -> Prefixed $ Construct x (TU Nothing)
--	morphing (run . premorph -> Construct x (TU (Just subtree))) = T_U $ \(TU (breadcrumbs :*: Identity value)) -> case breadcrumbs of
--		Construct key Nothing -> Prefixed $ attached x != key ? Construct x # lift subtree
--			$ Construct (key :*: value) (lift subtree)
--		Construct key (Just keys) -> Prefixed $ attached x != key ? Construct x # lift subtree
--			$ Construct (key :*: value) . lift $ vary @Element @_ @_ @(Nonempty (Prefixed Rose k)) keys value =||$> 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 :: * -> *) a. Extractable t => 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 :: * -> *) 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
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 :: * -> *) a. Extractable t => 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)
$ 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 (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)
=<< (Maybe :. Nonempty Rose) := (k :*: a)
Maybe (Construction List (k :*: a))
subtree 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.
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 (Construction Maybe k -> k
forall (t :: * -> *) a. Extractable t => 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