git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3303 from zjhmale/let-reverse-ranges-work-again
652b0feJan de Muijnck-Hughes
CHANGELOG.md+1
compare with master
unifiedsplit
@@ -25,6 +25,7 @@
25
25
26* The File Effect has been updated to take into account changes in
26* The File Effect has been updated to take into account changes in
27 `Prelude.File` and to provide a 'better' API.
27 `Prelude.File` and to provide a 'better' API.
28+* `natEnumFromThen` and `natEnumFromTo` have been updated to correctly calculate reverse ranges. Range syntax `[a,b..c]` now can be used again to generate reverse ranges.
28
29
29## Tool updates
30## Tool updates
30
31
libs/prelude/Prelude.idr+31−23
@@ -146,12 +146,18 @@ natRange n = List.reverse (go n)
146
146
147-- predefine Nat versions of Enum, so we can use them in the default impls
147-- predefine Nat versions of Enum, so we can use them in the default impls
148total natEnumFromThen : Nat -> Nat -> Stream Nat
148total natEnumFromThen : Nat -> Nat -> Stream Nat
149−natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
149+natEnumFromThen n next = n :: natEnumFromThen next (minus next n)
150total natEnumFromTo : Nat -> Nat -> List Nat
150total natEnumFromTo : Nat -> Nat -> List Nat
151+natEnumFromTo n m = if n <= m
152+ then go n m
153+ else List.reverse $ go m n
154+ where go : Nat -> Nat -> List Nat
151−natEnumFromTo n m = map (plus n) (natRange (minus (S m) n))
155+ go n m = map (plus n) (natRange (minus (S m) n))
156+total natEnumFromThenTo' : Nat -> Nat -> Nat -> List Nat
157+natEnumFromThenTo' _ Z _ = []
158+natEnumFromThenTo' n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))
152total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
159total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
153−natEnumFromThenTo _ Z _ = []
160+natEnumFromThenTo n next m = natEnumFromThenTo' n (minus next n) m
154−natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))
155
161
156interface Enum a where
162interface Enum a where
157 total pred : a -> a
163 total pred : a -> a
@@ -184,36 +190,38 @@ Enum Integer where
184 fromNat n = cast n
190 fromNat n = cast n
185 enumFromThen n inc = n :: enumFromThen (inc + n) inc
191 enumFromThen n inc = n :: enumFromThen (inc + n) inc
186 enumFromTo n m = if n <= m
192 enumFromTo n m = if n <= m
193+ then go n m
194+ else List.reverse $ go m n
195+ where go' : Integer -> List Nat -> List Integer
196+ go' _ [] = []
197+ go' n (x :: xs) = n + cast x :: go' n xs
198+ go : Integer -> Integer -> List Integer
187− then go (natRange (S (cast {to = Nat} (m - n))))
199+ go n m = go' n (natRange (S (cast {to = Nat} (m - n))))
188− else []
189− where go : List Nat -> List Integer
190− go [] = []
191− go (x :: xs) = n + cast x :: go xs
192 enumFromThenTo _ 0 _ = []
200 enumFromThenTo _ 0 _ = []
193− enumFromThenTo n inc m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs inc) - 1))) SIsNotZ)))
201+ enumFromThenTo n next m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs (next - n)) - 1))) SIsNotZ)))
194 where go : List Nat -> List Integer
202 where go : List Nat -> List Integer
195 go [] = []
203 go [] = []
196− go (x :: xs) = n + (cast x * inc) :: go xs
204+ go (x :: xs) = n + (cast x * (next - n)) :: go xs
197
205
198Enum Int where
206Enum Int where
199 pred n = n - 1
207 pred n = n - 1
200 succ n = n + 1
208 succ n = n + 1
201 toNat n = cast n
209 toNat n = cast n
202 fromNat n = cast n
210 fromNat n = cast n
203− enumFromTo n m =
211+ enumFromTo n m = if n <= m
204− if n <= m
205− then go [] (cast {to = Nat} (m - n)) m
212+ then go n m
206− else []
213+ else List.reverse $ go m n
207− where
208− go : List Int -> Nat -> Int -> List Int
214+ where go' : List Int -> Nat -> Int -> List Int
209− go acc Z m = m :: acc
215+ go' acc Z m = m :: acc
210− go acc (S k) m = go (m :: acc) k (m - 1)
216+ go' acc (S k) m = go' (m :: acc) k (m - 1)
217+ go : Int -> Int -> List Int
218+ go n m = go' [] (cast {to = Nat} (m - n)) m
211 enumFromThen n inc = n :: enumFromThen (inc + n) inc
219 enumFromThen n inc = n :: enumFromThen (inc + n) inc
212 enumFromThenTo _ 0 _ = []
220 enumFromThenTo _ 0 _ = []
213− enumFromThenTo n inc m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs inc) - 1))) SIsNotZ)))
221+ enumFromThenTo n next m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))
214 where go : List Nat -> List Int
222 where go : List Nat -> List Int
215 go [] = []
223 go [] = []
216− go (x :: xs) = n + (cast x * inc) :: go xs
224+ go (x :: xs) = n + (cast x * (next - n)) :: go xs
217
225
218Enum Char where
226Enum Char where
219 toNat c = toNat (ord c)
227 toNat c = toNat (ord c)
@@ -224,12 +232,12 @@ Enum Char where
224syntax "[" [start] ".." [end] "]"
232syntax "[" [start] ".." [end] "]"
225 = enumFromTo start end
233 = enumFromTo start end
226syntax "[" [start] "," [next] ".." [end] "]"
234syntax "[" [start] "," [next] ".." [end] "]"
227− = enumFromThenTo start (next - start) end
235+ = enumFromThenTo start next end
228
236
229syntax "[" [start] ".." "]"
237syntax "[" [start] ".." "]"
230 = enumFrom start
238 = enumFrom start
231syntax "[" [start] "," [next] ".." "]"
239syntax "[" [start] "," [next] ".." "]"
232− = enumFromThen start (next - start)
240+ = enumFromThen start next
233
241
234---- More utilities
242---- More utilities
235
243
test/basic013/basic013.idr+9
@@ -31,4 +31,13 @@ main = do putStrLn foo
31 putStrLn ("Tail Tail: " ++ strTail (strTail newstr))
31 putStrLn ("Tail Tail: " ++ strTail (strTail newstr))
32 putStrLn ("Cons: " ++ strCons 'λ' newstr)
32 putStrLn ("Cons: " ++ strCons 'λ' newstr)
33 putStrLn ("Reverse: " ++ reverse newstr)
33 putStrLn ("Reverse: " ++ reverse newstr)
34+ printLn [1..5]
35+ printLn [5..1]
36+ printLn [(-9), (-7)..(-1)]
37+ printLn [17,15..1]
38+ printLn [19,15..2]
39+ printLn $ the (List Nat) [1..5]
40+ printLn $ the (List Nat) [5..1]
41+ printLn $ the (List Int) [(-1)..(-5)]
42+ printLn $ the (List Nat) [1,3..5]
34
43
test/basic013/expected+9
@@ -12,3 +12,12 @@ Tail: x→xλx→xλx→xλx→xλx→x
12Tail Tail: →xλx→xλx→xλx→xλx→x
12Tail Tail: →xλx→xλx→xλx→xλx→x
13Cons: λλx→xλx→xλx→xλx→xλx→x
13Cons: λλx→xλx→xλx→xλx→xλx→x
14Reverse: x→xλx→xλx→xλx→xλx→xλ
14Reverse: x→xλx→xλx→xλx→xλx→xλ
15+[1, 2, 3, 4, 5]
16+[5, 4, 3, 2, 1]
17+[-9, -7, -5, -3, -1]
18+[17, 15, 13, 11, 9, 7, 5, 3, 1]
19+[19, 15, 11, 7, 3]
20+[1, 2, 3, 4, 5]
21+[5, 4, 3, 2, 1]
22+[-1, -2, -3, -4, -5]
23+[1, 3, 5]