Splay.hs

{-|
  Purely functional top-down splay sets.

   * D.D. Sleator and R.E. Rarjan,
     \"Self-Adjusting Binary Search Tree\",
     Journal of the Association for Computing Machinery,
     Vol 32, No 3, July 1985, pp 652-686.
     <http://www.cs.cmu.edu/~sleator/papers/self-adjusting.pdf>
-}

module Data.Set.Splay (
  -- * Data structures
    Splay(..)
  -- * Creating sets
  , empty
  , singleton
  , insert
  , fromList
  -- * Converting a list
  , toList
  -- * Membership
  , member
  -- * Deleting
  , delete
  , deleteMin
  , deleteMax
  -- * Checking
  , null
  -- * Set operations
  , union
  , intersection
  , difference
  -- * Helper functions
  , split
  , minimum
  , maximum
  , valid
  , (===)
  , showSet
  , printSet
  ) where

import Data.List (foldl')
import Prelude hiding (minimum, maximum, null)
import Language.Haskell.Liquid.Prelude

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

-- LIQUID left depends on value, so their order had to be changed
{-@ 
  data Splay a <l :: root:a -> a -> Bool, r :: root:a -> a -> Bool>
       = Node (value :: a) 
              (left  :: Splay <l, r> (a <l value>)) 
              (right :: Splay <l, r> (a <r value>)) 
       | Leaf 
@-}

data Splay a = Leaf | Node a (Splay a) (Splay a) deriving Show

{-@ type OSplay a = Splay <{v:a | v < root}, {v:a | v > root}> a @-}

{-@ type MinSPair   a = (a, OSplay a) <{v : Splay {v:a|v>fld} | 0=0}> @-}
{-@ type MinEqSPair a = (a, OSplay a) <{v : Splay {v:a|v>=fld}| 0=0}> @-}

{-@ type MaxSPair   a = (a, OSplay a) <{v : Splay {v:a|v<fld} | 0=0}> @-}
{-@ type MaxEqSPair a = (a, OSplay a) <{v : Splay {v:a|v<=fld}| 0=0}> @-}

instance (Eq a) => Eq (Splay a) where
    t1 == t2 = toList t1 == toList t2

{-| Checking if two splay sets are exactly the same shape.
-}
(===) :: Eq a => Splay a -> Splay a -> Bool
Leaf            === Leaf            = True
(Node x1 l1 r1) === (Node x2 l2 r2) = x1 == x2 && l1 === l2 && r1 === r2
_               === _               = False

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

{-| Splitting smaller and bigger with splay.
    Since this is a set implementation, members must be unique.
-}

{-@ split :: Ord a => x:a -> OSplay a
             -> (OSplay {v:a | v<x}, Bool, OSplay {v:a | v>x}) 
@-}

split :: Ord a => a -> Splay a -> (Splay a, Bool, Splay a)
split _ Leaf = (Leaf,False,Leaf)
split k (Node xk xl xr) = case compare k xk of
    EQ -> (xl, True, xr)
    GT -> case xr of
        Leaf -> (Node xk xl Leaf, False, Leaf)
        Node yk yl yr -> case compare k yk of
            EQ ->     (Node xk xl yl, True, yr)           -- R  :zig
            GT -> let (lt, b, gt) = split k yr            -- RR :zig zag
                  in  (Node yk (Node xk xl yl) lt, b, gt)
            LT -> let (lt, b, gt) = split k yl
                  in  (Node xk xl lt, b, Node yk gt yr)   -- RL :zig zig
    LT -> case xl of
        Leaf          -> (Leaf, False, Node xk Leaf xr)
        Node yk yl yr -> case compare k yk of
            EQ ->     (yl, True, Node xk yr xr)           -- L  :zig
            GT -> let (lt, b, gt) = split k yr            -- LR :zig zag
                  in  (Node yk yl lt, b, Node xk gt xr)
            LT -> let (lt, b, gt) = split k yl            -- LL :zig zig
                  in  (lt, b, Node yk gt (Node xk yr xr))

----------------------------------------------------------------
{-| Empty set.
-}

{-@ empty :: OSplay a @-}
empty :: Splay a
empty = Leaf

{-|
See if the splay set is empty.

>>> Data.Set.Splay.null empty
True
>>> Data.Set.Splay.null (singleton 1)
False
-}

null :: Splay a -> Bool
null Leaf = True
null _ = False

{-| Singleton set.
-}

{-@ singleton :: a -> OSplay a @-}
singleton :: a -> Splay a
singleton x = Node x Leaf Leaf

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

{-| Insertion.

>>> insert 5 (fromList [5,3]) == fromList [3,5]
True
>>> insert 7 (fromList [5,3]) == fromList [3,5,7]
True
>>> insert 5 empty            == singleton 5
True
-}

{-@ insert :: Ord a => a -> OSplay a -> OSplay a @-}
insert :: Ord a => a -> Splay a -> Splay a
insert x t = Node x l r
  where
    (l,_,r) = split x t

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

{-| Creating a set from a list.

>>> empty == fromList []
True
>>> singleton 'a' == fromList ['a']
True
>>> fromList [5,3,5] == fromList [5,3]
True
-}

{-@ fromList :: Ord a => [a] -> OSplay a @-}
fromList :: Ord a => [a] -> Splay a
fromList = foldl' (flip insert) empty

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

{-| Creating a list from a set.

>>> toList (fromList [5,3])
[3,5]
>>> toList empty
[]
-}

toList :: Splay a -> [a]
toList t = inorder t []
  where
    inorder Leaf xs = xs
    inorder (Node x l r) xs = inorder l (x : inorder r xs)

----------------------------------------------------------------
{-| Checking if this element is a member of a set?

>>> fst $ member 5 (fromList [5,3])
True
>>> fst $ member 1 (fromList [5,3])
False
-}

{- member :: Ord a => a -> OSplay a -> (Bool, OSplay a) @-}
member :: Ord a => a -> Splay a -> (Bool, Splay a)
member x t = case split x t of
    (l,True,r) -> (True, Node x l r)
    (Leaf,_,r) -> (False, r)
    (l,_,Leaf) -> (False, l)
    (l,_,r)    -> let (m,l') = deleteMax l
                  in (False, Node m l' r)

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

{-| Finding the minimum element.

>>> fst $ minimum (fromList [3,5,1])
1
>>> minimum empty
*** Exception: minimum
-}

{-@ minimum :: OSplay a -> MinEqSPair a @-}
minimum :: Splay a -> (a, Splay a)
minimum Leaf = error "minimum"
minimum t = let (x,mt) = deleteMin t in (x, Node x Leaf mt)

{-| Finding the maximum element.

>>> fst $ maximum (fromList [3,5,1])
5
>>> maximum empty
*** Exception: maximum
-}

{-@ maximum :: OSplay a -> MaxEqSPair a @-}
maximum :: Splay a -> (a, Splay a)
maximum Leaf = error "maximum"
maximum t = let (x,mt) = deleteMax t in (x, Node x mt Leaf)

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

{-| Deleting the minimum element.

>>> snd (deleteMin (fromList [5,3,7])) == fromList [5,7]
True
>>> deleteMin empty
*** Exception: deleteMin
-}

{-@ deleteMin :: OSplay a -> MinSPair a @-}
deleteMin :: Splay a -> (a, Splay a)
deleteMin Leaf                          = error "deleteMin"
deleteMin (Node x Leaf r)               = (x,r)
deleteMin (Node x (Node lx Leaf lr) r)  = (lx, Node x lr r)
deleteMin (Node x (Node lx ll lr) r)    = let (k,mt) = deleteMin ll
                                          in (k, Node lx mt (Node x lr r))

{-| Deleting the maximum

>>> snd (deleteMax (fromList [(5,"a"), (3,"b"), (7,"c")])) == fromList [(3,"b"), (5,"a")]
True
>>> deleteMax empty
*** Exception: deleteMax
-}


{-@ deleteMax :: OSplay a -> MaxSPair a @-}
deleteMax :: Splay a -> (,) a (Splay a)
deleteMax Leaf                          = error "deleteMax"
deleteMax (Node x l Leaf)               = (x,l)
deleteMax (Node x l (Node rx rl Leaf))  = (rx, Node x l rl)
deleteMax (Node x l (Node rx rl rr))    = let (k,mt) = deleteMax rr
                                          in (k, Node rx (Node x l rl) mt)
----------------------------------------------------------------

{-| Deleting this element from a set.

>>> delete 5 (fromList [5,3]) == singleton 3
True
>>> delete 7 (fromList [5,3]) == fromList [3,5]
True
>>> delete 5 empty            == empty
True
-}

-- Liquid TOPROVE
--  delete :: Ord a => x:a -> OSplay a -> OSplay {v:a| v!=x}
{-@ delete :: Ord a => x:a -> OSplay a -> OSplay a @-}
delete :: Ord a => a -> Splay a -> Splay a
delete x t = case split x t of
    (l, True, r) -> union l r
    _            -> t

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

{-| Creating a union set from two sets.

>>> union (fromList [5,3]) (fromList [5,7]) == fromList [3,5,7]
True
-}

{-@ union :: Ord a => OSplay a -> OSplay a -> OSplay a@-}
union :: Ord a => Splay a -> Splay a -> Splay a
union Leaf t = t
union (Node x a b) t = Node x (union ta a) (union tb b)
  where
    (ta,_,tb) = split x t

{-| Creating a intersection set from sets.

>>> intersection (fromList [5,3]) (fromList [5,7]) == singleton 5
True
-}

{-@ intersection :: Ord a => OSplay a -> OSplay a -> OSplay a @-}
intersection :: Ord a => Splay a -> Splay a -> Splay a
intersection Leaf _          = Leaf
intersection _ Leaf          = Leaf
intersection t1 (Node x l r) = case split x t1 of
    (l', True,  r') -> Node x (intersection l' l) (intersection r' r)
    (l', False, r') -> union (intersection l' l) (intersection r' r)

{-| Creating a difference set from sets.

>>> difference (fromList [5,3]) (fromList [5,7]) == singleton 3
True
-}

{-@ difference :: Ord a => OSplay a -> OSplay a -> OSplay a @-}
difference :: Ord a => Splay a -> Splay a -> Splay a
difference Leaf _          = Leaf
difference t1 Leaf         = t1
difference t1 (Node x l r) = union (difference l' l) (difference r' r)
  where
    (l',_,r') = split x t1

----------------------------------------------------------------
-- Basic operations
----------------------------------------------------------------
{-| Checking validity of a set.
-}

valid :: Ord a => Splay a -> Bool
valid t = isOrdered t

isOrdered :: Ord a => Splay a -> Bool
isOrdered t = ordered $ toList t
  where
    ordered [] = True
    ordered [_] = True
    ordered (x:y:xys) = x < y && ordered (y:xys)


showSet :: Show a => Splay a -> String
showSet = showSet' ""

showSet' :: Show a => String -> Splay a -> String
showSet' _ Leaf = "\n"
showSet' pref (Node x l r) = show x ++ "\n"
                        ++ pref ++ "+ " ++ showSet' pref' l
                        ++ pref ++ "+ " ++ showSet' pref' r
  where
    pref' = "  " ++ pref

printSet :: Show a => Splay a -> IO ()
printSet = putStr . showSet

{-
Demo: http://www.link.cs.cmu.edu/splay/
Paper: http://www.cs.cmu.edu/~sleator/papers/self-adjusting.pdf
TopDown: http://www.cs.umbc.edu/courses/undergraduate/341/fall02/Lectures/Splay/TopDownSplay.ppt
Blog: http://chasen.org/~daiti-m/diary/?20061223
      http://www.geocities.jp/m_hiroi/clisp/clispb07.html


               fromList    minimum          delMin          member
Blanced Tree   N log N     log N            log N           log N
Skew Heap      N log N     1                log N(???)      N/A
Splay Heap     N           log N or A(N)?   log N or A(N)?  log N or A(N)?

-}