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