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 (mult))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
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.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Paradigm.Controlflow.Effect.Interpreted ((!))

infixr 1 :*:

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

instance Covariant (->) (->) ((:*:) s) where
	a -> b
f <-|- :: (a -> b) -> (s :*: a) -> s :*: b
<-|- ~(s
s :*: a
x) = s
s s -> b -> s :*: b
forall s a. s -> a -> s :*: a
:*: a -> b
f 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 :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
m (t a) (Primary t a)
! a -> b
f a
x b -> a -> b :*: a
forall s a. s -> a -> s :*: a
:*: a
y

instance Extendable (->) ((:*:) s) where
	(s :*: a) -> b
f <<= :: ((s :*: a) -> b) -> (s :*: a) -> s :*: b
<<= ~(s
s :*: a
x) = s
s s -> b -> s :*: b
forall s a. s -> a -> s :*: a
:*: (s :*: a) -> b
f (s
s s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x)

instance (Setoid s, Setoid a) => Setoid (s :*: a) where
	~(s
sx :*: a
x) == :: (s :*: a) -> (s :*: a) -> Boolean
== ~(s
sy :*: a
y) = (s
sx s -> s -> Boolean
forall a. Setoid a => a -> a -> Boolean
== s
sy) Boolean -> Boolean -> Boolean
forall a. Ringoid a => a -> a -> a
* (a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
y)

instance (Semigroup s, Semigroup a) => Semigroup (s :*: a) where
	~(s
sx :*: a
x) + :: (s :*: a) -> (s :*: a) -> s :*: a
+ ~(s
sy :*: a
y) = s
sx s -> s -> s
forall a. Semigroup a => a -> a -> a
+ s
sy s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
+ 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
sx :*: a
x) * :: (s :*: a) -> (s :*: a) -> s :*: a
* ~(s
sy :*: a
y) = s
sx s -> s -> s
forall a. Ringoid a => a -> a -> a
* s
sy s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x a -> a -> a
forall a. Ringoid a => a -> a -> a
* 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
sx :*: a
x) /\ :: (s :*: a) -> (s :*: a) -> s :*: a
/\ ~(s
sy :*: a
y) = s
sx s -> s -> s
forall a. Infimum a => a -> a -> a
/\ s
sy s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x a -> a -> a
forall a. Infimum a => a -> a -> a
/\ a
y

instance (Supremum s, Supremum a) => Supremum (s :*: a) where
	~(s
sx :*: a
x) \/ :: (s :*: a) -> (s :*: a) -> s :*: a
\/ ~(s
sy :*: a
y) = s
sx s -> s -> s
forall a. Supremum a => a -> a -> a
\/ s
sy s -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a
x a -> a -> a
forall a. Supremum a => a -> a -> a
\/ 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
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
s 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)
# a
x

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