7e93d70 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix enumFromThenTo

This worked in almost no cases... now uses a function to count with an increment, and adds a test for ranges. Fixes #3512

commit7e93d70ad49cac2f5afb6c0315e21abe96f6df1b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 9 Dec 2016, 16:08 (10 years ago) parent4c4a07a

5 files changed+37−4

compare with master

unifiedsplit

libs/prelude/Prelude.idr+9−3 test/TestData.hs+2−1 test/basic019/basic019.idr+10 test/basic019/expected+12 test/basic019/run+4

libs/prelude/Prelude.idr+9−3

@@ -146,9 +146,14 @@ natRange n = List.reverse (go n)

146146 where go Z = []

147147 go (S n) = n :: go n

148148

149+

149150-- predefine Nat versions of Enum, so we can use them in the default impls

151+countFrom : Num n => n -> n -> Stream n

152+countFrom start diff = start :: countFrom (start + diff) diff

153+

150154total natEnumFromThen : Nat -> Nat -> Stream Nat

151−natEnumFromThen n next = n :: natEnumFromThen next (minus next n)

155+natEnumFromThen n next = countFrom n (minus next n)

156+

152157total natEnumFromTo : Nat -> Nat -> List Nat

153158natEnumFromTo n m = if n <= m

154159 then go n m

@@ -197,7 +202,7 @@ Enum Integer where

197202 succ n = n + 1

198203 toNat n = cast n

199204 fromNat n = cast n

200− enumFromThen n inc = n :: enumFromThen (inc + n) inc

205+ enumFromThen n inc = countFrom n (inc - n)

201206 enumFromTo n m = if n <= m

202207 then go n m

203208 else List.reverse $ go m n

@@ -226,7 +231,8 @@ Enum Int where

226231 go' acc (S k) m = go' (m :: acc) k (m - 1)

227232 go : Int -> Int -> List Int

228233 go n m = go' [] (cast {to = Nat} (m - n)) m

229− enumFromThen n inc = n :: enumFromThen (inc + n) inc

234+ enumFromThen n inc = countFrom n (inc - n)

235+

230236 enumFromThenTo n next m = if n == m then [n]

231237 else if next - n == 0 || next - n < 0 /= m - n < 0 then []

232238 else go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs (next - n)) - 1))) SIsNotZ)))

test/TestData.hs+2−1

@@ -70,7 +70,8 @@ testFamiliesData = [

7070 ( 15, ANY ),

7171 ( 16, ANY ),

7272 ( 17, ANY ),

73− ( 18, ANY )]),

73+ ( 18, ANY ),

74+ ( 19, ANY )]),

7475 ("bignum", "Bignum",

7576 [ ( 1, ANY ),

7677 ( 2, ANY )]),

test/basic019/basic019.idrnew file+10

@@ -0,0 +1,10 @@

1+printRange : (t : Type) -> (Show t, Num t, Enum t) => IO ()

2+printRange t = do printLn [(the t 1)..10]

3+ printLn [(the t 10),9..1]

4+ printLn (take 10 [(the t 1)..])

5+ printLn (take 10 [(the t 1),3..])

7+main : IO ()

8+main = do printRange Nat

9+ printRange Int

10+ printRange Integer

test/basic019/expectednew file+12

@@ -0,0 +1,12 @@

1+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

2+[10, 9, 8, 7, 6, 5, 4, 3, 2, 1]

3+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

4+[1, 3, 5, 7, 9, 11, 13, 15, 17, 19]

5+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

6+[10, 9, 8, 7, 6, 5, 4, 3, 2, 1]

7+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

8+[1, 3, 5, 7, 9, 11, 13, 15, 17, 19]

9+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

10+[10, 9, 8, 7, 6, 5, 4, 3, 2, 1]

11+[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

12+[1, 3, 5, 7, 9, 11, 13, 15, 17, 19]

test/basic019/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ basic019.idr -o basic019

3+./basic019

4+rm -f basic019 *.ibc