git.iko.soy/Idris-dev
on master help sign in
Fix buglet in Show instances for list/vect
ddba413Edwin Brady
lib/prelude.idr+4−4
compare with master
unifiedsplit
@@ -44,8 +44,8 @@ instance (Show a, Show b) => Show (a, b) where {
44instance Show a => Show (List a) where {
44instance Show a => Show (List a) where {
45 show xs = "[" ++ show' xs ++ "]" where {
45 show xs = "[" ++ show' xs ++ "]" where {
46 show' : Show a => List a -> String;
46 show' : Show a => List a -> String;
47− show' Nil = "";
47+ show' [] = "";
48− show' (x :: Nil) = show x;
48+ show' [x] = show x;
49 show' (x :: xs) = show x ++ ", " ++ show' xs;
49 show' (x :: xs) = show x ++ ", " ++ show' xs;
50 }
50 }
51}
51}
@@ -53,8 +53,8 @@ instance Show a => Show (List a) where {
53instance Show a => Show (Vect a n) where {
53instance Show a => Show (Vect a n) where {
54 show xs = "[" ++ show' xs ++ "]" where {
54 show xs = "[" ++ show' xs ++ "]" where {
55 show' : Show a => Vect a n -> String;
55 show' : Show a => Vect a n -> String;
56− show' VNil = "";
56+ show' [] = "";
57− show' (x :: VNil) = show x;
57+ show' [x] = show x;
58 show' (x :: xs) = show x ++ ", " ++ show' xs;
58 show' (x :: xs) = show x ++ ", " ++ show' xs;
59 }
59 }
60}
60}
lib/prelude/list.idr+8−8
@@ -7,32 +7,32 @@ infixr 7 :: ;
7data List a = Nil | (::) a (List a);
7data List a = Nil | (::) a (List a);
8
8
9rev : List a -> List a;
9rev : List a -> List a;
10−rev xs = revAcc Nil xs where {
10+rev xs = revAcc [] xs where {
11 revAcc : List a -> List a -> List a;
11 revAcc : List a -> List a -> List a;
12− revAcc acc Nil = acc;
12+ revAcc acc [] = acc;
13 revAcc acc (x :: xs) = revAcc (x :: acc) xs;
13 revAcc acc (x :: xs) = revAcc (x :: acc) xs;
14}
14}
15
15
16length : List a -> Int;
16length : List a -> Int;
17−length Nil = 0;
17+length [] = 0;
18length (x :: xs) = 1 + length xs;
18length (x :: xs) = 1 + length xs;
19
19
20take : Int -> List a -> List a;
20take : Int -> List a -> List a;
21−take 0 xs = Nil;
21+take 0 xs = [];
22−take n Nil = Nil;
22+take n [] = [];
23take n (x :: xs) = x :: take (n-1) xs;
23take n (x :: xs) = x :: take (n-1) xs;
24
24
25drop : Int -> List a -> List a;
25drop : Int -> List a -> List a;
26drop 0 xs = xs;
26drop 0 xs = xs;
27−drop n Nil = Nil;
27+drop n [] = [];
28drop n (x :: xs) = drop (n-1) xs;
28drop n (x :: xs) = drop (n-1) xs;
29
29
30map : (a -> b) -> List a -> List b;
30map : (a -> b) -> List a -> List b;
31−map f Nil = Nil;
31+map f [] = [];
32map f (x :: xs) = f x :: map f xs;
32map f (x :: xs) = f x :: map f xs;
33
33
34filter : (y -> Bool) -> List y -> List y;
34filter : (y -> Bool) -> List y -> List y;
35−filter pred Nil = Nil;
35+filter pred [] = [];
36filter pred (x :: xs) with (pred x, filter pred xs) {
36filter pred (x :: xs) with (pred x, filter pred xs) {
37 filter pred (x :: xs) | (True, fxs) = x :: fxs;
37 filter pred (x :: xs) | (True, fxs) = x :: fxs;
38 filter pred (x :: xs) | (False, fxs) = fxs;
38 filter pred (x :: xs) | (False, fxs) = fxs;
lib/prelude/vect.idr+3−3
@@ -17,7 +17,7 @@ instance Eq (Fin n) where {
17infixr 7 :: ;
17infixr 7 :: ;
18
18
19data Vect : Set -> Nat -> Set where
19data Vect : Set -> Nat -> Set where
20− Nil : Vect a O
20+ Nil : Vect a O
21 | (::) : a -> Vect a k -> Vect a (S k);
21 | (::) : a -> Vect a k -> Vect a (S k);
22
22
23vlookup : Fin n -> Vect a n -> a;
23vlookup : Fin n -> Vect a n -> a;
@@ -25,11 +25,11 @@ vlookup fO (x :: xs) = x;
25vlookup (fS k) (x :: xs) = vlookup k xs;
25vlookup (fS k) (x :: xs) = vlookup k xs;
26
26
27vapp : Vect a n -> Vect a m -> Vect a (n + m);
27vapp : Vect a n -> Vect a m -> Vect a (n + m);
28−vapp Nil ys = ys;
28+vapp [] ys = ys;
29vapp (x :: xs) ys = x :: vapp xs ys;
29vapp (x :: xs) ys = x :: vapp xs ys;
30
30
31vfilter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
31vfilter : (a -> Bool) -> Vect a n -> (p ** Vect a p);
32−vfilter p Nil = ( _ ** Nil );
32+vfilter p [] = ( _ ** [] );
33vfilter p (x :: xs) with (vfilter p xs) {
33vfilter p (x :: xs) with (vfilter p xs) {
34 vfilter p (x :: xs) | ( _ ** xs' )
34 vfilter p (x :: xs) | ( _ ** xs' )
35 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );
35 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );