import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Map (Map)
import Data.Set (Set)
import Data.Maybe

data Formula = Or [Formula]
             | Not Formula
             | Var Char

type Assignment = Map Char Bool

type CNFFormula = [Assignment -> Bool]

satisfies :: Assignment -> CNFFormula -> Bool
satisfies = all . flip ($)

asCNF :: [Formula] -> CNFFormula
asCNF = map asMap
  where
    -- asMap :: Formula -> (Assignment -> Bool)
    asMap (Or xs) = \a -> any (($ a) . asMap) xs
    asMap (Not x) = \a -> not $ (asMap x) a
    asMap (Var x) = \a -> fromMaybe (error $ "Key " ++ [x] ++ " not in assignment") $ Map.lookup x a

keys :: Formula -> Set Char
keys (Or xs) = Set.unions $ map keys xs
keys (Not x) = keys x
keys (Var c) = Set.singleton c

doDPLL :: CNFFormula -> [Char] -> Maybe Assignment
doDPLL [] _ = Just Map.empty
doDPLL _ [] = Just Map.empty
doDPLL f keys = doDPLL' as f
  where
    as = map (Map.fromList . zip keys) . takeWhile ((== length keys) . length) . dropWhile ((< length keys) . length) $ bs
    bs = [[True], [False]] ++ [ head : tail | tail <- bs, head <- [True, False] ]
    doDPLL' [] f = Nothing
    doDPLL' (a:as) f
      | a `satisfies` f = Just a
      | otherwise = doDPLL' as f

main = do
  let
    fs = [ Var 'D'
         , Or [ Not $ Var 'D'
              , Not $ Var 'A'
              , Var 'B'
              ]
         , Or [ Not $ Var 'B'
              , Not $ Var 'E'
              ]
         , Or [ Var 'E'
              , Var 'A'
              , Not $ Var 'D'
              ]
         , Or [ Not $ Var 'F'
              , Var 'G'
              ]
         , Or [ Not $ Var 'G'
              , Not $ Var 'D'
              , Not $ Var 'C'
              ]
         , Or [ Var 'C'
              , Not $ Var 'H'
              ]
         , Or [ Var 'H'
              , Var 'F'
              ]
         , Or [ Var 'D'
              , Var 'A'
              , Var 'B'
              ]
         ]
  print $ doDPLL (asCNF fs) (Set.toList . Set.unions $ map keys fs)
  -- Just (fromList [('A',False),('B',False),('C',True),('D',True),('E',True),('F',False),('G',False),('H',True)])