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

libs/prelude/Prelude.idr+9−3

compare with master

unifiedsplit

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

146 where go Z = []

147 go (S n) = n :: go n

148

149+

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

150-- 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+

150total natEnumFromThen : Nat -> Nat -> Stream Nat

154total 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+

152total natEnumFromTo : Nat -> Nat -> List Nat

157total natEnumFromTo : Nat -> Nat -> List Nat

153natEnumFromTo n m = if n <= m

158natEnumFromTo n m = if n <= m

154 then go n m

159 then go n m

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

197 succ n = n + 1

202 succ n = n + 1

198 toNat n = cast n

203 toNat n = cast n

199 fromNat n = cast n

204 fromNat n = cast n

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

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

201 enumFromTo n m = if n <= m

206 enumFromTo n m = if n <= m

202 then go n m

207 then go n m

203 else List.reverse $ go m n

208 else List.reverse $ go m n

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

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

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

227 go : Int -> Int -> List Int

232 go : Int -> Int -> List Int

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

233 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+

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

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

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

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

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

238 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 = [

70 ( 15, ANY ),

71 ( 16, ANY ),

72 ( 17, ANY ),

73− ( 18, ANY )]),

73+ ( 18, ANY ),

74+ ( 19, ANY )]),

74 ("bignum", "Bignum",

75 ("bignum", "Bignum",

75 [ ( 1, ANY ),

76 [ ( 1, ANY ),

76 ( 2, ANY )]),

77 ( 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..])

6+

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