module Logic.Statement where

import Data.Set (singleton, union, toAscList)

data Statement
  = Atom String
  | Not Statement
  | And Statement Statement
  | Or Statement Statement
  | Implies Statement Statement
  | Iff Statement Statement
  deriving (Eq, Ord, Show)

atoms :: Statement -> [String]
atoms = toAscList . mkSet
  where
    mkSet (Atom key)      = singleton key
    mkSet (Not s)         = mkSet s
    mkSet (And s1 s2)     = union (mkSet s1) (mkSet s2)
    mkSet (Or s1 s2)      = union (mkSet s1) (mkSet s2)
    mkSet (Implies s1 s2) = union (mkSet s1) (mkSet s2)
    mkSet (Iff s1 s2)     = union (mkSet s1) (mkSet s2)

substatements :: Statement -> [Statement]
substatements s@(Atom _) = [s]
substatements s@(Not s1) = s:(substatements s1)
substatements s@(And s1 s2)     = (s:) $ substatements s1 ++ substatements s2
substatements s@(Or s1 s2)      = (s:) $ substatements s1 ++ substatements s2
substatements s@(Implies s1 s2) = (s:) $ substatements s1 ++ substatements s2
substatements s@(Iff s1 s2)     = (s:) $ substatements s1 ++ substatements s2

relabellings :: Statement -> Statement -> Bool
relabellings (Atom _) (Atom _) = True
relabellings (Not s1) (Not r1) = relabellings s1 r1
relabellings (And     s1 s2) (And     r1 r2) = relabellings s1 r1 && relabellings s2 r2
relabellings (Or      s1 s2) (Or      r1 r2) = relabellings s1 r1 && relabellings s2 r2
relabellings (Implies s1 s2) (Implies r1 r2) = relabellings s1 r1 && relabellings s2 r2
relabellings (Iff     s1 s2) (Iff     r1 r2) = relabellings s1 r1 && relabellings s2 r2
relabellings _ _ = False