git.iko.soy/Idris-dev
on master help sign in
Merge pull request #638 from david-christiansen/issue/328

Total version of [a..b] and [a,b..c]

commit32852af248f0f0e15d9018264024274d13a55f69 authorEdwin Brady <edwin.brady@gmail.com> dateTue 19 Nov 2013, 12:34 (13 years ago) parent6c0ae329a1b66f
6 files changed+90−15
compare with master
unifiedsplit
CHANGELOG+3 lib/Prelude.idr+64−11 lib/Prelude/Nat.idr+9 lib/Prelude/Stream.idr+10 lib/base.ipkg+1−1 test/test016/test016.idr+3−3
CHANGELOG+3
@@ -14,6 +14,9 @@ New in 0.9.10:
1414* Some prettifying of error message
1515* The contents of ~/.idris/repl/init are run at REPL start-up.
1616* The REPL stores a command history in ~/.idris/repl/history
17+* The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality
18+ checker and can thus be used in types. The [x..] syntax now returns an
19+ actually infinite stream.
1720
1821Internal changes
1922
lib/Prelude.idr+64−11
@@ -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,76 @@ 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 _ Z _ = []
372+ enumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S (( m - n) `div` inc)))
373+ enumFromTo n m = map (plus n) (natRange (S (m - n)))
374+
375+
376+instance Enum Integer where
377+ pred n = n - 1
378+ succ n = n + 1
379+ toNat n = cast n
380+ fromNat n = cast n
381+ enumFromThen n inc = n :: enumFromThen (inc + n) inc
382+ enumFromTo n m = go (natRange (S (cast {to = Nat} (m - n))))
383+ where go : List Nat -> List Integer
384+ go [] = []
385+ go (x :: xs) = n + cast x :: go xs
386+ enumFromThenTo _ 0 _ = []
387+ enumFromThenTo n inc m = go (natRange (S (fromInteger (abs (m - n)) `div` fromInteger (abs inc))))
388+ where go : List Nat -> List Integer
389+ go [] = []
390+ go (x :: xs) = n + (cast x * inc) :: go xs
391+
392+instance Enum Int where
393+ pred n = n - 1
394+ succ n = n + 1
395+ toNat n = cast n
396+ fromNat n = cast n
397+ enumFromThen n inc = n :: enumFromThen (inc + n) inc
398+ enumFromTo n m = go (natRange (S (cast {to = Nat} (m - n))))
399+ where go : List Nat -> List Int
400+ go [] = []
401+ go (x :: xs) = n + cast x :: go xs
402+ enumFromThenTo _ 0 _ = []
403+ enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))
404+ where go : List Nat -> List Int
405+ go [] = []
406+ go (x :: xs) = n + (cast x * inc) :: go xs
354407
355408syntax "[" [start] ".." [end] "]"
356− = count start 1 end
409+ = enumFromTo start end
357410syntax "[" [start] "," [next] ".." [end] "]"
358− = count start (next - start) end
411+ = enumFromThenTo start (next - start) end
359412
360413syntax "[" [start] "..]"
361− = countFrom start 1
414+ = enumFrom start 1
362415syntax "[" [start] "," [next] "..]"
363− = countFrom start (next - start)
416+ = enumFromThen start (next - start)
364417
365418---- More utilities
366419
lib/Prelude/Nat.idr+9
@@ -190,6 +190,15 @@ instance Lattice Nat where { }
190190instance BoundedJoinSemilattice Nat where
191191 bottom = Z
192192
193+
194+instance Cast Int Nat where
195+ cast i = fromInteger (cast i)
196+
197+instance Cast Nat Int where
198+ cast Z = 0
199+ cast (S n) = 1 + cast {to=Int} n
200+
201+
193202--------------------------------------------------------------------------------
194203-- Auxilliary notions
195204--------------------------------------------------------------------------------
lib/Prelude/Stream.idrnew file+10
@@ -0,0 +1,10 @@
1+module Prelude.Stream
2+
3+import Prelude.Vect
4+
5+codata Stream : Type -> Type where
6+ (::) : a -> Stream a -> Stream a
7+
8+take : (n : Nat) -> Stream a -> Vect n a
9+take Z _ = []
10+take (S n) (x :: xs) = x :: (take n xs)
lib/base.ipkg+1−1
@@ -7,7 +7,7 @@ modules = Builtins, Prelude, IO, System,
77 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
88 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
99 Prelude.Heap, Prelude.Complex, Prelude.Functor, Prelude.Foldable,
10− Prelude.Traversable, Prelude.Bits,
10+ Prelude.Traversable, Prelude.Bits, Prelude.Stream,
1111
1212 Network.Cgi,
1313 Debug.Trace,
test/test016/test016.idr+3−3
@@ -2,12 +2,12 @@ module Main
22
33%default total
44
5−codata Stream a = Nil | (::) a (Stream a)
5+codata Stream' a = Nil | (::) a (Stream' a)
66
7−countFrom : Int -> Stream Int
7+countFrom : Int -> Stream' Int
88countFrom x = x :: countFrom (x + 1)
99
10−take : Nat -> Stream a -> List a
10+take : Nat -> Stream' a -> List a
1111take Z _ = []
1212take (S n) (x :: xs) = x :: take n xs
1313take n [] = []