module Ersatz.Relation.Prop

( implies
, symmetric
, anti_symmetric
, transitive
, irreflexive
, reflexive
, regular
, regular_in_degree
, regular_out_degree
, max_in_degree
, min_in_degree
, max_out_degree
, min_out_degree
, empty
, complete
, total
, disjoint
, equals
)

where

import Prelude hiding ( and, or, not, product )
import Ersatz.Bit
import Ersatz.Relation.Data
import Ersatz.Relation.Op
import Ersatz.Counting

import Data.Ix

implies :: ( Ix a, Ix b )
        => Relation a b -> Relation a b -> Bit
implies :: Relation a b -> Relation a b -> Bit
implies Relation a b
r Relation a b
s = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and ([Bit] -> Bit) -> [Bit] -> Bit
forall a b. (a -> b) -> a -> b
$ do
    (a, b)
i <- Relation a b -> [(a, b)]
forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r
    Bit -> [Bit]
forall (m :: * -> *) a. Monad m => a -> m a
return (Bit -> [Bit]) -> Bit -> [Bit]
forall a b. (a -> b) -> a -> b
$ [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
or [ Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit) -> Bit -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a b
r Relation a b -> (a, b) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a, b)
i, Relation a b
s Relation a b -> (a, b) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a, b)
i ]

empty ::  ( Ix a, Ix b )
        => Relation a b -> Bit
empty :: Relation a b -> Bit
empty Relation a b
r = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and ([Bit] -> Bit) -> [Bit] -> Bit
forall a b. (a -> b) -> a -> b
$ do
    (a, b)
i <- Relation a b -> [(a, b)]
forall a b. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r
    Bit -> [Bit]
forall (m :: * -> *) a. Monad m => a -> m a
return (Bit -> [Bit]) -> Bit -> [Bit]
forall a b. (a -> b) -> a -> b
$ Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit) -> Bit -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a b
r Relation a b -> (a, b) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a, b)
i

complete :: (Ix a, Ix b) => Relation a b -> Bit
complete :: Relation a b -> Bit
complete Relation a b
r = Relation a b -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> Bit
empty (Relation a b -> Bit) -> Relation a b -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a b -> Relation a b
forall a b. (Ix a, Ix b) => Relation a b -> Relation a b
complement Relation a b
r

total :: ( Ix a) => Relation a a -> Bit
total :: Relation a a -> Bit
total Relation a a
r = Relation a a -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> Bit
complete (Relation a a -> Bit) -> Relation a a -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a a -> Relation a a
forall a. Ix a => Relation a a -> Relation a a
symmetric_closure Relation a a
r

disjoint :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
disjoint :: Relation a b -> Relation a b -> Bit
disjoint Relation a b
r Relation a b
s = Relation a b -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> Bit
empty (Relation a b -> Bit) -> Relation a b -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a b -> Relation a b -> Relation a b
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

equals :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
equals :: Relation a b -> Relation a b -> Bit
equals Relation a b
r Relation a b
s = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and [Relation a b -> Relation a b -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
implies Relation a b
r Relation a b
s, Relation a b -> Relation a b -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
implies Relation a b
s Relation a b
r]

symmetric :: ( Ix a) => Relation a a -> Bit
symmetric :: Relation a a -> Bit
symmetric Relation a a
r = Relation a a -> Relation a a -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
implies Relation a a
r ( Relation a a -> Relation a a
forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a a
r )

anti_symmetric :: ( Ix a) => Relation a a -> Bit
anti_symmetric :: Relation a a -> Bit
anti_symmetric Relation a a
r = Relation a a -> Relation a a -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
implies (Relation a a -> Relation a a -> Relation a a
forall a b.
(Ix a, Ix b) =>
Relation a b -> Relation a b -> Relation a b
intersection Relation a a
r (Relation a a -> Relation a a
forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a a
r)) (((a, a), (a, a)) -> Relation a a
forall a. Ix a => ((a, a), (a, a)) -> Relation a a
identity (Relation a a -> ((a, a), (a, a))
forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
r))

irreflexive :: ( Ix a ) => Relation a a -> Bit
irreflexive :: Relation a a -> Bit
irreflexive Relation a a
r = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and ([Bit] -> Bit) -> [Bit] -> Bit
forall a b. (a -> b) -> a -> b
$ do
    let ((a
a,a
_),(a
c,a
_)) = Relation a a -> ((a, a), (a, a))
forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
r
    a
x <- (a, a) -> [a]
forall a. Ix a => (a, a) -> [a]
range (a
a, a
c)
    Bit -> [Bit]
forall (m :: * -> *) a. Monad m => a -> m a
return (Bit -> [Bit]) -> Bit -> [Bit]
forall a b. (a -> b) -> a -> b
$ Bit -> Bit
forall b. Boolean b => b -> b
not (Bit -> Bit) -> Bit -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a a
r Relation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,a
x)

