wang.hs

import System.Environment
import Data.Char (isSpace)
import Control.Applicative

data PF = Prop Char
        | Neg PF
        | Conj PF PF
        | Disj PF PF
        | Imp PF PF
        | Equiv PF PF
        deriving (Show, Eq)

data ProofConjecture = Conjecture [PF] [PF]
                     deriving (Show, Eq)

data ProofResult = Proven ProofConjecture
                 | Disproven ProofConjecture
                 | Composite [ProofConjecture]

rstrip = reverse . dropWhile isSpace . reverse

exists :: Eq a => [a] -> [a] -> Bool
exists x y = any id $ (==) <$> x <*> y

-- Parse Conjunctures Grammar
-- <conjucture> ::= <list> | <list> ⊢ <list>
-- <list> ::= <equiv> | <equiv> , <equiv>

parseConjecture :: [Char] -> Maybe ProofConjecture
parseConjecture s =
  case parseList s [] of
    Just (pf, []) -> Just (Conjecture [] pf)
    Just (pf1, '⊢':more) ->
      case parseList more [] of
        Just (pf2, []) -> Just (Conjecture pf1 pf2)
        _ -> Nothing
    _ -> Nothing

parseList :: [Char] -> [PF] -> Maybe ([PF], [Char])
parseList [] pf = Nothing
parseList s pf =
  case parseEquiv s of
    Just (newpf, ',':more) -> parseList more (pf ++ [newpf])
    Just (newpf, more) -> Just (pf ++ [newpf], more)
    _ -> Nothing

-- Parser PF Grammar
-- <equiv> ::= <imp>  | <equiv>  ≡  <imp>
-- <imp>   ::= <disj> | <imp>    ⇒  <disj>
-- <disj>  ::= <conj> | <disj>   ∨  <conj>
-- <conj>  ::= <neg>  | <conj>   ∧  <neg>
-- <neg>   ::= <elem> | ¬ <elem>
-- <elem>  ::= <prop> | ( <equiv> )
-- <prop>  ::= any char

parsePF :: [Char] -> Maybe PF
parsePF [] = Nothing
parsePF s =
  case parseEquiv s of
    Just (e, []) -> Just e
    _ -> Nothing

parseEquiv s =
  case parseImp s of
    Just (pf1, '≡':more) ->
      case parseEquiv more of
        Just (pf2, yet_more) -> Just (Equiv pf1 pf2, yet_more)
        _ -> Nothing
    Just (pf1, more) -> Just (pf1, more)
    _ -> Nothing

parseImp s =
  case parseDisj s of
    Just (pf1, '⇒':more) ->
      case parseImp more of
        Just (pf2, yet_more) -> Just (Imp pf1 pf2, yet_more)
        _ -> Nothing
    Just (pf1, more) -> Just (pf1, more)
    _ -> Nothing

parseDisj s =
  case parseConj s of
    Just (pf1, '∨':more) ->
      case parseDisj more of
        Just (pf2, yet_more) -> Just (Disj pf1 pf2, yet_more)
        _ -> Nothing
    Just (pf1, more) -> Just (pf1, more)
    _ -> Nothing

parseConj s =
  case parseNeg s of
    Just (pf1, '∧':more) ->
      case parseConj more of
        Just (pf2, yet_more) -> Just (Conj pf1 pf2, yet_more)
        _ -> Nothing
    Just (pf1, more) -> Just (pf1, more)
    _ -> Nothing

parseNeg ('¬':s) =
  case parseProp s of
    Just (pf, more) -> Just(Neg pf, more)
    _ -> Nothing
parseNeg s = parseProp s

parseProp [] = Nothing
parseProp ('(':s) =
  case parseEquiv s of
    Just (pf, ')':more) -> Just (pf, more)
    _ -> Nothing
parseProp (x:xs) = Just (Prop x, xs)

-- Wang's algorithm
checkConjectures :: [Char] -> [ProofConjecture] -> ([Char], Bool)
checkConjectures steps [] = (steps ++ "\n", True)
checkConjectures steps conjs@(x:xs) =
  case reduction x of
    (Proven conject) -> checkConjectures (steps ++ "\n" ++ (unparse [conject])) xs
    (Disproven conject) -> (steps ++ "\n" ++ (unparse [conject]) ++ "\n", False)
    (Composite more_conjs) -> checkConjectures (steps ++ "\n" ++ (unparse more_conjs)) (xs ++ more_conjs)

