-- 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 19 : Checking Satisfiability

module Chap19_checking_satisfiability where

import Chap06_features_and_predicates (Thing)

import Chap16_expression_trees (Prop (Var, Not, (:||:), (:&&:)))

import Data.List (intercalate, intersperse, delete, sortOn)

import Data.Char (intToDigit)

-- Representing CNF

cnf = 
  (Not (Var "A") :||: Not (Var "B") :||: (Var "C"))
  :&&: (Not (Var "A") :||: (Var "D") :||: (Var "F"))
  :&&: ((Var "A") :||: (Var "B") :||: (Var "E"))
  :&&: ((Var "A") :||: (Var "B") :||: Not (Var "C"))

data Var = A | B | C | D | E | F | G | H
  deriving (Eq,Show)

data PredApp = IsDisc Thing
             | IsTriangle Thing
             | IsWhite Thing
             | IsBlack Thing
             | IsGrey Thing
             | IsBig Thing
             | IsSmall Thing
  deriving (Eq,Show)

data Literal atom = P atom | N atom
  deriving Eq

data Clause atom = Or [Literal atom]
  deriving Eq

c0 = Or [P A, N B, N C]

c1 = Or [N A]

c2 = Or []

data Form atom = And [Clause atom]
  deriving Eq

cnf' = 
  And [Or [N A, N B, P C],
       Or [N A, P D, P F],
       Or [P A, P B, P E],
       Or [P A, P B, N C]]

cnf'' = And [Or [P A, N B, N C], Or []] 

instance Show a => Show (Literal a) where
  show (P x) = show x
  show (N x) = "not " ++ 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)

-- The DPLL algorithm: implementation

(<<) :: Eq atom => [Clause atom] -> Literal atom -> [Clause atom]
cs << l = [ Or (delete (neg l) ls)
            | Or ls <- cs, not (l `elem` ls) ]

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

example1 = cnf'

example2 =
  And [Or [N A, P C, P D],
       Or [N B, P F, P D],
       Or [N B, N F, N C],
       Or [N D, N B],
       Or [P B, N C, N A],
       Or [P B, P F, P C],
       Or [P B, N F, N D],
       Or [P A, P E],
       Or [P A, P F],
       Or [N F, P C, N E],
       Or [P A, N C, N E]]

dpll :: Eq atom => Form atom -> [[Literal atom]]
dpll (And [])               = [[]]  -- one trivial solution
dpll (And (Or [] : cs))     = []    -- no solution
dpll (And (Or (l:ls) : cs)) =
  [ l : ls | ls <- dpll (And (cs << l)) ]
  ++
  [ neg l : ls | ls <- dpll (And (Or ls : cs << neg l)) ]

b1 = dpll example1

b2 = dpll example2

