@@ -146,12 +146,18 @@ natRange n = List.reverse (go n)
146146
147147-- predefine Nat versions of Enum, so we can use them in the default impls
148148total natEnumFromThen : Nat -> Nat -> Stream Nat
149−natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
149+natEnumFromThen n next = n :: natEnumFromThen next (minus next n)
150150total natEnumFromTo : Nat -> Nat -> List Nat
151−natEnumFromTo n m = map (plus n) (natRange (minus (S m) n))
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
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)))
152159total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
153−natEnumFromThenTo _ Z _ = []
154−natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))
160+natEnumFromThenTo n next m = natEnumFromThenTo' n (minus next n) m
155161
156162interface Enum a where
157163 total pred : a -> a
@@ -184,36 +190,38 @@ Enum Integer where
184190 fromNat n = cast n
185191 enumFromThen n inc = n :: enumFromThen (inc + n) inc
186192 enumFromTo n m = if n <= m
187− then go (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
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
199+ go n m = go' n (natRange (S (cast {to = Nat} (m - n))))
192200 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)))
194202 where go : List Nat -> List Integer
195203 go [] = []
196− go (x :: xs) = n + (cast x * inc) :: go xs
204+ go (x :: xs) = n + (cast x * (next - n)) :: go xs
197205
198206Enum Int where
199207 pred n = n - 1
200208 succ n = n + 1
201209 toNat n = cast n
202210 fromNat n = cast n
203− enumFromTo n m =
204− if n <= m
205− then go [] (cast {to = Nat} (m - n)) m
206− else []
207− where
208− go : List Int -> Nat -> Int -> List Int
209− go acc Z m = m :: acc
210− go acc (S k) m = go (m :: acc) k (m - 1)
211+ enumFromTo n m = if n <= m
212+ then go n m
213+ else List.reverse $ go m n
214+ where go' : List Int -> Nat -> Int -> List Int
215+ go' acc Z m = m :: acc
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
211219 enumFromThen n inc = n :: enumFromThen (inc + n) inc
212220 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)))
214222 where go : List Nat -> List Int
215223 go [] = []
216− go (x :: xs) = n + (cast x * inc) :: go xs
224+ go (x :: xs) = n + (cast x * (next - n)) :: go xs
217225
218226Enum Char where
219227 toNat c = toNat (ord c)
@@ -224,12 +232,12 @@ Enum Char where
224232syntax "[" [start] ".." [end] "]"
225233 = enumFromTo start end
226234syntax "[" [start] "," [next] ".." [end] "]"
227− = enumFromThenTo start (next - start) end
235+ = enumFromThenTo start next end
228236
229237syntax "[" [start] ".." "]"
230238 = enumFrom start
231239syntax "[" [start] "," [next] ".." "]"
232− = enumFromThen start (next - start)
240+ = enumFromThen start next
233241
234242---- More utilities
235243