@@ -1,5 +1,6 @@
11module Data.BoundedList
22
3+%access public
34%default total
45
56data BoundedList : Type -> Nat -> Type where
@@ -10,15 +11,27 @@ length : BoundedList a n -> Fin (S n)
1011length [] = fO
1112length (x :: xs) = fS (length xs)
1213
14+--------------------------------------------------------------------------------
15+-- Indexing into bounded lists
16+--------------------------------------------------------------------------------
17+
1318index : Fin (S n) -> BoundedList a n -> Maybe a
1419index _ [] = Nothing
1520index fO (x :: _) = Just x
1621index (fS f) (_ :: xs) = index f xs
1722
23+--------------------------------------------------------------------------------
24+-- Adjusting bounds
25+--------------------------------------------------------------------------------
26+
1827weaken : BoundedList a n -> BoundedList a (n + m)
1928weaken [] = []
2029weaken (x :: xs) = x :: weaken xs
2130
31+--------------------------------------------------------------------------------
32+-- Conversions to and from list
33+--------------------------------------------------------------------------------
34+
2235take : (n : Nat) -> List a -> BoundedList a n
2336take _ [] = []
2437take O _ = []
@@ -32,11 +45,49 @@ fromList : (xs : List a) -> BoundedList a (length xs)
3245fromList [] = []
3346fromList (x :: xs) = x :: fromList xs
3447
48+--------------------------------------------------------------------------------
49+-- Building (bigger) bounded lists
50+--------------------------------------------------------------------------------
51+
52+replicate : (n : Nat) -> a -> BoundedList a n
53+replicate O _ = []
54+replicate (S n) x = x :: replicate n x
55+
56+--------------------------------------------------------------------------------
57+-- Folds
58+--------------------------------------------------------------------------------
59+
60+foldl : (a -> b -> a) -> a -> BoundedList b n -> a
61+foldl f e [] = e
62+foldl f e (x::xs) = foldl f (f e x) xs
63+
64+foldr : (a -> b -> b) -> b -> BoundedList a n -> b
65+foldr f e [] = e
66+foldr f e (x::xs) = f x (foldr f e xs)
67+
68+--------------------------------------------------------------------------------
69+-- Maps
70+--------------------------------------------------------------------------------
71+
3572map : (a -> b) -> BoundedList a n -> BoundedList b n
3673map f [] = []
3774map f (x :: xs) = f x :: map f xs
3875
76+--------------------------------------------------------------------------------
77+-- Misc
78+--------------------------------------------------------------------------------
79+
80+%assert_total -- not sure why this isn't accepted - clearly decreasing on n
81+pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
82+pad {n=O} [] _ = []
83+pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
84+pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding
85+
86+
87+--------------------------------------------------------------------------------
88+-- Simple properties
89+--------------------------------------------------------------------------------
90+
3991zeroBoundIsEmpty : (xs : BoundedList a 0) -> xs = the (BoundedList a 0) []
4092zeroBoundIsEmpty [] = refl
41−zeroBoundIsEmpty (_ :: _) impossible
42−
93+zeroBoundIsEmpty (_ :: _) impossible