{-# 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)