git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3508 from orokanasaru/ranges

Updating range behavior to match Haskell's where appropriate

commitd8fd36a248eb1d47cd19f0d2796b6a41cad5bf09 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateWed 16 Nov 2016, 16:22 (10 years ago) parent4057b483962e62
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']