Order propositional rules

Improve tableaux rendering

bayeux.cabal

@@ -18,6 +18,7 @@ library
                     , Bayeux.Lp
                     , Bayeux.Tableaux
     build-depends:    base
+                    , containers
                     , megaparsec
                     , parser-combinators
                     , prettyprinter

src/Bayeux.hs

@@ -4,9 +4,9 @@ import Bayeux.Cli
 import Bayeux.Lp
 import Data.Maybe
 import qualified Data.Text.IO as TIO
-import Text.Megaparsec
+import Text.Megaparsec hiding (parse)
 
 app :: Cli -> IO ()
-app cli = print . proveLp . fromJust =<< case input cli of
-  FileInput f -> parseMaybe (parseLp <* eof) <$> TIO.readFile f
-  StdInput    -> parseMaybe parseLp <$> TIO.getLine
+app cli = print . prove . fromJust =<< case input cli of
+  FileInput f -> parseMaybe (parse <* eof) <$> TIO.readFile f
+  StdInput    -> parseMaybe parse <$> TIO.getLine

src/Bayeux/Lp.hs

@@ -7,23 +7,24 @@ module Bayeux.Lp
   ( Lp(..)
   , (/\), (\/), (==>)
   , isSignedBv
-  , evalLp
-  , prettyLp
-  , parseLp
-  , growLp
-  , closeLp
-  , proveLp
+  , eval
+  , render
+  , parse
+  , grow
+  , close
+  , prove
   ) where
 
 import Bayeux.Tableaux
 import Control.Monad.Combinators.Expr
-import Data.List.NonEmpty
+import Data.Set (Set)
+import qualified Data.Set as S
 import Data.String
 import Data.Text (Text)
 import Data.Void
 import Prettyprinter hiding (parens)
 import Prettyprinter.Render.Text
-import Text.Megaparsec
+import Text.Megaparsec hiding (parse)
 import Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer as L
 
@@ -34,6 +35,15 @@ data Lp a = Bv a
           | Impl (Lp a) (Lp a)
   deriving (Eq, Foldable, Functor, Read, Show, Traversable)
 
+instance Eq a => Ord (Lp a) where
+  Bar Bar{}  <= _ = True
+  Conj{}     <= _ = True
+  Bar Disj{} <= _ = True
+  Bar Impl{} <= _ = True
+  Bv{}       <= _ = True
+  Bar Bv{}   <= _ = True
+  _          <= _ = False
+
 infixr 3 /\
 (/\) :: Lp a -> Lp a -> Lp a
 (/\) = Conj
@@ -57,13 +67,13 @@ isSignedBv = \case
   Bv{}     -> True
   _        -> False
 
-evalLp :: Lp Bool -> Bool
-evalLp = \case
+eval :: Lp Bool -> Bool
+eval = \case
   Bv b     -> b
-  Bar  x   -> not $ evalLp x
-  Conj x y -> evalLp x && evalLp y
-  Disj x y -> evalLp x || evalLp y
-  Impl x y -> not (evalLp x) || evalLp y
+  Bar  x   -> not $ eval x
+  Conj x y -> eval x && eval y
+  Disj x y -> eval x || eval y
+  Impl x y -> not (eval x) || eval y
 
 instance Pretty a => Pretty (Lp a) where
   pretty = \case
@@ -77,8 +87,8 @@ instance Pretty a => Pretty (Lp a) where
         e@Bv{} -> pretty e
         e      -> "(" <> pretty e <> ")"
 
-prettyLp :: Pretty a => Lp a -> Text
-prettyLp = renderStrict . layoutPretty defaultLayoutOptions . pretty
+render :: Pretty a => Lp a -> Text
+render = renderStrict . layoutPretty defaultLayoutOptions . pretty
 
 ------------
 -- Parser --
@@ -92,14 +102,14 @@ sc = L.space space1 (L.skipLineComment "--") (L.skipBlockComment "{-" "-}")
 symbol :: Text -> Parser Text
 symbol = L.symbol sc
 
-parseLp :: Parser (Lp Text)
-parseLp = makeExprParser term table <?> "Propositional logic expression"
+parse :: Parser (Lp Text)
+parse = makeExprParser term table <?> "Propositional logic expression"
 
 parens :: Parser a -> Parser a
 parens = between (symbol "(") (symbol ")")
 
 term :: Parser (Lp Text)
