packages feed

liquidhaskell-0.8.0.2: tests/todo/AVLTree.hs

module AVLTree where 

-- from: https://gist.github.com/gerard/109729

data BT a = L 
          | N { dep   :: !Int 
              , value :: a   
              , left  :: !(BT a)
              , right :: !(BT a) 
              }
          deriving (Show, Eq)

{-@ data BT a [dep] = L 
                    | N (dep   :: !Int) 
                        (value :: a   )
                        (left  :: Bt a) 
                        (right :: BT a) 
  @-}

-- Nice, small and useful functions
empty = L 
 
-- You could say, depth L == Nothing depth (N v L L) == Just 0, but works for
-- me better this way:
depth L = 0
depth (N d _ _ _) = d 

{-@ measure depth   :: BT a -> Int 
    depth (L)         = 0
    depth (N d x l r) = 1 + (if (depth l) <= (depth r) then (depth r) else (depth l)) 
  @-}

inorder             :: BT a -> [a]
inorder L           = []
inorder (N _ v l r) = inorder l ++ [v] ++ inorder r
 
-- left (N _ t _) = t
-- right (N _ _ u) = u
-- value (N v _ _) = v
 
btmin = head . inorder
 
-- FIXME: Could be cleaner BT -> Int using left and right of BT
balFactor :: BT -> BT -> Int
balFactor t u = (depth t) - (depth u)
 
-- Tricky but easy: we return a binary list with the route to the node
search :: BT -> Int -> Maybe [Int]
search L s = Nothing
search (N v t u) s 
    | v == s                  = Just []
    | (search t s) /= Nothing = fmap ((:) 0) (search t s)
    | (search u s) /= Nothing = fmap ((:) 1) (search u s)
    | otherwise               = Nothing
 
-- Complementary to search: get the node with the path
getelem :: BT -> [Int] -> Maybe Int
getelem L _ = Nothing
getelem (N v _ _) [] = Just v
getelem (N v t u) (x:xs)
    | x == 0    = getelem t xs
    | otherwise = getelem u xs
 
-- If you get confused (I do), check this nice picture:
-- http://en.wikipedia.org/wiki/Image:Tree_Rebalancing.gif
balanceLL (N v (N vl tl ul) u)              = (N vl tl (N v ul u))
balanceLR (N v (N vl tl (N vlr tlr ulr)) u) = (N vlr (N vl tl tlr) (N v ulr u))
balanceRL (N v t (N vr (N vrl trl url) ur)) = (N vrl (N v t trl) (N vr url ur)) 
balanceRR (N v t (N vr tr ur))              = (N vr (N v t tr) ur)
 
-- Balanced insert
insert :: BT -> Int -> BT
insert L i = (N i L L)
insert (N v t u) i
    | i == v = (N v t u)
    | i < v && (balFactor ti u) ==  2 && i < value t = balanceLL (N v ti u)
    | i < v && (balFactor ti u) ==  2 && i > value t = balanceLR (N v ti u)
    | i > v && (balFactor t ui) == -2 && i < value u = balanceRL (N v t ui)
    | i > v && (balFactor t ui) == -2 && i > value u = balanceRR (N v t ui)
    | i < v  = (N v ti u)
    | i > v  = (N v t ui)
        where ti = insert t i
              ui = insert u i
 
-- Balanced delete
delete :: BT -> Int -> BT
delete L d = L
delete (N v L L) d = if v == d then L else (N v L L)
delete (N v t L) d = if v == d then t else (N v t L)
delete (N v L u) d = if v == d then u else (N v L u)
delete (N v t u) d
    | v == d                            = (N mu t dmin)
    | v > d && abs (balFactor dt u) < 2 = (N v dt u)
    | v < d && abs (balFactor t du) < 2 = (N v t du)
    | v > d && (balFactor (left u) (right u)) < 0 = balanceRR (N v dt u) 
    | v < d && (balFactor (left t) (right t)) > 0 = balanceLL (N v t du)
    | v > d                                       = balanceRL (N v dt u)
    | v < d                                       = balanceLR (N v t du)
        where dmin = delete u mu
              dt   = delete t d
              du   = delete u d
              mu   = btmin u
 
-- Test Functions
load :: BT -> [Int] -> BT
load t []     = t
load t (x:xs) = insert (load t xs) x
 
unload :: BT -> [Int] -> BT
unload t []     = t
unload t (x:xs) = delete (unload t xs) x
 
sort :: [Int] -> [Int]
sort = inorder . (load empty)
 
isBalanced L = True
isBalanced (N _ t u) = isBalanced t && isBalanced u && abs (balFactor t u) < 2