{-# language FlexibleInstances, MultiParamTypeClasses #-}

module Ersatz.Relation.Op

( 
-- * Operations
  mirror
, union
, complement
, difference
, product, power
, intersection
, reflexive_closure
, symmetric_closure
)

where

import Ersatz.Relation.Data

import Prelude hiding ( and, or, not, product )
import Ersatz.Bit (and, or, not)

import Data.Ix

-- | Constructs the converse relation \( R^{-1} \subseteq B \times A \) of a relation 
-- \( R \subseteq A \times B \), which is defined by \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \).
mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a
mirror :: forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r =
    let ((a
a,b
b),(a
c,b
d)) = forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b
r
    in  forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ((b
b,a
a),(b
d,a
c)) forall a b. (a -> b) -> a -> b
$ do (a
x,b
y) <- forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r ; forall (m :: * -> *) a. Monad m => a -> m a
return ((b
y,a
x), Relation a b
rforall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a
x,b
y))

-- | Constructs the complement relation \( \overline{R} \) 
-- of a relation \( R \subseteq A \times B \), which is defined by 
-- \( \overline{R}  = \{ (x,y) \in A \times B ~|~ (x,y) \notin R \} \).
complement :: ( Ix a , Ix b ) => Relation a b -> Relation a b
complement :: forall a b. (Ix a, Ix b) => Relation a b -> Relation a b
complement Relation a b
r =
    forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build (forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b
r) forall a b. (a -> b) -> a -> b
$ do (a, b)
i <- forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r ; forall (m :: * -> *) a. Monad m => a -> m a
return ( (a, b)
i, forall b. Boolean b => b -> b
not forall a b. (a -> b) -> a -> b
$ Relation a b
rforall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a, b)
i )

-- | Constructs the difference \( R \setminus S \) of the relations 
-- \(R\) and \(S\), that contains all elements that are in \(R\) but not in \(S\), i.e.,
-- \( R \setminus S = \{ (x,y) \in R ~|~ (x,y) \notin S \} \).
--
-- Note that if \( R \subseteq A \times B \) and \( S \subseteq C \times D \),
-- then \( A \times B \) must be a subset of \( C \times D \) and
-- \( R \setminus S \subseteq A \times B \).
difference :: ( Ix a , Ix b )
        => Relation a b -> Relation a b ->  Relation a b
difference :: forall a b.
(Ix a, Ix b) =>
Relation a b -> Relation a b -> Relation a b
difference Relation a b
r Relation a b
s =
    forall a b.
(Ix a, Ix b) =>
Relation a b -> Relation a b -> Relation a b
intersection Relation a b
r forall a b. (a -> b) -> a -> b
$ forall a b. (Ix a, Ix b) => Relation a b -> Relation a b
complement Relation a b
s

-- | Constructs the union \( R \cup S \) of the relations \( R \) and \( S \).
--
-- Note that for \( R \subseteq A \times B \) and \( S \subseteq C \times D \),
-- it must hold that \( A \times B \subseteq C \times D \).
union :: ( Ix a , Ix b )
        => Relation a b -> Relation a b ->  Relation a b
union :: forall a b.
(Ix a, Ix b) =>
Relation a b -> Relation a b -> Relation a b
union Relation a b
r Relation a b
s =  forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ( forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b
r ) forall a b. (a -> b) -> a -> b
$ do
    (a, b)
i <- forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r
    forall (m :: * -> *) a. Monad m => a -> m a
return ((a, b)
i, forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
or [ Relation a b
rforall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a, b)
i, Relation a b
sforall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a, b)
i ] )

-- | Constructs the composition \( R \cdot S \) of the relations 
-- \( R \subseteq A \times B \) and \( S \subseteq B \times C \), which is 
-- defined by \( R \cdot S = \{ (a,c) ~|~ ((a,b) \in R) \land ((b,c) \in S) \} \).
product :: ( Ix a , Ix b, Ix c )
        => Relation a b -> Relation b c ->  Relation a c
product :: forall a b c.
(Ix a, Ix b, Ix c) =>
Relation a b -> Relation b c -> Relation a c
product Relation a b
a Relation b c
b =
    let ((a
ao,b
al),(a
au,b
ar)) = forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b
a
        ((b
_ ,c
bl),(b
_ ,c
br)) = forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation b c
b
        bnd :: ((a, c), (a, c))
