on master help sign in
Merge branch 'float-double' of https://github.com/enolan/Idris-dev into enolan-float-double
commit99a9eeeb22addbc0e482660b7f4db4f319f037b0 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 26 Nov 2015, 22:41 (11 years ago) parenta6d51668a17e9a
9 files changed+32−30
libs/base/Data/Complex.idr+7−7 libs/contrib/Control/Algebra/NumericInstances.idr+7−7 libs/effects/Effect/Default.idr+1−1 libs/oldeffects/Effect/Default.idr+1−1 libs/prelude/Builtins.idr+3−1 libs/prelude/IO.idr+2−2 libs/prelude/Prelude/Classes.idr+6−6 test/ffi001/test022.idr+2−2 test/interactive010/expected+3−3
libs/base/Data/Complex.idr+7−7
@@ -40,16 +40,16 @@ instance Fractional a => Fractional (Complex a) where
4040
4141------------------------------ Polarform
4242
43−mkPolar : Float -> Float -> Complex Float
43+mkPolar : Double -> Double -> Complex Double
4444mkPolar radius angle = radius * cos angle :+ radius * sin angle
4545
46−cis : Float -> Complex Float
46+cis : Double -> Complex Double
4747cis angle = cos angle :+ sin angle
4848
49−magnitude : Complex Float -> Float
49+magnitude : Complex Double -> Double
5050magnitude (r:+i) = sqrt (r*r+i*i)
5151
52−phase : Complex Float -> Float
52+phase : Complex Double -> Double
5353phase (x:+y) = atan2 y x
5454
5555
@@ -62,13 +62,13 @@ instance Functor Complex where
6262 map f (r :+ i) = f r :+ f i
6363
6464-- We can't do "instance Num a => Num (Complex a)" because
65−-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Float
66−instance Num (Complex Float) where
65+-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double
66+instance Num (Complex Double) where
6767 (+) (a:+b) (c:+d) = ((a+c):+(b+d))
6868 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))
6969 fromInteger x = (fromInteger x:+0)
7070
71−instance Neg (Complex Float) where
71+instance Neg (Complex Double) where
7272 negate = map negate
7373 (-) (a:+b) (c:+d) = ((a-c):+(b-d))
7474 abs (a:+b) = (magnitude (a:+b):+0)
libs/contrib/Control/Algebra/NumericInstances.idr+7−7
@@ -44,24 +44,24 @@ instance RingWithUnity Int where
4444 unity = 1
4545
4646
47−instance Semigroup Float where
47+instance Semigroup Double where
4848 (<+>) = (+)
4949
50−instance Monoid Float where
50+instance Monoid Double where
5151 neutral = 0
5252
53−instance Group Float where
53+instance Group Double where
5454 inverse = (* -1)
5555
56−instance AbelianGroup Float
56+instance AbelianGroup Double
5757
58−instance Ring Float where
58+instance Ring Double where
5959 (<.>) = (*)
6060
61−instance RingWithUnity Float where
61+instance RingWithUnity Double where
6262 unity = 1
6363
64−instance Field Float where
64+instance Field Double where
6565 inverseM f _ = 1 / f
6666
6767
libs/effects/Effect/Default.idr+1−1
@@ -11,7 +11,7 @@ instance Default Int where
1111instance Default Integer where
1212 default = 0
1313
14−instance Default Float where
14+instance Default Double where
1515 default = 0
1616
1717instance Default Nat where
libs/oldeffects/Effect/Default.idr+1−1
@@ -9,7 +9,7 @@ instance Default Int where
99instance Default Integer where
1010 default = 0
1111
12−instance Default Float where
12+instance Default Double where
1313 default = 0
1414
1515instance Default Nat where
libs/prelude/Builtins.idr+3−1
@@ -152,9 +152,11 @@ public %assert_total
152152really_believe_me : a -> b
153153really_believe_me x = prim__believe_me _ _ x
154154
155−-- Deprecated - for backward compatibility
155+||| Alias for `Double`. Idris does not support 32 bit floats at
156+||| present.
156157Float : Type
157158Float = Double
159+%deprecate Float
158160
159161-- Pointers as external primitive; there's no literals for these, so no
160162-- need for them to be part of the compiler.
libs/prelude/IO.idr+2−2
@@ -162,7 +162,7 @@ namespace FFI_C
162162 ||| Supported C foreign types
163163 data C_Types : Type -> Type where
164164 C_Str : C_Types String
165− C_Float : C_Types Float
165+ C_Float : C_Types Double
166166 C_Ptr : C_Types Ptr
167167 C_MPtr : C_Types ManagedPtr
168168 C_Unit : C_Types ()
@@ -221,7 +221,7 @@ mutual
221221
222222 data JS_Types : Type -> Type where
223223 JS_Str : JS_Types String
224− JS_Float : JS_Types Float
224+ JS_Float : JS_Types Double
225225 JS_Ptr : JS_Types Ptr
226226 JS_Unit : JS_Types ()
227227 JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
libs/prelude/Prelude/Classes.idr+6−6
@@ -37,7 +37,7 @@ instance Eq Int where
3737instance Eq Integer where
3838 (==) = boolOp prim__eqBigInt
3939
40−instance Eq Float where
40+instance Eq Double where
4141 (==) = boolOp prim__eqFloat
4242
4343instance Eq Char where
@@ -118,7 +118,7 @@ instance Ord Integer where
118118 GT
119119
120120
121−instance Ord Float where
121+instance Ord Double where
122122 compare x y = if (x == y) then EQ else
123123 if (boolOp prim__sltFloat x y) then LT else
124124 GT
@@ -170,7 +170,7 @@ instance Num Int where
170170 fromInteger = prim__truncBigInt_Int
171171
172172
173−instance Num Float where
173+instance Num Double where
174174 (+) = prim__addFloat
175175 (*) = prim__mulFloat
176176
@@ -215,7 +215,7 @@ instance Neg Int where
215215 (-) = prim__subInt
216216 abs x = if x < (prim__truncBigInt_Int 0) then -x else x
217217
218−instance Neg Float where
218+instance Neg Double where
219219 negate x = prim__negFloat x
220220 (-) = prim__subFloat
221221 abs x = if x < (prim__toFloatBigInt 0) then -x else x
@@ -306,8 +306,8 @@ instance MaxBound Bits64 where
306306
307307-- ------------------------------------------------------------- [ Fractionals ]
308308
309−||| Fractional division of two Floats.
310−(/) : Float -> Float -> Float
309+||| Fractional division of two Doubles.
310+(/) : Double -> Double -> Double
311311(/) = prim__divFloat
312312
313313
test/ffi001/test022.idr+2−2
@@ -2,8 +2,8 @@ module Main
22
33%dynamic "dummy", "libm", "msvcrt"
44
5−x : Float
6−x = unsafePerformIO (foreign FFI_C "sin" (Float -> IO Float) 1.6)
5+x : Double
6+x = unsafePerformIO (foreign FFI_C "sin" (Double -> IO Double) 1.6)
77
88main : IO ()
99main = putStrLn (show x)
test/interactive010/expected+3−3
@@ -1,14 +1,14 @@
11Prelude.List.(++) : List a -> List a -> List a
22Prelude.Strings.(++) : String -> String -> String
3−Prelude.Classes./ : (__pi_arg : Float) →
4− (__pi_arg1 : Float) → Float
3+Prelude.Classes./ : (__pi_arg : Double) →
4+ (__pi_arg1 : Double) → Double
55Usage is :doc <functionname>
66Usage is :wc <functionname>
77Usage is :printdef <functionname>
88prim__divFloat
99Prelude.Classes./
1010
11− : Float -> Float -> Float
11+ : Double -> Double -> Double
1212(input):1:1: error: expected: ":",
1313 dependent type signature,
1414 end of input