@@ -4,12 +4,12 @@ module Data.BoundedList
44%default total
55
66||| A list with an upper bound on its length.
7−data BoundedList : Type -> Nat -> Type where
8− Nil : BoundedList a n
9− (::) : a -> BoundedList a n -> BoundedList a (S n)
7+data BoundedList : Nat -> Type -> Type where
8+ Nil : BoundedList n a
9+ (::) : a -> BoundedList n a -> BoundedList (S n) a
1010
1111||| Compute the length of a list.
12−length : BoundedList a n -> Fin (S n)
12+length : BoundedList n a -> Fin (S n)
1313length [] = fZ
1414length (x :: xs) = fS (length xs)
1515
@@ -17,7 +17,7 @@ length (x :: xs) = fS (length xs)
1717-- Indexing into bounded lists
1818--------------------------------------------------------------------------------
1919
20−index : Fin (S n) -> BoundedList a n -> Maybe a
20+index : Fin (S n) -> BoundedList n a -> Maybe a
2121index _ [] = Nothing
2222index fZ (x :: _) = Just x
2323index (fS f) (_ :: xs) = index f xs
@@ -27,7 +27,7 @@ index (fS f) (_ :: xs) = index f xs
2727--------------------------------------------------------------------------------
2828
2929||| Loosen the bounds on a list's length.
30−weaken : BoundedList a n -> BoundedList a (n + m)
30+weaken : BoundedList n a -> BoundedList (n + m) a
3131weaken [] = []
3232weaken (x :: xs) = x :: weaken xs
3333
@@ -35,16 +35,16 @@ weaken (x :: xs) = x :: weaken xs
3535-- Conversions to and from list
3636--------------------------------------------------------------------------------
3737
38−take : (n : Nat) -> List a -> BoundedList a n
38+take : (n : Nat) -> List a -> BoundedList n a
3939take _ [] = []
4040take Z _ = []
4141take (S n') (x :: xs) = x :: take n' xs
4242
43−toList : BoundedList a n -> List a
43+toList : BoundedList n a -> List a
4444toList [] = []
45−toList (x :: xs) = x :: toList xs
45+toList (x :: xs) = x :: Data.BoundedList.toList xs
4646
47−fromList : (xs : List a) -> BoundedList a (length xs)
47+fromList : (xs : List a) -> BoundedList (length xs) a
4848fromList [] = []
4949fromList (x :: xs) = x :: fromList xs
5050
@@ -52,7 +52,7 @@ fromList (x :: xs) = x :: fromList xs
5252-- Building (bigger) bounded lists
5353--------------------------------------------------------------------------------
5454
55−replicate : (n : Nat) -> a -> BoundedList a n
55+replicate : (n : Nat) -> a -> BoundedList n a
5656replicate Z _ = []
5757replicate (S n) x = x :: replicate n x
5858
@@ -60,28 +60,26 @@ replicate (S n) x = x :: replicate n x
6060-- Folds
6161--------------------------------------------------------------------------------
6262
63−foldl : (a -> b -> a) -> a -> BoundedList b n -> a
64−foldl f e [] = e
65−foldl f e (x::xs) = foldl f (f e x) xs
66−
67−foldr : (a -> b -> b) -> b -> BoundedList a n -> b
68−foldr f e [] = e
69−foldr f e (x::xs) = f x (foldr f e xs)
63+instance Foldable (BoundedList n) where
64+ foldr f e [] = e
65+ foldr f e (x::xs) = f x (foldr f e xs)
66+ foldl f e [] = e
67+ foldl f e (x::xs) = foldl f (f e x) xs
7068
7169--------------------------------------------------------------------------------
7270-- Maps
7371--------------------------------------------------------------------------------
7472
75−map : (a -> b) -> BoundedList a n -> BoundedList b n
76−map f [] = []
77−map f (x :: xs) = f x :: map f xs
73+instance Functor (BoundedList n) where
74+ map f [] = []
75+ map f (x :: xs) = f x :: map f xs
7876
7977--------------------------------------------------------------------------------
8078-- Misc
8179--------------------------------------------------------------------------------
8280
8381||| Extend a bounded list to the maximum size by padding on the left.
84−pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
82+pad : BoundedList n a -> a -> BoundedList n a
8583pad {n=Z} [] _ = []
8684pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
8785pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding
@@ -91,6 +89,6 @@ pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding
9189-- Simple properties
9290--------------------------------------------------------------------------------
9391
94−zeroBoundIsEmpty : (xs : BoundedList a 0) -> xs = the (BoundedList a 0) []
92+zeroBoundIsEmpty : (xs : BoundedList 0 a) -> xs = the (BoundedList 0 a) []
9593zeroBoundIsEmpty [] = refl
9694zeroBoundIsEmpty (_ :: _) impossible