git.iko.soy/Idris-dev
on master help sign in
Updating range behavior to match Haskell's where appropriate
3962e62Michael Hensler
libs/prelude/Prelude.idr+14−5
compare with master
unifiedsplit
@@ -156,8 +156,15 @@ natEnumFromTo n m = if n <= m
156total natEnumFromThenTo' : Nat -> Nat -> Nat -> List Nat
156total natEnumFromThenTo' : Nat -> Nat -> Nat -> List Nat
157natEnumFromThenTo' _ Z _ = []
157natEnumFromThenTo' _ Z _ = []
158natEnumFromThenTo' n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))
158natEnumFromThenTo' n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))
159+
159total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
160total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
161+natEnumFromThenTo n next m = if n == m then [n]
160−natEnumFromThenTo n next m = natEnumFromThenTo' n (minus next n) m
162+ else if n < m then natEnumFromThenTo' n (minus next n) m
163+ else case minus n next of
164+ Z => []
165+ S step => List.reverse . map (+ (modNatNZ (minus n m) (S step) SIsNotZ)) $ natEnumFromThenTo' m (minus n next) n
166+ where modNatNZ : Nat -> (m : Nat) -> Not (m = 0) -> Nat
167+ modNatNZ n m nz = minus n $ mult m $ divNatNZ n m nz
161
168
162interface Enum a where
169interface Enum a where
163 total pred : a -> a
170 total pred : a -> a
@@ -197,8 +204,9 @@ Enum Integer where
197 go' n (x :: xs) = n + cast x :: go' n xs
204 go' n (x :: xs) = n + cast x :: go' n xs
198 go : Integer -> Integer -> List Integer
205 go : Integer -> Integer -> List Integer
199 go n m = go' n (natRange (S (cast {to = Nat} (m - n))))
206 go n m = go' n (natRange (S (cast {to = Nat} (m - n))))
200− enumFromThenTo _ 0 _ = []
207+ enumFromThenTo n next m = if n == m then [n]
208+ else if next - n == 0 || next - n < 0 /= m - n < 0 then []
201− enumFromThenTo n next m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))
209+ else go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))
202 where go : List Nat -> List Integer
210 where go : List Nat -> List Integer
203 go [] = []
211 go [] = []
204 go (x :: xs) = n + (cast x * (next - n)) :: go xs
212 go (x :: xs) = n + (cast x * (next - n)) :: go xs
@@ -217,8 +225,9 @@ Enum Int where
217 go : Int -> Int -> List Int
225 go : Int -> Int -> List Int
218 go n m = go' [] (cast {to = Nat} (m - n)) m
226 go n m = go' [] (cast {to = Nat} (m - n)) m
219 enumFromThen n inc = n :: enumFromThen (inc + n) inc
227 enumFromThen n inc = n :: enumFromThen (inc + n) inc
220− enumFromThenTo _ 0 _ = []
228+ enumFromThenTo n next m = if n == m then [n]
229+ else if next - n == 0 || next - n < 0 /= m - n < 0 then []
221− enumFromThenTo n next m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))
230+ else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))
222 where go : List Nat -> List Int
231 where go : List Nat -> List Int
223 go [] = []
232 go [] = []
224 go (x :: xs) = n + (cast x * (next - n)) :: go xs
233 go (x :: xs) = n + (cast x * (next - n)) :: go xs
test/basic013/basic013.idr+35−2
@@ -36,8 +36,41 @@ main = do putStrLn foo
36 printLn [(-9), (-7)..(-1)]
36 printLn [(-9), (-7)..(-1)]
37 printLn [17,15..1]
37 printLn [17,15..1]
38 printLn [19,15..2]
38 printLn [19,15..2]
39+ printLn [-2,0..4]
40+ printLn [1,0..-2]
41+ printLn [3,5..3]
42+ printLn [2,1..2]
43+ printLn [4,1..3]
44+ printLn [1,4..2]
45+ printLn [3,5..1]
46+ printLn [4,1..5]
47+ printLn [1,1..2]
48+ printLn [2,2..1]
39 printLn $ the (List Nat) [1..5]
49 printLn $ the (List Nat) [1..5]
40 printLn $ the (List Nat) [5..1]
50 printLn $ the (List Nat) [5..1]
41− printLn $ the (List Int) [(-1)..(-5)]
51+ printLn $ the (List Nat) [5,4..1]
42 printLn $ the (List Nat) [1,3..5]
52 printLn $ the (List Nat) [1,3..5]
43−
53+ printLn $ the (List Nat) [5,3..1]
54+ printLn $ the (List Nat) [3,5..3]
55+ printLn $ the (List Nat) [2,1..2]
56+ printLn $ the (List Nat) [4,1..3]
57+ printLn $ the (List Nat) [1,4..2]
58+ printLn $ the (List Nat) [3,5..1]
59+ printLn $ the (List Nat) [4,1..5]
60+ printLn $ the (List Nat) [1,1..2]
61+ printLn $ the (List Nat) [2,2..1]
62+ printLn $ the (List Int) [(-1)..(-5)]
63+ printLn $ the (List Int) [-2,0..4]
64+ printLn $ the (List Int) [1,0..-2]
65+ printLn $ the (List Int) [3,5..3]
66+ printLn $ the (List Int) [2,1..2]
67+ printLn $ the (List Int) [4,1..3]
68+ printLn $ the (List Int) [1,4..2]
69+ printLn $ the (List Int) [3,5..1]
70+ printLn $ the (List Int) [4,1..5]
71+ printLn $ the (List Int) [1,1..2]
72+ printLn $ the (List Int) [2,2..1]
73+ printLn ['z'..'x']
74+ printLn ['g','e'..'a']
75+ printLn ['x'..'z']
76+ printLn ['a','c'..'g']
test/basic013/expected+35−1
@@ -17,7 +17,41 @@ Reverse: x→xλx→xλx→xλx→xλx→xλ
17[-9, -7, -5, -3, -1]
17[-9, -7, -5, -3, -1]
18[17, 15, 13, 11, 9, 7, 5, 3, 1]
18[17, 15, 13, 11, 9, 7, 5, 3, 1]
19[19, 15, 11, 7, 3]
19[19, 15, 11, 7, 3]
20+[-2, 0, 2, 4]
21+[1, 0, -1, -2]
22+[3]
23+[2]
24+[4]
25+[1]
26+[]
27+[]
28+[]
29+[]
20[1, 2, 3, 4, 5]
30[1, 2, 3, 4, 5]
21[5, 4, 3, 2, 1]
31[5, 4, 3, 2, 1]
22−[-1, -2, -3, -4, -5]
32+[5, 4, 3, 2, 1]
23[1, 3, 5]
33[1, 3, 5]
34+[5, 3, 1]
35+[3]
36+[2]
37+[4]
38+[1]
39+[]
40+[]
41+[]
42+[]
43+[-1, -2, -3, -4, -5]
44+[-2, 0, 2, 4]
45+[1, 0, -1, -2]
46+[3]
47+[2]
48+[4]
49+[1]
50+[]
51+[]
52+[]
53+[]
54+['z', 'y', 'x']
55+['g', 'e', 'c', 'a']
56+['x', 'y', 'z']
57+['a', 'c', 'e', 'g']