git.iko.soy/Idris-dev
on master help sign in
Move / into Fractional interface
commit0c5f1de91fb4f223b2aec3163b936f5717b87bd0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 15 Jan 2016, 12:30 (11 years ago) parent07f6ff1
4 files changed+17−12
compare with master
unifiedsplit
CHANGELOG+1 libs/prelude/Prelude/Classes.idr+8−4 test/interactive010/expected+7−6 test/interactive010/input+1−2
CHANGELOG+1
@@ -4,6 +4,7 @@ New in 0.9.21:
44* 'class' and 'instance' are now deprecated keywords. They have been
55 replaced by 'interface' and 'implementation' respectively. This is to
66 properly reflect their purpose.
7+* (/) operator moved into new Fractional interface.
78* Idris' logging infrastructure has been categorised. Command line and repl
89 are available. For command line the option `--logging-categories CATS`
910 is used to pass in the categories. Here `CATS` is a colon separated quoted
libs/prelude/Prelude/Classes.idr+8−4
@@ -306,15 +306,19 @@ MaxBound Bits64 where
306306
307307-- ------------------------------------------------------------- [ Fractionals ]
308308
309−||| Fractional division of two Doubles.
310−(/) : Double -> Double -> Double
311−(/) = prim__divFloat
309+interface Num a => Fractional a where
310+ (/) : a -> a -> a
311+ recip : a -> a
312312
313+ recip x = 1 / x
314+
315+Fractional Double where
316+ (/) = prim__divFloat
313317
314318-- --------------------------------------------------------------- [ Integrals ]
315319%default partial
316320
317−interface Integral a where
321+interface Num a => Integral a where
318322 div : a -> a -> a
319323 mod : a -> a -> a
320324
test/interactive010/expected+7−6
@@ -1,14 +1,15 @@
11Prelude.List.(++) : List a -> List a -> List a
22Prelude.Strings.(++) : String -> String -> String
3−Prelude.Classes./ : (__pi_arg : Double) →
4− (__pi_arg1 : Double) → Double
3+Prelude.Classes./ Double
4+ Prelude.Classes.Double implementation of Prelude.Classes.Fractional : (__pi_arg : Double) →
5+ (__pi_arg3 : Double) →
6+ Double
57Usage is :doc <functionname>
68Usage is :wc <functionname>
79Usage is :printdef <functionname>
8−prim__divFloat
9−Prelude.Classes./
10+pat {a504} : Type u. pat {__class505} : Prelude.Classes.Fractional {a504}. Prelude.Classes./ {a504} {__class505}
1011
11− : Double -> Double -> Double
12+ : pty {a504} : Type u. pty {__class505} : Prelude.Classes.Fractional {a504}. {a504} -> {a504} -> {a504}
1213(input):1:1: error: expected: ":",
1314 dependent type signature,
1415 end of input
@@ -19,4 +20,4 @@ Prelude.Classes./
1920 end of input
2021++<EOF>
2122^
22−prim__divFloat
23+Can't resolve type class Fractional a
test/interactive010/input+1−2
@@ -1,9 +1,8 @@
11:type ++
2−:core /
2+:core (/) {a=Double}
33:doc +
44:wc +
55:printdef -
6−:spec /
76:patt /
87/
98++