{-# OPTIONS_GHC -fno-warn-orphans #-}
module Pandora.Paradigm.Inventory.Some.Accumulator (Accumulator (..), Accumulated, gather) where

import Pandora.Core.Interpreted (Interpreted (Primary, run, unite))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Functor.Monad (Monad)
import Pandora.Pattern.Object.Monoid (Monoid)
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Paradigm.Algebraic.Exponential (type (-->))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Algebraic (point)
import Pandora.Paradigm.Controlflow.Effect.Transformer.Monadic (Monadic (wrap), (:>) (TM))
import Pandora.Paradigm.Controlflow.Effect.Adaptable (Adaptable (adapt))
import Pandora.Paradigm.Schemes (Schematic, UT (UT), type (<.:>))

newtype Accumulator e a = Accumulator (e :*: a)

instance Covariant (->) (->) (Accumulator e) where
	a -> b
f <-|- :: (a -> b) -> Accumulator e a -> Accumulator e b
<-|- Accumulator e :*: a
x = (e :*: b) -> Accumulator e b
forall e a. (e :*: a) -> Accumulator e a
Accumulator ((e :*: b) -> Accumulator e b) -> (e :*: b) -> Accumulator e b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a -> b
f (a -> b) -> (e :*: a) -> e :*: b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- e :*: a
x

instance Semigroup e => Semimonoidal (-->) (:*:) (:*:) (Accumulator e) where
	mult :: (Accumulator e a :*: Accumulator e b) --> Accumulator e (a :*: b)
mult = ((Accumulator e a :*: Accumulator e b) -> Accumulator e (a :*: b))
-> (Accumulator e a :*: Accumulator e b)
   --> Accumulator e (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Accumulator e a :*: Accumulator e b) -> Accumulator e (a :*: b))
 -> (Accumulator e a :*: Accumulator e b)
    --> Accumulator e (a :*: b))
-> ((Accumulator e a :*: Accumulator e b)
    -> Accumulator e (a :*: b))
-> (Accumulator e a :*: Accumulator e b)
   --> Accumulator e (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Accumulator e a
x :*: Accumulator e b
y) -> (e :*: (a :*: b)) -> Accumulator e (a :*: b)
forall e a. (e :*: a) -> Accumulator e a
Accumulator ((e :*: (a :*: b)) -> Accumulator e (a :*: b))
-> (e :*: (a :*: b)) -> Accumulator e (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (e :*: a) -> (e :*: b) -> e :*: (a :*: b)
forall s s a.
Semigroup s =>
(s :*: s) -> (s :*: a) -> s :*: (s :*: a)
k ((e :*: a) -> (e :*: b) -> e :*: (a :*: b))
-> (e :*: a) -> (e :*: b) -> e :*: (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Accumulator e a -> e :*: a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Accumulator e a
x ((e :*: b) -> e :*: (a :*: b)) -> (e :*: b) -> e :*: (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Accumulator e b -> e :*: b
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run Accumulator e b
y where
		k :: (s :*: s) -> (s :*: a) -> s :*: (s :*: a)
k ~(s
ex :*: s
x') ~(s
ey :*: a
y') = (s
ex s -> s -> s
forall a. Semigroup a => a -> a -> a
+ s
ey) s -> (s :*: a) -> s :*: (s :*: a)
forall s a. s -> a -> s :*: a
:*: s
x' s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
y'

instance Semigroup e => Bindable (->) (Accumulator e) where
	a -> Accumulator e b
f =<< :: (a -> Accumulator e b) -> Accumulator e a -> Accumulator e b
=<< Accumulator (e
e :*: a
x) = let e
e' :*: b
b = forall (t :: * -> *) a.
Interpreted (->) t =>
((->) < t a) < Primary t a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run @(->) (Accumulator e b -> e :*: b) -> Accumulator e b -> e :*: b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> Accumulator e b
f a
x in
		(e :*: b) -> Accumulator e b
forall e a. (e :*: a) -> Accumulator e a
Accumulator ((e :*: b) -> Accumulator e b) -> (e :*: b) -> Accumulator e b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- (e
e e -> e -> e
forall a. Semigroup a => a -> a -> a
+ e
e') e -> b -> e :*: b
forall s a. s -> a -> s :*: a
:*: b
b

type instance Schematic Monad (Accumulator e) = (<.:>) ((:*:) e)

instance Interpreted (->) (Accumulator e) where
	type Primary (Accumulator e) a = e :*: a
	run :: ((->) < Accumulator e a) < Primary (Accumulator e) a
run ~(Accumulator e :*: a
x) = Primary (Accumulator e) a
e :*: a
x
	unite :: ((->) < Primary (Accumulator e) a) < Accumulator e a
unite = ((->) < Primary (Accumulator e) a) < Accumulator e a
forall e a. (e :*: a) -> Accumulator e a
Accumulator

instance Monoid e => Monadic (->) (Accumulator e) where
	wrap :: ((->) < Accumulator e a) < (:>) (Accumulator e) u a
wrap = (<.:>) ((:*:) e) u a -> (:>) (Accumulator e) u a
forall (t :: * -> *) (u :: * -> *) a.
Schematic Monad t u a -> (:>) t u a
TM ((<.:>) ((:*:) e) u a -> (:>) (Accumulator e) u a)
-> (Accumulator e a -> (<.:>) ((:*:) e) u a)
-> ((->) < Accumulator e a) < (:>) (Accumulator e) u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((u :. (:*:) e) >>> a) -> (<.:>) ((:*:) e) u a
forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *)
       (a :: k).
((u :. t) >>> a) -> UT ct cu t u a
UT (((u :. (:*:) e) >>> a) -> (<.:>) ((:*:) e) u a)
-> (Accumulator e a -> (u :. (:*:) e) >>> a)
-> Accumulator e a
-> (<.:>) ((:*:) e) u a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (e :*: a) -> (u :. (:*:) e) >>> a
forall (t :: * -> *) a. Pointable t => a -> t a
point ((e :*: a) -> (u :. (:*:) e) >>> a)
-> (Accumulator e a -> e :*: a)
-> Accumulator e a
-> (u :. (:*:) e) >>> a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Accumulator e a -> e :*: a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
run

type Accumulated e t = Adaptable t (->) (Accumulator e)

gather :: Accumulated e t => e -> t ()
gather :: e -> t ()
gather e
x = ((->) < Accumulator e ()) < t ()
forall k k k (u :: k -> k) (m :: k -> k -> *) (t :: k -> k)
       (a :: k).
Adaptable u m t =>
(m < t a) < u a
adapt (((->) < Accumulator e ()) < t ())
-> ((e :*: ()) -> Accumulator e ()) -> (e :*: ()) -> t ()
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (e :*: ()) -> Accumulator e ()
forall e a. (e :*: a) -> Accumulator e a
Accumulator ((e :*: ()) -> t ()) -> (e :*: ()) -> t ()
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- e
x e -> () -> e :*: ()
forall s a. s -> a -> s :*: a
:*: ()