diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -3,13 +3,13 @@ [![Hackage](https://img.shields.io/hackage/v/type-indexed-queues.svg)](https://hackage.haskell.org/package/type-indexed-queues) [![Build Status](https://travis-ci.org/oisdk/type-indexed-queues.svg?branch=master)](https://travis-ci.org/oisdk/type-indexed-queues) - - This library provides implementations of five different heaps (binomial, pairing, skew, leftist, and Braun), each in two flavours: one verified, and one not. At the moment, only structural invariants are maintained. + +More information, and a walkthrough of a couple implementations, can be found at this [blog post](http://doisinkidney.com/posts/2017-04-23-verifying-data-structures-in-haskell-lhs.html). ## Comparisons of verified and unverified heaps Both versions of each heap are provided for comparison: for diff --git a/bench/bench.hs b/bench/bench.hs --- a/bench/bench.hs +++ b/bench/bench.hs @@ -11,6 +11,7 @@ import qualified Data.Queue.Indexed.Skew as Indexed import qualified Data.Queue.Indexed.Leftist as Indexed import qualified Data.Queue.Indexed.Braun as Indexed +import qualified Data.Queue.Indexed.Splay as Indexed import Data.Queue.Indexed.Erased @@ -42,7 +43,8 @@ \xs -> bgroup "seq" - [ bench "trav binom" $ nf (queueTraversable (Proxy :: Proxy (Indexed.Binomial 0))) xs + [ bench "trav splay" $ nf (queueTraversable (Proxy :: Proxy Indexed.Splay)) xs + , bench "trav binom" $ nf (queueTraversable (Proxy :: Proxy (Indexed.Binomial 0))) xs , bench "trav pairing" $ nf (queueTraversable (Proxy :: Proxy Indexed.Pairing)) xs , bench "trav skew" $ nf (queueTraversable (Proxy :: Proxy Indexed.Skew)) xs , bench "trav leftist" $ nf (queueTraversable (Proxy :: Proxy Indexed.Leftist)) xs diff --git a/src/Data/BinaryTree.hs b/src/Data/BinaryTree.hs --- a/src/Data/BinaryTree.hs +++ b/src/Data/BinaryTree.hs @@ -44,7 +44,7 @@ instance NFData a => NFData (Tree a) where rnf Leaf = () - rnf (Node x l r) = rnf x `seq` rnf l `seq` rnf r `seq` () + rnf (Node x l r) = rnf x `seq` rnf l `seq` rnf r instance Eq1 Tree where liftEq _ Leaf Leaf = True diff --git a/src/Data/Queue/Binomial.hs b/src/Data/Queue/Binomial.hs --- a/src/Data/Queue/Binomial.hs +++ b/src/Data/Queue/Binomial.hs @@ -128,8 +128,8 @@ instance NFData a => NFData (Binomial rk a) where rnf Nil = () - rnf (Skip xs) = rnf xs `seq` () - rnf (x :- xs) = rnf x `seq` rnf xs `seq` () + rnf (Skip xs) = rnf xs + rnf (x :- xs) = rnf x `seq` rnf xs deriving instance Foldable (Binomial rk) deriving instance Functor (Binomial rk) diff --git a/src/Data/Queue/Braun.hs b/src/Data/Queue/Braun.hs --- a/src/Data/Queue/Braun.hs +++ b/src/Data/Queue/Braun.hs @@ -75,7 +75,7 @@ -- Instances -------------------------------------------------------------------------------- instance NFData a => NFData (Braun a) where - rnf (Braun xs) = rnf xs `seq` () + rnf (Braun xs) = rnf xs instance Ord a => Eq (Braun a) where (==) = eqQueue diff --git a/src/Data/Queue/Indexed/Binomial.hs b/src/Data/Queue/Indexed/Binomial.hs --- a/src/Data/Queue/Indexed/Binomial.hs +++ b/src/Data/Queue/Indexed/Binomial.hs @@ -148,8 +148,8 @@ instance NFData a => NFData (Binomial rk n a) where rnf Nil = () - rnf (Skip xs) = rnf xs `seq` () - rnf (x :- xs) = rnf x `seq` rnf xs `seq` () + rnf (Skip xs) = rnf xs + rnf (x :- xs) = rnf x `seq` rnf xs deriving instance Foldable (Binomial rk n) deriving instance Functor (Binomial rk n) diff --git a/src/Data/Queue/Indexed/Braun.hs b/src/Data/Queue/Indexed/Braun.hs --- a/src/Data/Queue/Indexed/Braun.hs +++ b/src/Data/Queue/Indexed/Braun.hs @@ -114,4 +114,4 @@ instance NFData a => NFData (Braun n a) where rnf Leaf = () - rnf (Node o x l r) = rnf o `seq` rnf x `seq` rnf l `seq` rnf r `seq` () + rnf (Node o x l r) = rnf o `seq` rnf x `seq` rnf l `seq` rnf r diff --git a/src/Data/Queue/Indexed/Leftist.hs b/src/Data/Queue/Indexed/Leftist.hs --- a/src/Data/Queue/Indexed/Leftist.hs +++ b/src/Data/Queue/Indexed/Leftist.hs @@ -92,4 +92,4 @@ instance NFData a => NFData (Leftist n a) where rnf Leaf = () - rnf (Node n x l r Refl) = n `seq` rnf x `seq` rnf l `seq` rnf r `seq` () + rnf (Node n x l r Refl) = n `seq` rnf x `seq` rnf l `seq` rnf r diff --git a/src/Data/Queue/Indexed/Pairing.hs b/src/Data/Queue/Indexed/Pairing.hs --- a/src/Data/Queue/Indexed/Pairing.hs +++ b/src/Data/Queue/Indexed/Pairing.hs @@ -66,4 +66,4 @@ instance NFData a => NFData (HVec n a) where rnf HNil = () - rnf (HCons x xs) = rnf x `seq` rnf xs `seq` () + rnf (HCons x xs) = rnf x `seq` rnf xs diff --git a/src/Data/Queue/Indexed/Skew.hs b/src/Data/Queue/Indexed/Skew.hs --- a/src/Data/Queue/Indexed/Skew.hs +++ b/src/Data/Queue/Indexed/Skew.hs @@ -40,4 +40,4 @@ instance NFData a => NFData (Skew n a) where rnf Empty = () - rnf (Node x l r) = rnf x `seq` rnf l `seq` rnf r `seq` () + rnf (Node x l r) = rnf x `seq` rnf l `seq` rnf r diff --git a/src/Data/Queue/Indexed/Splay.hs b/src/Data/Queue/Indexed/Splay.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Indexed/Splay.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE RankNTypes #-} + +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} + +-- | Size-indexed splay heaps. +module Data.Queue.Indexed.Splay + (Splay(..)) + where + +import Data.Queue.Indexed.Class + +import GHC.TypeLits + +import Control.DeepSeq (NFData(rnf)) + +-- | A size-indexed splay heap. Based on +-- . +data Splay n a where + Leaf :: Splay 0 a + Node :: a -> !(Splay n a) -> !(Splay m a) -> Splay (1 + n + m) a + +instance Ord a => IndexedQueue Splay a where + minView (Node xx aa bb) = minv aa xx bb where + minv :: Splay n a -> a -> Splay m a -> (a, Splay (n+m) a) + minv Leaf x b = (x, b) + minv (Node x Leaf b) y c = (x, Node y b c) + minv (Node y (Node a x b) c) z d = (w, Node y ab (Node z c d)) + where + (w,ab) = minv x a b + {-# INLINE minv #-} + {-# INLINE minView #-} + empty = Leaf + insert x xs = case partitionLeGt x xs of + SumsTo a b -> Node x a b + {-# INLINE insert #-} + minViewMay Leaf b _ = b + minViewMay n@Node {} _ f = uncurry f (minView n) + +instance Ord a => MeldableIndexedQueue Splay a where + merge Leaf ys = ys + merge xs Leaf = xs + merge (Node x a b) ys = case partitionLeGt x ys of + SumsTo c d -> Node x (merge c a) (merge d b) + {-# INLINE merge #-} + +instance NFData a => + NFData (Splay n a) where + rnf Leaf = () + rnf (Node x l r) = rnf x `seq` rnf l `seq` rnf r + +data SumsTo n a where + SumsTo :: !(Splay x a) -> !(Splay y a) -> SumsTo (x + y) a + +partitionLeGt :: Ord a => a -> Splay n a -> SumsTo n a +partitionLeGt _ Leaf = SumsTo Leaf Leaf +partitionLeGt k t@(Node x a b) = + if x > k + then case a of + Leaf -> SumsTo Leaf t + Node y aa ab -> + if y > k + then case partitionLeGt k aa of + SumsTo small big -> + SumsTo small (Node y big (Node x ab b)) + else case partitionLeGt k ab of + SumsTo small big -> + SumsTo (Node y aa small) (Node x big b) + else case b of + Leaf -> SumsTo t Leaf + Node y ba bb -> + if y > k + then case partitionLeGt k ba of + SumsTo small big -> + SumsTo (Node x a small) (Node y big bb) + else case partitionLeGt k bb of + SumsTo small big -> + SumsTo (Node y (Node x a ba) small) big +{-# INLINE partitionLeGt #-} diff --git a/src/Data/Queue/Leftist.hs b/src/Data/Queue/Leftist.hs --- a/src/Data/Queue/Leftist.hs +++ b/src/Data/Queue/Leftist.hs @@ -101,7 +101,7 @@ instance NFData a => NFData (Leftist a) where rnf Leaf = () - rnf (Node i x l r) = rnf i `seq` rnf x `seq` rnf l `seq` rnf r `seq` () + rnf (Node i x l r) = rnf i `seq` rnf x `seq` rnf l `seq` rnf r instance Ord a => Eq (Leftist a) where (==) = eqQueue diff --git a/src/Data/Queue/Pairing.hs b/src/Data/Queue/Pairing.hs --- a/src/Data/Queue/Pairing.hs +++ b/src/Data/Queue/Pairing.hs @@ -60,7 +60,7 @@ instance NFData a => NFData (Pairing a) where rnf E = () - rnf (T x xs) = rnf x `seq` rnf xs `seq` () + rnf (T x xs) = rnf x `seq` rnf xs instance Ord a => Eq (Pairing a) where (==) = eqQueue diff --git a/src/Data/Queue/Skew.hs b/src/Data/Queue/Skew.hs --- a/src/Data/Queue/Skew.hs +++ b/src/Data/Queue/Skew.hs @@ -50,7 +50,7 @@ -------------------------------------------------------------------------------- instance NFData a => NFData (Skew a) where - rnf (Skew x) = rnf x `seq` () + rnf (Skew x) = rnf x instance Ord a => Eq (Skew a) where (==) = eqQueue diff --git a/src/Data/Queue/Splay.hs b/src/Data/Queue/Splay.hs new file mode 100644 --- /dev/null +++ b/src/Data/Queue/Splay.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE DeriveFunctor #-} + +-- | Simple splay heaps. +module Data.Queue.Splay + (Splay(..)) + where + +import Data.BinaryTree +import Data.Queue.Class + +import Control.DeepSeq (NFData(rnf)) + +-- | A simple splay heap. Based on +-- . +newtype Splay a = Splay { runSplay :: Tree a } deriving Functor + +instance Ord a => Queue Splay a where + minView (Splay Leaf) = Nothing + minView (Splay (Node xx aa bb)) = Just (minv aa xx bb) where + minv Leaf x b = (x, Splay b) + minv (Node x Leaf b) y c = (x, Splay (Node y b c)) + minv (Node y (Node a x b) c) z d = (w, Splay (Node y ab (Node z c d))) + where + (w,Splay ab) = minv x a b + empty = Splay Leaf + insert x (Splay xs) = Splay (Node x a b) where + (a,b) = partitionLeGt x xs + +instance Ord a => MeldableQueue Splay a where + merge (Splay xx) (Splay yy) = Splay (go xx yy) where + go Leaf ys = ys + go (Node x a b) ys = Node x (go c a) (go d b) + where (c,d) = partitionLeGt x ys + +partitionLeGt :: Ord a => a -> Tree a -> (Tree a, Tree a) +partitionLeGt _ Leaf = (Leaf, Leaf) +partitionLeGt k t@(Node x a b) = + if x > k then + case a of + Leaf -> (Leaf,t) + Node y aa ab -> + if y > k then + let (small,big) = partitionLeGt k aa + in (small, Node y big (Node x ab b)) + else + let (small,big) = partitionLeGt k ab + in (Node y aa small, Node x big b) + else + case b of + Leaf -> (t,Leaf) + Node y ba bb -> + if y > k then + let (small,big) = partitionLeGt k ba + in (Node x a small, Node y big bb) + else + let (small,big) = partitionLeGt k bb + in (Node y (Node x a ba) small, big) + +instance Ord a => Monoid (Splay a) where + mempty = empty + mappend = merge + +-------------------------------------------------------------------------------- +-- Instances +-------------------------------------------------------------------------------- +instance NFData a => + NFData (Splay a) where + rnf (Splay x) = rnf x + +instance Ord a => Eq (Splay a) where + (==) = eqQueue + +instance Ord a => Ord (Splay a) where + compare = cmpQueue + +instance (Show a, Ord a) => Show (Splay a) where + showsPrec = showsPrecQueue + +instance (Read a, Ord a) => Read (Splay a) where + readsPrec = readPrecQueue diff --git a/src/Data/Queue/WithDict.hs b/src/Data/Queue/WithDict.hs --- a/src/Data/Queue/WithDict.hs +++ b/src/Data/Queue/WithDict.hs @@ -51,7 +51,7 @@ -- Instances -------------------------------------------------------------------------------- instance NFData (f a) => NFData (WithDict f a) where - rnf (WithDict x) = rnf x `seq` () + rnf (WithDict x) = rnf x deriving instance (Data a, Data (f a), Typeable f, Queue f a) => Data diff --git a/src/TypeLevel/Nat.hs b/src/TypeLevel/Nat.hs --- a/src/TypeLevel/Nat.hs +++ b/src/TypeLevel/Nat.hs @@ -90,11 +90,7 @@ fromInteger = go . abs where go 0 = Z - go n - | even n = r - | otherwise = S r - where - r = S (S Z) * go (n `div` 2) + go n = S (go (n-1)) S n - S m = n - m n - _ = n @@ -135,11 +131,7 @@ toEnum = go . abs where go 0 = Z - go n - | even n = r - | otherwise = S r - where - r = S (S Z) * go (n `div` 2) + go n = S (go (n-1)) enumFrom = iterate S enumFromTo n m = unfoldr f (n, S m - n) where diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -19,6 +19,7 @@ import Data.Queue.Leftist (Leftist,zygoLeftist) import Data.Queue.Pairing (Pairing(..)) import Data.Queue.Skew +import Data.Queue.Splay import qualified Data.Queue.Indexed.Binomial as Indexed import qualified Data.Queue.Indexed.Braun as Indexed @@ -26,6 +27,7 @@ import qualified Data.Queue.Indexed.Leftist as Indexed import qualified Data.Queue.Indexed.Pairing as Indexed import qualified Data.Queue.Indexed.Skew as Indexed +import qualified Data.Queue.Indexed.Splay as Indexed import Data.Queue.Class import Data.Queue.Indexed.Class @@ -38,6 +40,8 @@ import Data.Proxy import Data.Functor.Classes +import Data.Function (on) +import Control.Applicative nat :: Gen Nat nat = fmap (fromInteger . getNonNegative) arbitrary @@ -63,6 +67,9 @@ skew :: Ord a => Skew a -> Bool skew (Skew xs) = isHeap xs +splay :: Ord a => Splay a -> Bool +splay (Splay _) = True + lengthAlg :: (Int, a -> Int -> Int -> Int) lengthAlg = (0, const (+)) @@ -90,6 +97,51 @@ heapSort (Proxy :: Proxy (ErasedSize h)) (xs :: [Int]) === sort xs) +holdsForLength :: Foldable f => (a -> Bool) -> f a -> Int +holdsForLength p = flip (foldr f id ) 0 where + f e a i | p e = a (i + 1) + | otherwise = i + +enumSyntax :: (Ord a, Show a, Enum a) => (Int -> Bool) -> Gen a -> TestTree +enumSyntax p (xs :: Gen a) = + testGroup + "enum" + [ testProperty "from . to" $ + forAll arbitrary $ + \x -> + p x ==> (fromEnum . (toEnum :: Int -> a)) x === x + , testProperty "to . from" $ + forAll xs $ + \x -> + (toEnum . fromEnum) x === x + , testProperty "[n..]" $ + forAll (liftA2 (,) xs arbitrary) $ + \(x,Positive n) -> + let lhs = take n (map fromEnum [x ..]) + rhs = take n [fromEnum x ..] + len = min (holdsForLength p lhs) (holdsForLength p rhs) + in ((===) `on` take len) lhs rhs + , testProperty "[n,m..]" $ + forAll (liftA3 (,,) xs xs arbitrary) $ + \(x,y,Positive n) -> + let lhs = take n (map fromEnum [x,y ..]) + rhs = take n [fromEnum x,fromEnum y ..] + len = min (holdsForLength p lhs) (holdsForLength p rhs) + in ((===) `on` take len) lhs rhs + , testProperty "[n..m]" $ + forAll (liftA2 (,) xs xs) $ + \(x,y) -> + y >= x ==> map fromEnum [x .. y] === [fromEnum x .. fromEnum y] + , testProperty "[l,n..m]" $ + forAll (liftA3 (,,) xs xs xs) $ + \(x,y,z) -> + x > y && + y > + z ==> map fromEnum [x,y .. z] === + [fromEnum x,fromEnum y .. fromEnum z] .&&. + map fromEnum [z,y .. x] === + [fromEnum z,fromEnum y .. fromEnum x]] + leftist :: Ord a => Leftist a -> Bool leftist = zygoLeftist @@ -313,6 +365,16 @@ , ordProps , monoidProps , functorLaws (Proxy :: Proxy Int) (Proxy :: Proxy Int)] + , testGroup "Splay" $ + propHeapSort (Proxy :: Proxy Splay) : + withGen + (fmap (fromList :: [Int] -> Splay Int) arbitrary) + [ proper splay + , readShow + , equalityProps + , ordProps + , monoidProps + , functorLaws (Proxy :: Proxy Int) (Proxy :: Proxy Int)] , testGroup "Indexed Braun" [indexedSort (Proxy :: Proxy Indexed.Braun)] @@ -328,6 +390,9 @@ , testGroup "Indexed Skew" [indexedSort (Proxy :: Proxy Indexed.Skew)] + , testGroup + "Indexed Splay" + [indexedSort (Proxy :: Proxy Indexed.Splay)] , testGroup "Binary Tree" $ withGen intTree @@ -339,4 +404,7 @@ , liftedOrd , monoidProps , functorLaws (Proxy :: Proxy Int) (Proxy :: Proxy Int)] - , testGroup "Nat" $ withGen nat [readShow, equalityProps, ordProps]] + , testGroup "Nat" $ + withGen + nat + [readShow, equalityProps, ordProps, enumSyntax (0 <=)]] diff --git a/type-indexed-queues.cabal b/type-indexed-queues.cabal --- a/type-indexed-queues.cabal +++ b/type-indexed-queues.cabal @@ -1,5 +1,5 @@ name: type-indexed-queues -version: 0.1.0.1 +version: 0.2.0.0 synopsis: Queues with verified and unverified versions. description: This library provides implementations of five different queues @@ -11,7 +11,8 @@ More information, and a walkthough of a couple implementations, can be found at this . . - = Comparisons of verified and unverified queues + /Comparisons of verified and unverified queues/ + . Both versions of each queue are provided for comparison: for instance, compare the standard leftist queue (in "Data.Queue.Leftist"): @@ -77,7 +78,8 @@ > rl = rank r2 +. w1 > rr = rank l2 . - = Using type families and typechecker plugins to encode the invariants + /Using type families and typechecker plugins to encode the invariant/ + . The similarity is accomplished through overloading, and some handy functions. For instance, the second if-then-else works on boolean /singletons/, and the @<=.@ function provides a @@ -89,7 +91,8 @@ A typechecker plugin does most of the heavy lifting, although there are some (small) manual proofs. . - = Uses of verified queues + /Uses of verified queues/ + . The main interesting use of these sturctures is total traversable sorting (). An implementation of this is provided in "Data.Traversable.Parts". I'm @@ -111,6 +114,7 @@ exposed-modules: Data.Queue.Binomial , Data.Queue.Pairing , Data.Queue.Skew + , Data.Queue.Splay , Data.Queue.Leftist , Data.Queue.Braun , Data.Queue.Class @@ -123,6 +127,7 @@ , Data.Queue.Indexed.Class , Data.Queue.Indexed.Erased , Data.Queue.Indexed.List + , Data.Queue.Indexed.Splay , Data.Traversable.Parts , Data.Tree.Replicate @@ -133,10 +138,10 @@ , TypeLevel.Nat.Proofs , TypeLevel.Bool - build-depends: base >= 4.7 && < 5 - , ghc-typelits-natnormalise >= 0.5 - , deepseq >= 1.4 - , containers >= 0.5 + build-depends: base >=4.7 && <5 + , ghc-typelits-natnormalise >=0.4 + , deepseq >=1.4 + , containers >=0.5 default-language: Haskell2010 benchmark bench @@ -146,24 +151,24 @@ main-is: bench.hs ghc-options: -O2 -rtsopts -threaded - build-depends: base >= 4.8 + build-depends: base >=4.8 , type-indexed-queues - , criterion >= 0.6 - , containers >= 0.5 - , random >= 1.1 - , pqueue >= 1.3 + , criterion >=0.1 + , containers >=0.5 + , random >=1.0.0.0 + , pqueue >=1.0.0 test-suite type-indexed-queues-test type: exitcode-stdio-1.0 hs-source-dirs: test main-is: Spec.hs - build-depends: base + build-depends: base >=4.7 && <5 , type-indexed-queues - , QuickCheck >= 2.8 - , doctest - , containers >= 0.5 - , tasty >= 0.11 - , tasty-quickcheck >= 0.8 + , QuickCheck >=1.0 + , doctest >=0.3.0 + , containers >=0.5 + , tasty >=0.1 + , tasty-quickcheck >=0.1 ghc-options: -threaded -rtsopts -with-rtsopts=-N default-language: Haskell2010