on master help sign in
Move floating point operations out of Prelude
commitf38190dc031a7e0f9c1fc9287a28a822fedf8a5b authorMarkus Pfeiffer <markusp@mcs.st-andrews.ac.uk> dateWed 20 Nov 2013, 11:18 (13 years ago) parentd33d0bf
3 files changed+4−53
lib/Prelude/Complex.idr → lib/Data/Complex.idr+2 lib/Prelude.idr+1−53 lib/base.ipkg+1
lib/Prelude/Complex.idr → lib/Data/Complex.idrrenamed+2
@@ -8,6 +8,8 @@ module Prelude.Complex
88import Builtins
99import Prelude
1010
11+import Data.Floats
12+
1113------------------------------ Rectangular form
1214
1315infix 6 :+
lib/Prelude.idr+1−53
@@ -286,65 +286,13 @@ instance Traversable (Vect n) where
286286 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]
287287
288288---- some mathematical operations
289−
290−%include C "math.h"
291−%lib C "m"
292−
289+---- XXX this should probably go some place else,
293290pow : (Num a) => a -> Nat -> a
294291pow x Z = 1
295292pow x (S n) = x * (pow x n)
296293
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−
345294---- Ranges
346295
347−
348296natRange : Nat -> List Nat
349297natRange n = List.reverse (go n)
350298 where go Z = []
lib/base.ipkg+1
@@ -27,6 +27,7 @@ modules = Builtins, Prelude, IO, System,
2727 Data.ZZ, Data.Sign,
2828 Data.SortedMap, Data.SortedSet, Data.BoundedList,
2929 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
30+ Data.Floats, Data.Complex,
3031
3132 Control.Monad.Identity,
3233 Control.Monad.RWS,