{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Wang
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  portable
--
-----------------------------------------------------------------------------
module ToySolver.Wang
  ( Formula
  , Sequent
  , isValid
  ) where

import Control.Monad (guard,msum)
import Data.List (intersect)
import Data.Maybe (isJust, listToMaybe)
import ToySolver.Data.BoolExpr

type Formula a = BoolExpr a
type Sequent x = ([Formula x], [Formula x])

isValid :: Eq x => Sequent x -> Bool
isValid :: forall x. Eq x => Sequent x -> Bool
isValid = forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Eq x => Sequent x -> Maybe ()
isValid'

isValid' :: Eq x => Sequent x -> Maybe ()
isValid' :: forall x. Eq x => Sequent x -> Maybe ()
isValid' ([Formula x]
l,[Formula x]
r) =
    do [([Formula x], [Formula x])]
xs <- forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum forall a b. (a -> b) -> a -> b
$
         [ do let i :: [Formula x]
i = forall a. Eq a => [a] -> [a] -> [a]
intersect [Formula x]
l [Formula x]
r
              forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Formula x]
i
              forall (m :: * -> *) a. Monad m => a -> m a
return []
         , do (Not Formula x
p, [Formula x]
r) <- forall x. [x] -> [(x, [x])]
pick [Formula x]
r
              forall (m :: * -> *) a. Monad m => a -> m a
return [(Formula x
pforall a. a -> [a] -> [a]
:[Formula x]
l,[Formula x]
r)]
         , do (Not Formula x
p, [Formula x]
l) <- forall x. [x] -> [(x, [x])]
pick [Formula x]
l
              forall (m :: * -> *) a. Monad m => a -> m a
return [([Formula x]
l,Formula x
pforall a. a -> [a] -> [a]
:[Formula x]
r)]
         , do (Imply Formula x
p Formula x
q, [Formula x]
r) <- forall x. [x] -> [(x, [x])]
pick [Formula x]
r
              forall (m :: * -> *) a. Monad m => a -> m a
return [(Formula x
pforall a. a -> [a] -> [a]
:[Formula x]
l,Formula x
qforall a. a -> [a] -> [a]
:[Formula x]
r)]
         , do (Or [Formula x]
ps, [Formula x]
r) <- forall x. [x] -> [(x, [x])]
pick [Formula x]
r
              forall (m :: * -> *) a. Monad m => a -> m a
return [([Formula x]
l,[Formula x]
psforall a. [a] -> [a] -> [a]
++[Formula x]
r)]
         , do (And [Formula x]
ps, [Formula x]
l) <- forall x. [x] -> [(x, [x])]
pick [Formula x]
l
              forall (m :: * -> *) a. Monad m => a -> m a
return [([Formula x]
psforall a. [a] -> [a] -> [a]
++[Formula x]
l,[Formula x]
r)]
         , do (Or [Formula x]
ps, [Formula x]
l)  <- forall x. [x] -> [(x, [x])]
pick [Formula x]
l
              forall (m :: * -> *) a. Monad m => a -> m a
return [(Formula x
pforall a. a -> [a] -> [a]
:[Formula x]
l,[Formula x]
r) | Formula x
p <- [Formula x]
ps]
         , do (And [Formula x]
ps, [Formula x]
r) <- forall x. [x] -> [(x, [x])]
pick [Formula x]
r
              forall (m :: * -> *) a. Monad m => a -> m a
return [([Formula x]
l,Formula x
pforall a. a -> [a] -> [a]
:[Formula x]
r) | Formula x
p <- [Formula x]
ps]
         , do (Imply Formula x
p Formula x
q, [Formula x]
l) <- forall x. [x] -> [(x, [x])]
pick [Formula x]
l
              forall (m :: * -> *) a. Monad m => a -> m a
return [(Formula x
qforall a. a -> [a] -> [a]
:[Formula x]
l,[Formula x]
r), ([Formula x]
l,Formula x
pforall a. a -> [a] -> [a]
:[Formula x]
r)]

         , do (Equiv Formula x
p Formula x
q, [Formula x]
l) <- forall x. [x] -> [(x, [x])]
pick [Formula x]
l
              forall (m :: * -> *) a. Monad m => a -> m a
return [(forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Imply Formula x
p Formula x
q forall a. a -> [a] -> [a]
: forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Imply Formula x
q Formula x
p forall a. a -> [a] -> [a]
: [Formula x]
l, [Formula x]
r)]
         , do (Equiv Formula x
p Formula x
q, [Formula x]
r) <- forall x. [x] -> [(x, [x])]
pick [Formula x]
r
              forall (m :: * -> *) a. Monad m => a -> m a
return [([Formula x]
l, forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Imply Formula x
p Formula x
q forall a. a -> [a] -> [a]
: forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Imply Formula x
q Formula x
p forall a. a -> [a] -> [a]
: [Formula x]
r)]
         ]
       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall x. Eq x => Sequent x -> Maybe ()
isValid' [([Formula x], [Formula x])]
xs
       forall (m :: * -> *) a. Monad m => a -> m a
return ()

pick :: [x] -> [(x,[x])]
pick :: forall x. [x] -> [(x, [x])]
pick []     = []
pick (x
x:[x]
xs) = (x
x,[x]
xs) forall a. a -> [a] -> [a]
: [(x
y,x
xforall a. a -> [a] -> [a]
:[x]
ys) | (x
y,[x]
ys) <- forall x. [x] -> [(x, [x])]
pick [x]
xs]