bnd = ((a
ao,c
bl),(a
au,c
br))
    in  forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ((a, c), (a, c))
bnd forall a b. (a -> b) -> a -> b
$ do
          i :: (a, c)
i@(a
x,c
z) <- forall a. Ix a => (a, a) -> [a]
range ((a, c), (a, c))
bnd
          forall (m :: * -> *) a. Monad m => a -> m a
return ((a, c)
i, forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
or forall a b. (a -> b) -> a -> b
$ do
                b
y <- forall a. Ix a => (a, a) -> [a]
range ( b
al, b
ar )
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and [ Relation a b
aforall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a
x,b
y), Relation b c
bforall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(b
y,c
z) ]
                )

-- | Constructs the relation \( R^{n} \) that results if a relation
-- \( R \subseteq A \times A \) is composed \(n\) times with itself.
--
-- \( R^{0} \) is the identity relation \( I_{R} = \{ (x,x) ~|~ x \in A \} \) of \(R\).
power  :: ( Ix a  )
        => Int -- ^ \(n\)
        -> Relation a a -> Relation a a
power :: forall a. Ix a => Int -> Relation a a -> Relation a a
power Int
0 Relation a a
r = forall a. Ix a => ((a, a), (a, a)) -> Relation a a
identity ( forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
r )
power Int
1 Relation a a
r = Relation a a
r
power Int
e Relation a a
r =
    let (Int
d,Int
m) = forall a. Integral a => a -> a -> (a, a)
divMod Int
e Int
2
        s :: Relation a a
s = forall a. Ix a => Int -> Relation a a -> Relation a a
power Int
d Relation a a
r
        s2 :: Relation a a
s2 = forall a b c.
(Ix a, Ix b, Ix c) =>
Relation a b -> Relation b c -> Relation a c
product Relation a a
s Relation a a
s
    in  case Int
m of
        Int
0 -> Relation a a
s2
        Int
_ -> forall a b c.
(Ix a, Ix b, Ix c) =>
Relation a b -> Relation b c -> Relation a c
product Relation a a
s2 Relation a a
r

-- | Constructs the intersection \( R \cap S \) of the relations \( R \) and \( S \).
--
-- Note that for \( R \subseteq A \times B \) and \( S \subseteq C \times D \),
-- it must hold that \( A \times B \subseteq C \times D \).
intersection :: ( Ix a , Ix b)
      => Relation a b -> Relation a b
      -> Relation a b
intersection :: forall a b.
(Ix a, Ix b) =>
Relation a b -> Relation a b -> Relation a b
intersection Relation a b
r Relation a b
s = forall a b.
(Ix a, Ix b) =>
((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
build ( forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b
r ) forall a b. (a -> b) -> a -> b
$ do
        (a, b)
i <- forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r
        forall (m :: * -> *) a. Monad m => a -> m a
return ((a, b)
i, forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and [ Relation a b
rforall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a, b)
i, Relation a b
sforall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
!(a, b)
i ] )

-- | Constructs the reflexive closure \( R \cup I_{R} \) of the relation 
-- \( R \subseteq A \times A \), where \( I_{R} = \{ (x,x) ~|~ x \in A \} \) 
-- is the identity relation of \(R\).
reflexive_closure :: Ix a => Relation a a -> Relation a a
reflexive_closure :: forall a. Ix a => Relation a a -> Relation a a
reflexive_closure Relation a a
t =
    forall a b.
(Ix a, Ix b) =>
Relation a b -> Relation a b -> Relation a b
union Relation a a
t forall a b. (a -> b) -> a -> b
$ forall a. Ix a => ((a, a), (a, a)) -> Relation a a
identity forall a b. (a -> b) -> a -> b
$ forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
t

-- | Constructs the symmetric closure \( R \cup R^{-1} \) of the relation 
-- \( R \subseteq A \times A \), where \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \)
-- is converse relation of \(R\).
symmetric_closure :: Ix a => Relation a a -> Relation a a
symmetric_closure :: forall a. Ix a => Relation a a -> Relation a a
symmetric_closure Relation a a
r =
    forall a b.
(Ix a, Ix b) =>
Relation a b -> Relation a b -> Relation a b
union Relation a a
r forall a b. (a -> b) -> a -> b
$ forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a a
r