avl-static (empty) → 0.1.0.0
raw patch · 6 files changed
+581/−0 lines, 6 filesdep +QuickCheckdep +avl-staticdep +basesetup-changed
Dependencies added: QuickCheck, avl-static, base, test-framework, test-framework-quickcheck2
Files
- Data/Tree/AVL/Static.hs +87/−0
- Data/Tree/AVL/Static/Internal.hs +373/−0
- LICENSE +30/−0
- Setup.hs +2/−0
- avl-static.cabal +36/−0
- test/Main.hs +53/−0
+ Data/Tree/AVL/Static.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE GADTs #-}+module Data.Tree.AVL.Static (+ AVLTree,+ Zipper,+ empty,+ size,+ insert,+ search,+ delete,+ value,+ begin,+ end,+ predecessor,+ successor,+) where++import Data.Tree.AVL.Static.Internal++-- |An empty 'AVLTree'.+--+-- /O(1)/.+empty :: AVLTree a+empty = T Nil 0++-- |The number of nodes of an 'AVLTree'.+--+-- /O(1)/.+size :: AVLTree a -> Integer+size (T _ k) = k++-- |Insert a value into an 'AVLTree'.+-- If the value already exists, does nothing.+--+-- /O(log n)/.+insert :: Ord a => a -> AVLTree a -> AVLTree a+insert x t = case zipTo x (unZip t) of+ Zipper Nil ctx -> insertUnbalancedAt (Balanced x Nil Nil) ctx+ _ -> t++-- |Search for a node with a given value. Returns a 'Zipper' pointing to+-- a subtree whose root has that value, or 'Nothing' if the value is not+-- in the tree.+--+-- /O(log n)/.+search :: Ord a => a -> AVLTree a -> Maybe (Zipper a)+search x t = case zipTo x (unZip t) of+ Zipper Nil _ -> Nothing+ z -> Just z++-- |Returns a 'Zipper' to the predecessor of a value in a tree. If the input+-- 'Zipper' points to the smallest element in the tree, returns 'Nothing'.+--+-- /O(log n)/.+predecessor :: Ord a => Zipper a -> Maybe (Zipper a)+predecessor = zipToPredecessor++-- |Returns a 'Zipper' to the successor of a value in a tree. If the input+-- 'Zipper' points to the greatest element in the tree, returns 'Nothing'.+--+-- /O(log n)/.+successor :: Ord a => Zipper a -> Maybe (Zipper a)+successor = zipToSuccessor++-- |Deletes a value from an 'AVLTree'. If the value does not exist in the tree,+-- does nothing.+--+-- /O(log n)/.+delete :: Ord a => a -> AVLTree a -> AVLTree a+delete x t = case zipTo x (unZip t) of+ Zipper Nil _ -> t+ z -> deleteBST z++-- |Returns a 'Zipper' to the smallest element in the tree, or 'Nothing' if the+-- tree is empty.+--+-- /O(log n)/.+begin :: AVLTree a -> Maybe (Zipper a)+begin t | size t == 0 = Nothing+ | otherwise = Just . zipToSmallest . unZip $ t++-- |Returns a 'Zipper' to the greatest element in the tree, or 'Nothing' if the+-- tree is empty.+--+-- /O(log n)/.+end :: AVLTree a -> Maybe (Zipper a)+end t | size t == 0 = Nothing+ | otherwise = Just . zipToGreatest . unZip $ t
+ Data/Tree/AVL/Static/Internal.hs view
@@ -0,0 +1,373 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Data.Tree.AVL.Static.Internal where++import Prelude hiding (fmap)+import Control.Applicative (Applicative, pure, (<$>), (<*>))+import Data.Functor (Functor, fmap)+import Data.Traversable (Traversable, traverse)+import Data.Monoid (Monoid, mempty, (<>))+import Data.Foldable (Foldable, foldMap)++-- |A natural number datatype, hoisted to a Kind using DataKinds.+data Nat = Zero | Succ Nat deriving (Eq, Ord, Show)++-- |An @'AVLNode' n a@ is a node whose subtree has height @n@, and values of+-- type @a@.+data AVLNode :: Nat -> * -> * where+ Nil :: AVLNode Zero a+ Leftie :: a -> AVLNode (Succ n) a -> AVLNode n a -> AVLNode (Succ (Succ n)) a+ Rightie :: a -> AVLNode n a -> AVLNode (Succ n) a -> AVLNode (Succ (Succ n)) a+ Balanced :: a -> AVLNode n a -> AVLNode n a -> AVLNode (Succ n) a++deriving instance Show a => Show (AVLNode n a)+-- |An @'AVLTree' a@ is a statically balanced tree, whose non-nil values+-- have type @a@.+data AVLTree a = forall n. T (AVLNode n a) Integer+deriving instance Show a => Show (AVLTree a)++foldNode :: (b -> b -> a -> b) -> b -> AVLNode n a -> b+foldNode _ e Nil = e+foldNode f e (Balanced x l r) = f (foldNode f e l) (foldNode f e r) x+foldNode f e (Rightie x l r) = f (foldNode f e l) (foldNode f e r) x+foldNode f e (Leftie x l r) = f (foldNode f e l) (foldNode f e r) x++fmapNode :: (a -> b) -> AVLNode n a -> AVLNode n b+fmapNode _ Nil = Nil+fmapNode f (Balanced x l r) = Balanced (f x) (fmapNode f l) (fmapNode f r)+fmapNode f (Rightie x l r) = Rightie (f x) (fmapNode f l) (fmapNode f r)+fmapNode f (Leftie x l r) = Leftie (f x) (fmapNode f l) (fmapNode f r)++traverseNode :: Applicative f => (a -> f b) -> AVLNode n a -> f (AVLNode n b)+traverseNode _ Nil = pure Nil+traverseNode f (Balanced x l r) = flip Balanced <$> traverseNode f l+ <*> f x+ <*> traverseNode f r+traverseNode f (Rightie x l r) = flip Rightie <$> traverseNode f l+ <*> f x+ <*> traverseNode f r+traverseNode f (Leftie x l r) = flip Leftie <$> traverseNode f l+ <*> f x+ <*> traverseNode f r+instance Functor AVLTree where+ -- |Functor instance for AVLNodes. Note, this isn't actually a Functor, since+ -- we require f monotonic to maintain the AVL invariant. That is, the mapped+ -- morphism f needs to be (Ord a, Ord b) => a -> b, such that+ --+ -- > x < x' => f x < f x'.+ fmap f (T r k) = T (fmapNode f r) k++instance Foldable AVLTree where+ -- | The folding is in-order.+ -- >>> let t = foldr insert empty [1..10]+ -- >>> foldr (++) [] (pure <$> t)+ -- >>> [1,2,3,4,5,6,7,8,9,10]+ -- >>> foldr (+) 0 t+ -- >>> 55+ foldMap f (T r _) = foldNode (\x y z -> x <> z <> y) mempty (fmapNode f r)++instance Traversable AVLTree where+ -- |Traversable instance for AVLNodes. This is an in-order traversal of the+ -- subtree rooted at a given node.+ -- >>> let t = foldr insert empty [1, 2, 3]+ -- >>> traverse print t+ -- >>> 1+ -- >>> 2+ -- >>> 3+ traverse f (T r k) = flip T k <$> traverseNode f r++-- |The context for an 'AVLTree'\'s 'Zipper'.+-- The idea is that it represents an entire 'AVLTree', save for a hole in it.+-- A 'Context' @n@ @a@ means an entire 'AVLTree' @a@, with a hole of height n.+-- Its use is that, in a 'Zipper', we have a simple way to move around in the+-- tree, starting at that hole.+--+-- See <http://strictlypositive.org/diff.pdf this> paper by Conor McBride for+-- more information.+data Context :: Nat -> * -> * where+ -- A balanced context. BC isLeft x y means the traversal went left,+ -- on a node Balanced x, where y is the subtree not taken in the+ -- traversal.+ BC :: Bool -> a -> AVLNode n a -> Context (Succ n) a -> Context n a+ -- A leftie context, where we've taken the right branch of the subtree.+ LRC :: a -> AVLNode (Succ n) a -> Context (Succ (Succ n)) a -> Context n a+ -- A leftie context, where we've taken the left branch of the subtree.+ LLC :: a -> AVLNode n a -> Context (Succ (Succ n)) a -> Context (Succ n) a+ -- A rightie context, where we've taken the left branch of the subtree.+ RLC :: a -> AVLNode (Succ n) a -> Context (Succ (Succ n)) a -> Context n a+ -- A rightie context, where we've taken the right branch of the subtree.+ RRC :: a -> AVLNode n a -> Context (Succ (Succ n)) a -> Context (Succ n) a+ -- The root context, where every traversal of an AVLTree starts.+ Root :: Integer -> Context n a+deriving instance Show a => Show (Context n a)++-- |A 'Zipper' is a useful construct for functional datastructure traversals.+-- For us, it can be thought of as a pointer to a subtree in an 'AVLTree'.+--+-- See <http://yquem.inria.fr/~huet/PUBLIC/zip.pdf Functional Pearls: Zippers>+-- for more information.+data Zipper a = forall n. Zipper (AVLNode n a) (Context n a)+deriving instance Show a => Show (Zipper a)++-- |Gets the value at the root of the subtree pointed by that 'Zipper'.+value :: Zipper a -> a+value (Zipper (Balanced x _ _) _) = x+value (Zipper (Leftie x _ _) _) = x+value (Zipper (Rightie x _ _) _) = x+value (Zipper Nil _) = error "Zipper points to Nil."++-- |Constructs a 'Zipper' to the root of the given tree.+unZip :: AVLTree a -> Zipper a+unZip (T r k) = Zipper r (Root k)++-- |Given a function that manipulates the tree size (number of nodes), and a+-- 'Zipper', constructs an 'AVLTree' with the new height, by "zipping up" to+-- the root of the tree pointed to by the 'Zipper'.+zipUp :: (Integer -> Integer) -> Zipper a -> AVLTree a+zipUp f (Zipper t (Root k)) = T t (f k)+zipUp f z = zipUp f (up z)++-- |Navigates up in a 'Zipper'.+up :: Zipper a -> Zipper a+up (Zipper x (LRC v y ctx)) = Zipper (Leftie v y x) ctx+up (Zipper x (LLC v y ctx)) = Zipper (Leftie v x y) ctx+up (Zipper x (RLC v y ctx)) = Zipper (Rightie v x y) ctx+up (Zipper x (RRC v y ctx)) = Zipper (Rightie v y x) ctx+up (Zipper x (BC True v y ctx)) = Zipper (Balanced v x y) ctx+up (Zipper x (BC False v y ctx)) = Zipper (Balanced v y x) ctx+-- TODO: Should I error out on Root?+up z@(Zipper _ (Root _)) = z++-- |Returns whether we can navigate up.+canGoUp :: Zipper a -> Bool+canGoUp (Zipper _ (Root _)) = False+canGoUp _ = True++-- |Navigates left in a 'Zipper'.+left :: Zipper a -> Zipper a+left (Zipper (Balanced x l r) ctx) = Zipper l (BC True x r ctx)+left (Zipper (Leftie x l r) ctx) = Zipper l (LLC x r ctx)+left (Zipper (Rightie x l r) ctx) = Zipper l (RLC x r ctx)+-- TODO: Should I error out on Nil?+left z = z++-- |Returns whether we can navigate left.+canGoLeft :: Zipper a -> Bool+canGoLeft (Zipper (Rightie _ Nil _) _) = False+canGoLeft (Zipper (Balanced _ Nil _) _) = False+canGoLeft (Zipper Nil _) = False+canGoLeft _ = True++-- |Navigates right in a 'Zipper'.+right :: Zipper a -> Zipper a+right (Zipper (Rightie x l r) ctx) = Zipper r (RRC x l ctx)+right (Zipper (Leftie x l r) ctx) = Zipper r (LRC x l ctx)+right (Zipper (Balanced x l r) ctx) = Zipper r (BC False x l ctx)+-- TODO: Should I error out on Nil?+right z = z++-- |Returns whether we can navigate right.+canGoRight :: Zipper a -> Bool+canGoRight (Zipper (Leftie _ _ Nil) _) = False+canGoRight (Zipper (Balanced _ _ Nil) _ ) = False+canGoRight (Zipper Nil _) = False+canGoRight _ = True++-- |Returns whether the pointed to subtree is a left child of its parent.+isLeft :: Zipper a -> Bool+isLeft z | not (canGoUp z) = False+isLeft (Zipper _ (BC False _ _ _)) = False+isLeft (Zipper _ (RRC _ _ _)) = False+isLeft (Zipper _ (LRC _ _ _ )) = False+isLeft _ = True++-- |Returns whether the pointed to subtree is a right child of its parent.+isRight :: Zipper a -> Bool+isRight = (&&) <$> canGoUp <*> (not . isLeft)++-- |Returns whether the pointed to subtree is a leaf.+isLeaf :: Zipper a -> Bool+isLeaf = (&&) <$> (not . canGoLeft) <*> (not . canGoRight)++-- |Descends (never ascends) to a subtree whose root has a given value.+-- If no such subtree exists, points to a 'Nil' where the value would be found,+-- were it to exist.+zipTo :: Ord a => a -> Zipper a -> Zipper a+zipTo _ z@(Zipper Nil _) = z+zipTo x z = let v = value z+ in case compare x v of+ EQ -> z+ LT -> zipTo x $ left z+ GT -> zipTo x $ right z++-- |Insert an 'AVLNode' of height (n + 1) in a 'Context' with a hole of size n.+-- Since this cannot be done in the usual way, rotations are used to return+-- an 'AVLTree' that may nothave the same height as the 'Context'\'s tree did,+-- or have the same structure, but holds the same values, and has this enlarged+-- 'AVLNode' in it.+insertUnbalancedAt :: AVLNode (Succ n) a -> Context n a -> AVLTree a+insertUnbalancedAt t (LRC v y ctx) = zipUp (+1) $ Zipper (Balanced v y t) ctx+insertUnbalancedAt t (RLC v y ctx) = zipUp (+1) $ Zipper (Balanced v t y) ctx+insertUnbalancedAt t (Root k) = T t (k + 1)++{- LLC -}+insertUnbalancedAt (Leftie b g p) (LLC a d ctx) = zipUp (+1) z+ where+ z = Zipper (Balanced b g (Balanced a p d)) ctx+insertUnbalancedAt (Rightie b g q) (LLC a d ctx) = zipUp (+1) z+ where+ z = Zipper t ctx+ t = case q of+ Rightie p t1 t2 -> Balanced p (Leftie b g t1) (Balanced a t2 d)+ Leftie p t1 t2 -> Balanced p (Balanced b g t1) (Rightie a t2 d)+ Balanced p t1 t2 -> Balanced p (Balanced b g t1) (Balanced a t2 d)+insertUnbalancedAt (Balanced b g p) (LLC a d ctx) = goUp+ where+ goUp = insertUnbalancedAt (Rightie b g (Leftie a p d)) ctx++{- RRC -}+insertUnbalancedAt (Rightie b g p) (RRC a d ctx) = zipUp (+1) z+ where+ z = Zipper (Balanced b (Balanced a d g) p) ctx+insertUnbalancedAt (Leftie b q p) (RRC a d ctx) = zipUp (+1) z+ where+ z = Zipper t ctx+ t = case q of+ Leftie g t1 t2 -> Balanced g (Balanced a d t1) (Rightie b t2 p)+ Rightie g t1 t2 -> Balanced g (Leftie a d t1) (Balanced b t2 p)+ Balanced g t1 t2 -> Balanced g (Balanced a d t1) (Balanced b t2 p)+insertUnbalancedAt (Balanced b p g) (RRC a d ctx) = goUp+ where+ goUp = insertUnbalancedAt (Leftie b (Rightie a d p) g) ctx++{- BC -}+insertUnbalancedAt (Leftie b g p) (BC True a d ctx) = goUp+ where+ goUp = insertUnbalancedAt (Rightie b g (Rightie a p d)) ctx+insertUnbalancedAt (Rightie b g p) (BC False a d ctx) = goUp+ where+ goUp = insertUnbalancedAt (Leftie b (Leftie a d g) p) ctx+insertUnbalancedAt t (BC False a d ctx) = insertUnbalancedAt (Rightie a d t) ctx+insertUnbalancedAt t (BC True a d ctx) = insertUnbalancedAt (Leftie a t d) ctx++-- |Given a 'Zipper' to a node in the tree, returns a 'Zipper' to the successor+-- of this node. If no such successor exists, returns 'Nothing'.+zipToSuccessor :: Zipper a -> Maybe (Zipper a)+zipToSuccessor z | canGoRight z = Just . zipToSmallest $ right z+ | otherwise = let parent = zipToFirstLeftChild z+ in up <$> parent+-- |Given a 'Zipper' to a node in the tree, returns a Zipper to the predecessor+-- of this node. If no such predecessor exists, returns 'Nothing'.+zipToPredecessor :: Zipper a -> Maybe (Zipper a)+zipToPredecessor z | canGoLeft z = Just . zipToGreatest $ left z+ | otherwise = let parent = zipToFirstRightChild z+ in up <$> parent+-- |Given a 'Zipper' to a node @X@ in the tree, returns a 'Zipper' to the+-- smallest node in the subtree rooted at @X@.+zipToSmallest :: Zipper a -> Zipper a+zipToSmallest z | canGoLeft z = zipToSmallest (left z)+ | otherwise = z+-- |Given a 'Zipper' to a node @X@ in the tree, returns a 'Zipper' to the+-- greatest node in the subtree rooted at @X@.+zipToGreatest :: Zipper a -> Zipper a+zipToGreatest z | canGoRight z = zipToGreatest (right z)+ | otherwise = z++-- |Given a 'Zipper' @Z@, which points to a subtree @S@, returns a 'Zipper' to+-- the first ancestor of @S@ which is a left child of its parent. If such an+-- ancestor does not exist, returns 'Nothing'.+zipToFirstLeftChild :: Zipper a -> Maybe (Zipper a)+zipToFirstLeftChild z | isLeft z = Just z+zipToFirstLeftChild z | canGoUp z = zipToFirstLeftChild (up z)+ | otherwise = Nothing++-- |Given a 'Zipper' @Z@, which points to a subtree @S@, returns a 'Zipper' to+-- the first ancestor of @S@ which is a right child of its parent. If such an+-- ancestor does not exist, returns 'Nothing'.+zipToFirstRightChild :: Zipper a -> Maybe (Zipper a)+zipToFirstRightChild z | isRight z = Just z+zipToFirstRightChild z | canGoUp z = zipToFirstRightChild (up z)+ | otherwise = Nothing++-- |Replaces a given value by another, in the 'AVLTree' represented by a+-- 'Context'.+fixContext :: forall a n. Eq a => a -> a -> Context n a -> Context n a+fixContext k k' = go+ where+ z x = if x == k then k' else x+ go :: Context n' a -> Context n' a+ go r@(Root _) = r+ go (BC goLeft x y ctx) = BC goLeft (z x) y (go ctx)+ go (LLC x y ctx) = LLC (z x) y (go ctx)+ go (LRC x y ctx) = LRC (z x) y (go ctx)+ go (RRC x y ctx) = RRC (z x) y (go ctx)+ go (RLC x y ctx) = RLC (z x) y (go ctx)++-- |Given a 'Zipper' @Z@, deletes the value at the root of the subtree pointed+-- to by @Z@. It returns a modified 'AVLTree' with this change applied.+-- The removal is straight-up BST removal, folowed by an AVL rebalancing.+deleteBST :: Eq a => Zipper a -> AVLTree a+deleteBST (Zipper (Balanced _ Nil Nil) ctx) = rebalance Nil ctx+deleteBST (Zipper (Rightie _ Nil r) ctx) = rebalance r ctx+deleteBST (Zipper (Leftie _ l Nil) ctx) = rebalance l ctx+deleteBST z@(Zipper (Rightie k _ _) _) =+ let Just s = zipToSuccessor z+ in case s of+ Zipper (Balanced k' Nil Nil) ctx' -> rebalance Nil (fixContext k k' ctx')+ Zipper (Rightie k' Nil r) ctx' -> rebalance r (fixContext k k' ctx')+ _ -> error "The impossible has happened, bad successor found."+deleteBST z@(Zipper (Leftie k _ _) _) =+ let Just s = zipToPredecessor z+ in case s of+ Zipper (Balanced k' Nil Nil) ctx' -> rebalance Nil (fixContext k k' ctx')+ Zipper (Leftie k' l Nil) ctx' -> rebalance l (fixContext k k' ctx')+ _ -> error "The impossible has happened, bad predecessor found."+deleteBST z@(Zipper (Balanced k _ _) _) =+ let Just s = zipToSuccessor z+ in case s of+ Zipper (Balanced k' Nil Nil) ctx' -> rebalance Nil (fixContext k k' ctx')+ Zipper (Rightie k' Nil r) ctx' -> rebalance r (fixContext k k' ctx')+ _ -> error "The impossible has happened, bad successor found."+deleteBST (Zipper Nil _) = error "You cannot delete Nil."++-- | Given an 'AVLNode' @n@ @a@, and a 'Context' with a hole of size @(n + 1)@,+-- returns an 'AVLTree' @a@ with the 'AVLNode' being placed in that 'Context'.+-- Since this cannot be done normally, it uses rotations to return an 'AVLTree'+-- that has the same elements as the 'Context' and the 'AVLNode' together,+-- but may have a different structure than the tree the 'Context' represented.+rebalance :: AVLNode n a -> Context (Succ n) a -> AVLTree a+rebalance t (Root k) = (T t (k - 1))+rebalance t (BC True a d ctx) = zipUp (subtract 1) $ Zipper (Rightie a t d) ctx+rebalance t (BC False a d ctx) = zipUp (subtract 1) $ Zipper (Leftie a d t) ctx+rebalance t (LLC a d ctx) = rebalance (Balanced a t d) ctx+rebalance t (RRC a d ctx) = rebalance (Balanced a d t) ctx+rebalance t (RLC a (Balanced d t1 t2) ctx) = zipUp (subtract 1) z+ where+ z = Zipper (Leftie d (Rightie a t t1) t2) ctx+rebalance t (RLC a (Rightie d t1 t2) ctx) = rebalance z ctx+ where+ z = Balanced d (Balanced a t t1) t2+rebalance t (RLC a (Leftie d q t2) ctx) = rebalance z ctx+ where+ z = case q of+ Leftie t1 p1 p2 -> Balanced t1 (Balanced a t p1) (Rightie d p2 t2)+ Rightie t1 p1 p2 -> Balanced t1 (Leftie a t p1) (Balanced d p2 t2)+ Balanced t1 p1 p2 -> Balanced t1 (Balanced a t p1) (Balanced d p2 t2)+rebalance t (LRC a (Balanced d t1 t2) ctx) = zipUp (subtract 1) z+ where+ z = Zipper (Rightie d t1 (Leftie a t2 t)) ctx+rebalance t (LRC a (Leftie d t1 t2) ctx) = rebalance z ctx+ where+ z = Balanced d t1 (Balanced a t2 t)+rebalance t (LRC a (Rightie d t1 q) ctx) = rebalance z ctx+ where+ z = case q of+ Leftie t2 p1 p2 -> Balanced t2 (Balanced d t1 p1) (Rightie a p2 t)+ Rightie t2 p1 p2 -> Balanced t2 (Leftie d t1 p1) (Balanced a p2 t)+ Balanced t2 p1 p2 -> Balanced t2 (Balanced d t1 p1) (Balanced a p2 t)
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2014, Federico Lebrón++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Federico Lebrón nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ avl-static.cabal view
@@ -0,0 +1,36 @@+-- Initial avl.cabal generated by cabal init. For further documentation, +-- see http://haskell.org/cabal/users-guide/++name: avl-static+version: 0.1.0.0+synopsis: A compile-time balanced AVL tree.+description: A compile-time balanced AVL tree.+license: BSD3+license-file: LICENSE+author: Federico Lebrón+maintainer: federico.lebron@gmail.com+-- copyright: +category: Data+build-type: Simple+extra-source-files: test/Main.hs+cabal-version: >=1.10++library+ exposed-modules: Data.Tree.AVL.Static, Data.Tree.AVL.Static.Internal+ -- other-modules: + other-extensions: GADTs, ExistentialQuantification, DataKinds, InstanceSigs, StandaloneDeriving, KindSignatures, ScopedTypeVariables+ build-depends: base >=4.6 && <4.7+ -- hs-source-dirs: + default-language: Haskell2010++source-repository head+ type: git+ location: https://github.com/fedelebron/AVL++test-suite avl-test+ hs-source-dirs: test+ x-uses-tf: true+ type: exitcode-stdio-1.0+ main-is: Main.hs+ build-depends: base > 4, QuickCheck, test-framework >= 0.4.1, test-framework-quickcheck2, avl-static+ default-language: Haskell2010
+ test/Main.hs view
@@ -0,0 +1,53 @@+{-# LANGUAGE TemplateHaskell #-}++module Main where++import Test.QuickCheck+import Test.QuickCheck.All+import Data.Foldable (toList)+import Data.Tree.AVL.Static+import Data.Maybe+import System.Exit+import Data.List (nub, sort)++instance (Arbitrary a, Ord a) => Arbitrary (AVLTree a) where+ arbitrary = do+ n <- choose (0, 100)+ xs <- vector n+ return $ foldr insert empty xs+ shrink t = let xs = toList t+ in map (flip delete t) xs++prop_sizeEmpty = size empty == 0++prop_sizeInserted :: NonNegative Integer -> Bool+prop_sizeInserted (NonNegative k) = size (foldr insert empty [1..k]) == k++prop_toList xs = toList (foldr insert empty xs) == nub (sort xs)++prop_insertDelete t x = (isNothing $ search x t) ==>+ toList (delete x (insert x t)) == toList t++prop_searchAfterInsert x t = (isNothing $ search x t) ==>+ isJust . search x $ insert x t++prop_searchAfterDelete t x = (isJust $ search x t) ==>+ isNothing . search x $ delete x t++prop_successor t = let z = begin t+ zs = takeWhile isJust $ iterate (>>= successor) z+ d = map value (catMaybes zs)+ in toList t == d &&+ sort d == d++prop_predecessor t = let z = end t+ zs = takeWhile isJust $ iterate (>>= predecessor) z+ d = reverse . map value $ catMaybes zs+ in toList t == d &&+ sort d == d++main = do+ result <- $(quickCheckAll)+ if result+ then exitSuccess+ else exitFailure