git.iko.soy/Idris-dev
on master help sign in
Updating range behavior to match Haskell's where appropriate

This resolves #3502 and resolves #3503. This also fixes the issue that natEnumFromThenTo could not descend. I used make && make test on Ubuntu. After adding the new tests, the existing implementation crashed. basic013: Error: test/basic013 run: line 3: 19432 Segmentation fault (core dumped) ./basic013 With the new implementation, all 202 tests passed. I also built this on Windows, but was unable to run the tests, so I generated a stress test suite that passed range definitions to both Idris and Haskell to verify the output would be equivalent. There's one notable difference from Haskell. In Haskell, ranges of the form [A,A..B] generate an infinite sequence of As. I chose to follow the existing implementation, which returns [] instead. This rule conflicts with another rule that ranges of the the form [A,B..A] return [A] in the case that B == A (i.e. the form [A,A..A]). My implementation returns [A] in that case.

commit3962e62df51b529f4eed4bc33f7725aba4b456e9 authorMichael Hensler <mhensler@microsoft.com> dateSun 30 Oct 2016, 17:13 (10 years ago) parentbb3bc16
3 files changed+84−8
compare with master
unifiedsplit
libs/prelude/Prelude.idr+14−5 test/basic013/basic013.idr+35−2 test/basic013/expected+35−1
libs/prelude/Prelude.idr+14−5
@@ -156,8 +156,15 @@ natEnumFromTo n m = if n <= m
156156total natEnumFromThenTo' : Nat -> Nat -> Nat -> List Nat
157157natEnumFromThenTo' _ Z _ = []
158158natEnumFromThenTo' n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))
159+
159160total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
160−natEnumFromThenTo n next m = natEnumFromThenTo' n (minus next n) m
161+natEnumFromThenTo n next m = if n == m then [n]
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
161168
162169interface Enum a where
163170 total pred : a -> a
@@ -197,8 +204,9 @@ Enum Integer where
197204 go' n (x :: xs) = n + cast x :: go' n xs
198205 go : Integer -> Integer -> List Integer
199206 go n m = go' n (natRange (S (cast {to = Nat} (m - n))))
200− enumFromThenTo _ 0 _ = []
201− enumFromThenTo n next m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))
207+ enumFromThenTo n next m = if n == m then [n]
208+ else if next - n == 0 || next - n < 0 /= m - n < 0 then []
209+ else go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))
202210 where go : List Nat -> List Integer
203211 go [] = []
204212 go (x :: xs) = n + (cast x * (next - n)) :: go xs
@@ -217,8 +225,9 @@ Enum Int where
217225 go : Int -> Int -> List Int
218226 go n m = go' [] (cast {to = Nat} (m - n)) m
219227 enumFromThen n inc = n :: enumFromThen (inc + n) inc
220− enumFromThenTo _ 0 _ = []
221− enumFromThenTo n next m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))
228+ enumFromThenTo n next m = if n == m then [n]
229+ else if next - n == 0 || next - n < 0 /= m - n < 0 then []
230+ else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))
222231 where go : List Nat -> List Int
223232 go [] = []
224233 go (x :: xs) = n + (cast x * (next - n)) :: go xs
test/basic013/basic013.idr+35−2
@@ -36,8 +36,41 @@ main = do putStrLn foo
3636 printLn [(-9), (-7)..(-1)]
3737 printLn [17,15..1]
3838 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]
3949 printLn $ the (List Nat) [1..5]
4050 printLn $ the (List Nat) [5..1]
41− printLn $ the (List Int) [(-1)..(-5)]
51+ printLn $ the (List Nat) [5,4..1]
4252 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λ
1717[-9, -7, -5, -3, -1]
1818[17, 15, 13, 11, 9, 7, 5, 3, 1]
1919[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+[]
2030[1, 2, 3, 4, 5]
2131[5, 4, 3, 2, 1]
22−[-1, -2, -3, -4, -5]
32+[5, 4, 3, 2, 1]
2333[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']