0 | module AltBinaryRandomAccessList
 1 |
 2 | import RandomAccessList
 3 |
 4 | %default total
 5 |
 6 | export
 7 | data BinaryList a = Nil | Zero (BinaryList (a, a)) | One a (BinaryList (a,a))
 8 |
 9 | uncons : BinaryList a -> (a, BinaryList a)
10 | uncons Nil = assert_total $ idris_crash "empty list"
11 | uncons (One x Nil) = (x, Nil)
12 | uncons (One x ps) = (x, Zero ps)
13 | uncons (Zero ps) = let ((x, y), ps') = uncons ps in (x, One y ps')
14 |
15 | mutual
16 |   fupdate : (a -> a) -> Int -> BinaryList a -> BinaryList a
17 |   fupdate f i Nil = assert_total $ idris_crash "bad subscript"
18 |   fupdate f 0 (One x ps) = One (f x) ps
19 |   fupdate f i (One x ps) = assert_total $ cons x (fupdate f (i - 1) (Zero ps))
20 |   fupdate f i (Zero ps) = let i' : Int
21 |                               i' = assert_total $ i `div` 2
22 |                               r : Int
23 |                               r  = assert_total $ i `mod` 2
24 |                               f' : (a, a) -> (a, a)
25 |                               f' (x, y) = if 0 == r then (f x, y) else (x, f y)
26 |                           in Zero (assert_total $ fupdate f' i' ps)
27 |
28 |   export
29 |   RandomAccessList BinaryList where
30 |     empty = Nil
31 |     isEmpty Nil = True
32 |     isEmpty _   = False
33 |
34 |     cons x Nil        = One x Nil
35 |     cons x (Zero ps)  = One x ps
36 |     cons x (One y ps) = Zero (cons (x, y) ps)
37 |
38 |     head xs = fst (uncons xs)
39 |     tail xs = snd (uncons xs)
40 |
41 |     lookup i Nil = assert_total $ idris_crash "bad subscript"
42 |     lookup 0 (One x ps) = x
43 |     lookup i (One x ps) = lookup (i - 1) (assert_smaller (One x ps) $ Zero ps)
44 |     lookup i (Zero ps) = let i' = assert_total $ i `div` 2
45 |                              r  = assert_total $ i `mod` 2
46 |                              (x, y) = lookup i' ps
47 |                          in if 0 == r then x else y
48 |
49 |     update i y xs = fupdate (\x => y) i xs
50 |