summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Data/Tree/AVL/Static.hs87
-rw-r--r--Data/Tree/AVL/Static/Internal.hs373
-rw-r--r--LICENSE30
-rw-r--r--Setup.hs2
-rw-r--r--avl-static.cabal36
-rw-r--r--test/Main.hs53
6 files changed, 581 insertions, 0 deletions
diff --git a/Data/Tree/AVL/Static.hs b/Data/Tree/AVL/Static.hs
new file mode 100644
index 0000000..37a11ce
--- /dev/null
+++ b/Data/Tree/AVL/Static.hs
@@ -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
diff --git a/Data/Tree/AVL/Static/Internal.hs b/Data/Tree/AVL/Static/Internal.hs
new file mode 100644
index 0000000..d958733
--- /dev/null
+++ b/Data/Tree/AVL/Static/Internal.hs
@@ -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)
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..cb9f403
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/avl-static.cabal b/avl-static.cabal
new file mode 100644
index 0000000..df45df4
--- /dev/null
+++ b/avl-static.cabal
@@ -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
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
index 0000000..eebbb3c
--- /dev/null
+++ b/test/Main.hs
@@ -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