okasaki

commit c9661011beaf8c6c7cb19e3d7d1aad5a254388f5
parent 7cd3c0a67b96d157c0d98c2852a4b3d82ed19134
Author: Jared Tobin <jared@jtobin.io>
Date:   Wed, 15 Mar 2023 09:31:52 +0400

Verify right spine length properties.

Diffstat:
M
lib/Okasaki/Heap/Leftist.hs
 | 
7
+++++++
M
test/Heap/Leftist.hs
 | 
20
++++++++++++++++----
M
test/Heap/Weighted.hs
 | 
18
+++++++++++++++++-

3 files changed, 40 insertions(+), 5 deletions(-)
diff --git a/lib/Okasaki/Heap/Leftist.hs b/lib/Okasaki/Heap/Leftist.hs
@@ -11,6 +11,7 @@ module Okasaki.Heap.Leftist (
   , pat
   , bot
   , cut
+  , wyt
 
   , sor
   , set
@@ -135,6 +136,12 @@ gas = hylo alg lag where
     SinF a   -> one a
     BinF l r -> mer l r
 
+wyt :: Heap a -> Int
+wyt = getSum . cata alg where
+  alg = \case
+    LeafF -> 0
+    NodeF _ _ l r -> 1 <> l <> r
+
 -- reference
 
 nodF :: a -> Heap a -> Heap a -> HeapF a (Heap a)
diff --git a/test/Heap/Leftist.hs b/test/Heap/Leftist.hs
@@ -4,6 +4,7 @@ module Heap.Leftist (
     decorated
   , leftist
   , heap
+  , size
 
   , tests
   ) where
@@ -21,13 +22,21 @@ tests = [
     testProperty "decorations accurate" decorated
   , testProperty "leftist property invariant" leftist
   , testProperty "heap order invariant" heap
+  , testProperty "correct right-spine length" size
   ]
 
+spi :: H.Heap a -> Int
+spi = cata $ \case
+  H.LeafF         -> 0
+  H.NodeF _ _ _ r -> succ r
+
+mos :: H.Heap a -> Bool
+mos h =
+  let n = H.wyt h
+  in  spi h <= floor (logBase 2 ((fromIntegral (succ n)) :: Double))
+
 dec :: H.Heap a -> Bool
-dec h = getSum (H.ran h) == cata alg h where
-  alg = \case
-    H.LeafF         -> 0
-    H.NodeF _ _ _ r -> succ r
+dec h = getSum (H.ran h) == spi h
 
 wef :: H.Heap a -> Bool
 wef = para $ \case
@@ -86,3 +95,6 @@ leftist = forAllShrink (hep :: Gen (H.Heap Int)) lil wef
 
 heap :: Property
 heap = forAllShrink (hep :: Gen (H.Heap Int)) lil hor
+
+size :: Property
+size = forAllShrink (hep :: Gen (H.Heap Int)) lil mos
diff --git a/test/Heap/Weighted.hs b/test/Heap/Weighted.hs
@@ -4,13 +4,15 @@ module Heap.Weighted (
     bleftist
   , decorated
   , heap
+  , size
 
   , tests
   ) where
 
 import Control.Monad (foldM, replicateM)
 import Data.Fix (Fix(..))
-import Data.Functor.Foldable (project, para)
+import Data.Functor.Foldable (project, para, cata)
+import Data.Monoid
 import qualified Okasaki.Heap.Leftist.Weighted as H
 import Test.QuickCheck
 import Test.Tasty (TestTree)
@@ -21,12 +23,23 @@ tests = [
     testProperty "decorations accurate" decorated
   , testProperty "weight-biased leftist property invariant" bleftist
   , testProperty "heap order invariant" heap
+  , testProperty "correct right-spine length" size
   ]
 
 
 dec :: H.Heap a -> Bool
 dec h = H.siz h == H.wyt h
 
+spi :: H.Heap a -> Int
+spi = cata $ \case
+  H.LeafF         -> 0
+  H.NodeF _ _ _ r -> succ r
+
+mos :: H.Heap a -> Bool
+mos h =
+  let n = getSum (H.wyt h)
+  in  spi h <= floor (logBase 2 ((fromIntegral (succ n)) :: Double))
+
 wef :: H.Heap a -> Bool
 wef = para $ \case
   H.LeafF -> True
@@ -85,3 +98,6 @@ bleftist = forAllShrink (hep :: Gen (H.Heap Int)) lil wef
 
 heap :: Property
 heap = forAllShrink (hep :: Gen (H.Heap Int)) lil hor
+
+size :: Property
+size = forAllShrink (hep :: Gen (H.Heap Int)) lil mos