HasCacBDD 0.3.0.1 → 0.4.0.0
raw patch · 5 files changed
+80/−33 lines, 5 filesdep +parsecPVP ok
version bump matches the API change (PVP)
Dependencies added: parsec
API changes (from Hackage documentation)
Files
- CHANGELOG.md +4/−0
- HasCacBDD.cabal +3/−2
- README.md +9/−7
- hs/Data/HasCacBDD.hs +21/−4
- tests/Main.hs +43/−20
CHANGELOG.md view
@@ -1,5 +1,9 @@ # HasCacBDD Changelog +## v0.4.0.0 (2026-06-20)++- rewrite "Show" and "Read" instances using "top", "bot", "var", "ifthenelse" and parsec for "Read". This should make them lawful.+ ## v0.3.0.1 (2025-10-22) - let `svgGraph` try to find the `dot` executable in multiple common locations. This should make it work on non-Linux systems. (Thanks to @MitchBoontjes for the original patch.)
HasCacBDD.cabal view
@@ -1,5 +1,5 @@ name: HasCacBDD-version: 0.3.0.1+version: 0.4.0.0 synopsis: Haskell bindings for CacBDD homepage: https://github.com/m4lvin/HasCacBDD license: GPL-2@@ -30,7 +30,7 @@ source-repository head type: git- location: git://github.com/m4lvin/HasCacBDD.git+ location: https://github.com/m4lvin/HasCacBDD.git custom-setup setup-depends: base >= 4.8 && < 5,@@ -41,6 +41,7 @@ exposed-modules: Data.HasCacBDD, Data.HasCacBDD.Visuals build-depends: base >=4.8 && < 5,+ parsec >= 3.1 && < 3.2, process >= 1.1 && < 1.7, QuickCheck >= 2.4 && < 2.15, directory < 1.4
README.md view
@@ -33,12 +33,14 @@ 3. Now you can play with Boolean functions :-) - λ> import Data.HasCacBDD- λ> var 5- Var 5 Top Bot- λ> neg (var 5)- Var 5 Bot Top- λ> dis (neg (var 3)) (var 3)- Top+ ghci> import Data.HasCacBDD+ ghci> var 5+ var 5+ ghci> neg (var 5)+ neg (var 5)+ ghci> dis (neg (var 3)) (var 3)+ top+ ghci> dis (neg (var 1)) (var 3)+ ifthenelse (var 1) (var 3) top For further documentation, see <https://hackage.haskell.org/package/HasCacBDD/docs/Data-HasCacBDD.html>
hs/Data/HasCacBDD.hs view
@@ -28,7 +28,6 @@ maximumvar, showInfo ) where -import Control.Arrow (Arrow(first)) import Foreign.C (CInt(..)) import Foreign.Ptr (Ptr) import Foreign (ForeignPtr, newForeignPtr, withForeignPtr, finalizerFree)@@ -37,6 +36,7 @@ import Data.List ((\\), minimumBy, nub, permutations, sort) import Data.Maybe (fromJust, listToMaybe) import Test.QuickCheck (Arbitrary, Gen, arbitrary, shrink, choose, oneof, sized, listOf)+import Text.Parsec -- | The CacBDD datatype has no structure because -- from our perspective BDDs are just pointers.@@ -308,12 +308,29 @@ sizeOf = length . subsOf instance Show Bdd where- show = show . unravel+ showsPrec d b = f (d > 10) (unravel b) where+ f :: Bool -> BddTree -> ShowS+ f _ Bot = ("bot" ++)+ f _ Top = ("top" ++)+ f p (Var n Top Bot) = showParen p (("var " ++ show n) ++)+ f p (Var n Bot Top) = showParen p (("neg (var " ++ show n ++ ")") ++)+ f p (Var n a c) = showParen p+ (("ifthenelse (var " ++ show n ++ ") " ++ f True a "" ++ " " ++ f True c "") ++) instance Read Bdd where- readsPrec k input = map (first ravel) (readsPrec k input)+ readsPrec _ input = either (const []) return (parse pBdd "" input) --- | A simple tree definition to show BDDs as text.+-- | Parser for 'Bdd' values, used by the 'Read' instance.+pBdd :: Parsec String () (Bdd,String)+pBdd = (,) <$> pExp <*> getInput where -- No "<* eof" here, but getInput for readList.+ pExp = spaces >> (pAtom <|> pIfThenElse <|> pNeg)+ pAtom = (pConst <|> pVar <|> (char '(' *> pExp <* char ')')) <* spaces+ pConst = (string "top" >> return top) <|> (string "bot" >> return bot)+ pVar = string "var " >> (var . read <$> many1 digit)+ pNeg = string "neg " >> neg <$> pAtom+ pIfThenElse = string "ifthenelse " >> spaces >> ifthenelse <$> pAtom <*> pAtom <*> pAtom++-- | A tree definition that is also used to 'show' values ot the 'Bdd' type. data BddTree = Bot | Top | Var Int BddTree BddTree deriving (Eq,Read,Show) -- | Convert a BDD to a tree.
tests/Main.hs view
@@ -1,6 +1,6 @@ {-# OPTIONS_GHC -Wno-x-partial #-} -module Main where+module Main (main) where import Data.List ((\\),nub) import Data.Maybe (fromJust,isNothing)@@ -15,12 +15,12 @@ main :: IO () main = hspec $ do describe "Examples" $ do- describe "Creating BDDs" $ do- it "top == Top" $ show top `shouldBe` "Top"- it "show bot" $ show bot `shouldBe` "Bot"- it "show (var 1)" $ show (var 1) `shouldBe` "Var 1 Top Bot"- it "show (var 2)" $ show (var 1) `shouldBe` "Var 1 Top Bot"- it "show (var 3)" $ show (var 2) `shouldBe` "Var 2 Top Bot"+ describe "Creating and showing BDDs" $ do+ it "top == Top" $ show top `shouldBe` "top"+ it "show bot" $ show bot `shouldBe` "bot"+ it "show (var 1)" $ show (var 1) `shouldBe` "var 1"+ it "show (var 2)" $ show (var 1) `shouldBe` "var 1"+ it "show (var 3)" $ show (var 2) `shouldBe` "var 2" describe "Some tautologies" $ do it "bot == bot" $ bot `shouldBe` bot it "top == top" $ top `shouldBe` top@@ -67,12 +67,11 @@ it "imp (conSet [var 1,var 0]) (var 1) == top" $ imp (conSet [var 1,var 0]) (var 1) `shouldBe` top it "imp (conSet [var 0,var 1]) (var 0) == top" $ imp (conSet [var 0,var 1]) (var 0) `shouldBe` top it "imp (con (var 0) (var 1)) (var 0) == top" $ imp (con (var 0) (var 1)) (var 0) `shouldBe` top- it "show top == \"Top\"" $ show top `shouldBe` "Top"- it "show bot == \"Bot\"" $ show bot `shouldBe` "Bot"+ it "show top == \"top\"" $ show top `shouldBe` "top"+ it "show bot == \"bot\"" $ show bot `shouldBe` "bot" describe "QuickCheck Properties" $ do prop "selfEqual" (\b -> (b::Bdd) == b) prop "showReadEqual" (\b -> read (show b) == (b::Bdd))- prop "showReadTreeEq" (\b -> (ravel . read . show . unravel $ b) == b) prop "idSymmetry" (\a b -> ((a::Bdd) == (b::Bdd)) == (b == a)) prop "singleNegation" (\b -> neg b /= b) prop "doubleNegation" (\b -> neg (neg b) == b)@@ -90,7 +89,6 @@ prop "allSats" (\b -> all (\s -> restrictSet b s == top) (allSats b)) prop "anySat" (\b -> if b==bot then isNothing (anySat b) else restrictSet b (fromJust $ anySat b) == top) prop "ifthenelse" (\a b c -> ifthenelse a b c == neg (dis (con a (neg b)) (con (neg a) (neg c))))- prop "ravel-unravel" (\b -> b == ravel (unravel b)) prop "firstVarOf" (\b -> if b `elem` [bot,top] then isNothing (firstVarOf b) else Just (head (allVarsOfSorted b)) == firstVarOf b) prop "maxVarOf" (\b -> if b `elem` [bot,top] then isNothing (maxVarOf b) else Just (last (allVarsOfSorted b)) == maxVarOf b) prop "thenOf" (\b -> if b `elem` [bot,top] then thenOf b == b else thenOf b == restrict b (fromJust $ firstVarOf b, True ))@@ -120,16 +118,20 @@ gnippam = map swap mapping in relabel gnippam (relabel mapping b) == b)- prop "relabelFun" (\a -> relabelFun (\x -> x-7) (relabelFun (+7) a) == a)- prop "substit" (\b c -> substit 5 b c == ifthenelse b (restrict c (5,True)) (restrict c (5,False)))- prop "substit2" (\b c -> substit (head ([0..] \\ allVarsOf c)) b c == c)- prop "substitSimul" (\b -> substitSimul [] b == b)- prop "substitSimul2" (\b n -> substitSimul [(n,var n)] b == b)+ prop "relabelFun" (\a -> relabelFun (\x -> x-7) (relabelFun (+7) a) === a)+ prop "substit" (\b c -> substit 5 b c === ifthenelse b (restrict c (5,True)) (restrict c (5,False)))+ prop "substit2" (\b c -> substit (head ([0..] \\ allVarsOf c)) b c === c)+ prop "substitSimul" (\b -> substitSimul [] b === b)+ prop "substitSimul2" (\b n -> substitSimul [(n,var n)] b === b) prop "optimalOrder" (\b -> sizeOf b < 15 ==> sizeOf (relabel (optimalOrder b) b) <= sizeOf b)- prop "show" (\a b -> (show a == show b) == (a == (b::Bdd)))- prop "read" (\b -> read (show b) == (b :: Bdd))- prop "showList" (\a b -> (showList [unravel a] "" == showList [unravel b] "") == (a == (b::Bdd)))- prop "readList" (\a b -> readList (show [a,b]) == [([unravel a, unravel b] :: [BddTree], "")])+ describe "Unraveling to BddTree" $ do+ prop "ravel-unravel" (\b -> b == ravel (unravel b))+ prop "ravel-unravelN" (\b -> b /= ravel (unravel (neg b)))+ prop "showReadTreeEq" (\b -> (ravel . read . show . unravel $ b) == b)+ prop "treeShowReadEq" (\b -> (read . show . unravel $ b) == unravel b)+ prop "treeEqIffEq" (\a b -> (unravel a == unravel b) === (a == b))+ prop "treeNEqIffEq" (\a b -> (unravel a /= unravel b) === (a /= b))+ prop "listShowRead" (\a b c -> (read . show . map unravel $ [a,b,c]) == map unravel [a, b, c]) describe "QuickCheck Expected Failures" $ do prop "evaluate may return Nothing" $ expectFailure (\b ass -> evaluate b ass =/= Nothing)@@ -152,3 +154,24 @@ (svgGraph top >>= \ s -> return (length s < 1000)) `shouldReturn` True it "svgGraph (var 1) is longer" $ (svgGraph (var 1) >>= \ s -> return (length s > 1000)) `shouldReturn` True+ describe "instances Show Bdd and Read Bdd" $ do+ describe "show" $ do+ it "var 1 `con` var 2" $ show (var 1 `con` var 2) `shouldBe` "ifthenelse (var 1) (var 2) bot"+ prop "show ==" (\a b -> (show a == show b) === (a == (b::Bdd)))+ prop "read ==" (\b -> read (show b) === (b :: Bdd))+ describe "Pair for precendence test" $ do+ it "show (P (var 3) top)" $ show (P (var 3) top) `shouldBe` "P (var 3) top"+ it "show (P (var 3) (var 1 `con` var 2))" $ show (P (var 3) (var 1 `con` var 2)) `shouldBe` "P (var 3) (ifthenelse (var 1) (var 2) bot)"+ describe "showList" $ do+ prop "showList [a]" (\a b -> (showList [a] "" == showList [b] "") === (a == (b::Bdd)))+ prop "readList [a,b]" (\a b -> readList (show [a,b]) === [([a, b] :: [Bdd], "")])+ prop "readList [...]" (\l -> readList (show l) === [(l :: [Bdd], "")])+ describe "instance Read Bdd" $ do+ describe "single BDD value" $ do+ it "read \"var 1\"" $ read "var 1" `shouldBe` var 1+ it "read \"ifthenelse (var 1) (var 2) (var 2)\"" $ read "ifthenelse (var 1) (var 2) (var 2)" `shouldBe` ifthenelse (var 1) (var 2) (var 2)+ describe "list of BDDs" $ do+ it "read \"[var 1, var 3]\"" $ read "[var 1, var 3]" `shouldBe` [var 1, var 3]+ it "read \"[ top , ifthenelse ( var 3 ) bot bot]\"" $ read "[ top , ifthenelse ( var 3 ) bot bot]" `shouldBe` [top, bot]++data Pair = P Bdd Bdd deriving (Show)