module Pandora.Paradigm.Primary.Algebraic.Product where

import Pandora.Core.Functor (type (>))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
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.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Paradigm.Controlflow.Effect.Interpreted ()
import Pandora.Paradigm.Schemes.T_U (type (<:.:>), type (>:.:>), type (<:.:<), type (>:.:<))

infixr 8 :*:

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 (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 -> a -> s :*: a
forall s a. s -> a -> s :*: a
:*: a -> a
forall a. Group a => a -> a
invert 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

type (<:*:>) t u = t <:.:> u > (:*:)
type (>:*:>) t u = t >:.:> u > (:*:)
type (<:*:<) t u = t <:.:< u > (:*:)
type (>:*:<) t u = t >:.:< u > (:*:)