{-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Structure.Some.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.Some.List (List) type Rose = Maybe <:.> Construction List 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 List a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Rose a -> Maybe (Construction List a)) -> (Tagged 'Root (Rose a) -> Rose a) -> Tagged 'Root (Rose a) -> Maybe (Construction List 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 List 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 :: * -> * -> *). Category m => m ~~> m $ 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 List 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 List a) -> Rose a) -> (Maybe a -> Maybe (Construction List a)) -> Maybe a -> Rose a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> Construction List a) -> Maybe a -> Maybe (Construction List a) forall (t :: * -> *) a b. Covariant t => (a -> b) -> t a -> t b comap (a -> ((List :. Construction List) := a) -> Construction List a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((List :. Construction List) := a) -> Construction List a) -> ((List :. Construction List) := a) -> a -> Construction List a forall a b c. (a -> b -> c) -> b -> a -> c % (List :. Construction List) := a forall (t :: * -> *) a. Avoidable t => t a empty) focusing (Rose a -> Maybe (Construction List a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Rose a -> Maybe (Construction List a)) -> (Tagged 'Root (Rose a) -> Rose a) -> Tagged 'Root (Rose a) -> Maybe (Construction List 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 List 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 :: * -> * -> *). Category m => m ~~> m $ a -> Maybe a forall a. a -> Maybe a Just (a <:= Construction List forall (t :: * -> *) a. Extractable t => a <:= t extract Construction List 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 List a -> Rose a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction List a -> Rose a) -> (a -> Construction List a) -> a -> Rose a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> ((List :. Construction List) := a) -> Construction List a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((List :. Construction List) := a) -> Construction List a) -> ((List :. Construction List) := a) -> a -> Construction List a forall a b c. (a -> b -> c) -> b -> a -> c % Construction List a -> (List :. Construction List) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction List 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 :: * -> * -> *). Category m => m ~~> m $ \case { TU Maybe (Construction List a) Nothing -> Boolean True ; Rose a _ -> Boolean False } instance Substructure Just Rose where type Substructural Just Rose = List <:.> Construction List substructure :: Lens ((<:.>) (Tagged 'Just) Rose a) (Substructural 'Just Rose a) substructure (TU Covariant Covariant Maybe (Construction List) a -> Maybe (Construction List a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (TU Covariant Covariant Maybe (Construction List) a -> Maybe (Construction List a)) -> ((<:.>) (Tagged 'Just) Rose a -> TU Covariant Covariant Maybe (Construction List) a) -> (<:.>) (Tagged 'Just) Rose a -> Maybe (Construction List a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction List) a <:= Tagged 'Just forall (t :: * -> *) a. Extractable t => a <:= t extract (TU Covariant Covariant Maybe (Construction List) a <:= Tagged 'Just) -> ((<:.>) (Tagged 'Just) Rose a -> Tagged 'Just (TU Covariant Covariant Maybe (Construction List) a)) -> (<:.>) (Tagged 'Just) Rose a -> TU Covariant Covariant Maybe (Construction List) 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 List) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Maybe (Construction List a) Nothing) = (((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) Rose a) -> Store (TU Covariant Covariant List (Construction List) a) ((<:.>) (Tagged 'Just) Rose a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) Rose a) -> Store (TU Covariant Covariant List (Construction List) a) ((<:.>) (Tagged 'Just) Rose a)) -> (((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) Rose a) -> Store (TU Covariant Covariant List (Construction List) a) ((<:.>) (Tagged 'Just) Rose a) forall (m :: * -> * -> *). Category m => m ~~> m $ TU Covariant Covariant List (Construction List) a forall (t :: * -> *) a. Avoidable t => t a empty TU Covariant Covariant List (Construction List) a -> (TU Covariant Covariant List (Construction List) a -> (<:.>) (Tagged 'Just) Rose a) -> ((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) Rose a forall s a. s -> a -> Product s a :*: (TU Covariant Covariant Maybe (Construction List) a -> (<:.>) (Tagged 'Just) Rose a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift TU Covariant Covariant Maybe (Construction List) a forall (t :: * -> *) a. Avoidable t => t a empty (<:.>) (Tagged 'Just) Rose a -> TU Covariant Covariant List (Construction List) a -> (<:.>) (Tagged 'Just) Rose a forall a b. a -> b -> a !) substructure (TU Covariant Covariant Maybe (Construction List) a -> Maybe (Construction List a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (TU Covariant Covariant Maybe (Construction List) a -> Maybe (Construction List a)) -> ((<:.>) (Tagged 'Just) Rose a -> TU Covariant Covariant Maybe (Construction List) a) -> (<:.>) (Tagged 'Just) Rose a -> Maybe (Construction List a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant Maybe (Construction List) a <:= Tagged 'Just forall (t :: * -> *) a. Extractable t => a <:= t extract (TU Covariant Covariant Maybe (Construction List) a <:= Tagged 'Just) -> ((<:.>) (Tagged 'Just) Rose a -> Tagged 'Just (TU Covariant Covariant Maybe (Construction List) a)) -> (<:.>) (Tagged 'Just) Rose a -> TU Covariant Covariant Maybe (Construction List) 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 List) a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Just (Construct a x (List :. Construction List) := a xs)) = (((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) Rose a) -> Store (TU Covariant Covariant List (Construction List) a) ((<:.>) (Tagged 'Just) Rose a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) Rose a) -> Store (TU Covariant Covariant List (Construction List) a) ((<:.>) (Tagged 'Just) Rose a)) -> (((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) Rose a) -> Store (TU Covariant Covariant List (Construction List) a) ((<:.>) (Tagged 'Just) Rose a) forall (m :: * -> * -> *). Category m => m ~~> m $ ((List :. Construction List) := a) -> TU Covariant Covariant List (Construction List) 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 (List :. Construction List) := a xs TU Covariant Covariant List (Construction List) a -> (TU Covariant Covariant List (Construction List) a -> (<:.>) (Tagged 'Just) Rose a) -> ((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) Rose a forall s a. s -> a -> Product s a :*: TU Covariant Covariant Maybe (Construction List) a -> (<:.>) (Tagged 'Just) Rose a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (TU Covariant Covariant Maybe (Construction List) a -> (<:.>) (Tagged 'Just) Rose a) -> (TU Covariant Covariant List (Construction List) a -> TU Covariant Covariant Maybe (Construction List) a) -> TU Covariant Covariant List (Construction List) a -> (<:.>) (Tagged 'Just) Rose a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Construction List a -> TU Covariant Covariant Maybe (Construction List) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction List a -> TU Covariant Covariant Maybe (Construction List) a) -> (TU Covariant Covariant List (Construction List) a -> Construction List a) -> TU Covariant Covariant List (Construction List) a -> TU Covariant Covariant Maybe (Construction List) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> ((List :. Construction List) := a) -> Construction List a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (((List :. Construction List) := a) -> Construction List a) -> (TU Covariant Covariant List (Construction List) a -> (List :. Construction List) := a) -> TU Covariant Covariant List (Construction List) a -> Construction List a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant List (Construction List) a -> (List :. Construction List) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run type instance Nonempty Rose = Construction List instance Focusable Root (Construction List) where type Focusing Root (Construction List) a = a focusing :: Tagged 'Root (Construction List a) :-. Focusing 'Root (Construction List) a focusing (Tag Construction List a rose) = (((:*:) a :. (->) a) := Tagged 'Root (Construction List a)) -> Store a (Tagged 'Root (Construction List a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) a :. (->) a) := Tagged 'Root (Construction List a)) -> Store a (Tagged 'Root (Construction List a))) -> (((:*:) a :. (->) a) := Tagged 'Root (Construction List a)) -> Store a (Tagged 'Root (Construction List a)) forall (m :: * -> * -> *). Category m => m ~~> m $ a <:= Construction List forall (t :: * -> *) a. Extractable t => a <:= t extract Construction List a rose a -> (a -> Tagged 'Root (Construction List a)) -> ((:*:) a :. (->) a) := Tagged 'Root (Construction List a) forall s a. s -> a -> Product s a :*: Construction List a -> Tagged 'Root (Construction List a) forall k (tag :: k) a. a -> Tagged tag a Tag (Construction List a -> Tagged 'Root (Construction List a)) -> (a -> Construction List a) -> a -> Tagged 'Root (Construction List a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> ((List :. Construction List) := a) -> Construction List a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct (a -> ((List :. Construction List) := a) -> Construction List a) -> ((List :. Construction List) := a) -> a -> Construction List a forall a b c. (a -> b -> c) -> b -> a -> c % Construction List a -> (List :. Construction List) := a forall (t :: * -> *) a. Construction t a -> (t :. Construction t) := a deconstruct Construction List a rose instance Substructure Just (Construction List) where type Substructural Just (Construction List) = List <:.> Construction List substructure :: Lens ((<:.>) (Tagged 'Just) (Construction List) a) (Substructural 'Just (Construction List) a) substructure (Construction List a <:= Tagged 'Just forall (t :: * -> *) a. Extractable t => a <:= t extract (Construction List a <:= Tagged 'Just) -> ((<:.>) (Tagged 'Just) (Construction List) a -> Tagged 'Just (Construction List a)) -> (<:.>) (Tagged 'Just) (Construction List) a -> Construction List a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (<:.>) (Tagged 'Just) (Construction List) a -> Tagged 'Just (Construction List a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run -> Construct a x (List :. Construction List) := a xs) = (((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) (Construction List) a) -> Store (TU Covariant Covariant List (Construction List) a) ((<:.>) (Tagged 'Just) (Construction List) a) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) (Construction List) a) -> Store (TU Covariant Covariant List (Construction List) a) ((<:.>) (Tagged 'Just) (Construction List) a)) -> (((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) (Construction List) a) -> Store (TU Covariant Covariant List (Construction List) a) ((<:.>) (Tagged 'Just) (Construction List) a) forall (m :: * -> * -> *). Category m => m ~~> m $ ((List :. Construction List) := a) -> TU Covariant Covariant List (Construction List) 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 (List :. Construction List) := a xs TU Covariant Covariant List (Construction List) a -> (TU Covariant Covariant List (Construction List) a -> (<:.>) (Tagged 'Just) (Construction List) a) -> ((:*:) (TU Covariant Covariant List (Construction List) a) :. (->) (TU Covariant Covariant List (Construction List) a)) := (<:.>) (Tagged 'Just) (Construction List) a forall s a. s -> a -> Product s a :*: Construction List a -> (<:.>) (Tagged 'Just) (Construction List) a forall (t :: (* -> *) -> * -> *) (u :: * -> *). (Liftable t, Covariant u) => u ~> t u lift (Construction List a -> (<:.>) (Tagged 'Just) (Construction List) a) -> (TU Covariant Covariant List (Construction List) a -> Construction List a) -> TU Covariant Covariant List (Construction List) a -> (<:.>) (Tagged 'Just) (Construction List) a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> ((List :. Construction List) := a) -> Construction List a forall (t :: * -> *) a. a -> ((t :. Construction t) := a) -> Construction t a Construct a x (((List :. Construction List) := a) -> Construction List a) -> (TU Covariant Covariant List (Construction List) a -> (List :. Construction List) := a) -> TU Covariant Covariant List (Construction List) a -> Construction List a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . TU Covariant Covariant List (Construction List) a -> (List :. Construction List) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run