RBTree-appel-height.hs

{-@ LIQUID "--no-termination"   @-}

module Foo where

import Language.Haskell.Liquid.Prelude

data RBTree a = Leaf 
              | Node Color !(RBTree a) a !(RBTree a)
              deriving (Show)

data Color = B -- ^ Black
           | R -- ^ Red
           deriving (Eq,Show)

---------------------------------------------------------------------------
-- | Add an element -------------------------------------------------------
---------------------------------------------------------------------------

{-@ add :: (Ord a) => a -> RBT a -> RBT a @-}
add x s = makeBlack (ins x s)

{-@ ins :: (Ord a) => a -> t:RBT a -> {v: ARBTN a {(bh t)} | ((IsB t) => (isRB v))} @-}
ins kx Leaf             = Node R Leaf kx Leaf
ins kx s@(Node B l x r) = case compare kx x of
                            LT -> let zoo = lbal (ins kx l) x r in zoo
                            GT -> let zoo = rbal l x (ins kx r) in zoo
                            EQ -> s
ins kx s@(Node R l x r) = case compare kx x of
                            LT -> Node R (ins kx l) x r
                            GT -> Node R l x (ins kx r)
                            EQ -> s

---------------------------------------------------------------------------
-- | Delete an element ----------------------------------------------------
---------------------------------------------------------------------------

{-@ remove :: (Ord a) => a -> RBT a -> RBT a @-}
remove x t = makeBlack (del x t)

{-@ predicate HDel T V = (bh V) = (if (isB T) then (bh T) - 1 else (bh T)) @-}

{-@ del              :: (Ord a) => a -> t:RBT a -> {v:ARBT a | ((HDel t v) && ((isB t) || (isRB v)))} @-}
del x Leaf           = Leaf
del x (Node _ a y b) = case compare x y of
   EQ -> append a b 
   LT -> case a of
           Leaf         -> Node R Leaf y b
           Node B _ _ _ -> lbalS (del x a) y b
           _            -> let zoo = Node R (del x a) y b in zoo 
   GT -> case b of
           Leaf         -> Node R a y Leaf 
           Node B _ _ _ -> rbalS a y (del x b)
           _            -> Node R a y (del x b)

{-@ append                                  :: l:RBT a -> r:RBTN a {(bh l)} -> (ARBT2 a l r) @-}
append Leaf r                               = r
append l Leaf                               = l
append (Node R ll lx lr) (Node R rl rx rr)  = case append lr rl of 
                                                Node R lr' x rl' -> Node R (Node R ll lx lr') x (Node R rl' rx rr)
                                                lrl              -> Node R ll lx (Node R lrl rx rr)
append (Node B ll lx lr) (Node B rl rx rr)  = case append lr rl of 
                                                Node R lr' x rl' -> Node R (Node B ll lx lr') x (Node B rl' rx rr)
                                                lrl              -> lbalS ll lx (Node B lrl rx rr)
append l@(Node B _ _ _) (Node R rl rx rr)   = Node R (append l rl) rx rr
append l@(Node R ll lx lr) r@(Node B _ _ _) = Node R ll lx (append lr r)

---------------------------------------------------------------------------
-- | Delete Minimum Element -----------------------------------------------
---------------------------------------------------------------------------

{-@ deleteMin            :: RBT a -> RBT a @-}
deleteMin (Leaf)         = Leaf
deleteMin (Node _ l x r) = makeBlack t
  where 
    (_, t)               = deleteMin' l x r


