module Logic where
import Data.List
{-====================================================
=================== Aussagenlogik ====================
====================================================-}
dict2func :: (Eq a) => [(a,b)] -> (a -> b)
dict2func d = \x -> (head [b |(a,b)<-d, a==x ])

type Binary = [Int]

toBin :: Int -> Binary
toBin 0 = [0]
toBin 1 = [1]
toBin n
    | n `mod` 2 == 0 = toBin (n `div` 2) ++ [0]
    | otherwise = toBin (n `div` 2) ++ [1]

bloatBin :: Int -> Binary -> Binary
bloatBin n x
    | n==(length x) = x
    | otherwise = [0| i<-[1..n-(length x)]] ++ x

type Belegung = Char -> Bool
data Formel = TAUTO
            | ABSURD
            | Atom Char 
            | NOT Formel
            | Formel `OR` Formel
            | Formel `AND` Formel
            | Formel `THEN` Formel
            | Formel `EQUY` Formel
            | Formel `XOR` Formel

instance Show Formel where
    show TAUTO = "T" 
    show ABSURD = "_|_"
    show (Atom a) = [a] 
    show (NOT f) = "(-"++(show f)++")"
    show (a `AND` b) = "("++(show a)++"^"++(show b)++")"
    show (a `OR` b) = "("++(show a)++"v"++(show b)++")"
    show (a `THEN` b) = "("++(show a)++"=>"++(show b)++")"
    show (a `EQUY` b) = "("++(show a)++"<=>"++(show b)++")"
    show (a `XOR` b) = "("++(show a)++"<x>"++(show b)++")"

noArrows :: Formel -> Formel
noArrows TAUTO = TAUTO
noArrows ABSURD = ABSURD
noArrows (Atom a) = Atom a
noArrows (NOT a) = NOT $ noArrows a
noArrows (a `AND` b) = (noArrows a) `AND` (noArrows b)
noArrows (a `OR` b) = (noArrows a) `OR` (noArrows b)
noArrows (a `THEN` b) = (NOT $ noArrows a) `OR` noArrows b
noArrows (a `EQUY` b) = (noArrows $ a `THEN` b) `AND` (noArrows $ b `THEN` a)

nnf :: Formel -> Formel
nnf TAUTO = TAUTO
nnf ABSURD = ABSURD
nnf (Atom a) = Atom a             --literal pos
nnf (NOT (Atom a)) = NOT (Atom a) --literal neg
nnf (NOT TAUTO) = ABSURD
nnf (NOT ABSURD) = TAUTO
nnf (NOT (NOT f)) = nnf f --double neg
nnf (a `AND` b) = (nnf a) `AND` (nnf b)
nnf (a `OR` b) = (nnf a) `OR` (nnf b)
nnf (NOT (a `OR` b)) = (nnf $ NOT a) `AND` (nnf $ NOT b) --deMorgan 1
nnf (NOT (a `AND` b)) = (nnf $ NOT a) `OR` (nnf $ NOT b) --deMorgan 2
nnf (a `THEN` b) = nnf $ noArrows $ a `THEN` b             --remove arrows
nnf (a `EQUY` b) = nnf $ noArrows $ a `EQUY` b             --remove arrows
nnf (NOT (a `THEN` b)) = nnf $ NOT $ noArrows $ a `THEN` b --remove arrows
nnf (NOT (a `EQUY` b)) = nnf $ NOT $ noArrows $ a `EQUY` b --remove arrows

evalform :: Formel -> Belegung -> Bool
evalform TAUTO _ = True
evalform ABSURD _ = False
evalform (Atom a) f = f a
evalform (NOT a) f = not (evalform a f)
evalform (a `AND` b) f = (evalform a f) && (evalform b f)
evalform (a `OR` b) f = (evalform a f) || (evalform b f)
evalform (a `THEN` b) f = evalform (noArrows $ a `THEN` b) f
evalform (a `EQUY` b) f = evalform (noArrows $ a `EQUY` b) f

formLen :: Formel -> Int
formLen ABSURD = 1
formLen TAUTO = 1
formLen (Atom c) = 1
formLen (NOT a) = 1 + (formLen a)
formLen (a `AND` b) = (formLen a) + 1 + (formLen b)
formLen (a `OR` b) = (formLen a) + 1 + (formLen b)
formLen (a `THEN` b) = formLen $ noArrows $ a `THEN` b
formLen (a `EQUY` b) = formLen $ noArrows $ a `EQUY` b

atoms :: Formel -> [Char]
atoms ABSURD = []
atoms TAUTO = []
atoms (Atom c) = [c]
atoms (NOT a) = atoms a
atoms (a `AND` b) = (atoms a) `union` (atoms b)
atoms (a `OR` b) = (atoms a) `union` (atoms b)
atoms (a `THEN` b) = (atoms a) `union` (atoms b)
atoms (a `EQUY` b) = (atoms a) `union` (atoms b)
atoms (a `XOR` b) = (atoms a) `union` (atoms b)

allAlpha :: Int -> [Binary]
allAlpha n = let f = (bloatBin n).toBin in [ f x |x<-[0..(2^n)-1] ]

numAtoms :: Formel -> Int
numAtoms = length.atoms

--------------------------------------------------------------

{-
instance Eq Formel where
    TAUTO == TAUTO = True
    ABSURD == ABSURD = True
    (Atom a) == (Atom b) = a==b
    (a `OR` b) == (b `OR` a) = True
    (a `AND` b) == (b `AND` a) = True
-}


--todo
str2form :: String -> Formel
str2form s
    | (head s)=='-' = NOT $ str2form $ tail s
    | (head s) `elem` "ABCDEFGHIJKLMNOPQRSTUVWXYZ" = Atom $ head s
    | otherwise = Atom 'A'



{-

A B C | AvB | BvC
-------------------------
0 0 0 |
0 0 1 |

-}

truthTable :: Formel -> IO()
truthTable f = do
    let n = length $ atoms f
    let r = 2^n
    print $ "---"++(atoms f)++"---"
    sequence_ [print x | x <-allAlpha n]
    print "------"

showInfo :: Formel -> IO()
showInfo f = do
    print $ "Formula:"++(show f)
    print $ "NNF:    "++(show $ nnf f)
    print $ "Length: "++(show $ formLen f)
    print $ "Atoms:  "++(atoms f)
    truthTable f

--https://www.google.de/search?q=ukraine+nazis&tbm=isch&ei=Sb1wVdjyMMK8swHGxoPgDQ