Set Theory Expression Simplification

{-# LANGUAGE UnicodeSyntax #-}

data RuleCondition =

Universal

| Empty

| Set String String

| Union RuleCondition RuleCondition

| Intersection RuleCondition RuleCondition

data Rule = Rule RuleCondition Int deriving (Show, Eq)

data RuleSet = RuleSet [Rule] Int deriving (Show, Eq)

isSubRC :: RuleCondition -> RuleCondition -> Bool

isSubRC x y = isSubRC' (simplifyrc x) (simplifyrc y)

where

isSubRC' Empty _ = True

isSubRC' _ Empty = False

isSubRC' _ Universal = True

isSubRC' Universal _ = False

isSubRC' (Set t v) (Set t' v') = t == t' && v == v'

isSubRC' (a `Intersection` b) (c `Intersection` d) = -- generally not comprehensive

(a `isSubRC` c || a `isSubRC` d) && ((b `isSubRC` c) || (b `isSubRC` d))

isSubRC' (a `Union` b) c = a `isSubRC` c && b `isSubRC` c

isSubRC' a (b `Union` c) = a `isSubRC` b || a `isSubRC` c

isSubRC' a (b `Intersection` c) = a `isSubRC` b && a `isSubRC` c

isSubRC' (a `Intersection` b) c = a `isSubRC` c || b `isSubRC` c

rcLength :: RuleCondition -> Int

rcLength Empty = 0

rcLength Universal = 1

rcLength (Set _ _) = 1

rcLength (Union a b) = rcLength a + rcLength b

rcLength (Intersection a b) = rcLength a + rcLength b

rcSmallest :: RuleCondition -> RuleCondition -> RuleCondition

rcSmallest a b =

if rcLength a <= rcLength b then a else simplifyrc b

instance Show RuleCondition where

show Empty = "∅"

show Universal = "Universal"

show (Set t v) = "Set \"" ++ t ++ "\" \"" ++ v ++ "\""

show (Union a b) = "(" ++ show a ++ " ∪ " ++ show b ++ ")"

show (Intersection a b) = "(" ++ show a ++ " ∩ " ++ show b ++ ")"

(∪), (∩) :: RuleCondition -> RuleCondition -> RuleCondition

(∅) :: RuleCondition

(∪) = Union

(∩) = Intersection

(∅) = Empty

simplifyrc :: RuleCondition -> RuleCondition

simplifyrc Empty = Empty

simplifyrc Universal = Universal

simplifyrc ( Universal `Union` _ ) = Universal

simplifyrc ( _ `Union` Universal) = Universal

simplifyrc ( Universal `Intersection` a ) = a

simplifyrc ( a `Intersection` Universal) = a

simplifyrc ( Empty `Intersection` _ ) = Empty

simplifyrc ( _ `Intersection` Empty ) = Empty

simplifyrc ( Empty `Union` a ) = a

simplifyrc ( a `Union` Empty ) = a

simplifyrc s@(Set _ _ ) = s

simplifyrc s@(Set t v `Union` Set t' v') | t == t' && v == v' = Set t v -- A ∪ A = A

| otherwise = s

simplifyrc s@(Set t v `Intersection` Set t' v') | t == t' && v == v' = Set t v -- A ∩ A = A

| t == t' && v /= v' = Empty

| otherwise = s

-- ^^ Rules

-- Simplification tricks:

-- Assosiative rule: A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)

simplifyrc expr@(a@(Set _ _) `Intersection` (b@(Set _ _) `Union` c@(Set _ _))) = -- trace ("\n A ∩ (B ∪ C): " ++ show expr ++ "\n") $

if a == b || a == c then a else -- A ∩ (A ∪ C) = A

rcSmallest expr $

simplifyrc (a `Intersection` b) `Union` simplifyrc (a `Intersection` c)

-- Assosiative rule: A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C)

simplifyrc expr@(a@(Set _ _) `Union` (c@(Set _ _) `Intersection` d@(Set _ _))) = -- trace ("A ∪ (B ∩ C): " ++ show expr ++ "\n") $

if c == a || d == a then a else -- A ∪ (A ∩ C) = A

rcSmallest expr $

simplifyrc (a `Union` c) `Intersection` simplifyrc (a `Union` d)

