
  0 | module SplayHeap
  1 | 
  2 | import Heap
  3 | 
  4 | %default total
  5 | 
  6 | export
  7 | data SplayHeap a = E | T (SplayHeap a) a (SplayHeap a)
  8 | 
  9 | partition : Ord a => a -> SplayHeap a -> (SplayHeap a, SplayHeap a)
 10 | partition pivot E = (E, E)
 11 | partition pivot t@(T a x b) =
 12 |   if x <= pivot then
 13 |     case b of
 14 |       E         => (t, E)
 15 |       T b1 y b2 =>
 16 |         if y <= pivot then
 17 |           let (small, big) = partition pivot $ assert_smaller t b2
 18 |           in (T (T a x b1) y small, big)
 19 |         else
 20 |           let (small, big) = partition pivot $ assert_smaller t b1
 21 |           in (T a x small, T big y b2)
 22 |   else
 23 |     case a of
 24 |       E         => (E, t)
 25 |       T a1 y a2 =>
 26 |         if y <= pivot then
 27 |           let (small, big) = partition pivot $ assert_smaller t a2
 28 |           in (T a1 y small, T big x b)
 29 |         else
 30 |           let (small, big) = partition pivot $ assert_smaller t a1
 31 |           in (small, T (T big y a2) x b)
 32 | 
 33 | export
 34 | Heap SplayHeap where
 35 |   empty = E
 36 |   isEmpty E = True
 37 |   isEmpty _ = False
 38 | 
 39 |   insert x t = let (a, b) = partition x t in T a x b
 40 | 
 41 |   merge E t = t
 42 |   merge (T a x b) t = let (ta, tb) = partition x t
 43 |     in T (assert_total $ merge ta a) x (assert_total $ merge tb b)
 44 | 
 45 |   findMin E = assert_total $ idris_crash "empty heap"
 46 |   findMin (T E x b) = x
 47 |   findMin (T a x b) = findMin a
 48 | 
 49 |   deleteMin E = assert_total $ idris_crash "empty heap"
 50 |   deleteMin (T E x b) = b
 51 |   deleteMin (T (T E x b) y c) = T b y c
 52 |   deleteMin (T (T a x b) y c) = T (deleteMin a) x (T b y c)
 53 |