-term = parens parseLp <|> fromString `fmap` (L.lexeme sc (some alphaNumChar))
+term = parens parse <|> fromString `fmap` (L.lexeme sc (some alphaNumChar))
 
 table :: [[Operator Parser (Lp Text)]]
 table = [ [ prefix "~" Bar ]
@@ -119,45 +129,46 @@ prefix name f = Prefix (f <$ symbol name)
 -- Prover --
 ------------
 
-growLp
-  :: NonEmpty (Lp a) -- ^ Assumptions
+grow
+  :: Eq a
+  => Set (Lp a) -- ^ Assumptions
   -> Tableaux (Lp a)
-growLp (e :| es) =  case e of
-  Bv{}           -> case nonEmpty es of
-    Nothing      -> Leaf e
-    Just es'     -> Stem e $ growLp es'
-  Bar Bv{}       -> case nonEmpty es of
-    Nothing      -> Leaf e
-    Just es'     -> Stem e $ growLp es'
-  Bar (Bar x)    -> Stem e $ growLp $ x :| es
-  Conj x y       -> Stem e $ growLp $ x <| y :| es
-  Bar (Disj x y) -> Stem e $ growLp $ Bar x <| Bar y :| es
-  Bar (Impl x y) -> Stem e $ growLp $ x <| Bar y :| es
+grow s = case e of
+  Bv{}     | S.null s' -> Leaf e
+           | otherwise -> Stem e $ grow s'
+  Bar Bv{} | S.null s' -> Leaf e
+           | otherwise -> Stem e $ grow s'
+  Bar (Bar x)    -> Stem e $ grow $ S.insert x s'
+  Conj x y       -> Stem e $ grow $ S.insert x $ S.insert y s'
+  Bar (Disj x y) -> Stem e $ grow $ S.insert (Bar x) $ S.insert (Bar y) s'
+  Bar (Impl x y) -> Stem e $ grow $ S.insert x $ S.insert (Bar y) s'
   Bar (Conj x y) ->
-    let l = Bar x :| es
-        r = Bar y :| es
-    in Branch e (growLp l) (growLp r)
+    let l = S.insert (Bar x) s'
+        r = S.insert (Bar y) s'
+    in Branch e (grow l) (grow r)
   Disj x y ->
-    let l = x :| es
-        r = y :| es
-    in Branch e (growLp l) (growLp r)
+    let l = S.insert x s'
+        r = S.insert y s'
+    in Branch e (grow l) (grow r)
   Impl x y ->
-    let l = Bar x :| es
-        r =     y :| es
-    in Branch e (growLp l) (growLp r)
+    let l = S.insert (Bar x) s'
+        r = S.insert y s'
+    in Branch e (grow l) (grow r)
+  where
+    (e, s') = S.deleteFindMin s
 
-closeLp :: Eq a => [Lp a] -> Tableaux (Lp a) -> Bool
-closeLp signedBvs = \case
+close :: Eq a => [Lp a] -> Tableaux (Lp a) -> Bool
+close signedBvs = \case
   Leaf a -> hasContra $ a : signedBvs
   Stem a t
-    | isSignedBv a -> closeLp (a : signedBvs) t
-    | otherwise    -> closeLp signedBvs t
+    | isSignedBv a -> close (a : signedBvs) t
+    | otherwise    -> close signedBvs t
   Branch a l r
     | isSignedBv a -> let signedBvs' = a : signedBvs
-                      in closeLp signedBvs' l &&
-                         closeLp signedBvs' r
-    | otherwise    -> closeLp signedBvs l &&
-                      closeLp signedBvs r
+                      in close signedBvs' l &&
+                         close signedBvs' r
+    | otherwise    -> close signedBvs l &&
+                      close signedBvs r
   where
     hasContra :: Eq a => [Lp a] -> Bool
     hasContra bvs = any (flip elem bvs . invert) bvs
@@ -168,5 +179,5 @@ closeLp signedBvs = \case
           v@Bv{}     -> Bar v
           lp         -> lp
 
-proveLp :: Eq a => Lp a -> Bool
-proveLp = closeLp mempty . growLp . pure . Bar
+prove :: Eq a => Lp a -> Bool
+prove = close mempty . grow . S.singleton . Bar

src/Bayeux/Tableaux.hs

@@ -17,9 +17,11 @@ renderTableaux = unlines . draw
     draw = \case
       Leaf a       -> lines a
       Stem a t     -> lines a ++ drawSubTrees [t]
-      Branch a l r -> lines a ++ drawSubTrees [l, r]
+      Branch a l r -> lines a ++ drawSubTrees [r, l]
     drawSubTrees = \case
       []   -> []
       [t]  -> "\x2502" : shift "\x2502" "" (draw t)
-      t:ts -> "\x2502" : shift "\x251C\x2500\x2510" "\x2502 " (draw t) ++ drawSubTrees ts
+      t:ts -> case t of
+        Leaf{} -> "\x2502" : shift "\x251C\x2500 " "\x2502 " (draw t) ++ drawSubTrees ts
+        _      -> "\x2502" : shift "\x251C\x2500\x2510" "\x2502 " (draw t) ++ drawSubTrees ts
     shift first other = zipWith (++) (first : repeat other)

test/Main.hs

@@ -12,7 +12,7 @@ import qualified Hedgehog.Range as Range
 import Test.Tasty
 import Test.Tasty.Hedgehog
 import Test.Tasty.HUnit
-import Text.Megaparsec
+import Text.Megaparsec hiding (parse)
 
 main :: IO ()
 main = defaultMain $ testGroup "Bayeux"
@@ -23,10 +23,10 @@ main = defaultMain $ testGroup "Bayeux"
 
 mkTestCase :: (Lp Text, Bool, String) -> TestTree
 mkTestCase (lp, expected, description) =
-  let display = unwords [description, T.unpack $ prettyLp lp]
+  let display = unwords [description, T.unpack $ render lp]
   in testGroup display
-       [ testCase "prove" $ proveLp lp @?= expected
-       , testCase "parse . pretty" $ (parseMaybe parseLp . prettyLp) lp @?= Just (lp)
+       [ testCase "prove" $ prove lp @?= expected
+       , testCase "parse . pretty" $ (parseMaybe parse . render) lp @?= Just (lp)
        ]
 
 smullyan :: [(Lp Text, Bool, String)]
@@ -95,7 +95,7 @@ parseTests =
   , tc "~a \\/ ~b" $ "~a" \/ "~b"
   ]
   where
-    tc t lp = testCase (T.unpack t) $ parseMaybe parseLp t @?= Just lp
+    tc t lp = testCase (T.unpack t) $ parseMaybe parse t @?= Just lp
 
 genName :: MonadGen m => m Text
 genName = Gen.text (Range.linear 1 10) Gen.alphaNum
@@ -112,5 +112,5 @@ hedgehogTests :: [TestTree]
 hedgehogTests =
   [ testProperty "parse . pretty = id" $ property $ do
       lp <- forAll genLp
-      (fromJust . parseMaybe parseLp . prettyLp) lp === lp
+      (fromJust . parseMaybe parse . render) lp === lp
   ]