git.iko.soy/Idris-dev
on master help sign in
Merge pull request #290 from david-christiansen/boundedlist
d52534cEdwin Brady
lib/Data/BoundedList.idrnew file+42
compare with master
unifiedsplit
@@ -0,0 +1,42 @@
1+module Data.BoundedList
2+
3+%default total
4+
5+data BoundedList : Type -> Nat -> Type where
6+ Nil : BoundedList a n
7+ (::) : a -> BoundedList a n -> BoundedList a (S n)
8+
9+length : BoundedList a n -> Fin (S n)
10+length [] = fO
11+length (x :: xs) = fS (length xs)
12+
13+index : Fin (S n) -> BoundedList a n -> Maybe a
14+index _ [] = Nothing
15+index fO (x :: _) = Just x
16+index (fS f) (_ :: xs) = index f xs
17+
18+weaken : BoundedList a n -> BoundedList a (n + m)
19+weaken [] = []
20+weaken (x :: xs) = x :: weaken xs
21+
22+take : (n : Nat) -> List a -> BoundedList a n
23+take _ [] = []
24+take O _ = []
25+take (S n') (x :: xs) = x :: take n' xs
26+
27+toList : BoundedList a n -> List a
28+toList [] = []
29+toList (x :: xs) = x :: toList xs
30+
31+fromList : (xs : List a) -> BoundedList a (length xs)
32+fromList [] = []
33+fromList (x :: xs) = x :: fromList xs
34+
35+map : (a -> b) -> BoundedList a n -> BoundedList b n
36+map f [] = []
37+map f (x :: xs) = f x :: map f xs
38+
39+zeroBoundIsEmpty : (xs : BoundedList a 0) -> xs = the (BoundedList a 0) []
40+zeroBoundIsEmpty [] = refl
41+zeroBoundIsEmpty (_ :: _) impossible
42+
lib/base.ipkg+1−1
@@ -22,7 +22,7 @@ modules = Builtins, Prelude, IO, System,
22 Language.Reflection,
22 Language.Reflection,
23
23
24 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,
24 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,
25− Data.SortedMap, Data.SortedSet,
25+ Data.SortedMap, Data.SortedSet, Data.BoundedList,
26
26
27 Control.Monad.Identity, Control.Monad.State, Control.Category,
27 Control.Monad.Identity, Control.Monad.State, Control.Category,
28 Control.Arrow,
28 Control.Arrow,