dpll' :: Eq atom => Form atom -> [[Literal atom]]
dpll' f =
  case prioritise f of
    []             -> [[]]  -- the trivial solution
    Or [] : cs     -> []    -- no solution
    Or (l:ls) : cs ->
      [ l : ls | ls <- dpll' (And (cs << l)) ]
      ++
      [ neg l : ls | ls <- dpll' (And (Or ls : cs << neg l)) ]

prioritise :: Form atom -> [Clause atom]
prioritise (And cs) = sortOn (\(Or ls) -> length ls) cs

b1' = dpll' example1

b2' = dpll' example2

-- Application: Sudoku

allFilled :: Form (Int,Int,Int)
allFilled = And [ Or [ P (i,j,n) | n <- [1..9] ]
                  | i <- [1..9], j <- [1..9] ]

noneFilledTwice :: Form (Int,Int,Int)
noneFilledTwice = And [ Or [ N (i, j, n), N (i, j, n') ]
                        | i <- [1..9], j <- [1..9],
                          n <- [1..9], n' <- [1..(n-1)]]

rowsComplete :: Form (Int,Int,Int)
rowsComplete = And [ Or [ P (i, j, n) | j <- [1..9] ]
                     | i <- [1..9], n <- [1..9] ]

columnsComplete :: Form (Int,Int,Int)
columnsComplete = undefined

squaresComplete :: Form (Int,Int,Int)
squaresComplete = undefined

sudokuProblem =
  And [Or [P (1,2,9)], Or [P (1,9,2)],
       Or [P (2,5,9)], Or [P (2,7,4)], Or [P (2,8,6)], Or [P (2,9,3)],
       Or [P (3,1,3)], Or [P (3,3,6)], Or [P (3,6,8)], Or [P (3,7,1)],
       Or [P (4,1,6)], Or [P (4,4,9)], Or [P (4,7,3)],
       Or [P (5,1,9)], Or [P (5,4,8)], Or [P (5,6,2)], Or [P (5,9,1)],
       Or [P (6,3,2)], Or [P (6,6,7)], Or [P (6,9,5)],
       Or [P (7,3,3)], Or [P (7,4,5)], Or [P (7,7,7)], Or [P (7,9,4)],
       Or [P (8,1,5)], Or [P (8,2,1)], Or [P (8,3,7)], Or [P (8,5,8)],
       Or [P (9,1,4)], Or [P (9,8,1)]]

(<&&>) :: Form a -> Form a  -> Form a  
And xs <&&> And ys = And ( xs ++ ys )

sudoku =
  allFilled <&&> noneFilledTwice <&&> rowsComplete
  <&&> columnsComplete <&&> squaresComplete
  <&&> sudokuProblem

rowsNoRepetition :: Form (Int,Int,Int)
rowsNoRepetition = And [ Or [ N (i, j, n), N (i, j', n) ]
                         | i <- [1..9], n <- [1..9],
                           j <- [1..9], j' <- [1..(j-1)] ]

columnsNoRepetition :: Form (Int,Int,Int)
columnsNoRepetition = undefined

squaresNoRepetition :: Form (Int,Int,Int)
squaresNoRepetition = undefined

sudoku' =
  allFilled <&&> noneFilledTwice <&&> rowsComplete
  <&&> columnsComplete <&&> squaresComplete
  <&&> sudokuProblem <&&> rowsNoRepetition
  <&&> columnsNoRepetition <&&> squaresNoRepetition

-- Pretty printing for Sudoku problems and solutions
--
-- printProblem sudokuProblem
--   pretty prints sudokuProblem
--
-- printAllSolutions sudokuProblem
--   pretty prints all solutions to sudokuProblem
-- 
-- printSolution . head . dpll' $ sudokuProblem
--   pretty prints the first solution to sudokuProblem

toLiterals :: Form atom -> [Literal atom]
toLiterals (And clauses) = concat $ map unpack clauses
    where unpack (Or literals) = literals
                                 
showSquares :: [Literal (Int,Int,Int)] -> String
showSquares lits =
  let pos = [ a | P a <- lits ]
  in
   [ (intToDigit.last) [ k | k <-[0..9]
                       , (i, j, k)`elem`pos || k == 0 ]
   | i <- [1..9], j <- [1..9] ]
  
-- | pretty takes an 81 digit string and presents it in sudoku form
-- using unicode -- suitable for putStrLn
pretty :: String -> String
pretty = ((tl++dsh++dn++dsh++dn++dsh++tr++"\n"++vt++" ")++)
         . (++(" "++vt++" \n"++bl++dsh++up++dsh++up++dsh++br))
         . intercalate (" "++vt++"\n"++vl++dsh++pl++dsh++pl++dsh++vr++" \n"++vt++" ")
         . map (intercalate (" "++vt++"\n"++vt++" ")) . byThree
         . map (intercalate (" "++vt++" ")). byThree
         . map (intersperse ' ')  . byThree
         . map (\d -> if d == '0' then '\x005F' else d)
  where
    byThree :: [a] -> [[a]]
    byThree (a : b : c : xs) = [a,b,c] : byThree xs
    byThree [] = []
    tl = "\x250F" -- topleft
    tr = "\x2513" -- topright
    bl = "\x2517" -- botleft
    br = "\x251B" -- botright
    dn = "\x2533"
    up = "\x253B"
    vl = "\x2523" -- vertleft
    vr = "\x252B" -- vertright
    vt = "\x2503" -- vertical
    pl = "\x254B" -- plus
    dsh = take 7 $ repeat '\x2501'
  
printProblem :: Form (Int, Int, Int) -> IO ()
printProblem = putStrLn . pretty . showSquares . toLiterals

printSolution :: [Literal (Int, Int, Int)] -> IO ()
printSolution = putStrLn . pretty . showSquares

printAllSolutions :: Form (Int, Int, Int) -> IO ()
printAllSolutions = mapM_ printSolution . dpll'