{-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Structure (module Exports) where import Pandora.Paradigm.Structure.Ability as Exports import Pandora.Paradigm.Structure.Interface as Exports import Pandora.Paradigm.Structure.Rose as Exports import Pandora.Paradigm.Structure.Splay as Exports import Pandora.Paradigm.Structure.Binary as Exports import Pandora.Paradigm.Structure.Stack as Exports import Pandora.Paradigm.Structure.Stream as Exports import Pandora.Pattern (($), (.), extract) import Pandora.Paradigm.Controlflow.Effect.Interpreted (run, unite) import Pandora.Paradigm.Inventory (Store (Store), (^.), (.~)) import Pandora.Paradigm.Primary.Object.Boolean (Boolean (True, False)) import Pandora.Paradigm.Primary.Functor.Delta (Delta ((:^:))) import Pandora.Paradigm.Primary.Functor.Maybe (Maybe (Just)) import Pandora.Paradigm.Primary.Functor.Predicate (Predicate (Predicate)) import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:)), type (:*:), attached) import Pandora.Paradigm.Primary.Functor.Tagged (Tagged (Tag)) import Pandora.Paradigm.Primary.Functor.Wye (Wye (Left, Right)) import Pandora.Paradigm.Primary.Transformer.Tap (Tap (Tap)) import Pandora.Paradigm.Schemes.TU (type (<:.>)) instance Monotonic s a => Monotonic s (s :*: a) where reduce :: (s -> r -> r) -> r -> (s :*: a) -> r reduce s -> r -> r f r r s :*: a x = (s -> r -> r) -> r -> a -> r forall a e r. Monotonic a e => (a -> r -> r) -> r -> e -> r reduce s -> r -> r f (s -> r -> r f ((s :*: a) -> s forall a b. (a :*: b) -> a attached s :*: a x) r r) (a -> r) -> a -> r forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a <-| Product s forall (t :: * -> *) a. Extractable t => a <-| t extract s :*: a x instance Nullable Maybe where null :: (Predicate :. Maybe) := a null = (Maybe a -> Boolean) -> (Predicate :. Maybe) := a forall a. (a -> Boolean) -> Predicate a Predicate ((Maybe a -> Boolean) -> (Predicate :. Maybe) := a) -> (Maybe a -> Boolean) -> (Predicate :. Maybe) := a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ \case { Just a _ -> Boolean True ; Maybe a _ -> Boolean False } instance Substructure Left (Product s) where type Substructural Left (Product s) a = s substructure :: Tagged 'Left (Product s a) :-. Substructural 'Left (Product s) a substructure (Product s a <-| Tagged 'Left forall (t :: * -> *) a. Extractable t => a <-| t extract -> s s :*: a x) = ((Product s :. (->) s) := Tagged 'Left (Product s a)) -> Store s (Tagged 'Left (Product s a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store (((Product s :. (->) s) := Tagged 'Left (Product s a)) -> Store s (Tagged 'Left (Product s a))) -> ((Product s :. (->) s) := Tagged 'Left (Product s a)) -> Store s (Tagged 'Left (Product s a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ s s s -> (s -> Tagged 'Left (Product s a)) -> (Product s :. (->) s) := Tagged 'Left (Product s a) forall s a. s -> a -> Product s a :*: Product s a -> Tagged 'Left (Product s a) forall k (tag :: k) a. a -> Tagged tag a Tag (Product s a -> Tagged 'Left (Product s a)) -> (s -> Product s a) -> s -> Tagged 'Left (Product s a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (s -> a -> Product s a forall s a. s -> a -> Product s a :*: a x) instance Substructure Right (Product s) where type Substructural Right (Product s) a = a substructure :: Tagged 'Right (Product s a) :-. Substructural 'Right (Product s) a substructure (Product s a <-| Tagged 'Right forall (t :: * -> *) a. Extractable t => a <-| t extract -> s s :*: a x) = (((:*:) a :. (->) a) := Tagged 'Right (Product s a)) -> Store a (Tagged 'Right (Product s a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) a :. (->) a) := Tagged 'Right (Product s a)) -> Store a (Tagged 'Right (Product s a))) -> (((:*:) a :. (->) a) := Tagged 'Right (Product s a)) -> Store a (Tagged 'Right (Product s a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> (a -> Tagged 'Right (Product s a)) -> ((:*:) a :. (->) a) := Tagged 'Right (Product s a) forall s a. s -> a -> Product s a :*: Product s a -> Tagged 'Right (Product s a) forall k (tag :: k) a. a -> Tagged tag a Tag (Product s a -> Tagged 'Right (Product s a)) -> (a -> Product s a) -> a -> Tagged 'Right (Product s a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (s s s -> a -> Product s a forall s a. s -> a -> Product s a :*:) instance Substructure Left Delta where type Substructural Left Delta a = a substructure :: Tagged 'Left (Delta a) :-. Substructural 'Left Delta a substructure (Delta a <-| Tagged 'Left forall (t :: * -> *) a. Extractable t => a <-| t extract -> a l :^: a r) = (((:*:) a :. (->) a) := Tagged 'Left (Delta a)) -> Store a (Tagged 'Left (Delta a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) a :. (->) a) := Tagged 'Left (Delta a)) -> Store a (Tagged 'Left (Delta a))) -> (((:*:) a :. (->) a) := Tagged 'Left (Delta a)) -> Store a (Tagged 'Left (Delta a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a l a -> (a -> Tagged 'Left (Delta a)) -> ((:*:) a :. (->) a) := Tagged 'Left (Delta a) forall s a. s -> a -> Product s a :*: Delta a -> Tagged 'Left (Delta a) forall k (tag :: k) a. a -> Tagged tag a Tag (Delta a -> Tagged 'Left (Delta a)) -> (a -> Delta a) -> a -> Tagged 'Left (Delta a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a -> a -> Delta a forall a. a -> a -> Delta a :^: a r) instance Substructure Right Delta where type Substructural Right Delta a = a substructure :: Tagged 'Right (Delta a) :-. Substructural 'Right Delta a substructure (Delta a <-| Tagged 'Right forall (t :: * -> *) a. Extractable t => a <-| t extract -> a l :^: a r) = (((:*:) a :. (->) a) := Tagged 'Right (Delta a)) -> Store a (Tagged 'Right (Delta a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) a :. (->) a) := Tagged 'Right (Delta a)) -> Store a (Tagged 'Right (Delta a))) -> (((:*:) a :. (->) a) := Tagged 'Right (Delta a)) -> Store a (Tagged 'Right (Delta a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a r a -> (a -> Tagged 'Right (Delta a)) -> ((:*:) a :. (->) a) := Tagged 'Right (Delta a) forall s a. s -> a -> Product s a :*: Delta a -> Tagged 'Right (Delta a) forall k (tag :: k) a. a -> Tagged tag a Tag (Delta a -> Tagged 'Right (Delta a)) -> (a -> Delta a) -> a -> Tagged 'Right (Delta a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (a l a -> a -> Delta a forall a. a -> a -> Delta a :^:) instance Substructure Left (Delta <:.> t) where type Substructural Left (Delta <:.> t) a = t a substructure :: Tagged 'Left ((<:.>) Delta t a) :-. Substructural 'Left (Delta <:.> t) a substructure ((<:.>) Delta t a -> Delta (t a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:.>) Delta t a -> Delta (t a)) -> (Tagged 'Left ((<:.>) Delta t a) -> (<:.>) Delta t a) -> Tagged 'Left ((<:.>) Delta t a) -> Delta (t a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Left ((<:.>) Delta t a) -> (<:.>) Delta t a forall (t :: * -> *) a. Extractable t => a <-| t extract -> t a l :^: t a r) = (((:*:) (t a) :. (->) (t a)) := Tagged 'Left ((<:.>) Delta t a)) -> Store (t a) (Tagged 'Left ((<:.>) Delta t a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (t a) :. (->) (t a)) := Tagged 'Left ((<:.>) Delta t a)) -> Store (t a) (Tagged 'Left ((<:.>) Delta t a))) -> (((:*:) (t a) :. (->) (t a)) := Tagged 'Left ((<:.>) Delta t a)) -> Store (t a) (Tagged 'Left ((<:.>) Delta t a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ t a r t a -> (t a -> Tagged 'Left ((<:.>) Delta t a)) -> ((:*:) (t a) :. (->) (t a)) := Tagged 'Left ((<:.>) Delta t a) forall s a. s -> a -> Product s a :*: (<:.>) Delta t a -> Tagged 'Left ((<:.>) Delta t a) forall k (tag :: k) a. a -> Tagged tag a Tag ((<:.>) Delta t a -> Tagged 'Left ((<:.>) Delta t a)) -> (t a -> (<:.>) Delta t a) -> t a -> Tagged 'Left ((<:.>) Delta t a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Delta (t a) -> (<:.>) Delta t a forall (t :: * -> *) a. Interpreted t => Primary t a -> t a unite (Delta (t a) -> (<:.>) Delta t a) -> (t a -> Delta (t a)) -> t a -> (<:.>) Delta t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (t a l t a -> t a -> Delta (t a) forall a. a -> a -> Delta a :^:) instance Substructure Right (Delta <:.> t) where type Substructural Right (Delta <:.> t) a = t a substructure :: Tagged 'Right ((<:.>) Delta t a) :-. Substructural 'Right (Delta <:.> t) a substructure ((<:.>) Delta t a -> Delta (t a) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:.>) Delta t a -> Delta (t a)) -> (Tagged 'Right ((<:.>) Delta t a) -> (<:.>) Delta t a) -> Tagged 'Right ((<:.>) Delta t a) -> Delta (t a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Tagged 'Right ((<:.>) Delta t a) -> (<:.>) Delta t a forall (t :: * -> *) a. Extractable t => a <-| t extract -> t a l :^: t a r) = (((:*:) (t a) :. (->) (t a)) := Tagged 'Right ((<:.>) Delta t a)) -> Store (t a) (Tagged 'Right ((<:.>) Delta t a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (t a) :. (->) (t a)) := Tagged 'Right ((<:.>) Delta t a)) -> Store (t a) (Tagged 'Right ((<:.>) Delta t a))) -> (((:*:) (t a) :. (->) (t a)) := Tagged 'Right ((<:.>) Delta t a)) -> Store (t a) (Tagged 'Right ((<:.>) Delta t a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ t a l t a -> (t a -> Tagged 'Right ((<:.>) Delta t a)) -> ((:*:) (t a) :. (->) (t a)) := Tagged 'Right ((<:.>) Delta t a) forall s a. s -> a -> Product s a :*: (<:.>) Delta t a -> Tagged 'Right ((<:.>) Delta t a) forall k (tag :: k) a. a -> Tagged tag a Tag ((<:.>) Delta t a -> Tagged 'Right ((<:.>) Delta t a)) -> (t a -> (<:.>) Delta t a) -> t a -> Tagged 'Right ((<:.>) Delta t a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Delta (t a) -> (<:.>) Delta t a forall (t :: * -> *) a. Interpreted t => Primary t a -> t a unite (Delta (t a) -> (<:.>) Delta t a) -> (t a -> Delta (t a)) -> t a -> (<:.>) Delta t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (t a -> t a -> Delta (t a) forall a. a -> a -> Delta a :^: t a r) instance Substructure Left t => Substructure Left (Tap (t <:.> u)) where type Substructural Left (Tap (t <:.> u)) a = Substructural Left t (u a) substructure :: Tagged 'Left (Tap (t <:.> u) a) :-. Substructural 'Left (Tap (t <:.> u)) a substructure (Tap (t <:.> u) a <-| Tagged 'Left forall (t :: * -> *) a. Extractable t => a <-| t extract -> Tap a x (<:.>) t u a xs) = (((:*:) (Substructural 'Left t (u a)) :. (->) (Substructural 'Left t (u a))) := Tagged 'Left (Tap (t <:.> u) a)) -> Store (Substructural 'Left t (u a)) (Tagged 'Left (Tap (t <:.> u) a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Substructural 'Left t (u a)) :. (->) (Substructural 'Left t (u a))) := Tagged 'Left (Tap (t <:.> u) a)) -> Store (Substructural 'Left t (u a)) (Tagged 'Left (Tap (t <:.> u) a))) -> (((:*:) (Substructural 'Left t (u a)) :. (->) (Substructural 'Left t (u a))) := Tagged 'Left (Tap (t <:.> u) a)) -> Store (Substructural 'Left t (u a)) (Tagged 'Left (Tap (t <:.> u) a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ forall k (f :: * -> k) (t :: * -> *) a. Substructure f t => t a :-. Substructural f t a forall (t :: * -> *) a. Substructure 'Left t => t a :-. Substructural 'Left t a sub @Left (t (u a) :-. Substructural 'Left t (u a)) -> t (u a) -> Substructural 'Left t (u a) forall src tgt. Lens src tgt -> src -> tgt ^. (<:.>) t u a -> Primary (t <:.> u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<:.>) t u a xs Substructural 'Left t (u a) -> (Substructural 'Left t (u a) -> Tagged 'Left (Tap (t <:.> u) a)) -> ((:*:) (Substructural 'Left t (u a)) :. (->) (Substructural 'Left t (u a))) := Tagged 'Left (Tap (t <:.> u) a) forall s a. s -> a -> Product s a :*: Tap (t <:.> u) a -> Tagged 'Left (Tap (t <:.> u) a) forall k (tag :: k) a. a -> Tagged tag a Tag (Tap (t <:.> u) a -> Tagged 'Left (Tap (t <:.> u) a)) -> (Substructural 'Left t (u a) -> Tap (t <:.> u) a) -> Substructural 'Left t (u a) -> Tagged 'Left (Tap (t <:.> u) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (\Substructural 'Left t (u a) new -> forall k (f :: * -> k) (t :: * -> *) a. Substructure f t => t a :-. Substructural f t a forall (t :: * -> *) a. Substructure 'Left t => t a :-. Substructural 'Left t a sub @Left (Tap (t <:.> u) a -> Store (Substructural 'Left t (u a)) (Tap (t <:.> u) a)) -> Substructural 'Left t (u a) -> Tap (t <:.> u) a -> Tap (t <:.> u) a forall src tgt. Lens src tgt -> tgt -> src -> src .~ Substructural 'Left t (u a) new (Tap (t <:.> u) a -> Tap (t <:.> u) a) -> Tap (t <:.> u) a -> Tap (t <:.> u) a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a -> (<:.>) t u a -> Tap (t <:.> u) a forall (t :: * -> *) a. a -> t a -> Tap t a Tap a x (<:.>) t u a xs) instance Substructure Right t => Substructure Right (Tap (t <:.> u)) where type Substructural Right (Tap (t <:.> u)) a = Substructural Right t (u a) substructure :: Tagged 'Right (Tap (t <:.> u) a) :-. Substructural 'Right (Tap (t <:.> u)) a substructure (Tap (t <:.> u) a <-| Tagged 'Right forall (t :: * -> *) a. Extractable t => a <-| t extract -> Tap a x (<:.>) t u a xs) = (((:*:) (Substructural 'Right t (u a)) :. (->) (Substructural 'Right t (u a))) := Tagged 'Right (Tap (t <:.> u) a)) -> Store (Substructural 'Right t (u a)) (Tagged 'Right (Tap (t <:.> u) a)) forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) (Substructural 'Right t (u a)) :. (->) (Substructural 'Right t (u a))) := Tagged 'Right (Tap (t <:.> u) a)) -> Store (Substructural 'Right t (u a)) (Tagged 'Right (Tap (t <:.> u) a))) -> (((:*:) (Substructural 'Right t (u a)) :. (->) (Substructural 'Right t (u a))) := Tagged 'Right (Tap (t <:.> u) a)) -> Store (Substructural 'Right t (u a)) (Tagged 'Right (Tap (t <:.> u) a)) forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ forall k (f :: * -> k) (t :: * -> *) a. Substructure f t => t a :-. Substructural f t a forall (t :: * -> *) a. Substructure 'Right t => t a :-. Substructural 'Right t a sub @Right (t (u a) :-. Substructural 'Right t (u a)) -> t (u a) -> Substructural 'Right t (u a) forall src tgt. Lens src tgt -> src -> tgt ^. (<:.>) t u a -> Primary (t <:.> u) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (<:.>) t u a xs Substructural 'Right t (u a) -> (Substructural 'Right t (u a) -> Tagged 'Right (Tap (t <:.> u) a)) -> ((:*:) (Substructural 'Right t (u a)) :. (->) (Substructural 'Right t (u a))) := Tagged 'Right (Tap (t <:.> u) a) forall s a. s -> a -> Product s a :*: Tap (t <:.> u) a -> Tagged 'Right (Tap (t <:.> u) a) forall k (tag :: k) a. a -> Tagged tag a Tag (Tap (t <:.> u) a -> Tagged 'Right (Tap (t <:.> u) a)) -> (Substructural 'Right t (u a) -> Tap (t <:.> u) a) -> Substructural 'Right t (u a) -> Tagged 'Right (Tap (t <:.> u) a) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (\Substructural 'Right t (u a) new -> forall k (f :: * -> k) (t :: * -> *) a. Substructure f t => t a :-. Substructural f t a forall (t :: * -> *) a. Substructure 'Right t => t a :-. Substructural 'Right t a sub @Right (Tap (t <:.> u) a -> Store (Substructural 'Right t (u a)) (Tap (t <:.> u) a)) -> Substructural 'Right t (u a) -> Tap (t <:.> u) a -> Tap (t <:.> u) a forall src tgt. Lens src tgt -> tgt -> src -> src .~ Substructural 'Right t (u a) new (Tap (t <:.> u) a -> Tap (t <:.> u) a) -> Tap (t <:.> u) a -> Tap (t <:.> u) a forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a -> (<:.>) t u a -> Tap (t <:.> u) a forall (t :: * -> *) a. a -> t a -> Tap t a Tap a x (<:.>) t u a xs)