3edef47 · Idris-dev · git.iko.soy

lib/builtins.idr+5−4

compare with master

unifiedsplit

@@ -186,14 +186,12 @@ instance (Ord a, Ord b) => Ord (a, b) where

186 else compare xr yr

187

188

189−class (Eq a, Ord a) => Num a where

189+class Eq a => Num a where

190 (+) : a -> a -> a

191 (-) : a -> a -> a

192 (*) : a -> a -> a

193

194 abs : a -> a

195− abs x = if (x < 0) then (-x) else x

196−

197 fromInteger : Int -> a

195 fromInteger : Int -> a

198

196

199

197

@@ -203,7 +201,8 @@ instance Num Int where

203 (-) = prim__subInt

201 (-) = prim__subInt

204 (*) = prim__mulInt

202 (*) = prim__mulInt

205

203

206− fromInteger = id -- prim__bigIntToInt

204+ fromInteger = id

205+ abs x = if x<0 then -x else x

207

206

208

207

209instance Num Integer where

208instance Num Integer where

@@ -211,6 +210,7 @@ instance Num Integer where

211 (-) = prim__subBigInt

210 (-) = prim__subBigInt

212 (*) = prim__mulBigInt

211 (*) = prim__mulBigInt

213

212

213+ abs x = if x<0 then -x else x

214 fromInteger = prim__intToBigInt

215

216

@@ -219,6 +219,7 @@ instance Num Float where

219 (-) = prim__subFloat

220 (*) = prim__mulFloat

221

222+ abs x = if x<0 then -x else x

222 fromInteger = prim__intToFloat

223 fromInteger = prim__intToFloat

223

224

225

lib/checkall.idr+1

@@ -21,6 +21,7 @@ import prelude.vect

21import prelude.strings

22import prelude.char

23import prelude.heap

24+import prelude.complex

24

25

25import network.cgi

26import network.cgi

26

27

lib/prelude.idr+5−2

@@ -143,6 +143,9 @@ acos x = prim__floatACos x

143atan : Float -> Float

144atan x = prim__floatATan x

145

146+atan2 : Float -> Float -> Float

147+atan2 y x = atan (y/x)

148+

146sqrt : Float -> Float

149sqrt : Float -> Float

147sqrt x = prim__floatSqrt x

150sqrt x = prim__floatSqrt x

148

151

@@ -154,11 +157,11 @@ ceiling x = prim__floatCeil x

154

157

155---- Ranges

158---- Ranges

156

159

157−count : Num a => a -> a -> a -> List a

160+count : (Ord a, Num a) => a -> a -> a -> List a

158count a inc b = if a <= b then a :: count (a + inc) inc b

161count a inc b = if a <= b then a :: count (a + inc) inc b

159 else []

162 else []

160

163

161−countFrom : Num a => a -> a -> List a

164+countFrom : (Ord a, Num a) => a -> a -> List a

162countFrom a inc = a :: lazy (countFrom (a + inc) inc)

165countFrom a inc = a :: lazy (countFrom (a + inc) inc)

163

166

164syntax "[" [start] ".." [end] "]"

167syntax "[" [start] ".." [end] "]"

lib/prelude/complex.idrnew file+65

@@ -0,0 +1,65 @@

1+module prelude.complex

2+

3+import builtins

4+

5+

6+------------------------------ Rectangular form

7+

8+infix 6 :+

9+data Complex a = (:+) a a

10+

11+realPart : Complex a -> a

12+realPart (r:+i) = r

13+

14+imagPart : Complex a -> a

15+imagPart (r:+i) = i

16+

17+instance Eq a => Eq (Complex a) where

18+ (==) a b = realPart a == realPart b && imagPart a == imagPart b

19+

20+instance Show a => Show (Complex a) where

21+ show (r:+i) = "("++show r++":+"++show i++")"

22+

23+

24+

25+-- when we have a type class 'Fractional' (which contains Float and Double),

26+-- we can do:

27+{-

28+instance Fractional a => Fractional (Complex a) where

29+ (/) (a:+b) (c:+d) = let

30+ real = (a*c+b*d)/(c*c+d*d)

31+ imag = (b*c-a*d)/(c*c+d*d)

32+ in

33+ (real:+imag)

34+-}

35+

36+

37+

38+------------------------------ Polarform

39+

40+mkPolar : Float -> Float -> Complex Float

41+mkPolar radius angle = radius * cos angle :+ radius * sin angle

42+

43+cis : Float -> Complex Float

44+cis angle = cos angle :+ sin angle

45+

46+magnitude : Complex Float -> Float

47+magnitude (r:+i) = sqrt (r*r+i*i)

48+

49+phase : Complex Float -> Float

50+phase (x:+y) = atan2 y x

51+

52+

53+------------------------------ Conjugate

54+

55+conjugate : Num a => Complex a -> Complex a

56+conjugate (r:+i) = (r :+ (0-i))

57+

58+-- We can't do "instance Num a => Num (Complex a)" because

59+-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float

60+instance Num (Complex Float) where

61+ (+) (a:+b) (c:+d) = ((a+b):+(c+d))

62+ (-) (a:+b) (c:+d) = ((a-b):+(c-d))

63+ (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))

64+ fromInteger x = (fromInteger x:+0)

65+ abs (a:+b) = (magnitude (a:+b):+0)

lib/prelude/nat.idr+2

@@ -113,6 +113,8 @@ instance Num Nat where

113 (-) = minus

114 (*) = mult

115

116+ abs x = x

117+

116 fromInteger = fromInteger'

118 fromInteger = fromInteger'

117 where

119 where

118 %assert_total

120 %assert_total