Lab5

import Data.List
import qualified Data.Map.Strict as Map

main = do
       print $ shipCovering $ ship [(0,0,SoundCell),(1,0,SoundCell)]
       print $ goodPosition $ map ship [[(0,0,SoundCell)],[(0,2,SoundCell)],[(0,4,SoundCell)],[(0,6,SoundCell)],
                                        [(2,0,SoundCell),(3,0,SoundCell)],[(2,2,SoundCell),(3,2,SoundCell)],[(2,4,SoundCell),(3,4,SoundCell)],
                                        [(5,0,SoundCell),(6,0,SoundCell),(7,0,SoundCell)],[(5,2,SoundCell),(6,2,SoundCell),(7,2,SoundCell)],
                                        [(9,0,SoundCell),(9,1,SoundCell),(9,2,SoundCell),(9,3,SoundCell)]]
       print $ vars $ (Inv (c :&& b)) :&& (a :|| b)
       print $ tautology (Inv ((a :&& b) :&& ((Inv a) :|| (Inv b))))
       where a = Var "a"
             b = Var "b"
             c = Var "c"

data Cell = Cell Int Int deriving (Show,Eq)
data CellCondition = DeadCell | HarmedCell | SoundCell deriving (Show,Eq)
newtype Ship = Ship [(Cell,CellCondition)] deriving (Show,Eq)
data TurnResult = Miss | Harmed | Dead | Already deriving (Show,Eq)

ship :: [(Int,Int,CellCondition)] -> Ship
ship = Ship . map (\(a,b,c) -> (Cell a b, c))

unship :: Ship -> [(Cell,CellCondition)]
unship (Ship xs) = xs

cell :: (Int,Int) -> Cell
cell = uncurry Cell

uncell :: Cell -> (Int,Int)
uncell (Cell a b) = (a,b)

hasCell :: Ship -> Cell -> Bool
hasCell s c = c `elem` (getShipCells s)

goodPos :: (Int,Int) -> Bool
goodPos (x,y) = x>=0 && x<=9 && y>=0 && y<=9

goodShipPos :: Ship -> Bool
goodShipPos = (all (goodPos . uncell)) . getShipCells

getShipCells :: Ship -> [Cell]
getShipCells (Ship xs) = map fst xs

covering :: Cell -> [Cell]
covering (Cell a b) = map cell $ filter goodPos xs
                      where xs = [(a-1,b-1),
                                  (a-1,b),
                                  (a-1,b+1),
                                  (a,b-1),
                                  (a,b),
                                  (a,b+1),
                                  (a+1,b-1),
                                  (a+1,b),
                                  (a+1,b+1)]

shipCovering :: Ship -> [Cell]
shipCovering = nub . (concatMap covering) . getShipCells

shipDegree :: Ship -> Int
shipDegree = length . getShipCells

checkDegrees :: [Ship] -> Bool
checkDegrees ss = all (\n -> 5-n == degreeCount n) [1..4]
                  where degreeCount n = length $ filter (\s -> shipDegree s == n) ss

remove :: (Eq a) => a -> [a] -> [a]
remove _ [] = []
remove x (y:ys) = if x == y then ys else y : (remove x ys)

goodPair :: Ship -> Ship -> Bool
goodPair a b = null $ intersect (shipCovering a) (getShipCells b)

goodPosition :: [Ship] -> Bool
goodPosition ss = all goodShipPos ss && (checkDegrees ss) && (and $ [goodPair x y | x <- ss, y <- ss, x /= y])

doTurn :: [Ship] -> Cell -> (TurnResult,[Ship])
doTurn ss c = case s of
              Nothing -> (Miss,ss)
              (Just oldShip) -> helper oldShip
              where s = find (flip hasCell c) ss
                    helper oldShip = (res,newShips)
                                     where (Just (cc,cond)) = find (\(a,_) -> a == c) (unship oldShip)
                                           newShips = replace oldShip newShip ss
                                           newShip = Ship $ replace (cc,cond) (cc,newCond) (unship oldShip)
                                           newCond = case cond of
                                                     SoundCell -> HarmedCell
                                                     HarmedCell -> DeadCell
                                                     DeadCell -> DeadCell
                                           res = case cond of
                                                     SoundCell -> Harmed
                                                     HarmedCell -> Dead
                                                     DeadCell -> Already
                                           replace y x xs = y : (remove x xs)


data Prop = Var String | (:&&) Prop Prop | (:||) Prop Prop | Inv Prop

vars :: Prop -> [String]
vars (Var s) = [s]
vars (p1 :&& p2) = nub $ vars p1 ++ vars p2
vars (p1 :|| p2) = nub $ vars p1 ++ vars p2
vars (Inv p) = vars p

truthValue :: Prop -> [(String,Bool)] -> Bool
truthValue p a = evaluate p (Map.fromList a)

evaluate :: Prop -> (Map.Map String Bool) -> Bool
evaluate (Var s) a = a Map.! s
evaluate (p1 :&& p2) a = (evaluate p1 a) && (evaluate p2 a)
evaluate (p1 :|| p2) a = (evaluate p1 a) || (evaluate p2 a)
evaluate (Inv p) a = not $ evaluate p a

arrange2 :: a -> a -> Int -> [[a]]
arrange2 x y n = foldl (\acc _ -> map (x :) acc ++ (map (y :) acc)) [[]] [1..n]

tautology :: Prop -> Bool
tautology p = all (\a -> truthValue p a) assignments
              where vs = vars p
                    vsl = length vs
                    assignments = map (\bs -> zip vs bs) $ arrange2 True False vsl