-- Assosiative rule inverse (with Set type): (A ∪ B) ∩ (A ∪ D) = A ∪ (B ∩ D)

simplifyrc expr@((a@(Set _ _) `Union` b@(Set _ _)) `Intersection` (c@(Set _ _) `Union` d@(Set _ _)) ) =

go where

go

| a == c = a `Union` simplifyrc (b `Intersection` d)

| a == d = a `Union` simplifyrc (b `Intersection` c)

| b == c = b `Union` simplifyrc (a `Intersection` d)

| b == d = b `Union` simplifyrc (a `Intersection` a)

| otherwise = expr

-- More generic rules over expressions:

-- Assosiative rule inverse: (A ∪ B) ∩ (A ∪ D) = A ∪ (B ∩ D)

simplifyrc expr@(l@(a `Union` b) `Intersection` r@(c `Union` d)) =

rcSmallest expr go

where

go | l' == r' = l

| a' == c' = a' `Union` simplifyrc (b' `Intersection` d')

| a' == d' = a' `Union` simplifyrc (b' `Intersection` c')

| b' == c' = b' `Union` simplifyrc (a' `Intersection` d')

| b' == d' = b' `Union` simplifyrc (a' `Intersection` c')

| otherwise = expr

a' = simplifyrc a

b' = simplifyrc b

c' = simplifyrc c

d' = simplifyrc d

l' = simplifyrc l

r' = simplifyrc r

-- Assosiative rule inverse: (A ∩ B) ∪ (A ∩ C) = A ∩ (B ∪ C)

simplifyrc expr@(l@(a `Intersection` b) `Union` r@(c `Intersection` d)) =

rcSmallest expr go

where

go | l' == r' = l'

| a' == c' = a' `Intersection` (b' `Union` d')

| a' == d' = a' `Intersection` (b' `Union` c')

| b' == c' = b' `Intersection` (a' `Union` d')

| b' == d' = b' `Intersection` (a' `Union` c')

| otherwise = expr

a' = simplifyrc a

b' = simplifyrc b

c' = simplifyrc c

d' = simplifyrc d

l' = simplifyrc l

r' = simplifyrc r

-- Distributive rule: (A ∩ B) ∩ (C ∩ D) = (A ∩ C) ∩ (B ∩ D)

simplifyrc expr@((a `Intersection` b) `Intersection` (c `Intersection` d)) =

rcSmallest expr $

simplifyrc (a `Intersection` c) `Intersection` simplifyrc (b `Intersection` d)

-- Distributive rule: A ∩ (B ∩ C) = (A ∩ B) ∩ C = (A ∩ C) ∩ B

simplifyrc (a `Intersection` r@(b `Intersection` c)) =

rcSmallest (a' `Intersection` r') $

rcSmallest

