Conjunctive normal form (for seminar)

cnf.hs

data PropL = PVar String | PNot PropL | PropL `PAnd` PropL | PropL `POr` PropL deriving Eq

instance Show PropL where
    show (PVar s) = s
    show (PNot p) = "~" ++ show p
    show (p `PAnd` q) = "(" ++ show p ++ " & " ++ show q ++ ")"
    show (p `POr` q) = "(" ++ show p ++ " | " ++ show q ++ ")"
    
-- recursive de Morgan's

dM :: PropL -> PropL
dM (PNot (p `PAnd` q)) = PNot (dM p) `POr` PNot (dM q)
dM (PNot (p `POr` q)) = PNot (dM p) `PAnd` PNot (dM q)
dM (PNot p) = PNot (dM p)
dM (p `PAnd` q) = dM p `PAnd` dM q
dM (p `POr` q) = dM p `POr` dM q
dM (PVar p) = PVar p

-- recursive double-negation elimination

dne :: PropL -> PropL
dne (PNot (PNot p)) = dne p
dne (PNot p) = PNot (dne p)
dne (p `PAnd` q) = dne p `PAnd` dne q 
dne (p `POr` q) = dne p `POr` dne q 
dne (PVar p) = PVar p

-- recursive distributive laws

distLaw :: PropL -> PropL 
distLaw ((p `PAnd` q) `POr` (r `PAnd` s)) = (distLaw p `POr` distLaw r) `PAnd` (distLaw p `POr` distLaw s) `PAnd` (distLaw q `POr` distLaw r) `PAnd` (distLaw q `POr` distLaw s) -- double distributivity
distLaw (p `POr` (q `PAnd` r)) = (distLaw p `POr` distLaw q) `PAnd` (distLaw p `POr` r) --left dist
distLaw ((q `PAnd` r) `POr` p) = (distLaw q `POr` distLaw p) `PAnd` (distLaw r `POr` distLaw p) --right dist
distLaw (PNot p) = PNot (distLaw p)
distLaw (p `PAnd` q) = distLaw p `PAnd` distLaw q
distLaw (p `POr` q) = distLaw p `POr` distLaw q
distLaw (PVar p) = PVar p

-- CNF conversion

toCNF :: PropL -> PropL
toCNF = distLaw . dne . dM