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