
  0 | module SkewBinaryRandomAccessList
  1 | 
  2 | import Data.List
  3 | 
  4 | import RandomAccessList
  5 | 
  6 | %default total
  7 | 
  8 | data Tree a = Leaf a | Node a (Tree a) (Tree a)
  9 | 
 10 | export
 11 | data SkewList a = SL (List (Int, Tree a))
 12 | 
 13 | ncCons : a -> List (Int, Tree a) -> SkewList a
 14 | ncCons x ts = SL ((1, Leaf x) :: ts)
 15 | 
 16 | export
 17 | RandomAccessList SkewList where
 18 |   empty = SL []
 19 |   isEmpty (SL ts) = isNil ts
 20 | 
 21 |   cons x (SL ts@((w1, t1) :: (w2, t2) :: tts)) =
 22 |     if w1 == w2 then SL ((1 + w1 + w2, Node x t1 t2) :: tts) else ncCons x ts
 23 |   cons x (SL ts) = ncCons x ts
 24 | 
 25 |   head (SL []) = assert_total $ idris_crash "empty list"
 26 |   head (SL ((_, Leaf x) :: ts)) = x
 27 |   head (SL ((w, Node x t1 t2) :: ts)) = x
 28 | 
 29 |   tail (SL []) = ?RandomAccessList_rhs_1
 30 |   tail (SL ((_, Leaf x) :: ts)) = SL ts
 31 |   tail (SL ((w, Node x t1 t2) :: ts)) = let hw = assert_total $ w `div` 2 in
 32 |     SL ((hw, t1) :: (hw, t2) :: ts)
 33 | 
 34 |   lookup i (SL ts) = look i ts
 35 |    where
 36 |     lookTree : Int -> Int -> Tree a -> a
 37 |     lookTree _ 0 (Leaf x) = x
 38 |     lookTree _ i (Leaf x) = assert_total $ idris_crash "bad subscript"
 39 |     lookTree w 0 (Node x t1 t2) = x
 40 |     lookTree w i (Node x t1 t2) = let w' = assert_total $ w `div` 2 in
 41 |       if i <= w' then lookTree w' (i - 1) t1 else lookTree w' (i - 1 - w') t2
 42 | 
 43 |     look : Int -> List (Int, Tree a) -> a
 44 |     look i []             = assert_total $ idris_crash "bad subscript"
 45 |     look i ((w, t) :: ts) =
 46 |       if i < w then lookTree w i t else look (i - w) ts
 47 | 
 48 |   update i y (SL ts) = SL (upd i ts)
 49 |    where
 50 |     updTree : Int -> Int -> Tree a -> Tree a
 51 |     updTree _ 0 (Leaf x) = Leaf y
 52 |     updTree _ i (Leaf x) = assert_total $ idris_crash "bad subscript"
 53 |     updTree w 0 (Node x t1 t2) = Node y t1 t2
 54 |     updTree w i (Node x t1 t2) = let w' = assert_total $ w `div` 2 in
 55 |       if i <= w' then Node x (updTree w' (i - 1) t1) t2
 56 |       else Node x t1 (updTree w' (i - 1 - w') t2)
 57 | 
 58 |     upd : Int -> List (Int, Tree a) -> List (Int, Tree a)
 59 |     upd i [] = assert_total $ idris_crash "bad subscript"
 60 |     upd i ((w, t) :: ts) =
 61 |       if i < w then (w, updTree w i t) :: ts else (w, t) :: upd (i - w) ts
 62 |