content: -- D. Sannella. M Fourman, H. Peng and P. Wadler
  -- Introduction to Computation: Haskell, Logic and Automata
  -- Undergraduate Topics in Computer Science, Springer (2021)
  -- ISBN 978-3-030-76907
  
  -- Chapter 22 : Efficient CNF Conversion
  
  module Chap22_efficient_CNF_conversion where
  
  import Data.List (nub)
  
  -- Implication and bi-implication
  
  type Name = String
  data Prop = Var Name
            | F
            | T
            | Not Prop
            | Prop :||: Prop
            | Prop :&&: Prop
            | Prop :->: Prop
            | Prop :<->: Prop
    deriving Eq
  
  instance Show Prop where
    show (Var x)    = x
    show F          = "F"
    show T          = "T"
    show (Not p)    = par ("not " ++ show p)
    show (p :||: q) = par (show p ++ " || " ++ show q)
    show (p :&&: q) = par (show p ++ " && " ++ show q)
  
  par :: String -> String
  par s = "(" ++ s ++ ")"
  
  type Valn = Name -> Bool
  
  evalProp :: Valn -> Prop -> Bool
  evalProp vn (Var x)    = vn x
  evalProp vn F          = False
  evalProp vn T          = True
  evalProp vn (Not p)    = not (evalProp vn p)
  evalProp vn (p :||: q) = evalProp vn p || evalProp vn q
  evalProp vn (p :&&: q) = evalProp vn p && evalProp vn q
  evalProp vn (p :->: q)  = not (evalProp vn p) || evalProp vn q
  evalProp vn (p :<->: q) = evalProp vn p == evalProp vn q
  
  type Names = [Name]
  
  names :: Prop -> Names
  names (Var x)     = [x]
  names F           = []
  names T           = []
  names (Not p)     = names p
  names (p :||: q)  = nub (names p ++ names q)
  names (p :&&: q)  = nub (names p ++ names q)
  names (p :->: q)  = nub (names p ++ names q)
  names (p :<->: q) = nub (names p ++ names q)
  
  
  