{-# LANGUAGE UndecidableInstances #-}
module Pandora.Paradigm.Structure.Modification.Turnover where

import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Transformer.Hoistable ((/|\))
import Pandora.Paradigm.Primary.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Primary.Algebraic ((>-|-<-|-))
import Pandora.Paradigm.Controlflow.Effect.Interpreted (Interpreted (Primary, run, unite, (=#-)))
import Pandora.Paradigm.Structure.Ability.Substructure (Substructure (Available, 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 Available segment (Turnover structure) = Available segment structure
	type Substance segment (Turnover structure) = Substance segment structure
	substructure :: Lens
  (Available segment (Turnover structure))
  ((<:.>) (Tagged segment) (Turnover structure) a)
  (Substance segment (Turnover structure) 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
      (Available segment structure (Substance segment structure a))
      (TU Covariant Covariant (Tagged segment) structure a)
    -> Store
         (Available segment structure (Substance segment structure a))
         ((<:.>) (Tagged segment) (Turnover structure) a))
-> ((<:.>) (Tagged segment) (Turnover structure) a
    -> TU Covariant Covariant (Tagged segment) structure a)
   :*: (Store
          (Available segment structure (Substance segment structure a))
          (TU Covariant Covariant (Tagged segment) structure a)
        -> Store
             (Available segment structure (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
     (Available segment structure (Substance segment structure a))
     (TU Covariant Covariant (Tagged segment) structure a)
-> Store
     (Available segment structure (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
        (Available segment structure (Substance segment structure a))
        (TU Covariant Covariant (Tagged segment) structure a)
      -> Store
           (Available segment structure (Substance segment structure a))
           ((<:.>) (Tagged segment) (Turnover structure) a)))
-> (TU Covariant Covariant (Tagged segment) structure a
    -> Store
         (Available segment structure (Substance segment structure a))
         (TU Covariant Covariant (Tagged segment) structure a))
-> (<:.>) (Tagged segment) (Turnover structure) a
-> Store
     (Available segment structure (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
      (Available segment structure)
      (TU Covariant Covariant (Tagged segment) structure a))
   (Substance segment structure a)
 -> Primary
      (P_Q_T
         (->)
         Store
         (Available segment structure)
         ((<:.>) (Tagged segment) (Turnover structure) a))
      (Substance segment structure a))
-> P_Q_T
     (->)
     Store
     (Available segment structure)
     (TU Covariant Covariant (Tagged segment) structure a)
     (Substance segment structure a)
-> P_Q_T
     (->)
     Store
     (Available segment structure)
     ((<:.>) (Tagged segment) (Turnover structure) a)
     (Substance segment structure 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)
:= Available segment structure
forall k (segment :: k) (structure :: * -> *).
Substructure segment structure =>
((Tagged segment <:.> structure) #=@ Substance segment structure)
:= Available segment structure
substructure @segment @structure