fe4d6d3 · Idris-dev · git.iko.soy

libs/base/Data/Complex.idr−2

compare with master

unifiedsplit

@@ -5,8 +5,6 @@

5

6module Data.Complex

7

8−import Data.Floats

9−

10------------------------------ Rectangular form

8------------------------------ Rectangular form

11

9

12infix 6 :+

10infix 6 :+

libs/base/base.ipkg+1−1

@@ -15,7 +15,7 @@ modules = System,

15 Data.Bits, Data.Mod2,

16 Data.Fin, Data.Vect, Data.VectType,

17 Data.HVect, Data.Vect.Quantifiers,

18− Data.Floats, Data.Complex,

18+ Data.Complex,

19 Data.Erased, Data.List,

20 Data.So,

21

libs/prelude/Prelude.idr+1

@@ -27,6 +27,7 @@ import public Prelude.Providers

27import public Prelude.Show

28import public Prelude.Interactive

29import public Prelude.File

30+import public Prelude.Doubles

30import public Decidable.Equality

31import public Decidable.Equality

31import public Language.Reflection

32import public Language.Reflection

32import public Language.Reflection.Errors

33import public Language.Reflection.Errors

libs/base/Data/Floats.idr → libs/prelude/Prelude/Doubles.idrrenamed+22−18

@@ -1,4 +1,7 @@

1−module Data.Floats

1+module Prelude.Doubles

2+

3+import Builtins

4+import Prelude.Classes

2

5

3%access public

6%access public

4%default total

7%default total

@@ -6,54 +9,55 @@ module Data.Floats

6%include C "math.h"

9%include C "math.h"

7%lib C "m"

10%lib C "m"

8

11

9−pi : Float

12+pi : Double

10pi = 3.14159265358979323846

13pi = 3.14159265358979323846

11

14

12−euler : Float

15+euler : Double

13euler = 2.7182818284590452354

16euler = 2.7182818284590452354

14

17

15−exp : Float -> Float

18+exp : Double -> Double

16exp x = prim__floatExp x

19exp x = prim__floatExp x

17

20

18−log : Float -> Float

21+log : Double -> Double

19log x = prim__floatLog x

22log x = prim__floatLog x

20

23

21−sin : Float -> Float

24+sin : Double -> Double

22sin x = prim__floatSin x

25sin x = prim__floatSin x

23

26

24−cos : Float -> Float

27+cos : Double -> Double

25cos x = prim__floatCos x

28cos x = prim__floatCos x

26

29

27−tan : Float -> Float

30+tan : Double -> Double

28tan x = prim__floatTan x

31tan x = prim__floatTan x

29

32

30−asin : Float -> Float

33+asin : Double -> Double

31asin x = prim__floatASin x

34asin x = prim__floatASin x

32

35

33−acos : Float -> Float

36+acos : Double -> Double

34acos x = prim__floatACos x

37acos x = prim__floatACos x

35

38

36−atan : Float -> Float

39+atan : Double -> Double

37atan x = prim__floatATan x

40atan x = prim__floatATan x

38

41

39−atan2 : Float -> Float -> Float

42+atan2 : Double -> Double -> Double

40atan2 y x = atan (y/x)

43atan2 y x = atan (y/x)

41

44

42−sinh : Float -> Float

45+sinh : Double -> Double

43sinh x = (exp x - exp (-x)) / 2

46sinh x = (exp x - exp (-x)) / 2

44

47

45−cosh : Float -> Float

48+cosh : Double -> Double

46cosh x = (exp x + exp (-x)) / 2

49cosh x = (exp x + exp (-x)) / 2

47

50

48−tanh : Float -> Float

51+tanh : Double -> Double

49tanh x = sinh x / cosh x

52tanh x = sinh x / cosh x

50

53

51−sqrt : Float -> Float

54+sqrt : Double -> Double

52sqrt x = prim__floatSqrt x

55sqrt x = prim__floatSqrt x

53

56

54−floor : Float -> Float

57+floor : Double -> Double

55floor x = prim__floatFloor x

58floor x = prim__floatFloor x

56

59

57−ceiling : Float -> Float

60+ceiling : Double -> Double

58ceiling x = prim__floatCeil x

61ceiling x = prim__floatCeil x

59

62

63+

libs/prelude/prelude.ipkg+1−1

@@ -9,7 +9,7 @@ modules = Builtins, Prelude, IO,

9 Prelude.Strings, Prelude.Chars, Prelude.Show, Prelude.Functor,

10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,

12− Prelude.Interactive, Prelude.File,

12+ Prelude.Interactive, Prelude.File, Prelude.Doubles,

13

14 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,

15

test/primitives001/expected−1

@@ -1,5 +1,4 @@

18

2−1

3("abc", "123")

2("abc", "123")

4("abc", "123")

3("abc", "123")

5([1, 2], [3, 4, 5])

4([1, 2], [3, 4, 5])

test/primitives001/test005.idr−1

@@ -8,7 +8,6 @@ tlist = [1, 2, 3, 4, 5]

8

9main : IO ()

10main = do printLn (abs (-8))

11− printLn (abs (S Z))

12 printLn (span isAlpha tstr)

11 printLn (span isAlpha tstr)

13 printLn (break isDigit tstr)

12 printLn (break isDigit tstr)

14 printLn (span (\x => x < 3) tlist)

13 printLn (span (\x => x < 3) tlist)

test/proofsearch002/Process.idr+1−1

@@ -339,7 +339,7 @@ removeConn cl acc [] = (cl, reverse acc)

339removeConn cl acc ((pid, ConnectMsg) :: xs)

340 = removeConn (cl + 1) acc xs

341removeConn cl acc ((pid, CloseMsg) :: xs)

342− = removeConn (cl - 1) acc xs

342+ = removeConn (minus cl 1) acc xs

343removeConn cl acc (x :: xs) = removeConn cl (x :: acc) xs

344

345-- Remove the first thing in the event list which is a request, if it