reduction :: ProofConjecture -> ProofResult

reduction (Conjecture ((Neg pf):h) g) =
  (Composite [(Conjecture h (g ++ [pf]))])
reduction (Conjecture h ((Neg pf):g)) =
  (Composite [(Conjecture (h ++ [pf]) g)])

reduction (Conjecture ((Conj pf1 pf2):h) g) =
  (Composite [Conjecture (h ++ [pf1] ++ [pf2]) g])
reduction (Conjecture h ((Conj pf1 pf2):g)) =
  (Composite [(Conjecture h (g ++ [pf1])), (Conjecture h (g ++ [pf2]))])

reduction (Conjecture ((Disj pf1 pf2):h) g) =
  (Composite [(Conjecture (h ++ [pf1]) g), (Conjecture (h ++ [pf2]) g)])
reduction (Conjecture h ((Disj pf1 pf2):g)) =
  (Composite [Conjecture h (g ++ [pf1] ++ [pf2])])

reduction (Conjecture ((Imp pf1 pf2):h) g) =
  (Composite [(Conjecture (h ++ [pf2])  g), (Conjecture h (g ++ [pf1]))])
reduction (Conjecture h ((Imp pf1 pf2):g)) =
  (Composite [Conjecture (h ++ [pf1]) (g ++ [pf2])])

reduction (Conjecture ((Equiv pf1 pf2):h) g) =
  (Composite [(Conjecture (h ++ [pf1] ++ [pf2]) g), (Conjecture h (g ++ [pf1] ++ [pf2]))])
reduction (Conjecture h ((Equiv pf1 pf2):g)) =
  (Composite [(Conjecture (h ++ [pf1]) (g ++ [pf2])), (Conjecture (h ++ [pf2]) (g ++ [pf1]))])

reduction (Conjecture h g) = groundRules h g (filter isProp h) (filter isProp g)

groundRules :: [PF] -> [PF] -> [PF] -> [PF] -> ProofResult
groundRules h g filterH filterG
  | exists filterG h = Proven (Conjecture h g)
  | (length filterG) == (length g) && (length filterH) == (length h) = Disproven (Conjecture h g)
  | otherwise = reduction (Conjecture h g)
--  | otherwise = Disproven (Conjecture h g)

isProp (Prop _) = True
isProp _ = False

-- Unparsing

unparse :: [ProofConjecture] -> [Char]
unparse [] = ""
unparse ((Conjecture h g):[]) = ((unparsePFList h) ++ " ⊢ " ++ (unparsePFList g))
unparse ((Conjecture h g):xs) = (unparsePFList h) ++ " ⊢ " ++ (unparsePFList g) ++ " and " ++ (unparse xs)

unparsePFList :: [PF] -> [Char]
unparsePFList [] = ""
unparsePFList (x:[]) = (unparsePF x)
unparsePFList (x:xs) = (unparsePF x) ++ ", " ++ (unparsePFList xs)

-- included parenthesis everywhere, otherwise it seems to be ambiguous
unparsePF :: PF -> [Char]
unparsePF (Equiv fp1 fp2) = "(" ++ (unparsePF fp1) ++ " ≡ " ++ (unparsePF fp2) ++ ")"
unparsePF (Imp fp1 fp2)   = "(" ++ (unparsePF fp1) ++ " ⇒ " ++ (unparsePF fp2) ++ ")"
unparsePF (Conj fp1 fp2)  = "(" ++ (unparsePF fp1) ++ " ∧ " ++ (unparsePF fp2) ++ ")"
unparsePF (Disj fp1 fp2)  = "(" ++ (unparsePF fp1) ++ " ∨ " ++ (unparsePF fp2) ++ ")"
unparsePF (Neg fp1)       = "(" ++ " ¬ " ++ (unparsePF fp1) ++ ")"
unparsePF (Prop x)        = [x]

main = do
  (file:rest) <- getArgs
  srcText <- readFile file
  case parseConjecture (filter (/= ' ') (rstrip srcText)) of
    Just x ->
      case checkConjectures "" [x] of
        (steps, True) -> putStr ("Proof Representation:" ++ steps)
        (steps, _) -> putStr ("Refutation Representation:" ++ steps)
    _ -> print "Could not parse"