@@ -17,6 +17,7 @@ import Prelude.Strings
17import Prelude.Chars
17import Prelude.Chars
18import Prelude.Traversable
18import Prelude.Traversable
19import Prelude.Bits
19import Prelude.Bits
21%access public
22%access public
22%default total
23%default total
@@ -343,24 +344,73 @@ ceiling x = prim__floatCeil x
344---- Ranges
345---- Ranges
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
351−partial abstract
348+natRange : Nat -> List Nat
352−countFrom : (Ord a, Num a) => a -> a -> List a
349+natRange n = List.reverse (go n)
353−countFrom a inc = a :: lazy (countFrom (a + inc) inc)
350+ where go Z = []
351+ go (S n) = n :: go n
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
365+instance Enum Nat where
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)))
375+instance Enum Integer where
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
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
388+ go (x :: xs) = n + (cast x * inc) :: go xs
390+instance Enum Int where
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
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
403+ go (x :: xs) = n + (cast x * inc) :: go xs
355syntax "[" [start] ".." [end] "]"
405syntax "[" [start] ".." [end] "]"
356− = count start 1 end
406+ = enumFromTo start end
357syntax "[" [start] "," [next] ".." [end] "]"
407syntax "[" [start] "," [next] ".." [end] "]"
358− = count start (next - start) end
408+ = enumFromThenTo start (next - start) end
360syntax "[" [start] "..]"
410syntax "[" [start] "..]"
361− = countFrom start 1
411+ = enumFrom start 1
362syntax "[" [start] "," [next] "..]"
412syntax "[" [start] "," [next] "..]"
363− = countFrom start (next - start)
413+ = enumFromThen start (next - start)
365---- More utilities
415---- More utilities