module Main where
import Data.Maybe
import DS
import Grammar
import Tokens
import System (getArgs)

main :: IO ()
main = do
    input <- getLine
    let prob = Problem [] (parse $ alexScanTokens $ input)
    putStr $ output $ solve $ prob

done :: Prob -> Bool
done (Problem _ dis) = (forall dis disdone) && (cansolve dis) 

disdone :: Conjuct -> Bool
disdone a = forall a condone 

condone :: Varible -> Bool
condone Tru = True
condone Fals = True
condone (Var _) = False
condone (NotVar _) = False

cansolve' :: Prob -> Bool
cansolve' (Problem _ dis) = cansolve dis

cansolve :: Disjuct-> Bool
cansolve dis = forall dis cansolvedis 

cansolvedis :: Conjuct -> Bool
cansolvedis con = exists con notFalse 

notFalse :: Varible -> Bool
notFalse Tru = True
notFalse (Var _) = True
notFalse Fals = False
notFalse (NotVar _) = True

solve :: Prob -> Maybe Prob 
solve a 
      | (done a) = Just a
      | (cansolve' a) = solve' a
      | otherwise = Nothing

solve' :: Prob -> Maybe Prob
solve' a 
    | isJust (solve (mkAssumption a True)) =   (solve (mkAssumption a True))
    | isJust (solve (mkAssumption a False)) = (solve (mkAssumption a False))
    | otherwise = Nothing

assume :: Prob ->Bool->Bool
assume p b = cansolve' (mkAssumption p b)

mkAssumption :: Prob ->Bool-> Prob
mkAssumption (Problem ass dis) val = Problem (ass++[Ass (findVar dis) val]) (setdis dis (findVar dis) val ) 

setdis :: Disjuct -> String -> Bool ->Disjuct
setdis []  _ _ = []
setdis (x:xs) str bool = [(setCon x str bool)] ++ setdis xs str bool

setCon :: Conjuct -> String -> Bool -> Conjuct
setCon [] _ _ = []
setCon (x:xs) str bool = [(setVar x str bool )]++setCon xs str bool

setVar :: Varible -> String -> Bool -> Varible
setVar Tru _ _ = Tru
setVar Fals _ _  = Fals
setVar (Var strr) str bool 
       | ((strr==str) && (bool)) = Tru
       | (strr==str) = Fals
       | otherwise = Var strr 
setVar (NotVar strr) str bool
       | ((strr==str) && (bool)) = Fals
       | (strr==str) = Tru
       | otherwise = NotVar strr
       
findVar :: Disjuct -> String
findVar dis = maxvar $ count $ map fromVar $ filter isVar $ foldl (++) [] dis  

isVar :: Varible -> Bool
isVar (NotVar _) = True
isVar (Var _ ) = True
isVar _ = False

fromVar :: Varible -> String
fromVar (NotVar a) = a
fromVar (Var a) = a
fromVar _ = error "fukcup in fromVar"

maxvar :: [(Int, a)] -> a
maxvar input = fromJust $ lookup ( max' 0 input) input

max' :: Int->[(Int, a)]->Int
max' int [] =  int
max' int ((x,y):ys) 
    | (x>int) = max' x ys
    | otherwise = max' int ys 

count :: Eq a => [a] -> [(Int, a)]
count input = count' input []     

count' :: Eq a => [a] -> [(Int, a)]->[(Int, a)]
count' [] a = a
count' (x:xs) a = count' xs $ insert x a

insert :: Eq a => a->[(Int, a)]->[(Int,a)]
insert a [] = [(1, a)]
insert a ((y, x):xs) 
    | (a==x) = [(y+1, x)]++xs
    | otherwise = [(y, x)]++insert a xs

exists :: [a] -> (a->Bool)->Bool
exists [a] f = f a
exists (x:xs) f = f x || any f xs         

forall :: [a] -> (a->Bool) -> Bool
forall [a] f = f a
forall (x:xs) f = f x && forall xs f 

output :: Maybe Prob -> String
output Nothing = "Problem is unsolvable\n"
output (Just (Problem ass _)) = foldl (++) [] $ map outputAss ass 

outputAss :: Assumption -> String
outputAss (Ass str bool ) = str ++ ": " ++ (show bool)++"\n"