module Main where

import FOLSyntax ( Formula(Conj, Neg, Impl), Term(..) )
import Parser ( parseFormula, parseFormulaE )
import Resolution ( CNF, doResolution, doResolutionIO, showCNF )
import Normalforms
    ( makeNNF,
      renameBinders,
      makePNF,
      makeSkolem,
      makeCNF,
      makeClauseSet )
import Control.Monad (void)

{-
To prove a formula we:
1. Construct `Neg phi`
2. Transform `Neg phi` to a clause list
3. doResolution on clause list
-}
proveFormula :: Formula -> Either () CNF
proveFormula form = doResolution . makeClauseSet . makeCNF . makeSkolem . makePNF . renameBinders . makeNNF $ Neg form

proveFormulaIO :: Formula -> IO ()
proveFormulaIO form = do
    let clauseSet = makeClauseSet . makeCNF . makeSkolem . makePNF . renameBinders . makeNNF $ Neg form
    void $ doResolutionIO clauseSet 

-- unification examples
terma1 :: Term
terma1 = Fun "f" [Var "x", Fun "g" [Var "y"]]
termb1 :: Term
termb1 = Fun "f" [Fun "g" [Var "z"], Var "z"]
terma2 :: Term
terma2 = Fun "f" [Var "x", Fun "g" [Var "x"], Fun "h" [Var "y"]]
termb2 :: Term
termb2 = Fun "f" [Fun "k" [Var "y"], Fun "g" [Var "z"], Var "z"]
terma3 :: Term
terma3 = Fun "f" [Var "x", Fun "g" [Var "x"]]
termb3 :: Term
termb3 = Fun "f" [Var "z", Var "z"]

-- NNF example from gloin
formula1 :: Formula
formula1 = parseFormula "!((A () \\/ !B()) /\\ (C ()))"

-- PNF and skolem example from gloin
formula2 :: Formula
formula2 = parseFormula "forall x. (forall y. L(y,x)) -> exists y.M(x,y)"

-- Resolution example from gloin script
formula3 :: Formula
formula3 = parseFormula "P(a()) /\\ (forall x. P(x) -> P(f(x))) -> (exists x. P(f(f(x)))) "

-- Resolution example from gloin exercises (sheet 11, ex 5) [already in CNF]
formula4 :: Formula
formula4 = parseFormula "((S(f(x), y)) \\/ (S(y, z)) \\/ (P(y))) /\\ (!(S(f(f(x)), x))) /\\ (!P(f(z)))"

-- now a big example, sheet 11, exercise 6: Drogenschmuggel, this doesn't work yet but I'm sure its just the exercise thats wrong...
formula5 :: Formula
formula5 = Impl (Conj phi1 (Conj phi2 phi3)) psi
    where
        phi1 = parseFormula "forall x.E(x) /\\ !I(x) -> exists y.Z(y) /\\ S(y,x)"
        phi2 = parseFormula "exists x. (D(x) /\\ E(x)) /\\ forall y. S(y,x) -> D(y)"
        phi3 = parseFormula "forall x.I(x) -> !D(x)"
        psi = parseFormula "exists x. Z(x) /\\ D(x)"

-- aerzte und quacksalber v2
formula6 :: Formula
formula6 = Impl (Conj psi1 psi2) psi3
    where
        psi1 = parseFormula "forall x. D(x) -> exists y. P(y) /\\ L(y,x)"
        psi2 = parseFormula "forall x. P(x) -> forall y. Q(y) -> !L(x, y)"
        psi3 = parseFormula "forall x. D(x) -> !Q(x)"

testing :: IO ()
testing = do
    putStrLn $ "Now making NNF of formula: " ++ show formula1
    print $ makeNNF formula1
    putStrLn $ "Now making PNF of formula: " ++ show formula2
    print . makePNF . renameBinders $ makeNNF formula2
    putStrLn $ "Now making Skolemform of formula: " ++ show formula2
    print . makeSkolem . makePNF . renameBinders $ makeNNF formula2
    putStrLn $ "Now proving formula by resolution: " ++ show formula3
    case proveFormula formula3 of
        Left _ -> putStrLn "Success!"
        Right _ -> return ()
    putStrLn $ "Now Proving formula by resolution: " ++ show formula4
    case doResolution $ makeClauseSet formula4 of
        Left _ -> putStrLn "Success!"
        Right _ -> return ()
    putStrLn $ "Now Proving formula by resolution: " ++ show formula5
    case proveFormula formula5 of
        Left _ -> putStrLn "Success!"
        Right _ -> return ()
    putStrLn $ "Now Proving formula by resolution: " ++ show formula6
    case proveFormula (Neg formula6) of
        Left _ -> putStrLn "Success!"
        Right _ -> return ()

main :: IO ()
main = do
    showIntroText
    go
    where
        go = do
            putStrLn "\nYou can now enter a formula that should be proven or enter the name of a predefined formula to proof them."
            putStrLn "Type 'help' to see the information again."
            -- TODO use haskeline...
            line <- getLine
            case line of
                "script" -> fullProof formula3
                "doctors" -> fullProof formula6
                "drugs" -> fullProof formula5
                "help" -> showIntroText
                str -> case parseFormulaE str of
                    Left err -> putStrLn err
                    Right formula -> fullProof formula
            go
        fullProof f = do
            putStr "\n\n\n"
            putStrLn $ "1. Negation of formula:\n" ++ show (Neg f)
            let f' = makeNNF (Neg f)
            putStrLn $ "2. Negation normalform:\n" ++ show f'
            let f'' = makePNF $ renameBinders f'
            putStrLn $ "3. Prenex normalform (with renamed binders):\n" ++ show f''
            let f''' = makeSkolem f''
            putStrLn $ "4. Skolemization:\n" ++ show f'''
            let g = makeClauseSet . makeCNF $ f'''
            putStrLn $ "5. Clause set:\n" ++ showCNF g
            putStrLn "6. Do resolution:\n"
            _ <- doResolutionIO g
            putStrLn "7. Negation of formula is unsatisfiable, so the formula is valid!"
        showIntroText = do
            putStrLn "This is a simple program implementing a resolution algorithm on first order logic (FOL)."
            putStrLn "Caution: resoluton on FOL is only a semi-decider, if you try to prove an unprovable formula the algorithm will diverge!"
            putStrLn "\nProcedure:"
            putStrLn "To proof a formula the program takes the following steps:"
            putStrLn "1. Negate the formula"
            putStrLn "2. Transform it to negation normalform"
            putStrLn "3. Transform it to prenex normalform"
            putStrLn "4. Skolemize formula"
            putStrLn "5. Transform it to a clause set"
            putStrLn "6. Exhaustively use the reduction rule, until the empty clause is found."
            putStrLn "7. If an empty clause was found the negation of the formula is unsatisfiable, making the the formula valid!"
            putStrLn "\nPrelude:"
            putStrLn "There are some predefined formulas that can be called for a proof:"
            putStrLn $ "script = " ++ show formula3 ++ " [a small resolution example taken from lecture notes]"
            -- putStrLn $ "exercises = " ++ show formula4 ++ " [another small resolution example taken from exercises]" TODO this is already negated...
            putStrLn $ "doctors = " ++ show formula6 ++ " [a little more complex example from exercises]"
            putStrLn $ "drugs = " ++ show formula5 ++ " [most complex example from exercises]"