32852af · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

@@ -14,6 +14,9 @@ New in 0.9.10:

14* Some prettifying of error message

15* The contents of ~/.idris/repl/init are run at REPL start-up.

16* 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.

17

20

18Internal changes

21Internal changes

19

22

lib/Prelude.idr+64−11

@@ -17,6 +17,7 @@ import Prelude.Strings

17import Prelude.Chars

18import Prelude.Traversable

19import Prelude.Bits

20+import Prelude.Stream

20

21

21%access public

22%access public

22%default total

23%default total

@@ -343,24 +344,76 @@ ceiling x = prim__floatCeil x

343

344

344---- Ranges

345---- Ranges

345

346

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 []

350

347

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

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

354

407

355syntax "[" [start] ".." [end] "]"

408syntax "[" [start] ".." [end] "]"

356− = count start 1 end

409+ = enumFromTo start end

357syntax "[" [start] "," [next] ".." [end] "]"

410syntax "[" [start] "," [next] ".." [end] "]"

358− = count start (next - start) end

411+ = enumFromThenTo start (next - start) end

359

412

360syntax "[" [start] "..]"

413syntax "[" [start] "..]"

361− = countFrom start 1

414+ = enumFrom start 1

362syntax "[" [start] "," [next] "..]"

415syntax "[" [start] "," [next] "..]"

363− = countFrom start (next - start)

416+ = enumFromThen start (next - start)

364

417

365---- More utilities

418---- More utilities

366

419

lib/Prelude/Nat.idr+9

@@ -190,6 +190,15 @@ instance Lattice Nat where { }

190instance BoundedJoinSemilattice Nat where

191 bottom = Z

192

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+

193--------------------------------------------------------------------------------

202--------------------------------------------------------------------------------

194-- Auxilliary notions

203-- Auxilliary notions

195--------------------------------------------------------------------------------

204--------------------------------------------------------------------------------

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,

7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,

8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,

9 Prelude.Heap, Prelude.Complex, Prelude.Functor, Prelude.Foldable,

10− Prelude.Traversable, Prelude.Bits,

10+ Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11

12 Network.Cgi,

13 Debug.Trace,

test/test016/test016.idr+3−3

@@ -2,12 +2,12 @@ module Main

2

3%default total

4

5−codata Stream a = Nil | (::) a (Stream a)

5+codata Stream' a = Nil | (::) a (Stream' a)

6

7−countFrom : Int -> Stream Int

7+countFrom : Int -> Stream' Int

8countFrom x = x :: countFrom (x + 1)

9

10−take : Nat -> Stream a -> List a

10+take : Nat -> Stream' a -> List a

11take Z _ = []

12take (S n) (x :: xs) = x :: take n xs

13take n [] = []