0 | ||| The content of this file is taken from the paper
 1 | ||| Heterogeneous Binary Random-access lists
 2 |
 3 | module Data.Vect.Binary
 4 |
 5 | import Data.Binary.Digit
 6 | import Data.Binary
 7 | import Data.IMaybe
 8 | import Data.Nat
 9 | import Data.Nat.Exponentiation
10 | import Data.Tree.Perfect
11 |
12 | %default total
13 |
14 | public export
15 | data BVect : Nat -> Bin -> Type -> Type where
16 |   Nil  : BVect n [] a
17 |   (::) : IMaybe (isI b) (Tree n a) -> BVect (S n) bs a -> BVect n (b :: bs) a
18 |
19 | public export
20 | data Path : Nat -> Bin -> Type where
21 |   Here  : Path n -> Path n (I :: bs)
22 |   There : Path (S n) bs -> Path n (b :: bs)
23 |
24 | public export
25 | zero : {bs : Bin} -> {n : Nat} -> Path n (suc bs)
26 | zero {bs} = case bs of
27 |   [] => Here (fromNat 0 n (ltePow2 {m = n}))
28 |   (O :: bs) => Here (fromNat 0 n (ltePow2 {m = n}))
29 |   (I :: bs) => There zero
30 |
31 | public export
32 | lookup : BVect n bs a -> Path n bs -> a
33 | lookup (hd :: _) (Here p) = lookup (fromJust hd) p
34 | lookup (_ :: tl) (There p) = lookup tl p
35 |
36 | public export
37 | cons : {bs : _} -> Tree n a -> BVect n bs a -> BVect n (suc bs) a
38 | cons t [] = [Just t]
39 | cons {bs = b :: _} t (u :: us) = case b of
40 |   I => Nothing :: cons (Node t (fromJust u)) us
41 |   O => Just t :: us
42 |