git.iko.soy/Idris-dev
on master help sign in
Make "implementation" keyword optional
e81d6acEdwin Brady
libs/contrib/Control/Algebra/NumericInstances.idr+35−35
compare with master
unifiedsplit
@@ -8,106 +8,106 @@ import Data.Complex
8import Data.ZZ
8import Data.ZZ
9
9
10
10
11−implementation Semigroup Integer where
11+Semigroup Integer where
12 (<+>) = (+)
12 (<+>) = (+)
13
13
14−implementation Monoid Integer where
14+Monoid Integer where
15 neutral = 0
15 neutral = 0
16
16
17−implementation Group Integer where
17+Group Integer where
18 inverse = (* -1)
18 inverse = (* -1)
19
19
20−implementation AbelianGroup Integer
20+AbelianGroup Integer where
21
21
22−implementation Ring Integer where
22+Ring Integer where
23 (<.>) = (*)
23 (<.>) = (*)
24
24
25−implementation RingWithUnity Integer where
25+RingWithUnity Integer where
26 unity = 1
26 unity = 1
27
27
28
28
29−implementation Semigroup Int where
29+Semigroup Int where
30 (<+>) = (+)
30 (<+>) = (+)
31
31
32−implementation Monoid Int where
32+Monoid Int where
33 neutral = 0
33 neutral = 0
34
34
35−implementation Group Int where
35+Group Int where
36 inverse = (* -1)
36 inverse = (* -1)
37
37
38−implementation AbelianGroup Int
38+AbelianGroup Int where
39
39
40−implementation Ring Int where
40+Ring Int where
41 (<.>) = (*)
41 (<.>) = (*)
42
42
43−implementation RingWithUnity Int where
43+RingWithUnity Int where
44 unity = 1
44 unity = 1
45
45
46
46
47−implementation Semigroup Double where
47+Semigroup Double where
48 (<+>) = (+)
48 (<+>) = (+)
49
49
50−implementation Monoid Double where
50+Monoid Double where
51 neutral = 0
51 neutral = 0
52
52
53−implementation Group Double where
53+Group Double where
54 inverse = (* -1)
54 inverse = (* -1)
55
55
56−implementation AbelianGroup Double
56+AbelianGroup Double where
57
57
58−implementation Ring Double where
58+Ring Double where
59 (<.>) = (*)
59 (<.>) = (*)
60
60
61−implementation RingWithUnity Double where
61+RingWithUnity Double where
62 unity = 1
62 unity = 1
63
63
64−implementation Field Double where
64+Field Double where
65 inverseM f _ = 1 / f
65 inverseM f _ = 1 / f
66
66
67
67
68−implementation Semigroup Nat where
68+Semigroup Nat where
69 (<+>) = (+)
69 (<+>) = (+)
70
70
71−implementation Monoid Nat where
71+Monoid Nat where
72 neutral = 0
72 neutral = 0
73
73
74−implementation Semigroup ZZ where
74+Semigroup ZZ where
75 (<+>) = (+)
75 (<+>) = (+)
76
76
77−implementation Monoid ZZ where
77+Monoid ZZ where
78 neutral = 0
78 neutral = 0
79
79
80−implementation Group ZZ where
80+Group ZZ where
81 inverse = (* -1)
81 inverse = (* -1)
82
82
83−implementation AbelianGroup ZZ
83+AbelianGroup ZZ where
84
84
85−implementation Ring ZZ where
85+Ring ZZ where
86 (<.>) = (*)
86 (<.>) = (*)
87
87
88−implementation RingWithUnity ZZ where
88+RingWithUnity ZZ where
89 unity = 1
89 unity = 1
90
90
91
91
92−implementation Semigroup a => Semigroup (Complex a) where
92+Semigroup a => Semigroup (Complex a) where
93 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
93 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
94
94
95−implementation Monoid a => Monoid (Complex a) where
95+Monoid a => Monoid (Complex a) where
96 neutral = (neutral :+ neutral)
96 neutral = (neutral :+ neutral)
97
97
98−implementation Group a => Group (Complex a) where
98+Group a => Group (Complex a) where
99 inverse (r :+ i) = (inverse r :+ inverse i)
99 inverse (r :+ i) = (inverse r :+ inverse i)
100
100
101−implementation Ring a => AbelianGroup (Complex a) where {}
101+Ring a => AbelianGroup (Complex a) where {}
102
102
103−implementation Ring a => Ring (Complex a) where
103+Ring a => Ring (Complex a) where
104 (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
104 (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
105
105
106−implementation RingWithUnity a => RingWithUnity (Complex a) where
106+RingWithUnity a => RingWithUnity (Complex a) where
107 unity = (unity :+ neutral)
107 unity = (unity :+ neutral)
108
108
109−implementation RingWithUnity a => Module a (Complex a) where
109+RingWithUnity a => Module a (Complex a) where
110 (<#>) x = map (x <.>)
110 (<#>) x = map (x <.>)
111
111
112−implementation RingWithUnity a => InnerProductSpace a (Complex a) where
112+RingWithUnity a => InnerProductSpace a (Complex a) where
113 (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z
113 (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z
libs/prelude/Prelude.idr+19−19
@@ -48,78 +48,78 @@ decAsBool (No _) = False
48
48
49---- Functor implementations
49---- Functor implementations
50
50
51−implementation Functor PrimIO where
51+Functor PrimIO where
52 map f io = prim_io_bind io (prim_io_return . f)
52 map f io = prim_io_bind io (prim_io_return . f)
53
53
54−implementation Functor Maybe where
54+Functor Maybe where
55 map f (Just x) = Just (f x)
55 map f (Just x) = Just (f x)
56 map f Nothing = Nothing
56 map f Nothing = Nothing
57
57
58−implementation Functor (Either e) where
58+Functor (Either e) where
59 map f (Left l) = Left l
59 map f (Left l) = Left l
60 map f (Right r) = Right (f r)
60 map f (Right r) = Right (f r)
61
61
62---- Applicative implementations
62---- Applicative implementations
63
63
64−implementation Applicative PrimIO where
64+Applicative PrimIO where
65 pure = prim_io_return
65 pure = prim_io_return
66
66
67 am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
67 am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
68
68
69−implementation Applicative Maybe where
69+Applicative Maybe where
70 pure = Just
70 pure = Just
71
71
72 (Just f) <*> (Just a) = Just (f a)
72 (Just f) <*> (Just a) = Just (f a)
73 _ <*> _ = Nothing
73 _ <*> _ = Nothing
74
74
75−implementation Applicative (Either e) where
75+Applicative (Either e) where
76 pure = Right
76 pure = Right
77
77
78 (Left a) <*> _ = Left a
78 (Left a) <*> _ = Left a
79 (Right f) <*> (Right r) = Right (f r)
79 (Right f) <*> (Right r) = Right (f r)
80 (Right _) <*> (Left l) = Left l
80 (Right _) <*> (Left l) = Left l
81
81
82−implementation Applicative List where
82+Applicative List where
83 pure x = [x]
83 pure x = [x]
84
84
85 fs <*> vs = concatMap (\f => map f vs) fs
85 fs <*> vs = concatMap (\f => map f vs) fs
86
86
87---- Alternative implementations
87---- Alternative implementations
88
88
89−implementation Alternative Maybe where
89+Alternative Maybe where
90 empty = Nothing
90 empty = Nothing
91
91
92 (Just x) <|> _ = Just x
92 (Just x) <|> _ = Just x
93 Nothing <|> v = v
93 Nothing <|> v = v
94
94
95−implementation Alternative List where
95+Alternative List where
96 empty = []
96 empty = []
97
97
98 (<|>) = (++)
98 (<|>) = (++)
99
99
100---- Monad implementations
100---- Monad implementations
101
101
102−implementation Monad PrimIO where
102+Monad PrimIO where
103 b >>= k = prim_io_bind b k
103 b >>= k = prim_io_bind b k
104
104
105−implementation Monad Maybe where
105+Monad Maybe where
106 Nothing >>= k = Nothing
106 Nothing >>= k = Nothing
107 (Just x) >>= k = k x
107 (Just x) >>= k = k x
108
108
109−implementation Monad (Either e) where
109+Monad (Either e) where
110 (Left n) >>= _ = Left n
110 (Left n) >>= _ = Left n
111 (Right r) >>= f = f r
111 (Right r) >>= f = f r
112
112
113−implementation Monad List where
113+Monad List where
114 m >>= f = concatMap f m
114 m >>= f = concatMap f m
115
115
116---- Traversable implementations
116---- Traversable implementations
117
117
118−implementation Traversable Maybe where
118+Traversable Maybe where
119 traverse f Nothing = pure Nothing
119 traverse f Nothing = pure Nothing
120 traverse f (Just x) = [| Just (f x) |]
120 traverse f (Just x) = [| Just (f x) |]
121
121
122−implementation Traversable List where
122+Traversable List where
123 traverse f [] = pure List.Nil
123 traverse f [] = pure List.Nil
124 traverse f (x::xs) = [| List.(::) (f x) (traverse f xs) |]
124 traverse f (x::xs) = [| List.(::) (f x) (traverse f xs) |]
125
125
@@ -160,7 +160,7 @@ interface Enum a where
160 total enumFromThenTo : a -> a -> a -> List a
160 total enumFromThenTo : a -> a -> a -> List a
161 enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))
161 enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))
162
162
163−implementation Enum Nat where
163+Enum Nat where
164 pred n = Nat.pred n
164 pred n = Nat.pred n
165 succ n = S n
165 succ n = S n
166 toNat x = id x
166 toNat x = id x
@@ -169,7 +169,7 @@ implementation Enum Nat where
169 enumFromThenTo x y z = natEnumFromThenTo x y z
169 enumFromThenTo x y z = natEnumFromThenTo x y z
170 enumFromTo x y = natEnumFromTo x y
170 enumFromTo x y = natEnumFromTo x y
171
171
172−implementation Enum Integer where
172+Enum Integer where
173 pred n = n - 1
173 pred n = n - 1
174 succ n = n + 1
174 succ n = n + 1
175 toNat n = cast n
175 toNat n = cast n
@@ -187,7 +187,7 @@ implementation Enum Integer where
187 go [] = []
187 go [] = []
188 go (x :: xs) = n + (cast x * inc) :: go xs
188 go (x :: xs) = n + (cast x * inc) :: go xs
189
189
190−implementation Enum Int where
190+Enum Int where
191 pred n = n - 1
191 pred n = n - 1
192 succ n = n + 1
192 succ n = n + 1
193 toNat n = cast n
193 toNat n = cast n
@@ -207,7 +207,7 @@ implementation Enum Int where
207 go [] = []
207 go [] = []
208 go (x :: xs) = n + (cast x * inc) :: go xs
208 go (x :: xs) = n + (cast x * inc) :: go xs
209
209
210−implementation Enum Char where
210+Enum Char where
211 toNat c = toNat (ord c)
211 toNat c = toNat (ord c)
212 fromNat n = chr (fromNat n)
212 fromNat n = chr (fromNat n)
213
213
libs/prelude/Prelude/Cast.idr+12−12
@@ -12,46 +12,46 @@ interface Cast from to where
12
12
13-- String casts
13-- String casts
14
14
15−implementation Cast String Int where
15+Cast String Int where
16 cast = prim__fromStrInt
16 cast = prim__fromStrInt
17
17
18−implementation Cast String Double where
18+Cast String Double where
19 cast = prim__strToFloat
19 cast = prim__strToFloat
20
20
21−implementation Cast String Integer where
21+Cast String Integer where
22 cast = prim__fromStrBigInt
22 cast = prim__fromStrBigInt
23
23
24-- Int casts
24-- Int casts
25
25
26−implementation Cast Int String where
26+Cast Int String where
27 cast = prim__toStrInt
27 cast = prim__toStrInt
28
28
29−implementation Cast Int Double where
29+Cast Int Double where
30 cast = prim__toFloatInt
30 cast = prim__toFloatInt
31
31
32−implementation Cast Int Integer where
32+Cast Int Integer where
33 cast = prim__sextInt_BigInt
33 cast = prim__sextInt_BigInt
34
34
35-- Double casts
35-- Double casts
36
36
37−implementation Cast Double String where
37+Cast Double String where
38 cast = prim__floatToStr
38 cast = prim__floatToStr
39
39
40−implementation Cast Double Int where
40+Cast Double Int where
41 cast = prim__fromFloatInt
41 cast = prim__fromFloatInt
42
42
43−implementation Cast Double Integer where
43+Cast Double Integer where
44 cast = prim__fromFloatBigInt
44 cast = prim__fromFloatBigInt
45
45
46-- Integer casts
46-- Integer casts
47
47
48−implementation Cast Integer String where
48+Cast Integer String where
49 cast = prim__toStrBigInt
49 cast = prim__toStrBigInt
50
50
51−implementation Cast Integer Double where
51+Cast Integer Double where
52 cast = prim__toFloatBigInt
52 cast = prim__toFloatBigInt
53
53
54-- Char casts
54-- Char casts
55
55
56−implementation Cast Char Int where
56+Cast Char Int where
57 cast = prim__charToInt
57 cast = prim__charToInt
libs/prelude/Prelude/Chars.idr+1−1
@@ -13,7 +13,7 @@ chr x = if (x >= 0 && x < 0x110000)
13 then assert_total (prim__intToChar x)
13 then assert_total (prim__intToChar x)
14 else '\0'
14 else '\0'
15
15
16−implementation Cast Int Char where
16+Cast Int Char where
17 cast = chr
17 cast = chr
18
18
19||| Return the ASCII representation of the character.
19||| Return the ASCII representation of the character.
libs/prelude/Prelude/Classes.idr+52−52
@@ -28,44 +28,44 @@ interface Eq a where
28 x /= y = not (x == y)
28 x /= y = not (x == y)
29 x == y = not (x /= y)
29 x == y = not (x /= y)
30
30
31−implementation Eq () where
31+Eq () where
32 () == () = True
32 () == () = True
33
33
34−implementation Eq Int where
34+Eq Int where
35 (==) = boolOp prim__eqInt
35 (==) = boolOp prim__eqInt
36
36
37−implementation Eq Integer where
37+Eq Integer where
38 (==) = boolOp prim__eqBigInt
38 (==) = boolOp prim__eqBigInt
39
39
40−implementation Eq Double where
40+Eq Double where
41 (==) = boolOp prim__eqFloat
41 (==) = boolOp prim__eqFloat
42
42
43−implementation Eq Char where
43+Eq Char where
44 (==) = boolOp prim__eqChar
44 (==) = boolOp prim__eqChar
45
45
46−implementation Eq String where
46+Eq String where
47 (==) = boolOp prim__eqString
47 (==) = boolOp prim__eqString
48
48
49−implementation Eq Ptr where
49+Eq Ptr where
50 (==) = boolOp prim__eqPtr
50 (==) = boolOp prim__eqPtr
51
51
52−implementation Eq ManagedPtr where
52+Eq ManagedPtr where
53 (==) = boolOp prim__eqManagedPtr
53 (==) = boolOp prim__eqManagedPtr
54
54
55−implementation Eq Bool where
55+Eq Bool where
56 True == True = True
56 True == True = True
57 True == False = False
57 True == False = False
58 False == True = False
58 False == True = False
59 False == False = True
59 False == False = True
60
60
61−implementation (Eq a, Eq b) => Eq (a, b) where
61+(Eq a, Eq b) => Eq (a, b) where
62 (==) (a, c) (b, d) = (a == b) && (c == d)
62 (==) (a, c) (b, d) = (a == b) && (c == d)
63
63
64
64
65-- ---------------------------------------------------------- [ Ordering Interface ]
65-- ---------------------------------------------------------- [ Ordering Interface ]
66%elim data Ordering = LT | EQ | GT
66%elim data Ordering = LT | EQ | GT
67
67
68−implementation Eq Ordering where
68+Eq Ordering where
69 LT == LT = True
69 LT == LT = True
70 EQ == EQ = True
70 EQ == EQ = True
71 GT == GT = True
71 GT == GT = True
@@ -103,47 +103,47 @@ interface Eq a => Ord a where
103 min : a -> a -> a
103 min : a -> a -> a
104 min x y = if (x < y) then x else y
104 min x y = if (x < y) then x else y
105
105
106−implementation Ord () where
106+Ord () where
107 compare () () = EQ
107 compare () () = EQ
108
108
109−implementation Ord Int where
109+Ord Int where
110 compare x y = if (x == y) then EQ else
110 compare x y = if (x == y) then EQ else
111 if (boolOp prim__sltInt x y) then LT else
111 if (boolOp prim__sltInt x y) then LT else
112 GT
112 GT
113
113
114
114
115−implementation Ord Integer where
115+Ord Integer where
116 compare x y = if (x == y) then EQ else
116 compare x y = if (x == y) then EQ else
117 if (boolOp prim__sltBigInt x y) then LT else
117 if (boolOp prim__sltBigInt x y) then LT else
118 GT
118 GT
119
119
120
120
121−implementation Ord Double where
121+Ord Double where
122 compare x y = if (x == y) then EQ else
122 compare x y = if (x == y) then EQ else
123 if (boolOp prim__sltFloat x y) then LT else
123 if (boolOp prim__sltFloat x y) then LT else
124 GT
124 GT
125
125
126
126
127−implementation Ord Char where
127+Ord Char where
128 compare x y = if (x == y) then EQ else
128 compare x y = if (x == y) then EQ else
129 if (boolOp prim__sltChar x y) then LT else
129 if (boolOp prim__sltChar x y) then LT else
130 GT
130 GT
131
131
132
132
133−implementation Ord String where
133+Ord String where
134 compare x y = if (x == y) then EQ else
134 compare x y = if (x == y) then EQ else
135 if (boolOp prim__ltString x y) then LT else
135 if (boolOp prim__ltString x y) then LT else
136 GT
136 GT
137
137
138
138
139−implementation Ord Bool where
139+Ord Bool where
140 compare True True = EQ
140 compare True True = EQ
141 compare False False = EQ
141 compare False False = EQ
142 compare False True = LT
142 compare False True = LT
143 compare True False = GT
143 compare True False = GT
144
144
145
145
146−implementation (Ord a, Ord b) => Ord (a, b) where
146+(Ord a, Ord b) => Ord (a, b) where
147 compare (xl, xr) (yl, yr) =
147 compare (xl, xr) (yl, yr) =
148 if xl /= yl
148 if xl /= yl
149 then compare xl yl
149 then compare xl yl
@@ -157,41 +157,41 @@ interface Num a where
157 ||| Conversion from Integer.
157 ||| Conversion from Integer.
158 fromInteger : Integer -> a
158 fromInteger : Integer -> a
159
159
160−implementation Num Integer where
160+Num Integer where
161 (+) = prim__addBigInt
161 (+) = prim__addBigInt
162 (*) = prim__mulBigInt
162 (*) = prim__mulBigInt
163
163
164 fromInteger = id
164 fromInteger = id
165
165
166−implementation Num Int where
166+Num Int where
167 (+) = prim__addInt
167 (+) = prim__addInt
168 (*) = prim__mulInt
168 (*) = prim__mulInt
169
169
170 fromInteger = prim__truncBigInt_Int
170 fromInteger = prim__truncBigInt_Int
171
171
172
172
173−implementation Num Double where
173+Num Double where
174 (+) = prim__addFloat
174 (+) = prim__addFloat
175 (*) = prim__mulFloat
175 (*) = prim__mulFloat
176
176
177 fromInteger = prim__toFloatBigInt
177 fromInteger = prim__toFloatBigInt
178
178
179−implementation Num Bits8 where
179+Num Bits8 where
180 (+) = prim__addB8
180 (+) = prim__addB8
181 (*) = prim__mulB8
181 (*) = prim__mulB8
182 fromInteger = prim__truncBigInt_B8
182 fromInteger = prim__truncBigInt_B8
183
183
184−implementation Num Bits16 where
184+Num Bits16 where
185 (+) = prim__addB16
185 (+) = prim__addB16
186 (*) = prim__mulB16
186 (*) = prim__mulB16
187 fromInteger = prim__truncBigInt_B16
187 fromInteger = prim__truncBigInt_B16
188
188
189−implementation Num Bits32 where
189+Num Bits32 where
190 (+) = prim__addB32
190 (+) = prim__addB32
191 (*) = prim__mulB32
191 (*) = prim__mulB32
192 fromInteger = prim__truncBigInt_B32
192 fromInteger = prim__truncBigInt_B32
193
193
194−implementation Num Bits64 where
194+Num Bits64 where
195 (+) = prim__addB64
195 (+) = prim__addB64
196 (*) = prim__mulB64
196 (*) = prim__mulB64
197 fromInteger = prim__truncBigInt_B64
197 fromInteger = prim__truncBigInt_B64
@@ -199,41 +199,41 @@ implementation Num Bits64 where
199-- --------------------------------------------------------- [ Negatable Interface ]
199-- --------------------------------------------------------- [ Negatable Interface ]
200||| The `Neg` interface defines operations on numbers which can be negative.
200||| The `Neg` interface defines operations on numbers which can be negative.
201interface Num a => Neg a where
201interface Num a => Neg a where
202− ||| The underlying implementation of unary minus. `-5` desugars to `negate (fromInteger 5)`.
202+ ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
203 negate : a -> a
203 negate : a -> a
204 (-) : a -> a -> a
204 (-) : a -> a -> a
205 ||| Absolute value
205 ||| Absolute value
206 abs : a -> a
206 abs : a -> a
207
207
208−implementation Neg Integer where
208+Neg Integer where
209 negate x = prim__subBigInt 0 x
209 negate x = prim__subBigInt 0 x
210 (-) = prim__subBigInt
210 (-) = prim__subBigInt
211 abs x = if x < 0 then -x else x
211 abs x = if x < 0 then -x else x
212
212
213−implementation Neg Int where
213+Neg Int where
214 negate x = prim__subInt 0 x
214 negate x = prim__subInt 0 x
215 (-) = prim__subInt
215 (-) = prim__subInt
216 abs x = if x < (prim__truncBigInt_Int 0) then -x else x
216 abs x = if x < (prim__truncBigInt_Int 0) then -x else x
217
217
218−implementation Neg Double where
218+Neg Double where
219 negate x = prim__negFloat x
219 negate x = prim__negFloat x
220 (-) = prim__subFloat
220 (-) = prim__subFloat
221 abs x = if x < (prim__toFloatBigInt 0) then -x else x
221 abs x = if x < (prim__toFloatBigInt 0) then -x else x
222
222
223-- ------------------------------------------------------------
223-- ------------------------------------------------------------
224−implementation Eq Bits8 where
224+Eq Bits8 where
225 x == y = intToBool (prim__eqB8 x y)
225 x == y = intToBool (prim__eqB8 x y)
226
226
227−implementation Eq Bits16 where
227+Eq Bits16 where
228 x == y = intToBool (prim__eqB16 x y)
228 x == y = intToBool (prim__eqB16 x y)
229
229
230−implementation Eq Bits32 where
230+Eq Bits32 where
231 x == y = intToBool (prim__eqB32 x y)
231 x == y = intToBool (prim__eqB32 x y)
232
232
233−implementation Eq Bits64 where
233+Eq Bits64 where
234 x == y = intToBool (prim__eqB64 x y)
234 x == y = intToBool (prim__eqB64 x y)
235
235
236−implementation Ord Bits8 where
236+Ord Bits8 where
237 (<) = boolOp prim__ltB8
237 (<) = boolOp prim__ltB8
238 (>) = boolOp prim__gtB8
238 (>) = boolOp prim__gtB8
239 (<=) = boolOp prim__lteB8
239 (<=) = boolOp prim__lteB8
@@ -242,7 +242,7 @@ implementation Ord Bits8 where
242 else if l > r then GT
242 else if l > r then GT
243 else EQ
243 else EQ
244
244
245−implementation Ord Bits16 where
245+Ord Bits16 where
246 (<) = boolOp prim__ltB16
246 (<) = boolOp prim__ltB16
247 (>) = boolOp prim__gtB16
247 (>) = boolOp prim__gtB16
248 (<=) = boolOp prim__lteB16
248 (<=) = boolOp prim__lteB16
@@ -251,7 +251,7 @@ implementation Ord Bits16 where
251 else if l > r then GT
251 else if l > r then GT
252 else EQ
252 else EQ
253
253
254−implementation Ord Bits32 where
254+Ord Bits32 where
255 (<) = boolOp prim__ltB32
255 (<) = boolOp prim__ltB32
256 (>) = boolOp prim__gtB32
256 (>) = boolOp prim__gtB32
257 (<=) = boolOp prim__lteB32
257 (<=) = boolOp prim__lteB32
@@ -260,7 +260,7 @@ implementation Ord Bits32 where
260 else if l > r then GT
260 else if l > r then GT
261 else EQ
261 else EQ
262
262
263−implementation Ord Bits64 where
263+Ord Bits64 where
264 (<) = boolOp prim__ltB64
264 (<) = boolOp prim__ltB64
265 (>) = boolOp prim__gtB64
265 (>) = boolOp prim__gtB64
266 (<=) = boolOp prim__lteB64
266 (<=) = boolOp prim__lteB64
@@ -279,28 +279,28 @@ interface Ord b => MaxBound b where
279 ||| The upper bound for the type
279 ||| The upper bound for the type
280 maxBound : b
280 maxBound : b
281
281
282−implementation MinBound Bits8 where
282+MinBound Bits8 where
283 minBound = 0x0
283 minBound = 0x0
284
284
285−implementation MaxBound Bits8 where
285+MaxBound Bits8 where
286 maxBound = 0xff
286 maxBound = 0xff
287
287
288−implementation MinBound Bits16 where
288+MinBound Bits16 where
289 minBound = 0x0
289 minBound = 0x0
290
290
291−implementation MaxBound Bits16 where
291+MaxBound Bits16 where
292 maxBound = 0xffff
292 maxBound = 0xffff
293
293
294−implementation MinBound Bits32 where
294+MinBound Bits32 where
295 minBound = 0x0
295 minBound = 0x0
296
296
297−implementation MaxBound Bits32 where
297+MaxBound Bits32 where
298 maxBound = 0xffffffff
298 maxBound = 0xffffffff
299
299
300−implementation MinBound Bits64 where
300+MinBound Bits64 where
301 minBound = 0x0
301 minBound = 0x0
302
302
303−implementation MaxBound Bits64 where
303+MaxBound Bits64 where
304 maxBound = 0xffffffffffffffff
304 maxBound = 0xffffffffffffffff
305
305
306
306
@@ -327,7 +327,7 @@ modBigInt : Integer -> Integer -> Integer
327modBigInt x y = case y == 0 of
327modBigInt x y = case y == 0 of
328 False => prim__sremBigInt x y
328 False => prim__sremBigInt x y
329
329
330−implementation Integral Integer where
330+Integral Integer where
331 div = divBigInt
331 div = divBigInt
332 mod = modBigInt
332 mod = modBigInt
333
333
@@ -341,7 +341,7 @@ modInt : Int -> Int -> Int
341modInt x y = case y == 0 of
341modInt x y = case y == 0 of
342 False => prim__sremInt x y
342 False => prim__sremInt x y
343
343
344−implementation Integral Int where
344+Integral Int where
345 div = divInt
345 div = divInt
346 mod = modInt
346 mod = modInt
347
347
@@ -354,7 +354,7 @@ modB8 : Bits8 -> Bits8 -> Bits8
354modB8 x y = case y == 0 of
354modB8 x y = case y == 0 of
355 False => prim__sremB8 x y
355 False => prim__sremB8 x y
356
356
357−implementation Integral Bits8 where
357+Integral Bits8 where
358 div = divB8
358 div = divB8
359 mod = modB8
359 mod = modB8
360
360
@@ -367,7 +367,7 @@ modB16 : Bits16 -> Bits16 -> Bits16
367modB16 x y = case y == 0 of
367modB16 x y = case y == 0 of
368 False => prim__sremB16 x y
368 False => prim__sremB16 x y
369
369
370−implementation Integral Bits16 where
370+Integral Bits16 where
371 div = divB16
371 div = divB16
372 mod = modB16
372 mod = modB16
373
373
@@ -380,7 +380,7 @@ modB32 : Bits32 -> Bits32 -> Bits32
380modB32 x y = case y == 0 of
380modB32 x y = case y == 0 of
381 False => prim__sremB32 x y
381 False => prim__sremB32 x y
382
382
383−implementation Integral Bits32 where
383+Integral Bits32 where
384 div = divB32
384 div = divB32
385 mod = modB32
385 mod = modB32
386
386
@@ -393,7 +393,7 @@ modB64 : Bits64 -> Bits64 -> Bits64
393modB64 x y = case y == 0 of
393modB64 x y = case y == 0 of
394 False => prim__sremB64 x y
394 False => prim__sremB64 x y
395
395
396−implementation Integral Bits64 where
396+Integral Bits64 where
397 div = divB64
397 div = divB64
398 mod = modB64
398 mod = modB64
399
399
libs/prelude/Prelude/Either.idr+1−1
@@ -90,7 +90,7 @@ maybeToEither def Nothing = Left def
90-- Instances
90-- Instances
91--------------------------------------------------------------------------------
91--------------------------------------------------------------------------------
92
92
93−implementation (Eq a, Eq b) => Eq (Either a b) where
93+(Eq a, Eq b) => Eq (Either a b) where
94 (==) (Left x) (Left y) = x == y
94 (==) (Left x) (Left y) = x == y
95 (==) (Right x) (Right y) = x == y
95 (==) (Right x) (Right y) = x == y
96 (==) _ _ = False
96 (==) _ _ = False
libs/prelude/Prelude/File.idr+1−1
@@ -43,7 +43,7 @@ getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"
43 (Ptr -> IO (Raw FileError)) prim__vm
43 (Ptr -> IO (Raw FileError)) prim__vm
44 return err
44 return err
45
45
46−implementation Show FileError where
46+Show FileError where
47 show FileNotFound = "File Not Found"
47 show FileNotFound = "File Not Found"
48 show PermissionDenied = "Permission Denied"
48 show PermissionDenied = "Permission Denied"
49 show (GenericFileError errno) = strError errno
49 show (GenericFileError errno) = strError errno
libs/prelude/Prelude/List.idr+8−8
@@ -56,7 +56,7 @@ data NonEmpty : (xs : List a) -> Type where
56 ||| The proof that a cons cell is non-empty
56 ||| The proof that a cons cell is non-empty
57 IsNonEmpty : NonEmpty (x :: xs)
57 IsNonEmpty : NonEmpty (x :: xs)
58
58
59−implementation Uninhabited (NonEmpty []) where
59+Uninhabited (NonEmpty []) where
60 uninhabited IsNonEmpty impossible
60 uninhabited IsNonEmpty impossible
61
61
62||| Decide whether a list is non-empty
62||| Decide whether a list is non-empty
@@ -74,7 +74,7 @@ data InBounds : (k : Nat) -> (xs : List a) -> Type where
74 ||| Valid indices can be extended
74 ||| Valid indices can be extended
75 InLater : InBounds k xs -> InBounds (S k) (x :: xs)
75 InLater : InBounds k xs -> InBounds (S k) (x :: xs)
76
76
77−implementation Uninhabited (InBounds k []) where
77+Uninhabited (InBounds k []) where
78 uninhabited InFirst impossible
78 uninhabited InFirst impossible
79
79
80||| Decide whether `k` is a valid index into `xs`
80||| Decide whether `k` is a valid index into `xs`
@@ -252,7 +252,7 @@ replicate (S n) x = x :: replicate n x
252-- Instances
252-- Instances
253--------------------------------------------------------------------------------
253--------------------------------------------------------------------------------
254
254
255−implementation (Eq a) => Eq (List a) where
255+(Eq a) => Eq (List a) where
256 (==) [] [] = True
256 (==) [] [] = True
257 (==) (x::xs) (y::ys) =
257 (==) (x::xs) (y::ys) =
258 if x == y then
258 if x == y then
@@ -262,7 +262,7 @@ implementation (Eq a) => Eq (List a) where
262 (==) _ _ = False
262 (==) _ _ = False
263
263
264
264
265−implementation Ord a => Ord (List a) where
265+Ord a => Ord (List a) where
266 compare [] [] = EQ
266 compare [] [] = EQ
267 compare [] _ = LT
267 compare [] _ = LT
268 compare _ [] = GT
268 compare _ [] = GT
@@ -272,13 +272,13 @@ implementation Ord a => Ord (List a) where
272 else
272 else
273 compare xs ys
273 compare xs ys
274
274
275−implementation Semigroup (List a) where
275+Semigroup (List a) where
276 (<+>) = (++)
276 (<+>) = (++)
277
277
278−implementation Monoid (List a) where
278+Monoid (List a) where
279 neutral = []
279 neutral = []
280
280
281−implementation Functor List where
281+Functor List where
282 map f [] = []
282 map f [] = []
283 map f (x::xs) = f x :: map f xs
283 map f (x::xs) = f x :: map f xs
284
284
@@ -349,7 +349,7 @@ mapMaybe f (x::xs) =
349-- Folds
349-- Folds
350--------------------------------------------------------------------------------
350--------------------------------------------------------------------------------
351
351
352−implementation Foldable List where
352+Foldable List where
353 foldr c n [] = n
353 foldr c n [] = n
354 foldr c n (x::xs) = c x (foldr c n xs)
354 foldr c n (x::xs) = c x (foldr c n xs)
355
355
libs/prelude/Prelude/Maybe.idr+7−7
@@ -79,7 +79,7 @@ maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b
79maybe_bind Nothing k = Nothing
79maybe_bind Nothing k = Nothing
80maybe_bind (Just x) k = k x
80maybe_bind (Just x) k = k x
81
81
82−implementation (Eq a) => Eq (Maybe a) where
82+(Eq a) => Eq (Maybe a) where
83 Nothing == Nothing = True
83 Nothing == Nothing = True
84 Nothing == (Just _) = False
84 Nothing == (Just _) = False
85 (Just _) == Nothing = False
85 (Just _) == Nothing = False
@@ -90,7 +90,7 @@ implementation (Eq a) => Eq (Maybe a) where
90|||
90|||
91||| **NB**: This is a different choice than in the Haskell libraries.
91||| **NB**: This is a different choice than in the Haskell libraries.
92||| Use `collectJust` to get the Haskell behaviour.
92||| Use `collectJust` to get the Haskell behaviour.
93−implementation Semigroup (Maybe a) where
93+Semigroup (Maybe a) where
94 Nothing <+> m = m
94 Nothing <+> m = m
95 (Just x) <+> _ = Just x
95 (Just x) <+> _ = Just x
96
96
@@ -98,20 +98,20 @@ implementation Semigroup (Maybe a) where
98||| designated neutral element and collecting the contents of the
98||| designated neutral element and collecting the contents of the
99||| `Just` constructors using a semigroup structure on `a`. This is
99||| `Just` constructors using a semigroup structure on `a`. This is
100||| the behaviour in the Haskell libraries.
100||| the behaviour in the Haskell libraries.
101−implementation [collectJust] Semigroup a => Semigroup (Maybe a) where
101+[collectJust] Semigroup a => Semigroup (Maybe a) where
102 Nothing <+> m = m
102 Nothing <+> m = m
103 m <+> Nothing = m
103 m <+> Nothing = m
104 (Just m1) <+> (Just m2) = Just (m1 <+> m2)
104 (Just m1) <+> (Just m2) = Just (m1 <+> m2)
105
105
106−implementation Monoid (Maybe a) where
106+ Monoid (Maybe a) where
107 neutral = Nothing
107 neutral = Nothing
108
108
109−implementation (Monoid a, Eq a) => Cast a (Maybe a) where
109+(Monoid a, Eq a) => Cast a (Maybe a) where
110 cast = raiseToMaybe
110 cast = raiseToMaybe
111
111
112−implementation (Monoid a) => Cast (Maybe a) a where
112+(Monoid a) => Cast (Maybe a) a where
113 cast = lowerMaybe
113 cast = lowerMaybe
114
114
115−implementation Foldable Maybe where
115+Foldable Maybe where
116 foldr _ z Nothing = z
116 foldr _ z Nothing = z
117 foldr f z (Just x) = f x z
117 foldr f z (Just x) = f x z
libs/prelude/Prelude/Monad.idr+3−3
@@ -27,16 +27,16 @@ return = pure
27-- Annoyingly, these need to be here, so that we can use them in other
27-- Annoyingly, these need to be here, so that we can use them in other
28-- Prelude modules other than the top level.
28-- Prelude modules other than the top level.
29
29
30−implementation Functor (IO' ffi) where
30+Functor (IO' ffi) where
31 map f io = io_bind io (\b => io_return (f b))
31 map f io = io_bind io (\b => io_return (f b))
32
32
33−implementation Applicative (IO' ffi) where
33+Applicative (IO' ffi) where
34 pure x = io_return x
34 pure x = io_return x
35 f <*> a = io_bind f (\f' =>
35 f <*> a = io_bind f (\f' =>
36 io_bind a (\a' =>
36 io_bind a (\a' =>
37 io_return (f' a')))
37 io_return (f' a')))
38
38
39
39
40−implementation Monad (IO' ffi) where
40+Monad (IO' ffi) where
41 b >>= k = io_bind b k
41 b >>= k = io_bind b k
42
42
libs/prelude/Prelude/Nat.idr+17−17
@@ -23,7 +23,7 @@ import Prelude.Uninhabited
23-- name hints for interactive editing
23-- name hints for interactive editing
24%name Nat k,j,i,n,m
24%name Nat k,j,i,n,m
25
25
26−implementation Uninhabited (Z = S n) where
26+Uninhabited (Z = S n) where
27 uninhabited Refl impossible
27 uninhabited Refl impossible
28
28
29--------------------------------------------------------------------------------
29--------------------------------------------------------------------------------
@@ -100,7 +100,7 @@ data LTE : (n, m : Nat) -> Type where
100 ||| If n <= m, then n + 1 <= m + 1
100 ||| If n <= m, then n + 1 <= m + 1
101 LTESucc : LTE left right -> LTE (S left) (S right)
101 LTESucc : LTE left right -> LTE (S left) (S right)
102
102
103−implementation Uninhabited (LTE (S n) Z) where
103+Uninhabited (LTE (S n) Z) where
104 uninhabited LTEZero impossible
104 uninhabited LTEZero impossible
105
105
106||| Greater than or equal to
106||| Greater than or equal to
@@ -187,34 +187,34 @@ toIntNat n = toIntNat' n 0 where
187-- Type class implementations
187-- Type class implementations
188--------------------------------------------------------------------------------
188--------------------------------------------------------------------------------
189
189
190−implementation Eq Nat where
190+Eq Nat where
191 Z == Z = True
191 Z == Z = True
192 (S l) == (S r) = l == r
192 (S l) == (S r) = l == r
193 _ == _ = False
193 _ == _ = False
194
194
195−implementation Cast Nat Integer where
195+Cast Nat Integer where
196 cast = toIntegerNat
196 cast = toIntegerNat
197
197
198−implementation Ord Nat where
198+Ord Nat where
199 compare Z Z = EQ
199 compare Z Z = EQ
200 compare Z (S k) = LT
200 compare Z (S k) = LT
201 compare (S k) Z = GT
201 compare (S k) Z = GT
202 compare (S x) (S y) = compare x y
202 compare (S x) (S y) = compare x y
203
203
204−implementation Num Nat where
204+Num Nat where
205 (+) = plus
205 (+) = plus
206 (*) = mult
206 (*) = mult
207
207
208 fromInteger = fromIntegerNat
208 fromInteger = fromIntegerNat
209
209
210−implementation MinBound Nat where
210+MinBound Nat where
211 minBound = Z
211 minBound = Z
212
212
213||| Casts negative `Integers` to 0.
213||| Casts negative `Integers` to 0.
214−implementation Cast Integer Nat where
214+Cast Integer Nat where
215 cast = fromInteger
215 cast = fromInteger
216
216
217−implementation Cast String Nat where
217+Cast String Nat where
218 cast str = cast (the Integer (cast str))
218 cast str = cast (the Integer (cast str))
219
219
220||| A wrapper for Nat that specifies the semigroup and monad implementations that use (*)
220||| A wrapper for Nat that specifies the semigroup and monad implementations that use (*)
@@ -227,7 +227,7 @@ record Additive where
227 constructor GetAdditive
227 constructor GetAdditive
228 _ : Nat
228 _ : Nat
229
229
230−implementation Semigroup Multiplicative where
230+Semigroup Multiplicative where
231 (<+>) left right = GetMultiplicative $ left' * right'
231 (<+>) left right = GetMultiplicative $ left' * right'
232 where
232 where
233 left' : Nat
233 left' : Nat
@@ -240,7 +240,7 @@ implementation Semigroup Multiplicative where
240 case right of
240 case right of
241 GetMultiplicative m => m
241 GetMultiplicative m => m
242
242
243−implementation Semigroup Additive where
243+Semigroup Additive where
244 left <+> right = GetAdditive $ left' + right'
244 left <+> right = GetAdditive $ left' + right'
245 where
245 where
246 left' : Nat
246 left' : Nat
@@ -253,20 +253,20 @@ implementation Semigroup Additive where
253 case right of
253 case right of
254 GetAdditive m => m
254 GetAdditive m => m
255
255
256−implementation Monoid Multiplicative where
256+Monoid Multiplicative where
257 neutral = GetMultiplicative $ S Z
257 neutral = GetMultiplicative $ S Z
258
258
259−implementation Monoid Additive where
259+Monoid Additive where
260 neutral = GetAdditive Z
260 neutral = GetAdditive Z
261
261
262||| Casts negative `Ints` to 0.
262||| Casts negative `Ints` to 0.
263−implementation Cast Int Nat where
263+Cast Int Nat where
264 cast i = fromInteger (cast i)
264 cast i = fromInteger (cast i)
265
265
266−implementation Cast Nat Int where
266+Cast Nat Int where
267 cast = toIntNat
267 cast = toIntNat
268
268
269−implementation Cast Nat Double where
269+Cast Nat Double where
270 cast = cast . toIntegerNat
270 cast = cast . toIntegerNat
271
271
272--------------------------------------------------------------------------------
272--------------------------------------------------------------------------------
@@ -341,7 +341,7 @@ partial
341divCeil : Nat -> Nat -> Nat
341divCeil : Nat -> Nat -> Nat
342divCeil x (S y) = divCeilNZ x (S y) SIsNotZ
342divCeil x (S y) = divCeilNZ x (S y) SIsNotZ
343
343
344−implementation Integral Nat where
344+Integral Nat where
345 div = divNat
345 div = divNat
346 mod = modNat
346 mod = modNat
347
347
libs/prelude/Prelude/Providers.idr+3−3
@@ -15,16 +15,16 @@ data Provider : (a : Type) -> Type where
15 ||| @ msg the error message
15 ||| @ msg the error message
16 Error : (msg : String) -> Provider a
16 Error : (msg : String) -> Provider a
17
17
18−implementation Functor Provider where
18+Functor Provider where
19 map f (Provide a) = Provide (f a)
19 map f (Provide a) = Provide (f a)
20 map f (Error err) = Error err
20 map f (Error err) = Error err
21
21
22−implementation Applicative Provider where
22+Applicative Provider where
23 (Provide f) <*> (Provide x) = Provide (f x)
23 (Provide f) <*> (Provide x) = Provide (f x)
24 (Provide f) <*> (Error err) = Error err
24 (Provide f) <*> (Error err) = Error err
25 (Error err) <*> _ = Error err
25 (Error err) <*> _ = Error err
26 pure = Provide
26 pure = Provide
27
27
28−implementation Monad Provider where
28+Monad Provider where
29 (Provide x) >>= f = f x
29 (Provide x) >>= f = f x
30 (Error err) >>= _ = Error err
30 (Error err) >>= _ = Error err
libs/prelude/Prelude/Show.idr+20−20
@@ -29,11 +29,11 @@ precCon (User n) = 4
29precCon PrefixMinus = 5
29precCon PrefixMinus = 5
30precCon App = 6
30precCon App = 6
31
31
32−implementation Eq Prec where
32+Eq Prec where
33 (==) (User m) (User n) = m == n
33 (==) (User m) (User n) = m == n
34 (==) x y = precCon x == precCon y
34 (==) x y = precCon x == precCon y
35
35
36−implementation Ord Prec where
36+Ord Prec where
37 compare (User m) (User n) = compare m n
37 compare (User m) (User n) = compare m n
38 compare x y = compare (precCon x) (precCon y)
38 compare x y = compare (precCon x) (precCon y)
39
39
@@ -78,7 +78,7 @@ showParens True s = "(" ++ s ++ ")"
78||| ```
78||| ```
79||| data Ann a = MkAnn String a
79||| data Ann a = MkAnn String a
80|||
80|||
81−||| implementation Show a => Show (Ann a) where
81+||| Show a => Show (Ann a) where
82||| showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x
82||| showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x
83||| ```
83||| ```
84showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String
84showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String
@@ -100,13 +100,13 @@ firstCharIs p s with (strM s)
100primNumShow : (a -> String) -> Prec -> a -> String
100primNumShow : (a -> String) -> Prec -> a -> String
101primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str
101primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str
102
102
103−implementation Show Int where
103+Show Int where
104 showPrec = primNumShow prim__toStrInt
104 showPrec = primNumShow prim__toStrInt
105
105
106−implementation Show Integer where
106+Show Integer where
107 showPrec = primNumShow prim__toStrBigInt
107 showPrec = primNumShow prim__toStrBigInt
108
108
109−implementation Show Double where
109+Show Double where
110 showPrec = primNumShow prim__floatToStr
110 showPrec = primNumShow prim__floatToStr
111
111
112protectEsc : (Char -> Bool) -> String -> String -> String
112protectEsc : (Char -> Bool) -> String -> String -> String
@@ -144,52 +144,52 @@ showLitString [] = id
144showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs
144showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs
145showLitString (c ::cs) = showLitChar c . showLitString cs
145showLitString (c ::cs) = showLitChar c . showLitString cs
146
146
147−implementation Show Char where
147+Show Char where
148 show '\'' = "'\\''"
148 show '\'' = "'\\''"
149 show c = strCons '\'' (showLitChar c "'")
149 show c = strCons '\'' (showLitChar c "'")
150
150
151−implementation Show String where
151+Show String where
152 show cs = strCons '"' (showLitString (cast cs) "\"")
152 show cs = strCons '"' (showLitString (cast cs) "\"")
153
153
154−implementation Show Nat where
154+Show Nat where
155 show n = show (the Integer (cast n))
155 show n = show (the Integer (cast n))
156
156
157−implementation Show Bool where
157+Show Bool where
158 show True = "True"
158 show True = "True"
159 show False = "False"
159 show False = "False"
160
160
161−implementation Show () where
161+Show () where
162 show () = "()"
162 show () = "()"
163
163
164−implementation Show Bits8 where
164+Show Bits8 where
165 show b = b8ToString b
165 show b = b8ToString b
166
166
167−implementation Show Bits16 where
167+Show Bits16 where
168 show b = b16ToString b
168 show b = b16ToString b
169
169
170−implementation Show Bits32 where
170+Show Bits32 where
171 show b = b32ToString b
171 show b = b32ToString b
172
172
173−implementation Show Bits64 where
173+Show Bits64 where
174 show b = b64ToString b
174 show b = b64ToString b
175
175
176−implementation (Show a, Show b) => Show (a, b) where
176+(Show a, Show b) => Show (a, b) where
177 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
177 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
178
178
179−implementation Show a => Show (List a) where
179+Show a => Show (List a) where
180 show xs = "[" ++ show' "" xs ++ "]" where
180 show xs = "[" ++ show' "" xs ++ "]" where
181 show' acc [] = acc
181 show' acc [] = acc
182 show' acc [x] = acc ++ show x
182 show' acc [x] = acc ++ show x
183 show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
183 show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
184
184
185−implementation Show a => Show (Maybe a) where
185+Show a => Show (Maybe a) where
186 showPrec d Nothing = "Nothing"
186 showPrec d Nothing = "Nothing"
187 showPrec d (Just x) = showCon d "Just" $ showArg x
187 showPrec d (Just x) = showCon d "Just" $ showArg x
188
188
189−implementation (Show a, Show b) => Show (Either a b) where
189+(Show a, Show b) => Show (Either a b) where
190 showPrec d (Left x) = showCon d "Left" $ showArg x
190 showPrec d (Left x) = showCon d "Left" $ showArg x
191 showPrec d (Right x) = showCon d "Right" $ showArg x
191 showPrec d (Right x) = showCon d "Right" $ showArg x
192
192
193−implementation (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
193+(Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where
194 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
194 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
195
195
libs/prelude/Prelude/Stream.idr+3−3
@@ -22,7 +22,7 @@ codata Stream : Type -> Type where
22-- Usage hints for erasure analysis
22-- Usage hints for erasure analysis
23%used Stream.(::) e
23%used Stream.(::) e
24
24
25−implementation Functor Stream where
25+Functor Stream where
26 map f (x::xs) = f x :: map f xs
26 map f (x::xs) = f x :: map f xs
27
27
28||| The first element of an infinite stream
28||| The first element of an infinite stream
@@ -121,10 +121,10 @@ cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs
121 cycle' [] = x :: cycle' xs
121 cycle' [] = x :: cycle' xs
122 cycle' (y :: ys) = y :: cycle' ys
122 cycle' (y :: ys) = y :: cycle' ys
123
123
124−implementation Applicative Stream where
124+Applicative Stream where
125 pure = repeat
125 pure = repeat
126 (<*>) = zipWith apply
126 (<*>) = zipWith apply
127
127
128−implementation Monad Stream where
128+Monad Stream where
129 s >>= f = diag (map f s)
129 s >>= f = diag (map f s)
130
130
libs/prelude/Prelude/Strings.idr+5−5
@@ -143,19 +143,19 @@ pack = foldr strCons ""
143singleton : Char -> String
143singleton : Char -> String
144singleton c = strCons c ""
144singleton c = strCons c ""
145
145
146−implementation Cast String (List Char) where
146+Cast String (List Char) where
147 cast = unpack
147 cast = unpack
148
148
149−implementation Cast (List Char) String where
149+Cast (List Char) String where
150 cast = pack
150 cast = pack
151
151
152−implementation Cast Char String where
152+Cast Char String where
153 cast = singleton
153 cast = singleton
154
154
155−implementation Semigroup String where
155+Semigroup String where
156 (<+>) = (++)
156 (<+>) = (++)
157
157
158−implementation Monoid String where
158+Monoid String where
159 neutral = ""
159 neutral = ""
160
160
161||| Splits the string into a part before the predicate
161||| Splits the string into a part before the predicate
libs/prelude/Prelude/Uninhabited.idr+1−1
@@ -11,7 +11,7 @@ interface Uninhabited t where
11 ||| @ t the uninhabited type
11 ||| @ t the uninhabited type
12 total uninhabited : t -> Void
12 total uninhabited : t -> Void
13
13
14−implementation Uninhabited Void where
14+Uninhabited Void where
15 uninhabited a = a
15 uninhabited a = a
16
16
17||| Use an absurd assumption to discharge a proof obligation
17||| Use an absurd assumption to discharge a proof obligation
src/Idris/ParseExpr.hs+1−1
@@ -1118,7 +1118,7 @@ constraintList1 syn = try (do lchar '('
1118 return (n, fc, e))
1118 return (n, fc, e))
1119 <|> do e <- expr syn
1119 <|> do e <- expr syn
1120 return (defname, NoFC, e)
1120 return (defname, NoFC, e)
1121− defname = sMN 0 "constrarg"
1121+ defname = sMN 0 "constraint"
1122
1122
1123{- | Parses a type declaration list
1123{- | Parses a type declaration list
1124@
1124@
src/Idris/Parser.hs+14−10
@@ -211,13 +211,14 @@ internalDecl syn
211 declBody continue)
211 declBody continue)
212 <|> fail "End of readable input"
212 <|> fail "End of readable input"
213 where declBody :: Bool -> IdrisParser [PDecl]
213 where declBody :: Bool -> IdrisParser [PDecl]
214− declBody b = declBody' b
214+ declBody b =
215+ try (instance_ True syn)
216+ <|> declBody' b
215 <|> using_ syn
217 <|> using_ syn
216 <|> params syn
218 <|> params syn
217 <|> mutual syn
219 <|> mutual syn
218 <|> namespace syn
220 <|> namespace syn
219 <|> class_ syn
221 <|> class_ syn
220− <|> instance_ syn
221 <|> do d <- dsl syn; return [d]
222 <|> do d <- dsl syn; return [d]
222 <|> directive syn
223 <|> directive syn
223 <|> provider syn
224 <|> provider syn
@@ -798,7 +799,7 @@ instanceBlock syn = do reservedHL "where"
798 ds <- many (fnDecl syn)
799 ds <- many (fnDecl syn)
799 closeBlock
800 closeBlock
800 return (concat ds)
801 return (concat ds)
801− <?> "instance block"
802+ <?> "implementation block"
802
803
803{- | Parses a methods and instances block (for type classes)
804{- | Parses a methods and instances block (for type classes)
804
805
@@ -825,7 +826,7 @@ classBlock syn = do reservedHL "where"
825 ist <- get
826 ist <- get
826 let cd' = annotate syn ist cd
827 let cd' = annotate syn ist cd
827
828
828− ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
829+ ds <- many (notEndBlock >> try (instance_ True syn) <|> fnDecl syn)
829 closeBlock
830 closeBlock
830 return (cn, cd', concat ds)
831 return (cn, cd', concat ds)
831 <?> "class block"
832 <?> "class block"
@@ -901,9 +902,12 @@ class_ syn = do (doc, argDocs, acc)
901InstanceName ::= '[' Name ']';
902InstanceName ::= '[' Name ']';
902@
903@
903-}
904-}
904−instance_ :: SyntaxInfo -> IdrisParser [PDecl]
905+instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
906+instance_ kwopt syn
905−instance_ syn = do (doc, argDocs)
907+ = do (doc, argDocs)
906− <- try (docstring syn <* instanceKeyword)
908+ <- try (docstring syn <* if kwopt then optional instanceKeyword
909+ else do instanceKeyword
910+ return (Just ()))
907 fc <- getFC
911 fc <- getFC
908 en <- optional instanceName
912 en <- optional instanceName
909 cs <- constraintList syn
913 cs <- constraintList syn
@@ -912,14 +916,14 @@ instance_ syn = do (doc, argDocs)
912 args <- many (simpleExpr syn)
916 args <- many (simpleExpr syn)
913 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
917 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
914 let t = bindList (PPi constraint) cs sc
918 let t = bindList (PPi constraint) cs sc
915− ds <- option [] (instanceBlock syn)
919+ ds <- instanceBlock syn
916 return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]
920 return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]
917− <?> "instance declaration"
921+ <?> "implementation declaration"
918 where instanceName :: IdrisParser Name
922 where instanceName :: IdrisParser Name
919 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
923 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
920 let n = expandNS syn n_in
924 let n = expandNS syn n_in
921 return n
925 return n
922− <?> "instance name"
926+ <?> "implementation name"
923 instanceKeyword :: IdrisParser ()
927 instanceKeyword :: IdrisParser ()
924 instanceKeyword = reservedHL "implementation"
928 instanceKeyword = reservedHL "implementation"
925 <|> do reservedHL "instance"
929 <|> do reservedHL "instance"