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

module Pandora.Paradigm.Structure.Rose where

import Pandora.Core.Functor (type (:.), type (:=))
import Pandora.Core.Morphism ((!), (%))
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.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) (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)
forall a. Maybe a
Nothing)

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

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) a = Stack :. Construction Stack := a
	substructure :: Tagged 'Just (Construction Stack a)
:-. Substructural 'Just (Construction Stack) a
substructure (Construction Stack a <-| Tagged 'Just
forall (t :: * -> *) a. Extractable t => a <-| t
extract -> Construct a
x (Stack :. Construction Stack) := a
xs) = (((:*:) ((Stack :. Construction Stack) := a)
  :. (->) ((Stack :. Construction Stack) := a))
 := Tagged 'Just (Construction Stack a))
-> Store
     ((Stack :. Construction Stack) := a)
     (Tagged 'Just (Construction Stack a))
forall s a. (((:*:) s :. (->) s) := a) -> Store s a
Store ((((:*:) ((Stack :. Construction Stack) := a)
   :. (->) ((Stack :. Construction Stack) := a))
  := Tagged 'Just (Construction Stack a))
 -> Store
      ((Stack :. Construction Stack) := a)
      (Tagged 'Just (Construction Stack a)))
-> (((:*:) ((Stack :. Construction Stack) := a)
     :. (->) ((Stack :. Construction Stack) := a))
    := Tagged 'Just (Construction Stack a))
-> Store
     ((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
xs ((Stack :. Construction Stack) := a)
-> (((Stack :. Construction Stack) := a)
    -> Tagged 'Just (Construction Stack a))
-> ((:*:) ((Stack :. Construction Stack) := a)
    :. (->) ((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 k (tag :: k) a. a -> Tagged tag a
Tag (Construction Stack a -> Tagged 'Just (Construction Stack a))
-> (((Stack :. Construction Stack) := a) -> Construction Stack a)
-> ((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