-- Datentyp Formel (mit Typkonstruktoren T, F, Var, Not, Or, And)

data Formula = T | F | Var String | Not Formula | Or Formula Formula
             | And Formula Formula
   deriving (Eq, Show)


-- Vereinfachung von in der Formel auftretenden T und F

simplify :: Formula -> Formula
simplify T = T
simplify F = F
simplify (Var x) = (Var x)
simplify (Not f) =
  let f' = simplify f
  in if f' == T then F
     else if f' == F then T
          else Not f'
simplify (Or f g) =
  let f' = simplify f
      g' = simplify g
  in if f' == T || g' == T then T
     else if f' == F then g' 
          else if g' == F then f'
               else (Or f' g')
simplify (And f g) =
  let f' = simplify f
      g' = simplify g
  in if f' == F || g' == F then F
     else if f' == T then g' 
          else if g' == T then f'
               else (And f' g')


-- Negationsnormalform

-- a) fuer positive Formeln
nnf :: Formula -> Formula
nnf (Not f)   = negnnf f
nnf (Or f g)  = Or (nnf f) (nnf g)
nnf (And f g) = And (nnf f) (nnf g)
nnf f = f

-- b) fuer negative Formeln
negnnf :: Formula -> Formula
negnnf T = F
negnnf F = T
negnnf (Var x) = Not (Var x)
negnnf (Not f) = nnf f
negnnf (Or f g) = And (negnnf f) (negnnf g)
negnnf (And f g) = Or (negnnf f) (negnnf g)


-- Kombination aus Vereinfachung und NNF

snnf :: Formula -> Formula
snnf = nnf . simplify