git.iko.soy/Idris-dev
on master help sign in
Merge pull request #648 from markuspf/float-prelude
3e2141bEdwin Brady
lib/Prelude/Complex.idr → lib/Data/Complex.idrrenamed+2
compare with master
unifiedsplit
@@ -8,6 +8,8 @@ module Prelude.Complex
8import Builtins
8import Builtins
9import Prelude
9import Prelude
10
10
11+import Data.Floats
12+
11------------------------------ Rectangular form
13------------------------------ Rectangular form
12
14
13infix 6 :+
15infix 6 :+
lib/Data/Floats.idrnew file+61
@@ -0,0 +1,61 @@
1+module Data.Floats
2+
3+import Prelude
4+
5+%access public
6+%default total
7+
8+%include C "math.h"
9+%lib C "m"
10+
11+pi : Float
12+pi = 3.14159265358979323846
13+
14+euler : Float
15+euler = 2.7182818284590452354
16+
17+exp : Float -> Float
18+exp x = prim__floatExp x
19+
20+log : Float -> Float
21+log x = prim__floatLog x
22+
23+sin : Float -> Float
24+sin x = prim__floatSin x
25+
26+cos : Float -> Float
27+cos x = prim__floatCos x
28+
29+tan : Float -> Float
30+tan x = prim__floatTan x
31+
32+asin : Float -> Float
33+asin x = prim__floatASin x
34+
35+acos : Float -> Float
36+acos x = prim__floatACos x
37+
38+atan : Float -> Float
39+atan x = prim__floatATan x
40+
41+atan2 : Float -> Float -> Float
42+atan2 y x = atan (y/x)
43+
44+sinh : Float -> Float
45+sinh x = (exp x - exp (-x)) / 2
46+
47+cosh : Float -> Float
48+cosh x = (exp x + exp (-x)) / 2
49+
50+tanh : Float -> Float
51+tanh x = sinh x / cosh x
52+
53+sqrt : Float -> Float
54+sqrt x = prim__floatSqrt x
55+
56+floor : Float -> Float
57+floor x = prim__floatFloor x
58+
59+ceiling : Float -> Float
60+ceiling x = prim__floatCeil x
61+
lib/Prelude.idr+1−53
@@ -286,65 +286,13 @@ instance Traversable (Vect n) where
286 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
286 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
287
287
288---- some mathematical operations
288---- some mathematical operations
289−
289+---- XXX this should probably go some place else,
290−%include C "math.h"
291−%lib C "m"
292−
293pow : (Num a) => a -> Nat -> a
290pow : (Num a) => a -> Nat -> a
294pow x Z = 1
291pow x Z = 1
295pow x (S n) = x * (pow x n)
292pow x (S n) = x * (pow x n)
296
293
297−exp : Float -> Float
298−exp x = prim__floatExp x
299−
300−log : Float -> Float
301−log x = prim__floatLog x
302−
303−pi : Float
304−pi = 3.141592653589793
305−
306−sin : Float -> Float
307−sin x = prim__floatSin x
308−
309−cos : Float -> Float
310−cos x = prim__floatCos x
311−
312−tan : Float -> Float
313−tan x = prim__floatTan x
314−
315−asin : Float -> Float
316−asin x = prim__floatASin x
317−
318−acos : Float -> Float
319−acos x = prim__floatACos x
320−
321−atan : Float -> Float
322−atan x = prim__floatATan x
323−
324−atan2 : Float -> Float -> Float
325−atan2 y x = atan (y/x)
326−
327−sinh : Float -> Float
328−sinh x = (exp x - exp (-x)) / 2
329−
330−cosh : Float -> Float
331−cosh x = (exp x + exp (-x)) / 2
332−
333−tanh : Float -> Float
334−tanh x = sinh x / cosh x
335−
336−sqrt : Float -> Float
337−sqrt x = prim__floatSqrt x
338−
339−floor : Float -> Float
340−floor x = prim__floatFloor x
341−
342−ceiling : Float -> Float
343−ceiling x = prim__floatCeil x
344−
345---- Ranges
294---- Ranges
346
295
347−
348natRange : Nat -> List Nat
296natRange : Nat -> List Nat
349natRange n = List.reverse (go n)
297natRange n = List.reverse (go n)
350 where go Z = []
298 where go Z = []
lib/base.ipkg+2−1
@@ -6,7 +6,7 @@ modules = Builtins, Prelude, IO, System,
6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
6 Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
9− Prelude.Heap, Prelude.Complex, Prelude.Functor, Prelude.Foldable,
9+ Prelude.Heap, Prelude.Functor, Prelude.Foldable,
10 Prelude.Traversable, Prelude.Bits, Prelude.Stream,
10 Prelude.Traversable, Prelude.Bits, Prelude.Stream,
11
11
12 Network.Cgi,
12 Network.Cgi,
@@ -27,6 +27,7 @@ modules = Builtins, Prelude, IO, System,
27 Data.ZZ, Data.Sign,
27 Data.ZZ, Data.Sign,
28 Data.SortedMap, Data.SortedSet, Data.BoundedList,
28 Data.SortedMap, Data.SortedSet, Data.BoundedList,
29 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
29 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
30+ Data.Floats, Data.Complex,
30
31
31 Control.Monad.Identity,
32 Control.Monad.Identity,
32 Control.Monad.RWS,
33 Control.Monad.RWS,