Merge 7bd93c7 into 4626f7c

msakai · Nov 23, 2021 · 613117f · 613117f
2 parents 4626f7c + 7bd93c7
commit 613117f
Show file tree

Hide file tree

Showing 4 changed files with 84 additions and 13 deletions.
diff --git a/src/Data/DecisionDiagram/BDD.hs b/src/Data/DecisionDiagram/BDD.hs
@@ -32,7 +32,6 @@ module Data.DecisionDiagram.BDD
   (
   -- * The BDD type
     BDD (Leaf, Branch)
-  , Sig (..)
 
   -- * Item ordering
   , ItemOrder (..)
@@ -93,6 +92,11 @@ module Data.DecisionDiagram.BDD
   , countSat
   , uniformSatM
 
+  -- * (Co)algebraic structure
+  , Sig (..)
+  , inSig
+  , outSig
+
   -- * Fold
   , fold
   , fold'
@@ -675,10 +679,6 @@ unfoldOrd f b = m2 Map.! b
           let fx = f x
            in g (Map.insert x fx m) (xs ++ Foldable.toList fx)
 
-inSig :: Sig (BDD a) -> BDD a
-inSig (SLeaf b) = Leaf b
-inSig (SBranch x lo hi) = Branch x lo hi
-
 -- ------------------------------------------------------------------------
 
 -- | All the variables that this BDD depends on.
@@ -1054,14 +1054,24 @@ uniformSatM xs0 bdd0 = func IntMap.empty
 
 -- ------------------------------------------------------------------------
 
--- | Signature functor of 'BDD' type as a F-algebra and as a F-coalgebra.
+-- | Signature functor of 'BDD' type
 data Sig a
   = SLeaf !Bool
   | SBranch !Int a a
   deriving (Eq, Ord, Show, Read, Generic, Functor, Foldable, Traversable)
 
 instance Hashable a => Hashable (Sig a)
 
+-- | 'Sig'-algebra stucture of 'BDD', \(\mathrm{in}_\mathrm{Sig}\).
+inSig :: Sig (BDD a) -> BDD a
+inSig (SLeaf b) = Leaf b
+inSig (SBranch x lo hi) = Branch x lo hi
+
+-- | 'Sig'-coalgebra stucture of 'BDD', \(\mathrm{out}_\mathrm{Sig}\).
+outSig :: BDD a -> Sig (BDD a)
+outSig (Leaf b) = SLeaf b
+outSig (Branch x lo hi) = SBranch x lo hi
+
 -- ------------------------------------------------------------------------
 
 type Graph f = IntMap (f Int)

diff --git a/src/Data/DecisionDiagram/ZDD.hs b/src/Data/DecisionDiagram/ZDD.hs
@@ -33,7 +33,6 @@ module Data.DecisionDiagram.ZDD
   (
   -- * ZDD type
     ZDD (Empty, Base, Branch)
-  , Sig (..)
 
   -- * Item ordering
   , ItemOrder (..)
@@ -92,6 +91,11 @@ module Data.DecisionDiagram.ZDD
   , mapDelete
   , change
 
+  -- * (Co)algebraic structure
+  , Sig (..)
+  , inSig
+  , outSig
+
   -- * Fold
   , fold
   , fold'
@@ -897,11 +901,6 @@ unfoldOrd f b = m2 Map.! b
           let fx = f x
            in g (Map.insert x fx m) (xs ++ Foldable.toList fx)
 
-inSig :: Sig (ZDD a) -> ZDD a
-inSig SEmpty = Empty
-inSig SBase = Base
-inSig (SBranch x lo hi) = Branch x lo hi
-
 -- ------------------------------------------------------------------------
 
 -- | Sample a set from uniform distribution over elements of the ZDD.
@@ -1008,7 +1007,7 @@ findMaxSum weight =
 
 -- ------------------------------------------------------------------------
 
--- | Signature functor of 'ZDD' type as a F-algebra and as a F-coalgebra.
+-- | Signature functor of 'ZDD' type
 data Sig a
   = SEmpty
   | SBase
@@ -1017,6 +1016,18 @@ data Sig a
 
 instance Hashable a => Hashable (Sig a)
 
+-- | 'Sig'-algebra stucture of 'ZDD', \(\mathrm{in}_\mathrm{Sig}\).
+inSig :: Sig (ZDD a) -> ZDD a
+inSig SEmpty = Empty
+inSig SBase = Base
+inSig (SBranch x lo hi) = Branch x lo hi
+
+-- | 'Sig'-coalgebra stucture of 'ZDD', \(\mathrm{out}_\mathrm{Sig}\).
+outSig :: ZDD a -> Sig (ZDD a)
+outSig Empty = SEmpty
+outSig Base = SBase
+outSig (Branch x lo hi) = SBranch x lo hi
+
 -- ------------------------------------------------------------------------
 
 type Graph f = IntMap (f Int)

diff --git a/test/TestBDD.hs b/test/TestBDD.hs
@@ -546,6 +546,30 @@ case_fold'_strictness = do
     flag <- readIORef ref
     assertBool "unused value should be evaluated" flag
 
+prop_fold_inSig :: Property
+prop_fold_inSig =
+  forAllItemOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(bdd :: BDD o) ->
+      BDD.fold (BDD.inSig (BDD.SLeaf False)) (BDD.inSig (BDD.SLeaf True)) (\x lo hi -> BDD.inSig (BDD.SBranch x lo hi)) bdd
+      ===
+      bdd
+
+prop_fold'_inSig :: Property
+prop_fold'_inSig =
+  forAllItemOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(bdd :: BDD o) ->
+      BDD.fold' (BDD.inSig (BDD.SLeaf False)) (BDD.inSig (BDD.SLeaf True)) (\x lo hi -> BDD.inSig (BDD.SBranch x lo hi)) bdd
+      ===
+      bdd
+
+-- ------------------------------------------------------------------------
+
+prop_unfoldHashable_outSig :: Property
+prop_unfoldHashable_outSig =
+  forAllItemOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(bdd :: BDD o) ->
+      BDD.unfoldHashable BDD.outSig bdd === bdd
+
 -- ------------------------------------------------------------------------
 
 case_support_false :: Assertion

diff --git a/test/TestZDD.hs b/test/TestZDD.hs
@@ -687,6 +687,8 @@ prop_findMaxSum =
               .&&.
               conjoin [counterexample (show (s, setWeight s)) $ obj0 >= setWeight s | s <- ZDD.toListOfIntSets a]
 
+-- ------------------------------------------------------------------------
+
 case_fold_laziness :: Assertion
 case_fold_laziness = do
   let bdd :: ZDD ZDD.AscOrder
@@ -710,6 +712,30 @@ case_fold'_strictness = do
     flag <- readIORef ref
     assertBool "unused value should be evaluated" flag
 
+prop_fold_inSig :: Property
+prop_fold_inSig =
+  forAllItemOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(zdd :: ZDD o) ->
+      ZDD.fold (ZDD.inSig ZDD.SEmpty) (ZDD.inSig ZDD.SBase) (\x lo hi -> ZDD.inSig (ZDD.SBranch x lo hi)) zdd
+      ===
+      zdd
+
+prop_fold'_inSig :: Property
+prop_fold'_inSig =
+  forAllItemOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(zdd :: ZDD o) ->
+      ZDD.fold' (ZDD.inSig ZDD.SEmpty) (ZDD.inSig ZDD.SBase) (\x lo hi -> ZDD.inSig (ZDD.SBranch x lo hi)) zdd
+      ===
+      zdd
+
+-- ------------------------------------------------------------------------
+
+prop_unfoldHashable_outSig :: Property
+prop_unfoldHashable_outSig =
+  forAllItemOrder $ \(_ :: Proxy o) ->
+    forAll arbitrary $ \(zdd :: ZDD o) ->
+      ZDD.unfoldHashable ZDD.outSig zdd === zdd
+
 -- ------------------------------------------------------------------------
 
 prop_toGraph_fromGraph :: Property