module UVMHS.Core.Data.Pair where

import UVMHS.Core.Init
import UVMHS.Core.Classes

import UVMHS.Core.Data.Arithmetic ()

instance (POrd a,POrd b)  POrd (a  b) where 
  (a
x₁ :* b
y₁) ⊑ :: (a ∧ b) -> (a ∧ b) -> 𝔹
 (a
x₂ :* b
y₂) = (a
x₁ a -> a -> 𝔹
forall a. POrd a => a -> a -> 𝔹
 a
x₂) 𝔹 -> 𝔹 -> 𝔹
 (b
y₁ b -> b -> 𝔹
forall a. POrd a => a -> a -> 𝔹
 b
y₂)
instance (Bot a,Bot b)  Bot (a  b) where 
  bot :: a ∧ b
bot = a
forall a. Bot a => a
bot a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
forall a. Bot a => a
bot
instance (Join a,Join b)  Join (a  b) where 
  (a
a₁ :* b
b₁) ⊔ :: (a ∧ b) -> (a ∧ b) -> a ∧ b
 (a
a₂ :* b
b₂) = (a
a₁ a -> a -> a
forall a. Join a => a -> a -> a
 a
a₂) a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* (b
b₁ b -> b -> b
forall a. Join a => a -> a -> a
 b
b₂)
instance (Top a,Top b)  Top (a  b) where 
  top :: a ∧ b
top = a
forall a. Top a => a
top a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
forall a. Top a => a
top
instance (Meet a,Meet b)  Meet (a  b) where 
  (a
a₁ :* b
b₁) ⊓ :: (a ∧ b) -> (a ∧ b) -> a ∧ b
 (a
a₂ :* b
b₂) = (a
a₁ a -> a -> a
forall a. Meet a => a -> a -> a
 a
a₂) a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* (b
b₁ b -> b -> b
forall a. Meet a => a -> a -> a
 b
b₂)
instance (Dual a,Dual b)  Dual (a  b) where 
  dual :: (a ∧ b) -> a ∧ b
dual (a
a :* b
b) = a -> a
forall a. Dual a => a -> a
dual a
a a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b -> b
forall a. Dual a => a -> a
dual b
b
instance (Difference a,Difference b)  Difference (a  b) where 
  (a
a₁ :* b
b₁) ⊟ :: (a ∧ b) -> (a ∧ b) -> a ∧ b
 (a
a₂ :* b
b₂) = (a
a₁ a -> a -> a
forall a. Difference a => a -> a -> a
 a
a₂) a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* (b
b₁ b -> b -> b
forall a. Difference a => a -> a -> a
 b
b₂)
instance (JoinLattice a,JoinLattice b)  JoinLattice (a  b)
instance (MeetLattice a,MeetLattice b)  MeetLattice (a  b)
instance (Lattice a,Lattice b)  Lattice (a  b)

instance (Null a,Null b)  Null (a  b) where 
  null :: a ∧ b
null = (a
forall a. Null a => a
null a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
forall a. Null a => a
null)
instance (Append a,Append b)  Append (a  b) where 
  (a
x₁ :* b
y₁) ⧺ :: (a ∧ b) -> (a ∧ b) -> a ∧ b
 (a
x₂ :* b
y₂) = (a
x₁ a -> a -> a
forall a. Append a => a -> a -> a
 a
x₂) a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* (b
y₁ b -> b -> b
forall a. Append a => a -> a -> a
 b
y₂)
instance (Monoid a,Monoid b)  Monoid (a  b)

instance Functor ((∧) a) where 
  map :: forall a b. (a -> b) -> (a ∧ a) -> a ∧ b
map a -> b
f (a
x :* a
y) = a
x a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* a -> b
f a
y
instance (Null a)  Return ((∧) a) where 
  return :: forall a. a -> a ∧ a
return = a -> a -> a ∧ a
forall a b. a -> b -> a ∧ b
(:*) a
forall a. Null a => a
null
instance (Append a)  Bind ((∧) a) where 
  (a
a :* a
b) ≫= :: forall a b. (a ∧ a) -> (a -> a ∧ b) -> a ∧ b
≫= a -> a ∧ b
f = let (a
a' :* b
c) = a -> a ∧ b
f a
b in (a
a a -> a -> a
forall a. Append a => a -> a -> a
 a
a') a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
c
instance (Monoid a)  Monad ((∧) a)

instance FunctorM ((∧) a) where 
  mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> (a ∧ a) -> m (a ∧ b)
mapM a -> m b
f (a
x :* a
y) = (b -> a ∧ b) -> m b -> m (a ∧ b)
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
(:*) a
x) (m b -> m (a ∧ b)) -> m b -> m (a ∧ b)
forall a b. (a -> b) -> a -> b
$ a -> m b
f a
y