{-@ deleteMin'                   :: l:RBT a -> a -> r:RBTN a {(bh l)} -> (a, ARBT2 a l r) @-}
deleteMin' Leaf k r              = (k, r)
deleteMin' (Node R ll lx lr) x r = (k, Node R l' x r)   where (k, l') = deleteMin' ll lx lr 
deleteMin' (Node B ll lx lr) x r = (k, lbalS l' x r )   where (k, l') = deleteMin' ll lx lr 

---------------------------------------------------------------------------
-- | Rotations ------------------------------------------------------------
---------------------------------------------------------------------------

{-@ lbalS                             :: l:ARBT a -> a -> r:RBTN a {1 + (bh l)} -> {v: ARBTN a {1 + (bh l)} | ((IsB r) => (isRB v))} @-}
lbalS (Node R a x b) k r              = Node R (Node B a x b) k r
lbalS l k (Node B a y b)              = let zoo = rbal l k (Node R a y b) in zoo 
lbalS l k (Node R (Node B a y b) z c) = Node R (Node B l k a) y (rbal b z (makeRed c))
lbalS l k r                           = liquidError "nein" -- Node R l k r

{-@ rbalS                             :: l:RBT a -> a -> r:ARBTN a {(bh l) - 1} -> {v: ARBTN a {(bh l)} | ((IsB l) => (isRB v))} @-}
rbalS l k (Node R b y c)              = Node R l k (Node B b y c)
rbalS (Node B a x b) k r              = let zoo = lbal (Node R a x b) k r in zoo
rbalS (Node R a x (Node B b y c)) k r = Node R (lbal (makeRed a) x b) y (Node B c k r)
rbalS l k r                           = liquidError "nein" -- Node R l k r

{-@ lbal                              :: l:ARBT a -> a -> RBTN a {(bh l)} -> RBTN a {1 + (bh l)} @-}
lbal (Node R (Node R a x b) y c) k r  = Node R (Node B a x b) y (Node B c k r)
lbal (Node R a x (Node R b y c)) k r  = Node R (Node B a x b) y (Node B c k r)
lbal l k r                            = Node B l k r

{-@ rbal                              :: l:RBT a -> a -> ARBTN a {(bh l)} -> RBTN a {1 + (bh l)} @-}
rbal a x (Node R b y (Node R c z d))  = Node R (Node B a x b) y (Node B c z d)
rbal a x (Node R (Node R b y c) z d)  = Node R (Node B a x b) y (Node B c z d)
rbal l x r                            = Node B l x r

---------------------------------------------------------------------------
---------------------------------------------------------------------------
---------------------------------------------------------------------------

{-@ type BlackRBT a = {v: RBT a | ((IsB v) && (bh v) > 0)} @-}

{-@ makeRed :: l:BlackRBT a -> ARBTN a {(bh l) - 1} @-}
makeRed (Node _ l x r) = Node R l x r
makeRed Leaf           = liquidError "nein" 

{-@ makeBlack :: ARBT a -> RBT a @-}
makeBlack Leaf           = Leaf
makeBlack (Node _ l x r) = Node B l x r

---------------------------------------------------------------------------
-- | Specifications -------------------------------------------------------
---------------------------------------------------------------------------

{-@ data RBTree a <l :: a -> a -> Prop, r :: a -> a -> Prop>
      = Leaf 
      | Node (color :: Color) 
             (left  :: RBTree <l, r> (a <l key>) 
             (key   :: a) 
             (right :: RBTree <l, r> (a <r key>) 
  @-}
  
-- | Red-Black Trees

{-@ type RBT a    = {v: (RBTree a) | ((isRB v) && (isBH v)) } @-}
{-@ type RBTN a N = {v: (RBT a) | (bh v) = N }                @-}

{-@ measure isRB        :: RBTree a -> Prop
    isRB (Leaf)         = true
    isRB (Node c l x r) = ((isRB l) && (isRB r) && ((Red c) => ((IsB l) && (IsB r))))
  @-}

-- | Almost Red-Black Trees

{-@ type ARBT a    = {v: (RBTree a) | ((isARB v) && (isBH v))} @-}
{-@ type ARBTN a N = {v: (ARBT a)   | (bh v) = N }             @-}

{-@ measure isARB        :: (RBTree a) -> Prop
    isARB (Leaf)         = true 
    isARB (Node c l x r) = ((isRB l) && (isRB r))
  @-}

-- | Conditionally Red-Black Tree

{-@ type ARBT2 a L R = {v:ARBTN a {(bh L)} | (((IsB L) && (IsB R)) => (isRB v))} @-}

-- | Color of a tree

{-@ measure col         :: RBTree a -> Color
    col (Node c l x r)  = c
    col (Leaf)          = B
  @-}

{-@ measure isB        :: RBTree a -> Prop
    isB (Leaf)         = false
    isB (Node c l x r) = c == B 
  @-}

{-@ predicate IsB T = not (Red (col T)) @-}
{-@ predicate Red C = C == R            @-}

-- | Black Height

{-@ measure isBH        :: RBTree a -> Prop
    isBH (Leaf)         = true
    isBH (Node c l x r) = ((isBH l) && (isBH r) && (bh l) = (bh r))
  @-}

{-@ measure bh        :: RBTree a -> Int
    bh (Leaf)         = 0
    bh (Node c l x r) = (bh l) + (if (c == R) then 0 else 1) 
  @-}



-------------------------------------------------------------------------------
-- Auxiliary Invariants -------------------------------------------------------
-------------------------------------------------------------------------------

{-@ predicate Invs V = ((Inv1 V) && (Inv2 V) && (Inv3 V))   @-}
{-@ predicate Inv1 V = (((isARB V) && (IsB V)) => (isRB V)) @-}
{-@ predicate Inv2 V = ((isRB v) => (isARB v))              @-}
{-@ predicate Inv3 V = 0 <= (bh v)                          @-}

{-@ invariant {v: Color | (v = R || v = B)}                 @-}

{-@ invariant {v: RBTree a | (Invs v)}                      @-}

{-@ inv            :: RBTree a -> {v:RBTree a | (Invs v)}   @-}
inv Leaf           = Leaf
inv (Node c l x r) = Node c (inv l) x (inv r)