{-# 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 = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool) -> (Sequent x -> Maybe ()) -> Sequent x -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sequent x -> Maybe ()
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 <- [[([Formula x], [Formula x])]]
-> Maybe [([Formula x], [Formula x])]
forall a. [a] -> Maybe a
listToMaybe ([[([Formula x], [Formula x])]]
 -> Maybe [([Formula x], [Formula x])])
-> [[([Formula x], [Formula x])]]
-> Maybe [([Formula x], [Formula x])]
forall a b. (a -> b) -> a -> b
$ [[[([Formula x], [Formula x])]]] -> [[([Formula x], [Formula x])]]
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([[[([Formula x], [Formula x])]]]
 -> [[([Formula x], [Formula x])]])
-> [[[([Formula x], [Formula x])]]]
-> [[([Formula x], [Formula x])]]
forall a b. (a -> b) -> a -> b
$
         [ do let i :: [Formula x]
i = [Formula x] -> [Formula x] -> [Formula x]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Formula x]
l [Formula x]
r
              Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Formula x] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Formula x]
i
              [([Formula x], [Formula x])] -> [[([Formula x], [Formula x])]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
         , do (Not Formula x
p, [Formula x]
r) <- [Formula x] -> [(Formula x, [Formula x])]
forall x. [x] -> [(x, [x])]
pick [Formula x]
r
              [([Formula x], [Formula x])] -> [[([Formula x], [Formula x])]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Formula x
pFormula x -> [Formula x] -> [Formula x]
forall a. a -> [a] -> [a]
:[Formula x]
l,[Formula x]
r)]
         , do (Not Formula x
p, [Formula x]
l) <- [Formula x] -> [(Formula x, [Formula x])]
forall x. [x] -> [(x, [x])]
pick [Formula x]
l
              [([Formula x], [Formula x])] -> [[([Formula x], [Formula x])]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [([Formula x]
l,Formula x
pFormula x -> [Formula x] -> [Formula x]
forall a. a -> [a] -> [a]
:[Formula x]
r)]
         , do (Imply Formula x
p Formula x
q, [Formula x]
r) <- [Formula x] -> [(Formula x, [Formula x])]
forall x. [x] -> [(x, [x])]
pick [Formula x]
r
              [([Formula x], [Formula x])] -> [[([Formula x], [Formula x])]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Formula x
pFormula x -> [Formula x] -> [Formula x]
forall a. a -> [a] -> [a]
:[Formula x]
l,Formula x
qFormula x -> [Formula x] -> [Formula x]
forall a. a -> [a] -> [a]
:[Formula x]
r)]
         , do (Or [Formula x]
ps, [Formula x]
r) <- [Formula x] -> [(Formula x, [Formula x])]
forall x. [x] -> [(x, [x])]
pick [Formula x]
r
              [([Formula x], [Formula x])] -> [[([Formula x], [Formula x])]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [([Formula x]
l,[Formula x]
ps[Formula x] -> [Formula x] -> [Formula x]
forall a. [a] -> [a] -> [a]
++[Formula x]
r)]
         , do (And [Formula x]
ps, [Formula x]
l) <- [Formula x] -> [(Formula x, [Formula x])]
forall x. [x] -> [(x, [x])]
pick [Formula x]
l
              [([Formula x], [Formula x])] -> [[([Formula x], [Formula x])]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [([Formula x]
ps[Formula x] -> [Formula x] -> [Formula x]
forall a. [a] -> [a] -> [a]
++[Formula x]
l,[Formula x]
r)]
         , do (Or [Formula x]
ps, [Formula x]
l)  <- [Formula x] -> [(Formula x, [Formula x])]
forall x. [x] -> [(x, [x])]
pick [Formula x]
l
              [([Formula x], [Formula x])] -> [[([Formula x], [Formula x])]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Formula x
pFormula x -> [Formula x] -> [Formula x]
forall a. a -> [a] -> [a]
:[Formula x]
l,[Formula x]
r) | Formula x
p <- [Formula x]
ps]
         , do (And [Formula x]
ps, [Formula x]
r) <- [Formula x] -> [(Formula x, [Formula x])]
forall x. [x] -> [(x, [x])]
pick [Formula x]
r
              [([Formula x], [Formula x])] -> [[([Formula x], [Formula x])]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [([Formula x]
l,Formula x
pFormula x -> [Formula x] -> [Formula x]
forall a. a -> [a] -> [a]
:[Formula x]
r) | Formula x
p <- [Formula x]
ps]
         , do (Imply Formula x
p Formula x
q, [Formula x]
l) <- [Formula x] -> [(Formula x, [Formula x])]
forall x. [x] -> [(x, [x])]
pick [Formula x]
l
              [([Formula x], [Formula x])] -> [[([Formula x], [Formula x])]]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Formula x
qFormula x -> [Formula x] -> [Formula x]
forall a. a -> [a] -> [a]
:[Formula x]
l,[Formula x]
r), ([Formula x]
l,Formula x
pFormula x -> [Formula x] -> [Formula x]
forall a. a -> [a] -> [a]
:[Formula x]
r)]

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