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