module Pandora.Paradigm.Algebraic.Product where

import Pandora.Core.Functor (type (>>>>>>))
import Pandora.Pattern.Category ((<---))
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.Schemes.T_U (T_U (T_U), type (<:.:>), type (>:.:>), type (<:.:<), type (>:.:<))

infixr 7 :*:
infixr 5 <:*:>

-- TODO Define :*:*:, :*:*:*:, ...

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 >>>>>> (:*:)

(<:*:>) :: t a -> u a -> t <:*:> u >>>>>> a
<:*:> :: t a -> u a -> (t <:*:> u) >>>>>> a
(<:*:>) t a
xs u a
ys = (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
xs t a -> u a -> t a :*: u a
forall s a. s -> a -> s :*: a
:*: u a
ys