import Control.Monad
import qualified Data.Map as Map

-- funkcja umozliwajaca wpisanie znaku pomiedzy dwa inne
wpiszPomiedzy :: String -> String -> String
wpiszPomiedzy "" str = ""
wpiszPomiedzy [s] str = [s]
wpiszPomiedzy (p:r) str = [p] ++ str ++ wpiszPomiedzy r str


-- definicje uzywanych symboli logicznych
data Zdanie = Z Char
                | N Zdanie
                | K Zdanie Zdanie
                | A Zdanie Zdanie
                | C Zdanie Zdanie


znajdz :: (Eq z) => z -> [z] -> Bool
znajdz _ [] = False
znajdz z (p:r) = if p == z then True else znajdz z r

-- funkcja usuwajaca duplikaty danych
usun_duplikat :: (Eq z) => [z] -> [z]
usun_duplikat [] = []
usun_duplikat (p:r) = if znajdz p r then usun_duplikat r else  p : usun_duplikat r

-- przeladowanie show dla wypisania
instance Show Zdanie where
    show (Z c) = [c]
    show (N x) = show x
    show (K x y) = usun_duplikat (show x ++ show y)
    show (A x y) = usun_duplikat (show x ++ show y)
    show (C x y) = usun_duplikat (show x ++ show y)

-- Zadanie 1
-- funkcja pobiera zdanie i tworzy ciag znakow gotowy do wyswietlenia w postaci cztelnej dla uzytkownika
-- Z oznacza zmienna/znak N negacje K koniunkcja A alternatywa C implikacja
drukuj :: Zdanie -> String
drukuj (Z x) = [x]
drukuj (N x) = "~" ++ drukuj x
drukuj (K x y) = "(" ++ drukuj x ++ " & " ++ drukuj y ++ ")"
drukuj (A x y) = "(" ++ drukuj x ++ " | " ++ drukuj y ++ ")"
drukuj (C x y) = "(" ++ drukuj x ++ " => " ++ drukuj y ++ ")"

-- Zadanie 2
-- funkcja wypisuje zmienne
wypisz_zmienne :: Zdanie -> IO ()
wypisz_zmienne a = putStrLn ("[" ++ (wpiszPomiedzy (show a) ", " ) ++ "]")

-- Zadanie 3
-- funkcja podstawia zadane wartosci parametrow i sprawdza zgodnosc zdania
sprawdz :: Zdanie -> Map.Map Char Bool -> Bool
sprawdz (Z x) map = Map.findWithDefault False x map
sprawdz (N x) map = not(sprawdz x map)
sprawdz (K x y) map = (sprawdz x map) && (sprawdz y map)
sprawdz (A x y) map = (sprawdz x map) || (sprawdz y map)
sprawdz (C x y) map = not(sprawdz x map) || (sprawdz y map)

-- Zadanie 4.b
-- funkcja sprawdza czy zdanie jest tautologia poprzez
-- wygenerowanie kazdej mozliwej mapy z parametrami
-- a nastepnie podstawienie tej mapy i sprawdzenie czy zdanie zachodzi
jest_tautologia :: Zdanie -> Bool
jest_tautologia z = usun_duplikat (map (sprawdz z) (wygeneruj_kombinacje z)) == [True]

-- generowanie mozliwych przypadkow parametrow dla zdania
wygeneruj_kombinacje :: Zdanie -> [Map.Map Char Bool]
wygeneruj_kombinacje z = map (polacz_w_mape (show z)) (replicateM (length (show z)) [True, False]);

-- laczenie wartosci w mape wartosci bool
polacz_w_mape :: [Char] -> [Bool]  -> Map.Map Char Bool
polacz_w_mape chars bools = Map.fromList (zip chars bools)

-- Przykładowe dane
taut = A (Z 'p') (N (Z 'p'))
predykat = (C (N (Z 'p')) (A (K (Z 'p') (Z 'q')) (Z 'r')))
testMap = Map.fromList [('p', True), ('q', True), ('r', True)]
testMap2 = Map.fromList [('p', False), ('q', True), ('r', False)]
testMap3 = Map.fromList [('p', True), ('q', False), ('r', False)]

main = do
  print $ drukuj predykat
  wypisz_zmienne predykat
  print $ sprawdz predykat testMap
  print $ sprawdz predykat testMap2
  print $ sprawdz predykat testMap3
  print $ jest_tautologia taut