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