type-indexed-queues 0.1.0.1 → 0.2.0.0

raw patch · 19 files changed

+279/−47 lines, 19 filesdep ~QuickCheckdep ~basedep ~criterionPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: QuickCheck, base, criterion, doctest, ghc-typelits-natnormalise, pqueue, random, tasty, tasty-quickcheck

API changes (from Hackage documentation)

Files

• README.md +2/−2
• bench/bench.hs +3/−1
• src/Data/BinaryTree.hs +1/−1
• src/Data/Queue/Binomial.hs +2/−2
• src/Data/Queue/Braun.hs +1/−1
• src/Data/Queue/Indexed/Binomial.hs +2/−2
• src/Data/Queue/Indexed/Braun.hs +1/−1
• src/Data/Queue/Indexed/Leftist.hs +1/−1
• src/Data/Queue/Indexed/Pairing.hs +1/−1
• src/Data/Queue/Indexed/Skew.hs +1/−1
• src/Data/Queue/Indexed/Splay.hs +83/−0
• src/Data/Queue/Leftist.hs +1/−1
• src/Data/Queue/Pairing.hs +1/−1
• src/Data/Queue/Skew.hs +1/−1
• src/Data/Queue/Splay.hs +82/−0
• src/Data/Queue/WithDict.hs +1/−1
• src/TypeLevel/Nat.hs +2/−10
• test/Spec.hs +69/−1
• type-indexed-queues.cabal +24/−19

@@ -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

@@ -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

@@ -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

@@ -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)

@@ -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

@@ -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)

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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+-- <https://hackage.haskell.org/package/EdisonCore-1.3.1.1/docs/src/Data-Edison-Coll-SplayHeap.html#Heap this>.+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 #-}

@@ -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

@@ -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

@@ -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

@@ -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+-- <https://hackage.haskell.org/package/EdisonCore-1.3.1.1/docs/src/Data-Edison-Coll-SplayHeap.html#Heap this>.+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

@@ -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

@@ -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

@@ -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 <=)]]

@@ -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 <http://doisinkidney.com/posts/2017-04-23-verifying-data-structures-in-haskell-lhs.html blog post>.   .-  = 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 (<https://github.com/treeowl/sort-traversable sort-traversable>).   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