fst  a  b  a
fst :: forall a b. (a ∧ b) -> a
fst (a
x :* b
_) = a
x

snd  a  b  b
snd :: forall a b. (a ∧ b) -> b
snd (a
_ :* b
y) = b
y

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

mapPair  (a₁  a₂)  (b₁  b₂)  a₁  b₁  a₂  b₂
mapPair :: forall a₁ a₂ b₁ b₂.
(a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∧ b₁) -> a₂ ∧ b₂
mapPair a₁ -> a₂
f b₁ -> b₂
g (a₁
x :* b₁
y) = a₁ -> a₂
f a₁
x a₂ -> b₂ -> a₂ ∧ b₂
forall a b. a -> b -> a ∧ b
:* b₁ -> b₂
g b₁
y

mapBoth  (a  a')  a  a  a'  a'
mapBoth :: forall a a'. (a -> a') -> (a ∧ a) -> a' ∧ a'
mapBoth a -> a'
f = (a -> a') -> (a -> a') -> (a ∧ a) -> a' ∧ a'
forall a₁ a₂ b₁ b₂.
(a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∧ b₁) -> a₂ ∧ b₂
mapPair a -> a'
f a -> a'
f

mapFst  (a₁  a₂)  a₁  b  a₂  b
mapFst :: forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst a₁ -> a₂
f = (a₁ -> a₂) -> (b -> b) -> (a₁ ∧ b) -> a₂ ∧ b
forall a₁ a₂ b₁ b₂.
(a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∧ b₁) -> a₂ ∧ b₂
mapPair a₁ -> a₂
f b -> b
forall a. a -> a
id

mapSnd  (b₁  b₂)  a  b₁  a  b₂
mapSnd :: forall b₁ b₂ a. (b₁ -> b₂) -> (a ∧ b₁) -> a ∧ b₂
mapSnd b₁ -> b₂
f = (a -> a) -> (b₁ -> b₂) -> (a ∧ b₁) -> a ∧ b₂
forall a₁ a₂ b₁ b₂.
(a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∧ b₁) -> a₂ ∧ b₂
mapPair a -> a
forall a. a -> a
id b₁ -> b₂
f

mapMPair  (Monad m)  (a  m a')  (b  m b')  a  b  m (a'  b')
mapMPair :: forall (m :: * -> *) a a' b b'.
Monad m =>
(a -> m a') -> (b -> m b') -> (a ∧ b) -> m (a' ∧ b')
mapMPair a -> m a'
f b -> m b'
g (a
x :* b
y) = do
  a'
x'  a -> m a'
f a
x
  b'
y'  b -> m b'
g b
y
  (a' ∧ b') -> m (a' ∧ b')
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((a' ∧ b') -> m (a' ∧ b')) -> (a' ∧ b') -> m (a' ∧ b')
forall a b. (a -> b) -> a -> b
$ a'
x' a' -> b' -> a' ∧ b'
forall a b. a -> b -> a ∧ b
:* b'
y'

mapMBoth  (Monad m)  (a  m a)  a  a  m (a  a)
mapMBoth :: forall (m :: * -> *) a.
Monad m =>
(a -> m a) -> (a ∧ a) -> m (a ∧ a)
mapMBoth a -> m a
f = (a -> m a) -> (a -> m a) -> (a ∧ a) -> m (a ∧ a)
forall (m :: * -> *) a a' b b'.
Monad m =>
(a -> m a') -> (b -> m b') -> (a ∧ b) -> m (a' ∧ b')
mapMPair a -> m a
f a -> m a
f

mapMFst  (Monad m)  (a  m a')  a  b  m (a'  b)
mapMFst :: forall (m :: * -> *) a a' b.
Monad m =>
(a -> m a') -> (a ∧ b) -> m (a' ∧ b)
mapMFst = ((a -> m a') -> (b -> m b) -> (a ∧ b) -> m (a' ∧ b))
-> (b -> m b) -> (a -> m a') -> (a ∧ b) -> m (a' ∧ b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m a') -> (b -> m b) -> (a ∧ b) -> m (a' ∧ b)
forall (m :: * -> *) a a' b b'.
Monad m =>
(a -> m a') -> (b -> m b') -> (a ∧ b) -> m (a' ∧ b')
mapMPair b -> m b
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return

mapMSnd  (Monad m)  (b  m b')  a  b  m (a  b')
mapMSnd :: forall (m :: * -> *) b b' a.
Monad m =>
(b -> m b') -> (a ∧ b) -> m (a ∧ b')
mapMSnd = (a -> m a) -> (b -> m b') -> (a ∧ b) -> m (a ∧ b')
forall (m :: * -> *) a a' b b'.
Monad m =>
(a -> m a') -> (b -> m b') -> (a ∧ b) -> m (a' ∧ b')
mapMPair a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return