module Pandora.Paradigm.Primary.Algebraic.Product where

import Pandora.Core.Functor (type (:=))
import Pandora.Pattern.Category (($), (#))
import Pandora.Pattern.Functor.Covariant (Covariant ((-<$>-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (multiply_))
import Pandora.Pattern.Functor.Extractable (Extractable (extract))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Functor.Bivariant (Bivariant ((<->)))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Pattern.Object.Ringoid (Ringoid ((*)))
import Pandora.Pattern.Object.Quasiring (Quasiring (one))
import Pandora.Pattern.Object.Semilattice (Infimum ((/\)), Supremum ((\/)))
import Pandora.Pattern.Object.Lattice (Lattice)
import Pandora.Pattern.Object.Group (Group (invert))
import Pandora.Paradigm.Primary.Transformer.Flip (Flip (Flip))
import Pandora.Paradigm.Schemes.T_U (T_U (T_U), type (<:.:>))

infixr 0 :*:

data (:*:) s a = s :*: a

instance Covariant ((:*:) s) (->) (->) where
	a -> b
f -<$>- :: (a -> b) -> (s :*: a) -> s :*: b
-<$>- s :*: a
x = (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> b -> s :*: b
forall s a. s -> a -> s :*: a
:*: a -> b
f (a -> b) -> a -> b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
x

instance Covariant (Flip (:*:) a) (->) (->) where
	a -> b
f -<$>- :: (a -> b) -> Flip (:*:) a a -> Flip (:*:) a b
-<$>- (Flip (a
x :*: a
y)) = (b :*: a) -> Flip (:*:) a b
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((b :*: a) -> Flip (:*:) a b) -> (b :*: a) -> Flip (:*:) a b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ a -> b
f a
x b -> a -> b :*: a
forall s a. s -> a -> s :*: a
:*: a
y

instance Extractable ((:*:) a) (->) where
	extract :: (a :*: a) -> a
extract ~(a
_ :*: a
y) = a
y

instance Extendable ((:*:) s) (->) where
	(s :*: a) -> b
f <<= :: ((s :*: a) -> b) -> (s :*: a) -> s :*: b
<<= s :*: a
x = (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> b -> s :*: b
forall s a. s -> a -> s :*: a
:*: (s :*: a) -> b
f ((s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
x)

instance Comonad ((:*:) s) (->) where

instance Bivariant (:*:) (->) (->) (->) where
	a -> b
f <-> :: (a -> b) -> (c -> d) -> (a :*: c) -> b :*: d
<-> c -> d
g = \ ~(a
s :*: c
x) -> a -> b
f a
s b -> d -> b :*: d
forall s a. s -> a -> s :*: a
:*: c -> d
g c
x

instance (Setoid s, Setoid a) => Setoid (s :*: a) where
	s :*: a
x == :: (s :*: a) -> (s :*: a) -> Boolean
== s :*: a
y = ((s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> s -> Boolean
forall a. Setoid a => a -> a -> Boolean
== (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
y) Boolean -> Boolean -> Boolean
forall a. Ringoid a => a -> a -> a
* ((s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
y)

instance (Semigroup s, Semigroup a) => Semigroup (s :*: a) where
	s :*: a
x + :: (s :*: a) -> (s :*: a) -> s :*: a
+ s :*: a
y = (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> s -> s
forall a. Semigroup a => a -> a -> a
+ (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
y s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
+ (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
y

instance (Monoid s, Monoid a) => Monoid (s :*: a) where
	zero :: s :*: a
zero = s
forall a. Monoid a => a
zero s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
forall a. Monoid a => a
zero

instance (Ringoid s, Ringoid a) => Ringoid (s :*: a) where
	s :*: a
x * :: (s :*: a) -> (s :*: a) -> s :*: a
* s :*: a
y = (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> s -> s
forall a. Ringoid a => a -> a -> a
* (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
y s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
x a -> a -> a
forall a. Ringoid a => a -> a -> a
* (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
y

instance (Quasiring s, Quasiring a) => Quasiring (s :*: a) where
	one :: s :*: a
one = s
forall a. Quasiring a => a
one s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
forall a. Quasiring a => a
one

instance (Infimum s, Infimum a) => Infimum (s :*: a) where
	s :*: a
x /\ :: (s :*: a) -> (s :*: a) -> s :*: a
/\ s :*: a
y = (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> s -> s
forall a. Infimum a => a -> a -> a
/\ (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
y s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
x a -> a -> a
forall a. Infimum a => a -> a -> a
/\ (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
y

instance (Supremum s, Supremum a) => Supremum (s :*: a) where
	s :*: a
x \/ :: (s :*: a) -> (s :*: a) -> s :*: a
\/ s :*: a
y = (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> s -> s
forall a. Supremum a => a -> a -> a
\/ (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
y s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
x a -> a -> a
forall a. Supremum a => a -> a -> a
\/ (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
y

instance (Lattice s, Lattice a) => Lattice (s :*: a) where

instance (Group s, Group a) => Group (s :*: a) where
	invert :: (s :*: a) -> s :*: a
invert s :*: a
x = s -> s
forall a. Group a => a -> a
invert (s -> s) -> s -> s
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (s :*: a) -> s
forall a b. (a :*: b) -> a
attached s :*: a
x s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a -> a
forall a. Group a => a -> a
invert (a -> a) -> a -> a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
# (s :*: a) -> a
forall (t :: * -> *) (source :: * -> * -> *) a.
Extractable t source =>
source (t a) a
extract s :*: a
x

instance {-# OVERLAPS #-} Semimonoidal t (->) (:*:) (:*:) => Semimonoidal (t <:.:> t := (:*:)) (->) (:*:) (:*:) where
	multiply_ :: ((:=) (t <:.:> t) (:*:) a :*: (:=) (t <:.:> t) (:*:) b)
-> (:=) (t <:.:> t) (:*:) (a :*: b)
multiply_ (T_U (t a
xls :*: t a
xrs) :*: T_U (t b
yls :*: t b
yrs)) = (t (a :*: b) :*: t (a :*: b)) -> (:=) (t <:.:> t) (:*:) (a :*: b)
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t (a :*: b) :*: t (a :*: b)) -> (:=) (t <:.:> t) (:*:) (a :*: b))
-> (t (a :*: b) :*: t (a :*: b))
-> (:=) (t <:.:> t) (:*:) (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ (t a :*: t b) -> t (a :*: b)
forall k (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (a :: k) (b :: k).
Semimonoidal t p source target =>
p (source (t a) (t b)) (t (target a b))
multiply_ (t a
xls t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yls) t (a :*: b) -> t (a :*: b) -> t (a :*: b) :*: t (a :*: b)
forall s a. s -> a -> s :*: a
:*: (t a :*: t b) -> t (a :*: b)
forall k (t :: k -> *) (p :: * -> * -> *) (source :: * -> * -> *)
       (target :: k -> k -> k) (a :: k) (b :: k).
Semimonoidal t p source target =>
p (source (t a) (t b)) (t (target a b))
multiply_ (t a
xrs t a -> t b -> t a :*: t b
forall s a. s -> a -> s :*: a
:*: t b
yrs)

delta :: a -> a :*: a
delta :: a -> a :*: a
delta a
x = a
x a -> a -> a :*: a
forall s a. s -> a -> s :*: a
:*: a
x

swap :: a :*: b -> b :*: a
swap :: (a :*: b) -> b :*: a
swap ~(a
x :*: b
y) = b
y b -> a -> b :*: a
forall s a. s -> a -> s :*: a
:*: a
x

attached :: a :*: b -> a
attached :: (a :*: b) -> a
attached ~(a
x :*: b
_) = a
x

twosome :: t a -> u a -> (<:.:>) t u (:*:) a
twosome :: t a -> u a -> (<:.:>) t u (:*:) a
twosome t a
x u a
y = (t a :*: u a) -> (<:.:>) t u (:*:) a
forall k k k k k (ct :: k) (cu :: k) (p :: k -> k -> *)
       (t :: k -> k) (u :: k -> k) (a :: k).
p (t a) (u a) -> T_U ct cu p t u a
T_U ((t a :*: u a) -> (<:.:>) t u (:*:) a)
-> (t a :*: u a) -> (<:.:>) t u (:*:) a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
$ t a
x t a -> u a -> t a :*: u a
forall s a. s -> a -> s :*: a
:*: u a
y