{-# 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.Functor.Maybe (Maybe (Just, Nothing), maybe)
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.Nonempty (Nonempty)
import Pandora.Paradigm.Structure.Ability.Focusable (Focusable (Focusing, focusing), Location (Root))
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 p a. (((:*:) p :. (->) p) := a) -> Store p 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 p a. (((:*:) p :. (->) p) := a) -> Store p 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
. Rose a -> (a -> Rose a) -> Maybe a -> Rose a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (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) (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)

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 p a. (((:*:) p :. (->) p) := a) -> Store p 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 p a. (((:*:) p :. (->) p) := a) -> Store p 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 p a. (((:*:) p :. (->) p) := a) -> Store p 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 (Tag (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 p a. (((:*:) p :. (->) p) := a) -> Store p 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