From 2d2bcae015a494c50f9b96d331fd4134425cece4 Mon Sep 17 00:00:00 2001 From: dopamane Date: Thu, 23 May 2024 02:17:02 -0700 Subject: [PATCH] Order propositional rules Improve tableaux rendering --- bayeux.cabal | 1 + src/Bayeux.hs | 8 +-- src/Bayeux/Lp.hs | 113 ++++++++++++++++++++++------------------- src/Bayeux/Tableaux.hs | 6 ++- test/Main.hs | 12 ++--- 5 files changed, 77 insertions(+), 63 deletions(-) diff --git a/bayeux.cabal b/bayeux.cabal index 17f2812..8b51b05 100644 --- a/bayeux.cabal +++ b/bayeux.cabal @@ -18,6 +18,7 @@ library , Bayeux.Lp , Bayeux.Tableaux build-depends: base + , containers , megaparsec , parser-combinators , prettyprinter diff --git a/src/Bayeux.hs b/src/Bayeux.hs index 74d5295..7baab44 100644 --- a/src/Bayeux.hs +++ b/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 diff --git a/src/Bayeux/Lp.hs b/src/Bayeux/Lp.hs index 7c67c55..3a630b4 100644 --- a/src/Bayeux/Lp.hs +++ b/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 diff --git a/src/Bayeux/Tableaux.hs b/src/Bayeux/Tableaux.hs index d970010..edf2be8 100644 --- a/src/Bayeux/Tableaux.hs +++ b/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) diff --git a/test/Main.hs b/test/Main.hs index 4224199..ef78693 100644 --- a/test/Main.hs +++ b/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 ]