reflexive :: ( Ix a ) => Relation a a -> Bit
reflexive :: Relation a a -> Bit
reflexive Relation a a
r = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and ([Bit] -> Bit) -> [Bit] -> Bit
forall a b. (a -> b) -> a -> b
$ do
    let ((a
a,a
_),(a
c,a
_)) = Relation a a -> ((a, a), (a, a))
forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
r
    a
x <- (a, a) -> [a]
forall a. Ix a => (a, a) -> [a]
range (a
a,a
c)
    Bit -> [Bit]
forall (m :: * -> *) a. Monad m => a -> m a
return (Bit -> [Bit]) -> Bit -> [Bit]
forall a b. (a -> b) -> a -> b
$ Relation a a
r Relation a a -> (a, a) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,a
x)

regular, regular_in_degree, regular_out_degree, max_in_degree, min_in_degree, max_out_degree, min_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit

regular :: Int -> Relation a b -> Bit
regular Int
deg Relation a b
r = [Bit] -> Bit
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and [ Int -> Relation a b -> Bit
forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_in_degree Int
deg Relation a b
r, Int -> Relation a b -> Bit
forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_out_degree Int
deg Relation a b
r ]

regular_out_degree :: Int -> Relation a b -> Bit
regular_out_degree = (Int -> [Bit] -> Bit) -> Int -> Relation a b -> Bit
forall b b1 a t.
(Boolean b, Ix b1, Ix a) =>
(t -> [Bit] -> b) -> t -> Relation a b1 -> b
out_degree_helper Int -> [Bit] -> Bit
exactly
max_out_degree :: Int -> Relation a b -> Bit
max_out_degree = (Int -> [Bit] -> Bit) -> Int -> Relation a b -> Bit
forall b b1 a t.
(Boolean b, Ix b1, Ix a) =>
(t -> [Bit] -> b) -> t -> Relation a b1 -> b
out_degree_helper Int -> [Bit] -> Bit
atmost
min_out_degree :: Int -> Relation a b -> Bit
min_out_degree = (Int -> [Bit] -> Bit) -> Int -> Relation a b -> Bit
forall b b1 a t.
(Boolean b, Ix b1, Ix a) =>
(t -> [Bit] -> b) -> t -> Relation a b1 -> b
out_degree_helper Int -> [Bit] -> Bit
atleast
regular_in_degree :: Int -> Relation a b -> Bit
regular_in_degree Int
deg Relation a b
r = Int -> Relation b a -> Bit
forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_out_degree Int
deg (Relation b a -> Bit) -> Relation b a -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a b -> Relation b a
forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r
max_in_degree :: Int -> Relation a b -> Bit
max_in_degree Int
deg Relation a b
r = Int -> Relation b a -> Bit
forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
max_out_degree Int
deg (Relation b a -> Bit) -> Relation b a -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a b -> Relation b a
forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r
min_in_degree :: Int -> Relation a b -> Bit
min_in_degree Int
deg Relation a b
r = Int -> Relation b a -> Bit
forall a b. (Ix a, Ix b) => Int -> Relation a b -> Bit
min_out_degree Int
deg (Relation b a -> Bit) -> Relation b a -> Bit
forall a b. (a -> b) -> a -> b
$ Relation a b -> Relation b a
forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r

out_degree_helper ::
  (Boolean b, Ix b1, Ix a) =>
  (t -> [Bit] -> b) -> t -> Relation a b1 -> b
out_degree_helper :: (t -> [Bit] -> b) -> t -> Relation a b1 -> b
out_degree_helper t -> [Bit] -> b
f t
deg Relation a b1
r = [b] -> b
forall b (t :: * -> *). (Boolean b, Foldable t) => t b -> b
and ([b] -> b) -> [b] -> b
forall a b. (a -> b) -> a -> b
$ do
    let ((a
a,b1
b),(a
c,b1
d)) = Relation a b1 -> ((a, b1), (a, b1))
forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b1
r
    a
x <- (a, a) -> [a]
forall a. Ix a => (a, a) -> [a]
range ( a
a , a
c )
    b -> [b]
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> [b]) -> b -> [b]
forall a b. (a -> b) -> a -> b
$ t -> [Bit] -> b
f t
deg ([Bit] -> b) -> [Bit] -> b
forall a b. (a -> b) -> a -> b
$ do
        b1
y <- (b1, b1) -> [b1]
forall a. Ix a => (a, a) -> [a]
range (b1
b,b1
d)
        Bit -> [Bit]
forall (m :: * -> *) a. Monad m => a -> m a
return (Bit -> [Bit]) -> Bit -> [Bit]
forall a b. (a -> b) -> a -> b
$ Relation a b1
r Relation a b1 -> (a, b1) -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
! (a
x,b1
y)

transitive :: ( Ix a )
           => Relation a a -> Bit
transitive :: Relation a a -> Bit
transitive Relation a a
r = Relation a a -> Relation a a -> Bit
forall a b. (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
implies (Relation a a -> Relation a a -> Relation a a
forall a b c.
(Ix a, Ix b, Ix c) =>
Relation a b -> Relation b c -> Relation a c
product Relation a a
r Relation a a
r) Relation a a
r