git.iko.soy/Idris-dev
on fa29447 help sign in
Idris-dev/lib/Data/BoundedList.idr
93 lines 3.2 kB history raw
1module Data.BoundedList
3%access public
4%default total
6data BoundedList : Type -> Nat -> Type where
7 Nil : BoundedList a n
8 (::) : a -> BoundedList a n -> BoundedList a (S n)
10length : BoundedList a n -> Fin (S n)
11length [] = fO
12length (x :: xs) = fS (length xs)
14--------------------------------------------------------------------------------
15-- Indexing into bounded lists
16--------------------------------------------------------------------------------
18index : Fin (S n) -> BoundedList a n -> Maybe a
19index _ [] = Nothing
20index fO (x :: _) = Just x
21index (fS f) (_ :: xs) = index f xs
23--------------------------------------------------------------------------------
24-- Adjusting bounds
25--------------------------------------------------------------------------------
27weaken : BoundedList a n -> BoundedList a (n + m)
28weaken [] = []
29weaken (x :: xs) = x :: weaken xs
31--------------------------------------------------------------------------------
32-- Conversions to and from list
33--------------------------------------------------------------------------------
35take : (n : Nat) -> List a -> BoundedList a n
36take _ [] = []
37take O _ = []
38take (S n') (x :: xs) = x :: take n' xs
40toList : BoundedList a n -> List a
41toList [] = []
42toList (x :: xs) = x :: toList xs
44fromList : (xs : List a) -> BoundedList a (length xs)
45fromList [] = []
46fromList (x :: xs) = x :: fromList xs
48--------------------------------------------------------------------------------
49-- Building (bigger) bounded lists
50--------------------------------------------------------------------------------
52replicate : (n : Nat) -> a -> BoundedList a n
53replicate O _ = []
54replicate (S n) x = x :: replicate n x
56--------------------------------------------------------------------------------
57-- Folds
58--------------------------------------------------------------------------------
60foldl : (a -> b -> a) -> a -> BoundedList b n -> a
61foldl f e [] = e
62foldl f e (x::xs) = foldl f (f e x) xs
64foldr : (a -> b -> b) -> b -> BoundedList a n -> b
65foldr f e [] = e
66foldr f e (x::xs) = f x (foldr f e xs)
68--------------------------------------------------------------------------------
69-- Maps
70--------------------------------------------------------------------------------
72map : (a -> b) -> BoundedList a n -> BoundedList b n
73map f [] = []
74map f (x :: xs) = f x :: map f xs
76--------------------------------------------------------------------------------
77-- Misc
78--------------------------------------------------------------------------------
80%assert_total -- not sure why this isn't accepted - clearly decreasing on n
81pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
82pad {n=O} [] _ = []
83pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
84pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding
87--------------------------------------------------------------------------------
88-- Simple properties
89--------------------------------------------------------------------------------
91zeroBoundIsEmpty : (xs : BoundedList a 0) -> xs = the (BoundedList a 0) []
92zeroBoundIsEmpty [] = refl
93zeroBoundIsEmpty (_ :: _) impossible