git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1240 from sellout/BoundedList
a4f1556Edwin Brady
CHANGELOG+2
compare with master
unifiedsplit
@@ -23,6 +23,8 @@ New in 0.9.13:
23* Added :makelemma command, which adds a new top level definition to solve
23* Added :makelemma command, which adds a new top level definition to solve
24 a metavariable.
24 a metavariable.
25* Extend :addclause to add instance bodies as well as definitions
25* Extend :addclause to add instance bodies as well as definitions
26+* Reverse parameters to BoundedList -- now matches Vect, and is easier to instantiate classes.
27+* Move foldl into Foldable so it can be overridden.
26
28
27Internal changes
29Internal changes
28
30
libs/base/Data/BoundedList.idr+21−23
@@ -4,12 +4,12 @@ module Data.BoundedList
4%default total
4%default total
5
5
6||| A list with an upper bound on its length.
6||| A list with an upper bound on its length.
7−data BoundedList : Type -> Nat -> Type where
7+data BoundedList : Nat -> Type -> Type where
8− Nil : BoundedList a n
8+ Nil : BoundedList n a
9− (::) : a -> BoundedList a n -> BoundedList a (S n)
9+ (::) : a -> BoundedList n a -> BoundedList (S n) a
10
10
11||| Compute the length of a list.
11||| Compute the length of a list.
12−length : BoundedList a n -> Fin (S n)
12+length : BoundedList n a -> Fin (S n)
13length [] = fZ
13length [] = fZ
14length (x :: xs) = fS (length xs)
14length (x :: xs) = fS (length xs)
15
15
@@ -17,7 +17,7 @@ length (x :: xs) = fS (length xs)
17-- Indexing into bounded lists
17-- Indexing into bounded lists
18--------------------------------------------------------------------------------
18--------------------------------------------------------------------------------
19
19
20−index : Fin (S n) -> BoundedList a n -> Maybe a
20+index : Fin (S n) -> BoundedList n a -> Maybe a
21index _ [] = Nothing
21index _ [] = Nothing
22index fZ (x :: _) = Just x
22index fZ (x :: _) = Just x
23index (fS f) (_ :: xs) = index f xs
23index (fS f) (_ :: xs) = index f xs
@@ -27,7 +27,7 @@ index (fS f) (_ :: xs) = index f xs
27--------------------------------------------------------------------------------
27--------------------------------------------------------------------------------
28
28
29||| Loosen the bounds on a list's length.
29||| 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
31weaken [] = []
31weaken [] = []
32weaken (x :: xs) = x :: weaken xs
32weaken (x :: xs) = x :: weaken xs
33
33
@@ -35,16 +35,16 @@ weaken (x :: xs) = x :: weaken xs
35-- Conversions to and from list
35-- Conversions to and from list
36--------------------------------------------------------------------------------
36--------------------------------------------------------------------------------
37
37
38−take : (n : Nat) -> List a -> BoundedList a n
38+take : (n : Nat) -> List a -> BoundedList n a
39take _ [] = []
39take _ [] = []
40take Z _ = []
40take Z _ = []
41take (S n') (x :: xs) = x :: take n' xs
41take (S n') (x :: xs) = x :: take n' xs
42
42
43−toList : BoundedList a n -> List a
43+toList : BoundedList n a -> List a
44toList [] = []
44toList [] = []
45−toList (x :: xs) = x :: toList xs
45+toList (x :: xs) = x :: Data.BoundedList.toList xs
46
46
47−fromList : (xs : List a) -> BoundedList a (length xs)
47+fromList : (xs : List a) -> BoundedList (length xs) a
48fromList [] = []
48fromList [] = []
49fromList (x :: xs) = x :: fromList xs
49fromList (x :: xs) = x :: fromList xs
50
50
@@ -52,7 +52,7 @@ fromList (x :: xs) = x :: fromList xs
52-- Building (bigger) bounded lists
52-- Building (bigger) bounded lists
53--------------------------------------------------------------------------------
53--------------------------------------------------------------------------------
54
54
55−replicate : (n : Nat) -> a -> BoundedList a n
55+replicate : (n : Nat) -> a -> BoundedList n a
56replicate Z _ = []
56replicate Z _ = []
57replicate (S n) x = x :: replicate n x
57replicate (S n) x = x :: replicate n x
58
58
@@ -60,28 +60,26 @@ replicate (S n) x = x :: replicate n x
60-- Folds
60-- Folds
61--------------------------------------------------------------------------------
61--------------------------------------------------------------------------------
62
62
63−foldl : (a -> b -> a) -> a -> BoundedList b n -> a
63+instance Foldable (BoundedList n) where
64−foldl f e [] = e
64+ foldr f e [] = e
65−foldl f e (x::xs) = foldl f (f e x) xs
65+ foldr f e (x::xs) = f x (foldr f e xs)
66−
66+ foldl f e [] = e
67−foldr : (a -> b -> b) -> b -> BoundedList a n -> b
67+ foldl f e (x::xs) = foldl f (f e x) xs
68−foldr f e [] = e
69−foldr f e (x::xs) = f x (foldr f e xs)
70
68
71--------------------------------------------------------------------------------
69--------------------------------------------------------------------------------
72-- Maps
70-- Maps
73--------------------------------------------------------------------------------
71--------------------------------------------------------------------------------
74
72
75−map : (a -> b) -> BoundedList a n -> BoundedList b n
73+instance Functor (BoundedList n) where
76−map f [] = []
74+ map f [] = []
77−map f (x :: xs) = f x :: map f xs
75+ map f (x :: xs) = f x :: map f xs
78
76
79--------------------------------------------------------------------------------
77--------------------------------------------------------------------------------
80-- Misc
78-- Misc
81--------------------------------------------------------------------------------
79--------------------------------------------------------------------------------
82
80
83||| Extend a bounded list to the maximum size by padding on the left.
81||| 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
85pad {n=Z} [] _ = []
83pad {n=Z} [] _ = []
86pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
84pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
87pad {n=S n'} (x :: xs) padding = x :: pad {n=n'} xs padding
85pad {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
91-- Simple properties
89-- Simple properties
92--------------------------------------------------------------------------------
90--------------------------------------------------------------------------------
93
91
94−zeroBoundIsEmpty : (xs : BoundedList a 0) -> xs = the (BoundedList a 0) []
92+zeroBoundIsEmpty : (xs : BoundedList 0 a) -> xs = the (BoundedList 0 a) []
95zeroBoundIsEmpty [] = refl
93zeroBoundIsEmpty [] = refl
96zeroBoundIsEmpty (_ :: _) impossible
94zeroBoundIsEmpty (_ :: _) impossible
libs/prelude/Prelude/Foldable.idr+2−3
@@ -10,9 +10,8 @@ import Prelude.Algebra
10
10
11class Foldable (t : Type -> Type) where
11class Foldable (t : Type -> Type) where
12 foldr : (elt -> acc -> acc) -> acc -> t elt -> acc
12 foldr : (elt -> acc -> acc) -> acc -> t elt -> acc
13−
14−foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc
13+ foldl : Foldable t => (acc -> elt -> acc) -> acc -> t elt -> acc
15−foldl f z t = foldr (flip (.) . flip f) id t z
14+ foldl f z t = foldr (flip (.) . flip f) id t z
16
15
17||| Combine each element of a structure into a monoid
16||| Combine each element of a structure into a monoid
18concat : (Foldable t, Monoid a) => t a -> a
17concat : (Foldable t, Monoid a) => t a -> a