@@ -17,6 +17,7 @@ import Prelude.Strings
1717import Prelude.Chars
1818import Prelude.Traversable
1919import Prelude.Bits
20+import Prelude.Stream
2021
2122%access public
2223%default total
@@ -343,24 +344,73 @@ ceiling x = prim__floatCeil x
343344
344345---- Ranges
345346
346−partial abstract
347−count : (Ord a, Num a) => a -> a -> a -> List a
348−count a inc b = if a <= b then a :: count (a + inc) inc b
349− else []
350347
351−partial abstract
352−countFrom : (Ord a, Num a) => a -> a -> List a
353−countFrom a inc = a :: lazy (countFrom (a + inc) inc)
348+natRange : Nat -> List Nat
349+natRange n = List.reverse (go n)
350+ where go Z = []
351+ go (S n) = n :: go n
352+
353+class Enum a where
354+ total pred : a -> a
355+ total succ : a -> a
356+ total toNat : a -> Nat
357+ total fromNat : Nat -> a
358+ total enumFrom : a -> Stream a
359+ enumFrom n = n :: enumFrom (succ n)
360+ total enumFromThen : a -> a -> Stream a
361+ total enumFromTo : a -> a -> List a
362+ total enumFromThenTo : a -> a -> a -> List a
363+
364+
365+instance Enum Nat where
366+ pred = Nat.pred
367+ succ = S
368+ toNat = id
369+ fromNat = id
370+ enumFromThen n inc = n :: enumFromThen (fromNat (plus (toNat inc) (toNat n))) inc
371+ enumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S (( m - n) `div` inc)))
372+ enumFromTo n m = map (plus n) (natRange (S (m - n)))
373+
374+
375+instance Enum Integer where
376+ pred n = n - 1
377+ succ n = n + 1
378+ toNat n = cast n
379+ fromNat n = cast n
380+ enumFromThen n inc = n :: enumFromThen (inc + n) inc
381+ enumFromTo n m = go (natRange (S (cast {to = Nat} (m - n))))
382+ where go : List Nat -> List Integer
383+ go [] = []
384+ go (x :: xs) = n + cast x :: go xs
385+ enumFromThenTo n inc m = go (natRange (S (fromInteger (abs (m - n)) `div` fromInteger (abs inc))))
386+ where go : List Nat -> List Integer
387+ go [] = []
388+ go (x :: xs) = n + (cast x * inc) :: go xs
389+
390+instance Enum Int where
391+ pred n = n - 1
392+ succ n = n + 1
393+ toNat n = cast n
394+ fromNat n = cast n
395+ enumFromThen n inc = n :: enumFromThen (inc + n) inc
396+ enumFromTo n m = go (natRange (S (cast {to = Nat} (m - n))))
397+ where go : List Nat -> List Int
398+ go [] = []
399+ go (x :: xs) = n + cast x :: go xs
400+ enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))
401+ where go : List Nat -> List Int
402+ go [] = []
403+ go (x :: xs) = n + (cast x * inc) :: go xs
354404
355405syntax "[" [start] ".." [end] "]"
356− = count start 1 end
406+ = enumFromTo start end
357407syntax "[" [start] "," [next] ".." [end] "]"
358− = count start (next - start) end
408+ = enumFromThenTo start (next - start) end
359409
360410syntax "[" [start] "..]"
361− = countFrom start 1
411+ = enumFrom start 1
362412syntax "[" [start] "," [next] "..]"
363− = countFrom start (next - start)
413+ = enumFromThen start (next - start)
364414
365415---- More utilities
366416