commit 0ba994d356688e72b4166a1a9b56121d2154b651
parent 40b2a0aeb92878a2acc851e167438c241114f03e
Author: Jared Tobin <jared@jtobin.io>
Date: Tue, 14 Mar 2023 23:32:06 +0400
Add property tests.
Diffstat:
9 files changed, 202 insertions(+), 8 deletions(-)
diff --git a/lib/Okasaki/Heap/Leftist.hs b/lib/Okasaki/Heap/Leftist.hs
@@ -8,9 +8,14 @@ module Okasaki.Heap.Leftist (
, lef
, one
, put
+ , pat
, bot
, cut
+ , sor
+ , set
+ , ran
+
, oil
, gas
) where
diff --git a/lib/Okasaki/Heap/Leftist/Weighted.hs b/lib/Okasaki/Heap/Leftist/Weighted.hs
@@ -11,6 +11,9 @@ module Okasaki.Heap.Leftist.Weighted (
, bot
, cut
+ , siz
+ , wyt
+
, oil
, gas
) where
@@ -43,16 +46,30 @@ lef = Fix LeafF
one :: a -> Heap a
one x = Fix (NodeF 1 x lef lef)
+siz :: Heap a -> Sum Int
+siz h = case project h of
+ LeafF -> 0
+ NodeF r _ _ _ -> r
+
+wyt :: Heap a -> Sum Int
+wyt = cata $ \case
+ LeafF -> 0
+ NodeF _ _ l r -> 1 <> l <> r
+
mer :: Ord a => Heap a -> Heap a -> Heap a
mer l r = apo lag (l, r) where
lag (a, b) = case (project a, project b) of
(c, LeafF) -> fmap Left c
(LeafF, d) -> fmap Left d
(NodeF p m c d, NodeF q n e f)
- | m <= n && p >= q -> NodeF (p <> q) m (Left c) (Right (d, b))
- | m <= n && p < q -> NodeF (p <> q) m (Right (d, b)) (Left c)
- | m > n && p >= q -> NodeF (p <> q) n (Left e) (Right (a, f))
- | otherwise -> NodeF (p <> q) n (Right (a, f)) (Left e)
+ | m <= n && wyt c >= (wyt b <> wyt d) ->
+ NodeF (p <> q) m (Left c) (Right (d, b))
+ | m <= n ->
+ NodeF (p <> q) m (Right (d, b)) (Left c)
+ | m > n && wyt e >= (wyt a <> wyt f) ->
+ NodeF (p <> q) n (Left e) (Right (a, f))
+ | otherwise ->
+ NodeF (p <> q) n (Right (a, f)) (Left e)
put :: Ord a => a -> Heap a -> Heap a
put x = mer (one x)
diff --git a/lib/Okasaki/Map.hs b/lib/Okasaki/Map.hs
@@ -1,6 +1,4 @@
{-# OPTIONS_GHC -Wall -fno-warn-unused-top-binds #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Okasaki.Map (
diff --git a/lib/Okasaki/Stack.hs b/lib/Okasaki/Stack.hs
@@ -22,6 +22,8 @@ import Data.Fix (Fix(..))
import Data.Functor.Foldable as RS
import Text.Show.Deriving
+-- NB should arguably be made strict
+
data StackF a r =
NilF
| ConsF !a r
diff --git a/lib/Okasaki/Tree.hs b/lib/Okasaki/Tree.hs
@@ -130,13 +130,13 @@ dep :: Integral b => Tree a -> b
dep = getSum . cata alg where
alg = \case
LeafF -> mempty
- NodeF l _ r -> Sum 1 <> max l r
+ NodeF l _ r -> 1 <> max l r
wyt :: Integral b => Tree a -> b
wyt = getSum . cata alg where
alg = \case
LeafF -> mempty
- NodeF l _ r -> Sum 1 <> l <> r
+ NodeF l _ r -> 1 <> l <> r
has :: Ord a => a -> Tree a -> Bool
has x = cata $ \case
diff --git a/okasaki.cabal b/okasaki.cabal
@@ -27,6 +27,7 @@ library
Okasaki.Heap.Leftist
, Okasaki.Heap.Leftist.Weighted
, Okasaki.Map
+ , Okasaki.Stack
, Okasaki.Stack.CPS
, Okasaki.Tree
, Okasaki.Tree.CPS
@@ -36,3 +37,19 @@ library
, deriving-compat
, recursion-schemes
+Test-suite tests
+ type: exitcode-stdio-1.0
+ hs-source-dirs: test
+ main-is: Main.hs
+ default-language: Haskell2010
+ other-modules:
+ Heap.Leftist
+ , Heap.Weighted
+ ghc-options:
+ -rtsopts -Wall
+ build-depends:
+ base
+ , data-fix
+ , okasaki
+ , QuickCheck
+ , recursion-schemes
diff --git a/test/Heap/Leftist.hs b/test/Heap/Leftist.hs
@@ -0,0 +1,72 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Heap.Leftist (
+ leftist
+ , heap
+ ) where
+
+import Control.Monad (foldM, replicateM)
+import Data.Functor.Foldable (project, cata, para)
+import Data.Monoid
+import qualified Okasaki.Heap.Leftist as H
+import Test.QuickCheck
+
+lef :: H.Heap a -> Bool
+lef h = getSum (H.ran h) == cata alg h where
+ alg = \case
+ H.LeafF -> 0
+ H.NodeF _ _ _ r -> succ r
+
+hor :: Ord a => H.Heap a -> Bool
+hor = para $ \case
+ H.LeafF -> True
+ H.NodeF _ a (l, c) (r, d) -> case (project l, project r) of
+ (H.LeafF, H.LeafF) -> True && c && d
+ (H.LeafF, H.NodeF _ v _ _) -> a <= v && c && d
+ (H.NodeF _ v _ _, H.LeafF) -> a <= v && c && d
+ (H.NodeF _ u _ _, H.NodeF _ v _ _) -> a <= u && a <= v && c && d
+
+data Act k =
+ Put k
+ | Cut
+ deriving (Eq, Show)
+
+act :: Arbitrary k => Gen (Act k)
+act = frequency [
+ (10, Put <$> arbitrary)
+ , (2, pure Cut)
+ ]
+
+use :: Ord k => Act k -> H.Heap k -> Gen (H.Heap k)
+use a h = case a of
+ Put k -> pure (H.pat k h)
+ Cut -> pure (H.cut h)
+
+hep :: (Ord k, Arbitrary k) => Gen (H.Heap k)
+hep = do
+ num <- choose (0, 10)
+ acts <- replicateM num act
+ foldM (flip use) H.lef acts
+
+lil :: Arbitrary k => H.Heap k -> [H.Heap k]
+lil h = case project h of
+ H.LeafF -> mempty
+ H.NodeF _ a l r -> mconcat [
+ [H.lef]
+ , [l, r]
+ , [H.set b k s | (b, k, s) <- (,,) <$> shrink a <*> lil l <*> lil r]
+ ]
+
+instance (Ord k, Arbitrary k) => Arbitrary (H.Heap k) where
+ arbitrary = hep
+ shrink = lil
+
+leftist :: Property
+leftist = forAllShrink (hep :: Gen (H.Heap Int)) lil lef
+
+heap :: Property
+heap = forAllShrink (hep :: Gen (H.Heap Int)) lil hor
diff --git a/test/Heap/Weighted.hs b/test/Heap/Weighted.hs
@@ -0,0 +1,79 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Heap.Weighted (
+ bleftist
+ , decorated
+ , heap
+ ) where
+
+import Control.Monad (foldM, replicateM)
+import Data.Fix (Fix(..))
+import Data.Functor.Foldable (project, para)
+import qualified Okasaki.Heap.Leftist.Weighted as H
+import Test.QuickCheck
+
+dec :: H.Heap a -> Bool
+dec h = H.siz h == H.wyt h
+
+wef :: H.Heap a -> Bool
+wef = para $ \case
+ H.LeafF -> True
+ H.NodeF _ _ (l, c) (r, d) -> H.siz l >= H.siz r && c && d
+
+hor :: Ord a => H.Heap a -> Bool
+hor = para $ \case
+ H.LeafF -> True
+ H.NodeF _ a (l, c) (r, d) -> case (project l, project r) of
+ (H.LeafF, H.LeafF) -> True && c && d
+ (H.LeafF, H.NodeF _ v _ _) -> a <= v && c && d
+ (H.NodeF _ v _ _, H.LeafF) -> a <= v && c && d
+ (H.NodeF _ u _ _, H.NodeF _ v _ _) -> a <= u && a <= v && c && d
+
+data Act k =
+ Put k
+ | Cut
+ deriving (Eq, Show)
+
+act :: Arbitrary k => Gen (Act k)
+act = frequency [
+ (10, Put <$> arbitrary)
+ , (2, pure Cut)
+ ]
+
+use :: Ord k => Act k -> H.Heap k -> Gen (H.Heap k)
+use a h = case a of
+ Put k -> pure (H.put k h)
+ Cut -> pure (H.cut h)
+
+hep :: (Ord k, Arbitrary k) => Gen (H.Heap k)
+hep = do
+ num <- choose (0, 10)
+ acts <- replicateM num act
+ foldM (flip use) H.lef acts
+
+lil :: Arbitrary k => H.Heap k -> [H.Heap k]
+lil h = case project h of
+ H.LeafF -> mempty
+ H.NodeF _ a l r -> mconcat [
+ [H.lef]
+ , [l, r]
+ , [ Fix (H.NodeF (1 <> H.siz k <> H.siz s) b k s) |
+ (b, k, s) <- (,,) <$> shrink a <*> lil l <*> lil r]
+ ]
+
+instance (Ord k, Arbitrary k) => Arbitrary (H.Heap k) where
+ arbitrary = hep
+ shrink = lil
+
+decorated :: Property
+decorated = forAllShrink (hep :: Gen (H.Heap Int)) lil dec
+
+bleftist :: Property
+bleftist = forAllShrink (hep :: Gen (H.Heap Int)) lil wef
+
+heap :: Property
+heap = forAllShrink (hep :: Gen (H.Heap Int)) lil hor
diff --git a/test/Main.hs b/test/Main.hs
@@ -0,0 +1,4 @@
+module Main where
+
+main :: IO ()
+main = pure ()
