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