(simplifyrc (a' `Intersection` b') `Intersection` c')

(simplifyrc (a' `Intersection` c') `Intersection` b')

where

r' = simplifyrc r

a' = simplifyrc a

b' = simplifyrc b

c' = simplifyrc c

simplifyrc (r@(_ `Intersection` _) `Intersection` a) = simplifyrc $ a `Intersection` r

-- Distributive rule: (A ∪ B) ∪ (C ∪ D) = (A ∪ C) ∪ (B ∪ D)

simplifyrc expr@((a `Union` b) `Union` (c `Union` d)) =

rcSmallest expr $

simplifyrc (a `Union` c) `Union` simplifyrc (b `Union` d)

-- Distributive rule: A (B ∪ C) = (A ∪ B) ∪ C

simplifyrc (a `Union` r@(b `Union` c)) =

rcSmallest (a' `Union` r') $ simplifyrc (a' `Union` b') `Union` c'

where

r' = simplifyrc r

a' = simplifyrc a

b' = simplifyrc b

c' = simplifyrc c

-- A ∪ B =

-- | A ⊆ B = B

-- | B ⊆ A = A

-- | _ = A ∪ B

simplifyrc (a `Union` b) =

let a' = simplifyrc a

b' = simplifyrc b

in go a' b'

where

go a' b' | a' `isSubRC` b' = b'

| b' `isSubRC` a' = a'

| otherwise = a' `Union` b'

-- A ∩ B =

-- | A ⊆ B = A

-- | B ⊆ A = B

-- | _ = A ∩ B

simplifyrc (a `Intersection` b) = -- trace ("A ∩ B: " ++ show expr ++ "\n")

go where

go

| a `isSubRC` b = simplifyrc a

| b `isSubRC` a = simplifyrc b

| otherwise = simplifyrc a `Intersection` simplifyrc b

instance Eq RuleCondition where

a == b = a `isSubRC` b && b `isSubRC` a

affJB, osIOS, osAndroid, langEn, affSAM, jbOrIOS, jbOrSAMorIOS, opCelcom, jbAndIOS, jbAndIOSOrCelcom ::

RuleCondition

affJB = Set "Affiliate" "JB"

osIOS = Set "OS" "iOS"

osAndroid = Set "OS" "Android"

affSAM = Set "Affiliate" "SAM"

opCelcom = Set "Operator" "Celcom"

langEn = Set "Lang" "EN"

jbOrIOS = Union affJB osIOS

jbOrSAMorIOS = Union (Union affJB affSAM) osIOS

jbAndIOS = Intersection affJB osIOS

jbAndIOSOrCelcom = Union jbAndIOS jbAndIOSOrCelcom

main :: IO ()

main = do

testSimplifyRC (affJB `Intersection` affSAM) Empty

testSimplifyRC ((affJB ∪ osIOS) ∩ (affJB ∪ osIOS)) (affJB ∪ osIOS)

testSimplifyRC (affSAM `Intersection` (osIOS `Intersection` affJB)) Empty

testSimplifyRC ((osIOS `Intersection` affJB) `Intersection` affSAM) Empty

testSimplifyRC ((affJB `Intersection` osIOS) `Union` opCelcom)

((affJB `Intersection` osIOS) `Union` opCelcom)

testSimplifyRC

( affSAM

`Union` (affJB `Union` affSAM)

`Union` (affSAM `Union` affJB)

`Union` affJB

)

(affSAM `Union` affJB)

testSimplifyRC (jbAndIOS `Union` affJB) affJB

testSimplifyRC

((affJB `Intersection` opCelcom) `Union` (affJB `Intersection` opCelcom))

(affJB `Intersection` opCelcom)

testSimplifyRC ((affJB `Intersection` osIOS) `Intersection` osIOS)

(affJB `Intersection` osIOS)

testSimplifyRC

( (affJB `Intersection` osIOS `Intersection` opCelcom)

`Union` (affJB `Intersection` opCelcom)

)

(affJB `Intersection` opCelcom)

testSimplifyRC

((affJB ∪ osIOS) ∩ (osIOS ∪ opCelcom))

(osIOS ∪ (affJB ∩ opCelcom))

testSimplifyRC (osIOS `Intersection` (osIOS `Union` affJB)) osIOS

testSimplifyRC (osIOS `Intersection` (affJB `Union` osIOS)) osIOS

testSimplifyRC (((affJB ∩ osIOS) ∪ (affSAM ∩ osIOS)) ∪ (affJB ∪ affSAM) ∪ osIOS) (affJB ∪ affSAM ∪ osIOS)

testSimplifyRC ((affSAM `Intersection` osIOS) `Intersection` (affJB `Intersection` osIOS)) Empty

testSimplifyRC (osIOS ∩ (osAndroid ∪ affJB)) (osIOS ∩ affJB)

testSimplifyRC ((osIOS ∩ affJB) ∩ (langEn ∩ opCelcom)) ((osIOS ∩ affJB) ∩ (langEn ∩ opCelcom))

testSimplifyRC ((osIOS ∩ affJB) ∩ (osAndroid ∩ affSAM)) Empty

testSimplifyRC ((osIOS ∩ (affJB ∪ opCelcom)) ∪ (osAndroid ∩ (affJB ∪ opCelcom))) ((affJB ∪ opCelcom) ∩ (osIOS ∪ osAndroid))

where

testSimplifyRC expr expected = do

putStrLn "---"

putStrLn $ "simplify: " ++ show expr

let res = simplifyrc expr

putStrLn $ "result : { " ++ show res ++ " }"

putStrLn $ "expected: { " ++ show expected ++ " }"

print (res == expected)