
  0 | module BinaryRandomAccessList
  1 | 
  2 | import Data.List
  3 | 
  4 | import RandomAccessList
  5 | 
  6 | %default total
  7 | 
  8 | data Tree a = Leaf a | Node Int (Tree a) (Tree a)
  9 | data Digit a = Zero | One (Tree a)
 10 | 
 11 | export
 12 | data BinaryList a = BL (List (Digit a))
 13 | 
 14 | size : Tree a -> Int
 15 | size (Leaf x) = 1
 16 | size (Node w t1 t2) = w
 17 | 
 18 | link : Tree a -> Tree a -> Tree a
 19 | link t1 t2 = Node (size t1 + size t2) t1 t2
 20 | 
 21 | consTree : Tree a -> List (Digit a) -> List (Digit a)
 22 | consTree t  []             = [One t]
 23 | consTree t  (Zero   :: ts) = One t :: ts
 24 | consTree t1 (One t2 :: ts) = Zero  :: consTree (link t1 t2) ts
 25 | 
 26 | unconsTree : List (Digit a) -> (Tree a, List (Digit a))
 27 | unconsTree [] = assert_total $ idris_crash "empty list"
 28 | unconsTree [One t] = (t, [])
 29 | unconsTree (One t :: ts) = (t, Zero :: ts)
 30 | unconsTree (Zero :: ts) = case unconsTree ts of
 31 |   (Node _ t1 t2, ts') => (t1, One t2 :: ts')
 32 |   (Leaf _      , _)   => assert_total $ idris_crash "assert_unreachable"
 33 | 
 34 | export
 35 | RandomAccessList BinaryList where
 36 |   empty = BL []
 37 |   isEmpty (BL ts) = isNil ts
 38 | 
 39 |   cons x (BL ts) = BL (consTree (Leaf x) ts)
 40 |   head (BL ts) = assert_total $ let (Leaf x, _) = unconsTree ts in x
 41 |   tail (BL ts) = let (_, ts') = unconsTree ts in BL ts'
 42 | 
 43 |   lookup i (BL ts) = look i ts
 44 |    where
 45 |     lookTree : Int -> Tree a -> a
 46 |     lookTree 0 (Leaf x)       = x
 47 |     lookTree i (Leaf x)       = assert_total $ idris_crash "bad subscript"
 48 |     lookTree i (Node w t1 t2) = let hw = assert_total $ w `div` 2
 49 |       in if i < hw then lookTree i t1 else lookTree (i - hw) t2
 50 | 
 51 |     look : Int -> List (Digit a) -> a
 52 |     look i []            = assert_total $ idris_crash "bad subscript"
 53 |     look i (Zero  :: ts) = look i ts
 54 |     look i (One t :: ts) =
 55 |       if i < size t then lookTree i t else look (i - size t) ts
 56 | 
 57 |   update i y (BL ts) = BL (upd i ts)
 58 |    where
 59 |     updTree : Int -> Tree a -> Tree a
 60 |     updTree 0 (Leaf x)       = Leaf y
 61 |     updTree i (Leaf x)       = assert_total $ idris_crash "bad subscript"
 62 |     updTree i (Node w t1 t2) = let hw = assert_total $ w `div` 2 in
 63 |       if i < hw then Node w (updTree i t1) t2
 64 |       else Node w t1 (updTree (i - hw) t2)
 65 | 
 66 |     upd : Int -> List (Digit a) -> List (Digit a)
 67 |     upd i []            = assert_total $ idris_crash "bad subscript"
 68 |     upd i (Zero  :: ts) = Zero :: upd i ts
 69 |     upd i (One t :: ts) =
 70 |       if i < size t then One (updTree i t) :: ts
 71 |       else One t :: upd (i - size t) ts
 72 |