import Data.List

-- [ The following lines code our language of forms ]
    
data Literal atom = P atom | N atom
                    deriving Eq

data Clause atom = Or [Literal atom]
                   deriving Eq

data Form atom = And [Clause atom]
                 deriving Eq

neg :: Literal atom -> Literal atom
neg (P a) = N a
neg (N a) = P a                          

-- this prints formulae in a prettier way

instance Show a => Show (Literal a) where
  show (P x) = show x
  show (N x) = "¬" ++ show x

instance Show a => Show (Clause a) where
  show (Or ls) = "(" ++ intercalate " || " (map show ls) ++ ")"

instance Show a => Show (Form a) where
  show (And ls) = intercalate " && " (map show ls)
  -- intercalate is from Data.List, and prints its
  -- first argument between the elements of the second

-- atoms for the simple case

data Atom = A|B|C|D|W|X|Y|Z deriving (Eq,Show)
 -- we have to be able to compare atomes

-- example from slides
eg = And[ Or[N A, N C, P D], Or[P A, P C], Or[N D] ]

-- valuations
data Val atom = Val [ Literal atom ] deriving (Eq,Show)

-- check valuation for consistency
isConsistent (Val []) = True
isConsistent (Val (l : ls)) =
  not(neg l `elem` ls) && isConsistent (Val ls)

-- evaluating formulae

-- eval (Val tls) (And cs) =
--  and [ or [ l `elem` tls | l <- c ] | Or c <- cs ]

eval (Val true_literals) (And clauses) =
  and [ or [ literal `elem` true_literals 
             | literal <- clause ] | Or clause <- clauses ]

-- eval (Val []) eg
  -- False

-- eval (Val [N C, P A, N D]) eg
  -- True

-- (very) brute force search for satisfying assignments

-- given a list of atoms, return a list of all possible
-- complete valuations of those atoms (forgetting the Val)
allValns :: [a] -> [[Literal a]]
allValns [] = [[]]
allValns (atom : atoms) =
  (map (P atom :) (allValns atoms)) ++ (map (N atom :) (allValns atoms))

-- return all atoms in a formula, deduplicated
atomsOf (And clauses) =
  nub ((map atomize (foldr (\ (Or x) y -> x++y) [] clauses)))
  where atomize (N a) = a
        atomize (P a) = a

-- given formula, return satisfying valuations
allSatisValns :: Eq a => Form a -> [Val a]
allSatisValns f = filter (\v->eval v f) (map Val (allValns (atomsOf f)))