git.iko.soy/Idris-dev
on master help sign in
Merge pull request #295 from david-christiansen/boundedlist
1f562fcEdwin Brady
lib/Data/BoundedList.idr+53−2
compare with master
unifiedsplit
@@ -1,5 +1,6 @@
1module Data.BoundedList
1module Data.BoundedList
2
2
3+%access public
3%default total
4%default total
4
5
5data BoundedList : Type -> Nat -> Type where
6data BoundedList : Type -> Nat -> Type where
@@ -10,15 +11,27 @@ length : BoundedList a n -> Fin (S n)
10length [] = fO
11length [] = fO
11length (x :: xs) = fS (length xs)
12length (x :: xs) = fS (length xs)
12
13
14+--------------------------------------------------------------------------------
15+-- Indexing into bounded lists
16+--------------------------------------------------------------------------------
17+
13index : Fin (S n) -> BoundedList a n -> Maybe a
18index : Fin (S n) -> BoundedList a n -> Maybe a
14index _ [] = Nothing
19index _ [] = Nothing
15index fO (x :: _) = Just x
20index fO (x :: _) = Just x
16index (fS f) (_ :: xs) = index f xs
21index (fS f) (_ :: xs) = index f xs
17
22
23+--------------------------------------------------------------------------------
24+-- Adjusting bounds
25+--------------------------------------------------------------------------------
26+
18weaken : BoundedList a n -> BoundedList a (n + m)
27weaken : BoundedList a n -> BoundedList a (n + m)
19weaken [] = []
28weaken [] = []
20weaken (x :: xs) = x :: weaken xs
29weaken (x :: xs) = x :: weaken xs
21
30
31+--------------------------------------------------------------------------------
32+-- Conversions to and from list
33+--------------------------------------------------------------------------------
34+
22take : (n : Nat) -> List a -> BoundedList a n
35take : (n : Nat) -> List a -> BoundedList a n
23take _ [] = []
36take _ [] = []
24take O _ = []
37take O _ = []
@@ -32,11 +45,49 @@ fromList : (xs : List a) -> BoundedList a (length xs)
32fromList [] = []
45fromList [] = []
33fromList (x :: xs) = x :: fromList xs
46fromList (x :: xs) = x :: fromList xs
34
47
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+
35map : (a -> b) -> BoundedList a n -> BoundedList b n
72map : (a -> b) -> BoundedList a n -> BoundedList b n
36map f [] = []
73map f [] = []
37map f (x :: xs) = f x :: map f xs
74map f (x :: xs) = f x :: map f xs
38
75
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+
39zeroBoundIsEmpty : (xs : BoundedList a 0) -> xs = the (BoundedList a 0) []
91zeroBoundIsEmpty : (xs : BoundedList a 0) -> xs = the (BoundedList a 0) []
40zeroBoundIsEmpty [] = refl
92zeroBoundIsEmpty [] = refl
41−zeroBoundIsEmpty (_ :: _) impossible
93+zeroBoundIsEmpty (_ :: _) impossible
42−