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

module Pandora.Paradigm.Structure.Some.Rose where

import Pandora.Pattern.Category ((.), ($))
import Pandora.Pattern.Functor.Covariant (Covariant (comap))
import Pandora.Pattern.Functor.Extractable (extract)
import Pandora.Pattern.Functor.Avoidable (Avoidable (empty))
import Pandora.Pattern.Transformer.Liftable (lift)
import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False))
import Pandora.Paradigm.Primary.Functor.Function ((!), (%))
import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just, Nothing))
import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate))
import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)))
import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag))
import Pandora.Paradigm.Primary.Transformer.Construction (Construction (Construct), deconstruct)
import Pandora.Paradigm.Schemes.TU (TU (TU), type (<:.>))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (run)
import Pandora.Paradigm.Inventory.Store (Store (Store))
import Pandora.Paradigm.Structure.Ability.Focusable (Focusable (Focusing, focusing), Location (Root))
import Pandora.Paradigm.Structure.Ability.Monotonic (resolve)
import Pandora.Paradigm.Structure.Ability.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Nullable (Nullable (null))
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substructural, substructure))
import Pandora.Paradigm.Structure.Some.List (List)

type Rose = Maybe <:.> Construction List

instance Focusable Root Rose where
	type Focusing Root Rose a = Maybe a
	focusing :: Tagged 'Root (Rose a) :-. Focusing 'Root Rose a
