import Data.List hiding (find)

data Prop =
    Const  Bool       -- 恒真命題（T），恒偽命題（⊥）
  | Var    Char       -- 論理変数（ p, q, r, ...）
  | Not    Prop       -- ¬ x
  | And    Prop Prop  -- x ∧ y
  | Or     Prop Prop  -- x ∨ y
  | Xor    Prop Prop  -- x ⊕ y
  | NotBut Prop Prop  -- x < y
  | ButNot Prop Prop  -- x > y
  | Imply  Prop Prop  -- x ⇒ y
  | Equiv  Prop Prop  -- x ⇔ y
  deriving (Show)

xor :: Bool -> Bool -> Bool
True  `xor` True  = False
False `xor` False = False
_     `xor` _     = True

notbut :: Bool -> Bool -> Bool
x `notbut` y = not x && y

butnot :: Bool -> Bool -> Bool
x `butnot` y = x && not y

type Assoc k v = [(k,v)]
find :: Eq k => k -> Assoc k v -> v
find k t = head [ v | (k', v) <- t, k == k' ]

type Subst = Assoc Char Bool -- Assign（付値）

eval :: Subst -> Prop -> Bool
eval _ (Const b)    = b
eval s (Var x)      = find x s
eval s (Not p)      = not (eval s p)
eval s (And p q)    = eval s p && eval s q
eval s (Or p q)     = eval s p || eval s q
eval s (Xor p q)    = (eval s p) `xor` (eval s q)
eval s (NotBut p q) = (eval s p) `notbut` (eval s q)
eval s (ButNot p q) = (eval s p) `butnot` (eval s q)
eval s (Imply p q)  = not (eval s p) || (eval s p)
eval s (Equiv p q)  = (eval s p <= eval s q) && (eval s q <= eval s p)

vars :: Prop -> [Char]
vars (Const _)    = []
vars (Var x)      = [x]
vars (Not p)      = vars p
vars (And p q)    = vars p ++ vars q
vars (Or p q)     = vars p ++ vars q
vars (Xor p q)    = vars p ++ vars q
vars (NotBut p q) = vars p ++ vars q
vars (ButNot p q) = vars p ++ vars q
vars (Imply p q)  = vars p ++ vars q
vars (Equiv p q)  = vars p ++ vars q

bools :: Int -> [[Bool]]
bools 0 = [[]]
bools n = map (False:) bss ++ map (True:) bss
  where bss = bools (n-1)

rmdups :: Eq a => [a] -> [a]
rmdups [] = []
rmdups (x:xs) = x : rmdups (filter (/= x) xs)

substs :: Prop -> [Subst]
substs p = map (zip vs) (bools (length vs))
  where vs = rmdups (vars p)

-- isTautology :: Prop -> Bool
-- isTautology p = and [eval s p | s <- substs p]

-- isSatisfiable :: Prop -> Bool
-- isSatisfiable p = or [eval s p | s <- substs p]

mkTruethTable :: Prop -> String
mkTruethTable p = group4 $ map (\x -> if x then '1' else '0') [eval s p | s <- substs p]

group4 :: String -> String
group4 s
  | length s <= 4 = s
  | otherwise    = take 4 s ++ " " ++ group4 (drop 4 s)

s4 = And
     (And (Var '1') (Var '2'))
     (And (Var '3') (Var '4'))

s3 = Xor
     (And
      (And (Var '1') (Var '2'))
      (Or (Var '3') (Var '4')))
     (And
      (Or (Var '1') (Var '2'))
      (And (Var '3') (Var '4')))

s34 = And
      (Or
       (And (Var '1') (Var '2'))
       (And (Var '3') (Var '4')))
      (And
       (Or (Var '1') (Var '2'))
       (Or (Var '3') (Var '4')))

s2 = ButNot
     (Or
      (Xor (Var '1') (Var '3'))
      (Xor (Var '1') (Var '2')))
     (Xor
      (Xor (Var '1') (Var '2'))
      (Xor (Var '3') (Var '4')))

s24 = ButNot
     (Or
      (Or (Var '1') (Var '2'))
      (Var '3'))
     (Xor
      (Xor (Var '1') (Var '2'))
      (Xor (Var '3') (Var '4')))

s23 = Xor
      (ButNot
       (Xor
        (Xor (Var '1') (Var '2'))
        (Var '3'))
       (Xor (Var '3') (Var '4')))
      (Or (Var '1') (Var '2'))

s14 = Xor
      (And
       (Or (Var '1') (Var '2'))
       (Or (Var '3') (Var '4')))
      (Or
       (Xor (Var '1') (Var '2'))
       (Xor (Var '3') (Var '4')))

-- "0001011001101000" is the truth table for S2
printTables p = mapM_ print $ map mkTruethTable (props p)

data State' = N | Y deriving (Eq, Show)

data Prop' =
    Const'  Bool  State'
  | Var'    Char  State'
  | Not'    Prop'
  | And'    Prop' Prop'
  | Or'     Prop' Prop'
  | Xor'    Prop' Prop'
  | NotBut' Prop' Prop'
  | ButNot' Prop' Prop'
  | Imply'  Prop' Prop'
  | Equiv'  Prop' Prop'
  deriving (Show)

addState :: Prop -> Prop'
addState (Const b)    = Const' b N
addState (Var x)      = Var' x N
addState (Not p)      = Not' (addState p)
addState (And p q)    = And' (addState p) (addState q)
addState (Or p q)     = Or' (addState p) (addState q)
addState (Xor p q)    = Xor' (addState p) (addState q)
addState (NotBut p q) = NotBut' (addState p) (addState q)
addState (ButNot p q) = ButNot' (addState p) (addState q)
addState (Imply p q)  = Imply' (addState p) (addState q)
addState (Equiv p q)  = Equiv' (addState p) (addState q)

eraseState :: Prop' -> Prop
eraseState (Const' b s)  = Const b
eraseState (Var' x s)    = Var x
eraseState (Not' p)      = Not (eraseState p)
eraseState (And' p q)    = And (eraseState p) (eraseState q)
eraseState (Or' p q)     = Or (eraseState p) (eraseState q)
eraseState (Xor' p q)    = Xor (eraseState p) (eraseState q)
eraseState (NotBut' p q) = NotBut (eraseState p) (eraseState q)
eraseState (ButNot' p q) = ButNot (eraseState p) (eraseState q)
eraseState (Imply' p q)  = Imply (eraseState p) (eraseState q)
eraseState (Equiv' p q)  = Equiv (eraseState p) (eraseState q)

change :: Prop' -> Char -> Char -> Prop'
change (Const' b s)    _ _ = Const' b s
change (Var' x s)      y z
  | s == N    = if y == x then Var' z Y else Var' x s
  | otherwise = (Var' x s)
change (Not' p)      y z = Not' (change p y z)
change (And' p q)    y z = And' (change p y z) (change q y z)
change (Or' p q)     y z = Or' (change p y z) (change q y z)
change (Xor' p q)    y z = Xor' (change p y z) (change q y z)
change (NotBut' p q) y z = NotBut' (change p y z) (change q y z)
change (ButNot' p q) y z = ButNot' (change p y z) (change q y z)
change (Imply' p q)  y z = Imply' (change p y z) (change q y z)
change (Equiv' p q)  y z = Equiv' (change p y z) (change q y z)

changes :: Prop' -> String -> Prop'
changes x qs = changes' x ps qs
  where ps = take (length qs) ['1'..'9']

changes' :: Prop' -> String -> String -> Prop'
changes' x []     _      = x
changes' x (p:ps) (q:qs) = changes' (change x p q) ps qs

perm :: Prop -> String -> Prop
perm x ps = eraseState x''
  where x' = addState x
        x'' = changes x' ps

props :: Prop -> [Prop]
props p = [perm p s | s <- ps]
  where vs = (rmdups . vars) p
        ps = permutations vs