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

module Pandora.Paradigm.Structure.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.Stack (Stack)

type Rose = Maybe <:.> Construction Stack

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 Stack a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Rose a -> Maybe (Construction Stack a))
-> (Tagged 'Root (Rose a) -> Rose a)
-> Tagged 'Root (Rose a)
-> Maybe (Construction Stack 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 Stack 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ 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 Stack 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 Stack a) -> Rose a)
-> (Maybe a -> Maybe (Construction Stack a)) -> Maybe a -> Rose a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. (a -> Construction Stack a)
-> Maybe a -> Maybe (Construction Stack a)
forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b
comap (a -> ((Stack :. Construction Stack) := a) -> Construction Stack a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Stack :. Construction Stack) := a) -> Construction Stack a)
-> ((Stack :. Construction Stack) := a)
-> a
-> Construction Stack a
forall a b c. (a -> b -> c) -> b -> a -> c
% (Stack :. Construction Stack) := a
forall (t :: * -> *) a. Avoidable t => t a
empty)
	focusing (Rose a -> Maybe (Construction Stack a)
forall (t :: * -> *) a. Interpreted t => t a -> Primary t a
run (Rose a -> Maybe (Construction Stack a))
-> (Tagged 'Root (Rose a) -> Rose a)
-> Tagged 'Root (Rose a)
-> Maybe (Construction Stack 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 Stack 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a <:= Construction Stack
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Stack 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 Stack a -> Rose a
forall (t :: (* -> *) -> * -> *) (u :: * -> *).
(Liftable t, Covariant u) =>
u ~> t u
lift (Construction Stack a -> Rose a)
-> (a -> Construction Stack a) -> a -> Rose a
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((Stack :. Construction Stack) := a) -> Construction Stack a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Stack :. Construction Stack) := a) -> Construction Stack a)
-> ((Stack :. Construction Stack) := a)
-> a
-> Construction Stack a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Stack a -> (Stack :. Construction Stack) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Stack 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 :: * -> * -> *) a b. Category m => m a b -> m a b
$ \case { TU Maybe (Construction Stack a)
Nothing -> Boolean
True ; Rose a
_ -> Boolean
False }

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

type instance Nonempty Rose = Construction Stack

instance Focusable Root (Construction Stack) where
	type Focusing Root (Construction Stack) a = a
	focusing :: Tagged 'Root (Construction Stack a)
:-. Focusing 'Root (Construction Stack) a
focusing (Tag Construction Stack a
rose) = (((:*:) a :. (->) a) := Tagged 'Root (Construction Stack a))
-> Store a (Tagged 'Root (Construction Stack a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) a :. (->) a) := Tagged 'Root (Construction Stack a))
 -> Store a (Tagged 'Root (Construction Stack a)))
-> (((:*:) a :. (->) a) := Tagged 'Root (Construction Stack a))
-> Store a (Tagged 'Root (Construction Stack a))
forall (m :: * -> * -> *) a b. Category m => m a b -> m a b
$ a <:= Construction Stack
forall (t :: * -> *) a. Extractable t => a <:= t
extract Construction Stack a
rose a
-> (a -> Tagged 'Root (Construction Stack a))
-> ((:*:) a :. (->) a) := Tagged 'Root (Construction Stack a)
forall s a. s -> a -> Product s a
:*: Construction Stack a -> Tagged 'Root (Construction Stack a)
forall k (tag :: k) a. a -> Tagged tag a
Tag (Construction Stack a -> Tagged 'Root (Construction Stack a))
-> (a -> Construction Stack a)
-> a
-> Tagged 'Root (Construction Stack a)
forall (m :: * -> * -> *) b c a.
Category m =>
m b c -> m a b -> m a c
. a -> ((Stack :. Construction Stack) := a) -> Construction Stack a
forall (t :: * -> *) a.
a -> ((t :. Construction t) := a) -> Construction t a
Construct (a -> ((Stack :. Construction Stack) := a) -> Construction Stack a)
-> ((Stack :. Construction Stack) := a)
-> a
-> Construction Stack a
forall a b c. (a -> b -> c) -> b -> a -> c
% Construction Stack a -> (Stack :. Construction Stack) := a
forall (t :: * -> *) a.
Construction t a -> (t :. Construction t) := a
deconstruct Construction Stack a
rose

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