focusing (Rose a -> Maybe (Construction List a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Rose a -> Maybe (Construction List a))
-> (Tagged 'Root (Rose a) -> Rose a)
-> Tagged 'Root (Rose a)
-> Maybe (Construction List a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Root (Rose a) -> Rose a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Maybe (Construction List a)
Nothing) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Rose a))
-> Store (Maybe a) (Tagged 'Root (Rose a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Rose a))
 -> Store (Maybe a) (Tagged 'Root (Rose a)))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Rose a))
-> Store (Maybe a) (Tagged 'Root (Rose a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ Maybe a
forall a. Maybe a
Nothing Maybe a
-> (Maybe a -> Tagged 'Root (Rose a))
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Rose a)
forall s a. s -> a -> Product s a
:*: Rose a -> Tagged 'Root (Rose a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Rose a -> Tagged 'Root (Rose a))
-> (Maybe a -> Rose a) -> Maybe 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) -> 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 (Maybe (Construction List a) -> Rose a)
-> (Maybe a -> Maybe (Construction List a)) -> Maybe a -> Rose a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> Construction List a)
-> Maybe a -> Maybe (Construction List a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
comap (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)
	focusing (Rose a -> Maybe (Construction List a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Rose a -> Maybe (Construction List a))
-> (Tagged 'Root (Rose a) -> Rose a)
-> Tagged 'Root (Rose a)
-> Maybe (Construction List a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. Tagged 'Root (Rose a) -> Rose a
forall (t :: * -> *) a. Extractable t => a <:= t
extract -> Just Construction List a
rose) = (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Rose a))
-> Store (Maybe a) (Tagged 'Root (Rose a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Rose a))
 -> Store (Maybe a) (Tagged 'Root (Rose a)))
-> (((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Rose a))
-> Store (Maybe a) (Tagged 'Root (Rose a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a -> Maybe a
forall a. a -> Maybe a
Just (a <:= Construction List
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction List a
rose)
		Maybe a
-> (Maybe a -> Tagged 'Root (Rose a))
-> ((:*:) (Maybe a) :. (->) (Maybe a)) := Tagged 'Root (Rose a)
forall s a. s -> a -> Product s a
:*: Rose a -> Tagged 'Root (Rose a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Rose a -> Tagged 'Root (Rose a))
-> (Maybe a -> Rose a) -> Maybe a -> Tagged 'Root (Rose a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> Rose a) -> Rose a -> Maybe a -> Rose a
forall a e r. Monotonic a e => (a -> r) -> r -> e -> r
resolve (Construction List a -> Rose a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction List a -> Rose a)
-> (a -> Construction List a) -> a -> Rose 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 Construction List a
rose) Rose a
forall (t :: * -> *) a. Avoidable t => t a
empty

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 :: * -> * -> *). Category m => m ~~> m
$ \case { TU Maybe (Construction List a)
Nothing -> Boolean
True ; Rose a
_ -> Boolean
False }

instance Substructure Just Rose where
	type Substructural Just Rose = List <:.> Construction List
	substructure :: Lens ((<:.>) (Tagged 'Just) Rose a) (Substructural 'Just Rose a)
substructure (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
. TU Covariant Covariant Maybe (Construction List) a <:= Tagged 'Just
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction List) a
 <:= Tagged 'Just)
-> ((<:.>) (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 -> Maybe (Construction List a)
Nothing) =
		(((:*:) (TU Covariant Covariant List (Construction List) a)
  :. (->) (TU Covariant Covariant List (Construction List) a))
 := (<:.>) (Tagged 'Just) Rose a)
-> Store
     (TU Covariant Covariant List (Construction List) a)
     ((<:.>) (Tagged 'Just) Rose a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant List (Construction List) a)
   :. (->) (TU Covariant Covariant List (Construction List) a))
  := (<:.>) (Tagged 'Just) Rose a)
 -> Store
      (TU Covariant Covariant List (Construction List) a)
      ((<:.>) (Tagged 'Just) Rose a))
-> (((:*:) (TU Covariant Covariant List (Construction List) a)
     :. (->) (TU Covariant Covariant List (Construction List) a))
    := (<:.>) (Tagged 'Just) Rose a)
-> Store
     (TU Covariant Covariant List (Construction List) a)
     ((<:.>) (Tagged 'Just) Rose a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ TU Covariant Covariant List (Construction List) a
forall (t :: * -> *) a. Avoidable t => t a
empty TU Covariant Covariant List (Construction List) a
-> (TU Covariant Covariant List (Construction List) a
    -> (<:.>) (Tagged 'Just) Rose a)
-> ((:*:) (TU Covariant Covariant List (Construction List) a)
    :. (->) (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
-> TU Covariant Covariant List (Construction List) a
-> (<:.>) (Tagged 'Just) Rose a
forall a b. a -> b -> a
!)
	substructure (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
. TU Covariant Covariant Maybe (Construction List) a <:= Tagged 'Just
forall (t :: * -> *) a. Extractable t => a <:= t
extract (TU Covariant Covariant Maybe (Construction List) a
 <:= Tagged 'Just)
-> ((<:.>) (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 -> Just (Construct a
x (List :. Construction List) := a
xs)) =
		(((:*:) (TU Covariant Covariant List (Construction List) a)
  :. (->) (TU Covariant Covariant List (Construction List) a))
 := (<:.>) (Tagged 'Just) Rose a)
-> Store
     (TU Covariant Covariant List (Construction List) a)
     ((<:.>) (Tagged 'Just) Rose a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant List (Construction List) a)
   :. (->) (TU Covariant Covariant List (Construction List) a))
  := (<:.>) (Tagged 'Just) Rose a)
 -> Store
      (TU Covariant Covariant List (Construction List) a)
      ((<:.>) (Tagged 'Just) Rose a))
-> (((:*:) (TU Covariant Covariant List (Construction List) a)
     :. (->) (TU Covariant Covariant List (Construction List) a))
    := (<:.>) (Tagged 'Just) Rose a)
-> Store
     (TU Covariant Covariant List (Construction List) a)
     ((<:.>) (Tagged 'Just) Rose a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ ((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 TU Covariant Covariant List (Construction List) a
-> (TU Covariant Covariant List (Construction List) a
    -> (<:.>) (Tagged 'Just) Rose a)
-> ((:*:) (TU Covariant Covariant List (Construction List) a)
    :. (->) (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)
-> (TU Covariant Covariant List (Construction List) a
    -> TU Covariant Covariant Maybe (Construction List) a)
-> 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)
-> (TU Covariant Covariant List (Construction List) a
    -> Construction List a)
-> 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)
-> (TU Covariant Covariant List (Construction List) a
    -> (List :. Construction List) := a)
-> 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

type instance Nonempty Rose = Construction List

instance Focusable Root (Construction List) where
	type Focusing Root (Construction List) a = a
	focusing :: Tagged 'Root (Construction List a)
:-. Focusing 'Root (Construction List) a
focusing (Tag Construction List a
rose) = (((:*:) a :. (->) a) := Tagged 'Root (Construction List a))
-> Store a (Tagged 'Root (Construction List a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := Tagged 'Root (Construction List a))
 -> Store a (Tagged 'Root (Construction List a)))
-> (((:*:) a :. (->) a) := Tagged 'Root (Construction List a))
-> Store a (Tagged 'Root (Construction List a))
forall (m :: * -> * -> *). Category m => m ~~> m
$ a <:= Construction List
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction List a
rose a
-> (a -> Tagged 'Root (Construction List a))
-> ((:*:) a :. (->) a) := Tagged 'Root (Construction List a)
forall s a. s -> a -> Product s a
:*: Construction List a -> Tagged 'Root (Construction List a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Construction List a -> Tagged 'Root (Construction List a))
-> (a -> Construction List a)
-> 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 Construction List a
rose

instance Substructure Just (Construction List) where
	type Substructural Just (Construction List) = List <:.> Construction List
	substructure :: Lens
  ((<:.>) (Tagged 'Just) (Construction List) a)
  (Substructural 'Just (Construction List) a)
substructure (Construction List a <:= Tagged 'Just
forall (t :: * -> *) a. Extractable t => a <:= t
extract (Construction List a <:= Tagged 'Just)
-> ((<:.>) (Tagged 'Just) (Construction List) a
    -> Tagged 'Just (Construction List a))
-> (<:.>) (Tagged 'Just) (Construction List) a
-> Construction List a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (<:.>) (Tagged 'Just) (Construction List) a
-> Tagged 'Just (Construction List a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run -> Construct a
x (List :. Construction List) := a
xs) = (((:*:) (TU Covariant Covariant List (Construction List) a)
  :. (->) (TU Covariant Covariant List (Construction List) a))
 := (<:.>) (Tagged 'Just) (Construction List) a)
-> Store
     (TU Covariant Covariant List (Construction List) a)
     ((<:.>) (Tagged 'Just) (Construction List) a)
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) (TU Covariant Covariant List (Construction List) a)
   :. (->) (TU Covariant Covariant List (Construction List) a))
  := (<:.>) (Tagged 'Just) (Construction List) a)
 -> Store
      (TU Covariant Covariant List (Construction List) a)
      ((<:.>) (Tagged 'Just) (Construction List) a))
-> (((:*:) (TU Covariant Covariant List (Construction List) a)
     :. (->) (TU Covariant Covariant List (Construction List) a))
    := (<:.>) (Tagged 'Just) (Construction List) a)
-> Store
     (TU Covariant Covariant List (Construction List) a)
     ((<:.>) (Tagged 'Just) (Construction List) a)
forall (m :: * -> * -> *). Category m => m ~~> m
$ ((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 TU Covariant Covariant List (Construction List) a
-> (TU Covariant Covariant List (Construction List) a
    -> (<:.>) (Tagged 'Just) (Construction List) a)
-> ((:*:) (TU Covariant Covariant List (Construction List) a)
    :. (->) (TU Covariant Covariant List (Construction List) a))
   := (<:.>) (Tagged 'Just) (Construction List) a
forall s a. s -> a -> Product s a
:*: Construction List a -> (<:.>) (Tagged 'Just) (Construction List) a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction List a
 -> (<:.>) (Tagged 'Just) (Construction List) a)
-> (TU Covariant Covariant List (Construction List) a
    -> Construction List a)
-> TU Covariant Covariant List (Construction List) a
-> (<:.>) (Tagged 'Just) (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)
-> (TU Covariant Covariant List (Construction List) a
    -> (List :. Construction List) := a)
-> 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