{-# LANGUAGE UndecidableInstances #-} module Pandora.Paradigm.Structure.Modification.Turnover where import Pandora.Core.Interpreted (Interpreted (Primary, run, unite, (=#-))) import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-))) import Pandora.Pattern.Transformer.Hoistable ((/|\)) import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:))) import Pandora.Paradigm.Algebraic ((>-|-<-|-)) import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Substance, substructure)) newtype Turnover t a = Turnover (t a) instance (Covariant m m t, Interpreted m (Turnover t)) => Covariant m m (Turnover t) where <-|- :: m a b -> m (Turnover t a) (Turnover t b) (<-|-) m a b f = ((m < Primary (Turnover t) a) < Primary (Turnover t) b) -> m (Turnover t a) (Turnover t b) forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Interpreted m t, Semigroupoid m, Interpreted m u) => ((m < Primary t a) < Primary u b) -> (m < t a) < u b (=#-) (m a b -> m (t a) (t b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) (<-|-) m a b f) instance Interpreted (->) (Turnover t) where type Primary (Turnover t) a = t a run :: ((->) < Turnover t a) < Primary (Turnover t) a run ~(Turnover t a x) = t a Primary (Turnover t) a x unite :: ((->) < Primary (Turnover t) a) < Turnover t a unite = ((->) < Primary (Turnover t) a) < Turnover t a forall k (t :: k -> *) (a :: k). t a -> Turnover t a Turnover instance (Covariant (->) (->) structure, Substructure segment structure) => Substructure segment (Turnover structure) where type Substance segment (Turnover structure) = Substance segment structure substructure :: Lens (Substance segment (Turnover structure)) ((<:.>) (Tagged segment) (Turnover structure) a) a substructure = (((forall a. Turnover structure a -> structure a forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < t a) < Primary t a run (forall a. Turnover structure a -> structure a) -> (<:.>) (Tagged segment) (Turnover structure) a -> TU Covariant Covariant (Tagged segment) structure a forall k (m :: * -> * -> *) (t :: (* -> *) -> k -> *) (u :: * -> *) (v :: * -> *). (Hoistable m t, Covariant m m u) => (forall a. m (u a) (v a)) -> forall (a :: k). m (t u a) (t v a) /|\) ((<:.>) (Tagged segment) (Turnover structure) a -> TU Covariant Covariant (Tagged segment) structure a) -> (Store (Substance segment structure a) (TU Covariant Covariant (Tagged segment) structure a) -> Store (Substance segment structure a) ((<:.>) (Tagged segment) (Turnover structure) a)) -> ((<:.>) (Tagged segment) (Turnover structure) a -> TU Covariant Covariant (Tagged segment) structure a) :*: (Store (Substance segment structure a) (TU Covariant Covariant (Tagged segment) structure a) -> Store (Substance segment structure a) ((<:.>) (Tagged segment) (Turnover structure) a)) forall s a. s -> a -> s :*: a :*: ((forall a. structure a -> Turnover structure a forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < Primary t a) < t a unite (forall a. structure a -> Turnover structure a) -> TU Covariant Covariant (Tagged segment) structure a -> (<:.>) (Tagged segment) (Turnover structure) a forall k (m :: * -> * -> *) (t :: (* -> *) -> k -> *) (u :: * -> *) (v :: * -> *). (Hoistable m t, Covariant m m u) => (forall a. m (u a) (v a)) -> forall (a :: k). m (t u a) (t v a) /|\) (TU Covariant Covariant (Tagged segment) structure a -> (<:.>) (Tagged segment) (Turnover structure) a) -> Store (Substance segment structure a) (TU Covariant Covariant (Tagged segment) structure a) -> Store (Substance segment structure a) ((<:.>) (Tagged segment) (Turnover structure) a) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) a b. Covariant source target t => source a b -> target (t a) (t b) <-|-)) (((<:.>) (Tagged segment) (Turnover structure) a -> TU Covariant Covariant (Tagged segment) structure a) :*: (Store (Substance segment structure a) (TU Covariant Covariant (Tagged segment) structure a) -> Store (Substance segment structure a) ((<:.>) (Tagged segment) (Turnover structure) a))) -> (TU Covariant Covariant (Tagged segment) structure a -> Store (Substance segment structure a) (TU Covariant Covariant (Tagged segment) structure a)) -> (<:.>) (Tagged segment) (Turnover structure) a -> Store (Substance segment structure a) ((<:.>) (Tagged segment) (Turnover structure) a) forall (m :: * -> * -> *) (p :: * -> * -> *) a b c d. (Contravariant m m (Flip p d), Covariant m m (p b), Interpreted m (Flip p d)) => (m a b :*: m c d) -> m (p b c) (p a d) >-|-<-|-) (Primary (P_Q_T (->) Store (Substance segment structure) (TU Covariant Covariant (Tagged segment) structure a)) a -> Primary (P_Q_T (->) Store (Substance segment structure) ((<:.>) (Tagged segment) (Turnover structure) a)) a) -> ((->) < P_Q_T (->) Store (Substance segment structure) (TU Covariant Covariant (Tagged segment) structure a) a) < P_Q_T (->) Store (Substance segment structure) ((<:.>) (Tagged segment) (Turnover structure) a) a forall (m :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. (Interpreted m t, Semigroupoid m, Interpreted m u) => ((m < Primary t a) < Primary u b) -> (m < t a) < u b =#- Substructure segment structure => (Tagged segment <:.> structure) @>>> Substance segment structure forall k (segment :: k) (structure :: * -> *). Substructure segment structure => (Tagged segment <:.> structure) @>>> Substance segment structure substructure @segment @structure