git.iko.soy/Idris-dev
on master help sign in
Make "implementation" keyword optional

This is at the cost of requiring a "where" after an implementation header even for implementations with no methods. This is probably something we should have required anyway, for consistency.

commite81d6acbffdcc21513406c9afea20e0da6c318d2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 13 Jan 2016, 14:11 (11 years ago) parent4d0a065
18 files changed+203−199
compare with master
unifiedsplit
libs/contrib/Control/Algebra/NumericInstances.idr+35−35 libs/prelude/Prelude.idr+19−19 libs/prelude/Prelude/Cast.idr+12−12 libs/prelude/Prelude/Chars.idr+1−1 libs/prelude/Prelude/Classes.idr+52−52 libs/prelude/Prelude/Either.idr+1−1 libs/prelude/Prelude/File.idr+1−1 libs/prelude/Prelude/List.idr+8−8 libs/prelude/Prelude/Maybe.idr+7−7 libs/prelude/Prelude/Monad.idr+3−3 libs/prelude/Prelude/Nat.idr+17−17 libs/prelude/Prelude/Providers.idr+3−3 libs/prelude/Prelude/Show.idr+20−20 libs/prelude/Prelude/Stream.idr+3−3 libs/prelude/Prelude/Strings.idr+5−5 libs/prelude/Prelude/Uninhabited.idr+1−1 src/Idris/ParseExpr.hs+1−1 src/Idris/Parser.hs+14−10
libs/contrib/Control/Algebra/NumericInstances.idr+35−35
@@ -8,106 +8,106 @@ import Data.Complex
88import Data.ZZ
99
1010
11−implementation Semigroup Integer where
11+Semigroup Integer where
1212 (<+>) = (+)
1313
14−implementation Monoid Integer where
14+Monoid Integer where
1515 neutral = 0
1616
17−implementation Group Integer where
17+Group Integer where
1818 inverse = (* -1)
1919
20−implementation AbelianGroup Integer
20+AbelianGroup Integer where
2121
22−implementation Ring Integer where
22+Ring Integer where
2323 (<.>) = (*)
2424
25−implementation RingWithUnity Integer where
25+RingWithUnity Integer where
2626 unity = 1
2727
2828
29−implementation Semigroup Int where
29+Semigroup Int where
3030 (<+>) = (+)
3131
32−implementation Monoid Int where
32+Monoid Int where
3333 neutral = 0
3434
35−implementation Group Int where
35+Group Int where
3636 inverse = (* -1)
3737
38−implementation AbelianGroup Int
38+AbelianGroup Int where
3939
40−implementation Ring Int where
40+Ring Int where
4141 (<.>) = (*)
4242
43−implementation RingWithUnity Int where
43+RingWithUnity Int where
4444 unity = 1
4545
4646
47−implementation Semigroup Double where
47+Semigroup Double where
4848 (<+>) = (+)
4949
50−implementation Monoid Double where
50+Monoid Double where
5151 neutral = 0
5252
53−implementation Group Double where
53+Group Double where
5454 inverse = (* -1)
5555
56−implementation AbelianGroup Double
56+AbelianGroup Double where
5757
58−implementation Ring Double where
58+Ring Double where
5959 (<.>) = (*)
6060
61−implementation RingWithUnity Double where
61+RingWithUnity Double where
6262 unity = 1
6363
64−implementation Field Double where
64+Field Double where
6565 inverseM f _ = 1 / f
6666
6767
68−implementation Semigroup Nat where
68+Semigroup Nat where
6969 (<+>) = (+)
7070
71−implementation Monoid Nat where
71+Monoid Nat where
7272 neutral = 0
7373
74−implementation Semigroup ZZ where
74+Semigroup ZZ where
7575 (<+>) = (+)
7676
77−implementation Monoid ZZ where
77+Monoid ZZ where
7878 neutral = 0
7979
80−implementation Group ZZ where
80+Group ZZ where
8181 inverse = (* -1)
8282
83−implementation AbelianGroup ZZ
83+AbelianGroup ZZ where
8484
85−implementation Ring ZZ where
85+Ring ZZ where
8686 (<.>) = (*)
8787
88−implementation RingWithUnity ZZ where
88+RingWithUnity ZZ where
8989 unity = 1
9090
9191
92−implementation Semigroup a => Semigroup (Complex a) where
92+Semigroup a => Semigroup (Complex a) where
9393 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
9494
95−implementation Monoid a => Monoid (Complex a) where
95+Monoid a => Monoid (Complex a) where
9696 neutral = (neutral :+ neutral)
9797
98−implementation Group a => Group (Complex a) where
98+Group a => Group (Complex a) where
9999 inverse (r :+ i) = (inverse r :+ inverse i)
100100
101−implementation Ring a => AbelianGroup (Complex a) where {}
101+Ring a => AbelianGroup (Complex a) where {}
102102
103−implementation Ring a => Ring (Complex a) where
103+Ring a => Ring (Complex a) where
104104 (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
105105
106−implementation RingWithUnity a => RingWithUnity (Complex a) where
106+RingWithUnity a => RingWithUnity (Complex a) where
107107 unity = (unity :+ neutral)
108108
109−implementation RingWithUnity a => Module a (Complex a) where
109+RingWithUnity a => Module a (Complex a) where
110110 (<#>) x = map (x <.>)
111111
112−implementation RingWithUnity a => InnerProductSpace a (Complex a) where
112+RingWithUnity a => InnerProductSpace a (Complex a) where
113113 (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z
libs/prelude/Prelude.idr+19−19
@@ -48,78 +48,78 @@ decAsBool (No _) = False
4848
4949---- Functor implementations
5050
51−implementation Functor PrimIO where
51+Functor PrimIO where
5252 map f io = prim_io_bind io (prim_io_return . f)
5353
54−implementation Functor Maybe where
54+Functor Maybe where
5555 map f (Just x) = Just (f x)
5656 map f Nothing = Nothing
5757
58−implementation Functor (Either e) where
58+Functor (Either e) where
5959 map f (Left l) = Left l
6060 map f (Right r) = Right (f r)
6161
6262---- Applicative implementations
6363
64−implementation Applicative PrimIO where
64+Applicative PrimIO where
6565 pure = prim_io_return
6666
6767 am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))
6868
69−implementation Applicative Maybe where
69+Applicative Maybe where
7070 pure = Just
7171
7272 (Just f) <*> (Just a) = Just (f a)
7373 _ <*> _ = Nothing
7474
75−implementation Applicative (Either e) where
75+Applicative (Either e) where
7676 pure = Right
7777
7878 (Left a) <*> _ = Left a
7979 (Right f) <*> (Right r) = Right (f r)
8080 (Right _) <*> (Left l) = Left l
8181
82−implementation Applicative List where
82+Applicative List where
8383 pure x = [x]
8484
8585 fs <*> vs = concatMap (\f => map f vs) fs
8686
8787---- Alternative implementations
8888
89−implementation Alternative Maybe where
89+Alternative Maybe where
9090 empty = Nothing
9191
9292 (Just x) <|> _ = Just x
9393 Nothing <|> v = v
9494
95−implementation Alternative List where
95+Alternative List where
9696 empty = []
9797
9898 (<|>) = (++)
9999
100100---- Monad implementations
101101
102−implementation Monad PrimIO where
102+Monad PrimIO where
103103 b >>= k = prim_io_bind b k
104104
105−implementation Monad Maybe where
105+Monad Maybe where
106106 Nothing >>= k = Nothing
107107 (Just x) >>= k = k x
108108
109−implementation Monad (Either e) where
109+Monad (Either e) where
110110 (Left n) >>= _ = Left n
111111 (Right r) >>= f = f r
112112
113−implementation Monad List where
113+Monad List where
114114 m >>= f = concatMap f m
115115
116116---- Traversable implementations
117117
118−implementation Traversable Maybe where
118+Traversable Maybe where
119119 traverse f Nothing = pure Nothing
120120 traverse f (Just x) = [| Just (f x) |]
121121
122−implementation Traversable List where
122+Traversable List where
123123 traverse f [] = pure List.Nil
124124 traverse f (x::xs) = [| List.(::) (f x) (traverse f xs) |]
125125
@@ -160,7 +160,7 @@ interface Enum a where
160160 total enumFromThenTo : a -> a -> a -> List a
161161 enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))
162162
163−implementation Enum Nat where
163+Enum Nat where
164164 pred n = Nat.pred n
165165 succ n = S n
166166 toNat x = id x
@@ -169,7 +169,7 @@ implementation Enum Nat where
169169 enumFromThenTo x y z = natEnumFromThenTo x y z
170170 enumFromTo x y = natEnumFromTo x y
171171
172−implementation Enum Integer where
172+Enum Integer where
173173 pred n = n - 1
174174 succ n = n + 1
175175 toNat n = cast n
@@ -187,7 +187,7 @@ implementation Enum Integer where
187187 go [] = []
188188 go (x :: xs) = n + (cast x * inc) :: go xs
189189
190−implementation Enum Int where
190+Enum Int where
191191 pred n = n - 1
192192 succ n = n + 1
193193 toNat n = cast n
@@ -207,7 +207,7 @@ implementation Enum Int where
207207 go [] = []
208208 go (x :: xs) = n + (cast x * inc) :: go xs
209209
210−implementation Enum Char where
210+Enum Char where
211211 toNat c = toNat (ord c)
212212 fromNat n = chr (fromNat n)
213213
libs/prelude/Prelude/Cast.idr+12−12
@@ -12,46 +12,46 @@ interface Cast from to where
1212
1313-- String casts
1414
15−implementation Cast String Int where
15+Cast String Int where
1616 cast = prim__fromStrInt
1717
18−implementation Cast String Double where
18+Cast String Double where
1919 cast = prim__strToFloat
2020
21−implementation Cast String Integer where
21+Cast String Integer where
2222 cast = prim__fromStrBigInt
2323
2424-- Int casts
2525
26−implementation Cast Int String where
26+Cast Int String where
2727 cast = prim__toStrInt
2828
29−implementation Cast Int Double where
29+Cast Int Double where
3030 cast = prim__toFloatInt
3131
32−implementation Cast Int Integer where
32+Cast Int Integer where
3333 cast = prim__sextInt_BigInt
3434
3535-- Double casts
3636
37−implementation Cast Double String where
37+Cast Double String where
3838 cast = prim__floatToStr
3939
40−implementation Cast Double Int where
40+Cast Double Int where
4141 cast = prim__fromFloatInt
4242
43−implementation Cast Double Integer where
43+Cast Double Integer where
4444 cast = prim__fromFloatBigInt
4545
4646-- Integer casts
4747
48−implementation Cast Integer String where
48+Cast Integer String where
4949 cast = prim__toStrBigInt
5050
51−implementation Cast Integer Double where
51+Cast Integer Double where
5252 cast = prim__toFloatBigInt
5353
5454-- Char casts
5555
56−implementation Cast Char Int where
56+Cast Char Int where
5757 cast = prim__charToInt
libs/prelude/Prelude/Chars.idr+1−1
@@ -13,7 +13,7 @@ chr x = if (x >= 0 && x < 0x110000)
1313 then assert_total (prim__intToChar x)
1414 else '\0'
1515
16−implementation Cast Int Char where
16+Cast Int Char where
1717 cast = chr
1818
1919||| Return the ASCII representation of the character.
libs/prelude/Prelude/Classes.idr+52−52
@@ -28,44 +28,44 @@ interface Eq a where
2828 x /= y = not (x == y)
2929 x == y = not (x /= y)
3030
31−implementation Eq () where
31+Eq () where
3232 () == () = True
3333
34−implementation Eq Int where
34+Eq Int where
3535 (==) = boolOp prim__eqInt
3636
37−implementation Eq Integer where
37+Eq Integer where
3838 (==) = boolOp prim__eqBigInt
3939
40−implementation Eq Double where
40+Eq Double where
4141 (==) = boolOp prim__eqFloat
4242
43−implementation Eq Char where
43+Eq Char where
4444 (==) = boolOp prim__eqChar
4545
46−implementation Eq String where
46+Eq String where
4747 (==) = boolOp prim__eqString
4848
49−implementation Eq Ptr where
49+Eq Ptr where
5050 (==) = boolOp prim__eqPtr
5151
52−implementation Eq ManagedPtr where
52+Eq ManagedPtr where
5353 (==) = boolOp prim__eqManagedPtr
5454
55−implementation Eq Bool where
55+Eq Bool where
5656 True == True = True
5757 True == False = False
5858 False == True = False
5959 False == False = True
6060
61−implementation (Eq a, Eq b) => Eq (a, b) where
61+(Eq a, Eq b) => Eq (a, b) where
6262 (==) (a, c) (b, d) = (a == b) && (c == d)
6363
6464
6565-- ---------------------------------------------------------- [ Ordering Interface ]
6666%elim data Ordering = LT | EQ | GT
6767
68−implementation Eq Ordering where
68+Eq Ordering where
6969 LT == LT = True
7070 EQ == EQ = True
7171 GT == GT = True
@@ -103,47 +103,47 @@ interface Eq a => Ord a where
103103 min : a -> a -> a
104104 min x y = if (x < y) then x else y
105105
106−implementation Ord () where
106+Ord () where
107107 compare () () = EQ
108108
109−implementation Ord Int where
109+Ord Int where
110110 compare x y = if (x == y) then EQ else
111111 if (boolOp prim__sltInt x y) then LT else
112112 GT
113113
114114
115−implementation Ord Integer where
115+Ord Integer where
116116 compare x y = if (x == y) then EQ else
117117 if (boolOp prim__sltBigInt x y) then LT else
118118 GT
119119
120120
121−implementation Ord Double where
121+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
125125
126126
127−implementation Ord Char where
127+Ord Char where
128128 compare x y = if (x == y) then EQ else
129129 if (boolOp prim__sltChar x y) then LT else
130130 GT
131131
132132
133−implementation Ord String where
133+Ord String where
134134 compare x y = if (x == y) then EQ else
135135 if (boolOp prim__ltString x y) then LT else
136136 GT
137137
138138
139−implementation Ord Bool where
139+Ord Bool where
140140 compare True True = EQ
141141 compare False False = EQ
142142 compare False True = LT
143143 compare True False = GT
144144
145145
146−implementation (Ord a, Ord b) => Ord (a, b) where
146+(Ord a, Ord b) => Ord (a, b) where
147147 compare (xl, xr) (yl, yr) =
148148 if xl /= yl
149149 then compare xl yl
@@ -157,41 +157,41 @@ interface Num a where
157157 ||| Conversion from Integer.
158158 fromInteger : Integer -> a
159159
160−implementation Num Integer where
160+Num Integer where
161161 (+) = prim__addBigInt
162162 (*) = prim__mulBigInt
163163
164164 fromInteger = id
165165
166−implementation Num Int where
166+Num Int where
167167 (+) = prim__addInt
168168 (*) = prim__mulInt
169169
170170 fromInteger = prim__truncBigInt_Int
171171
172172
173−implementation Num Double where
173+Num Double where
174174 (+) = prim__addFloat
175175 (*) = prim__mulFloat
176176
177177 fromInteger = prim__toFloatBigInt
178178
179−implementation Num Bits8 where
179+Num Bits8 where
180180 (+) = prim__addB8
181181 (*) = prim__mulB8
182182 fromInteger = prim__truncBigInt_B8
183183
184−implementation Num Bits16 where
184+Num Bits16 where
185185 (+) = prim__addB16
186186 (*) = prim__mulB16
187187 fromInteger = prim__truncBigInt_B16
188188
189−implementation Num Bits32 where
189+Num Bits32 where
190190 (+) = prim__addB32
191191 (*) = prim__mulB32
192192 fromInteger = prim__truncBigInt_B32
193193
194−implementation Num Bits64 where
194+Num Bits64 where
195195 (+) = prim__addB64
196196 (*) = prim__mulB64
197197 fromInteger = prim__truncBigInt_B64
@@ -199,41 +199,41 @@ implementation Num Bits64 where
199199-- --------------------------------------------------------- [ Negatable Interface ]
200200||| The `Neg` interface defines operations on numbers which can be negative.
201201interface 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)`.
203203 negate : a -> a
204204 (-) : a -> a -> a
205205 ||| Absolute value
206206 abs : a -> a
207207
208−implementation Neg Integer where
208+Neg Integer where
209209 negate x = prim__subBigInt 0 x
210210 (-) = prim__subBigInt
211211 abs x = if x < 0 then -x else x
212212
213−implementation Neg Int where
213+Neg Int where
214214 negate x = prim__subInt 0 x
215215 (-) = prim__subInt
216216 abs x = if x < (prim__truncBigInt_Int 0) then -x else x
217217
218−implementation Neg Double where
218+Neg Double where
219219 negate x = prim__negFloat x
220220 (-) = prim__subFloat
221221 abs x = if x < (prim__toFloatBigInt 0) then -x else x
222222
223223-- ------------------------------------------------------------
224−implementation Eq Bits8 where
224+Eq Bits8 where
225225 x == y = intToBool (prim__eqB8 x y)
226226
227−implementation Eq Bits16 where
227+Eq Bits16 where
228228 x == y = intToBool (prim__eqB16 x y)
229229
230−implementation Eq Bits32 where
230+Eq Bits32 where
231231 x == y = intToBool (prim__eqB32 x y)
232232
233−implementation Eq Bits64 where
233+Eq Bits64 where
234234 x == y = intToBool (prim__eqB64 x y)
235235
236−implementation Ord Bits8 where
236+Ord Bits8 where
237237 (<) = boolOp prim__ltB8
238238 (>) = boolOp prim__gtB8
239239 (<=) = boolOp prim__lteB8
@@ -242,7 +242,7 @@ implementation Ord Bits8 where
242242 else if l > r then GT
243243 else EQ
244244
245−implementation Ord Bits16 where
245+Ord Bits16 where
246246 (<) = boolOp prim__ltB16
247247 (>) = boolOp prim__gtB16
248248 (<=) = boolOp prim__lteB16
@@ -251,7 +251,7 @@ implementation Ord Bits16 where
251251 else if l > r then GT
252252 else EQ
253253
254−implementation Ord Bits32 where
254+Ord Bits32 where
255255 (<) = boolOp prim__ltB32
256256 (>) = boolOp prim__gtB32
257257 (<=) = boolOp prim__lteB32
@@ -260,7 +260,7 @@ implementation Ord Bits32 where
260260 else if l > r then GT
261261 else EQ
262262
263−implementation Ord Bits64 where
263+Ord Bits64 where
264264 (<) = boolOp prim__ltB64
265265 (>) = boolOp prim__gtB64
266266 (<=) = boolOp prim__lteB64
@@ -279,28 +279,28 @@ interface Ord b => MaxBound b where
279279 ||| The upper bound for the type
280280 maxBound : b
281281
282−implementation MinBound Bits8 where
282+MinBound Bits8 where
283283 minBound = 0x0
284284
285−implementation MaxBound Bits8 where
285+MaxBound Bits8 where
286286 maxBound = 0xff
287287
288−implementation MinBound Bits16 where
288+MinBound Bits16 where
289289 minBound = 0x0
290290
291−implementation MaxBound Bits16 where
291+MaxBound Bits16 where
292292 maxBound = 0xffff
293293
294−implementation MinBound Bits32 where
294+MinBound Bits32 where
295295 minBound = 0x0
296296
297−implementation MaxBound Bits32 where
297+MaxBound Bits32 where
298298 maxBound = 0xffffffff
299299
300−implementation MinBound Bits64 where
300+MinBound Bits64 where
301301 minBound = 0x0
302302
303−implementation MaxBound Bits64 where
303+MaxBound Bits64 where
304304 maxBound = 0xffffffffffffffff
305305
306306
@@ -327,7 +327,7 @@ modBigInt : Integer -> Integer -> Integer
327327modBigInt x y = case y == 0 of
328328 False => prim__sremBigInt x y
329329
330−implementation Integral Integer where
330+Integral Integer where
331331 div = divBigInt
332332 mod = modBigInt
333333
@@ -341,7 +341,7 @@ modInt : Int -> Int -> Int
341341modInt x y = case y == 0 of
342342 False => prim__sremInt x y
343343
344−implementation Integral Int where
344+Integral Int where
345345 div = divInt
346346 mod = modInt
347347
@@ -354,7 +354,7 @@ modB8 : Bits8 -> Bits8 -> Bits8
354354modB8 x y = case y == 0 of
355355 False => prim__sremB8 x y
356356
357−implementation Integral Bits8 where
357+Integral Bits8 where
358358 div = divB8
359359 mod = modB8
360360
@@ -367,7 +367,7 @@ modB16 : Bits16 -> Bits16 -> Bits16
367367modB16 x y = case y == 0 of
368368 False => prim__sremB16 x y
369369
370−implementation Integral Bits16 where
370+Integral Bits16 where
371371 div = divB16
372372 mod = modB16
373373
@@ -380,7 +380,7 @@ modB32 : Bits32 -> Bits32 -> Bits32
380380modB32 x y = case y == 0 of
381381 False => prim__sremB32 x y
382382
383−implementation Integral Bits32 where
383+Integral Bits32 where
384384 div = divB32
385385 mod = modB32
386386
@@ -393,7 +393,7 @@ modB64 : Bits64 -> Bits64 -> Bits64
393393modB64 x y = case y == 0 of
394394 False => prim__sremB64 x y
395395
396−implementation Integral Bits64 where
396+Integral Bits64 where
397397 div = divB64
398398 mod = modB64
399399
libs/prelude/Prelude/Either.idr+1−1
@@ -90,7 +90,7 @@ maybeToEither def Nothing = Left def
9090-- Instances
9191--------------------------------------------------------------------------------
9292
93−implementation (Eq a, Eq b) => Eq (Either a b) where
93+(Eq a, Eq b) => Eq (Either a b) where
9494 (==) (Left x) (Left y) = x == y
9595 (==) (Right x) (Right y) = x == y
9696 (==) _ _ = False
libs/prelude/Prelude/File.idr+1−1
@@ -43,7 +43,7 @@ getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"
4343 (Ptr -> IO (Raw FileError)) prim__vm
4444 return err
4545
46−implementation Show FileError where
46+Show FileError where
4747 show FileNotFound = "File Not Found"
4848 show PermissionDenied = "Permission Denied"
4949 show (GenericFileError errno) = strError errno
libs/prelude/Prelude/List.idr+8−8
@@ -56,7 +56,7 @@ data NonEmpty : (xs : List a) -> Type where
5656 ||| The proof that a cons cell is non-empty
5757 IsNonEmpty : NonEmpty (x :: xs)
5858
59−implementation Uninhabited (NonEmpty []) where
59+Uninhabited (NonEmpty []) where
6060 uninhabited IsNonEmpty impossible
6161
6262||| Decide whether a list is non-empty
@@ -74,7 +74,7 @@ data InBounds : (k : Nat) -> (xs : List a) -> Type where
7474 ||| Valid indices can be extended
7575 InLater : InBounds k xs -> InBounds (S k) (x :: xs)
7676
77−implementation Uninhabited (InBounds k []) where
77+Uninhabited (InBounds k []) where
7878 uninhabited InFirst impossible
7979
8080||| Decide whether `k` is a valid index into `xs`
@@ -252,7 +252,7 @@ replicate (S n) x = x :: replicate n x
252252-- Instances
253253--------------------------------------------------------------------------------
254254
255−implementation (Eq a) => Eq (List a) where
255+(Eq a) => Eq (List a) where
256256 (==) [] [] = True
257257 (==) (x::xs) (y::ys) =
258258 if x == y then
@@ -262,7 +262,7 @@ implementation (Eq a) => Eq (List a) where
262262 (==) _ _ = False
263263
264264
265−implementation Ord a => Ord (List a) where
265+Ord a => Ord (List a) where
266266 compare [] [] = EQ
267267 compare [] _ = LT
268268 compare _ [] = GT
@@ -272,13 +272,13 @@ implementation Ord a => Ord (List a) where
272272 else
273273 compare xs ys
274274
275−implementation Semigroup (List a) where
275+Semigroup (List a) where
276276 (<+>) = (++)
277277
278−implementation Monoid (List a) where
278+Monoid (List a) where
279279 neutral = []
280280
281−implementation Functor List where
281+Functor List where
282282 map f [] = []
283283 map f (x::xs) = f x :: map f xs
284284
@@ -349,7 +349,7 @@ mapMaybe f (x::xs) =
349349-- Folds
350350--------------------------------------------------------------------------------
351351
352−implementation Foldable List where
352+Foldable List where
353353 foldr c n [] = n
354354 foldr c n (x::xs) = c x (foldr c n xs)
355355
libs/prelude/Prelude/Maybe.idr+7−7
@@ -79,7 +79,7 @@ maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b
7979maybe_bind Nothing k = Nothing
8080maybe_bind (Just x) k = k x
8181
82−implementation (Eq a) => Eq (Maybe a) where
82+(Eq a) => Eq (Maybe a) where
8383 Nothing == Nothing = True
8484 Nothing == (Just _) = False
8585 (Just _) == Nothing = False
@@ -90,7 +90,7 @@ implementation (Eq a) => Eq (Maybe a) where
9090|||
9191||| **NB**: This is a different choice than in the Haskell libraries.
9292||| Use `collectJust` to get the Haskell behaviour.
93−implementation Semigroup (Maybe a) where
93+Semigroup (Maybe a) where
9494 Nothing <+> m = m
9595 (Just x) <+> _ = Just x
9696
@@ -98,20 +98,20 @@ implementation Semigroup (Maybe a) where
9898||| designated neutral element and collecting the contents of the
9999||| `Just` constructors using a semigroup structure on `a`. This is
100100||| the behaviour in the Haskell libraries.
101−implementation [collectJust] Semigroup a => Semigroup (Maybe a) where
101+[collectJust] Semigroup a => Semigroup (Maybe a) where
102102 Nothing <+> m = m
103103 m <+> Nothing = m
104104 (Just m1) <+> (Just m2) = Just (m1 <+> m2)
105105
106−implementation Monoid (Maybe a) where
106+ Monoid (Maybe a) where
107107 neutral = Nothing
108108
109−implementation (Monoid a, Eq a) => Cast a (Maybe a) where
109+(Monoid a, Eq a) => Cast a (Maybe a) where
110110 cast = raiseToMaybe
111111
112−implementation (Monoid a) => Cast (Maybe a) a where
112+(Monoid a) => Cast (Maybe a) a where
113113 cast = lowerMaybe
114114
115−implementation Foldable Maybe where
115+Foldable Maybe where
116116 foldr _ z Nothing = z
117117 foldr f z (Just x) = f x z
libs/prelude/Prelude/Monad.idr+3−3
@@ -27,16 +27,16 @@ return = pure
2727-- Annoyingly, these need to be here, so that we can use them in other
2828-- Prelude modules other than the top level.
2929
30−implementation Functor (IO' ffi) where
30+Functor (IO' ffi) where
3131 map f io = io_bind io (\b => io_return (f b))
3232
33−implementation Applicative (IO' ffi) where
33+Applicative (IO' ffi) where
3434 pure x = io_return x
3535 f <*> a = io_bind f (\f' =>
3636 io_bind a (\a' =>
3737 io_return (f' a')))
3838
3939
40−implementation Monad (IO' ffi) where
40+Monad (IO' ffi) where
4141 b >>= k = io_bind b k
4242
libs/prelude/Prelude/Nat.idr+17−17
@@ -23,7 +23,7 @@ import Prelude.Uninhabited
2323-- name hints for interactive editing
2424%name Nat k,j,i,n,m
2525
26−implementation Uninhabited (Z = S n) where
26+Uninhabited (Z = S n) where
2727 uninhabited Refl impossible
2828
2929--------------------------------------------------------------------------------
@@ -100,7 +100,7 @@ data LTE : (n, m : Nat) -> Type where
100100 ||| If n <= m, then n + 1 <= m + 1
101101 LTESucc : LTE left right -> LTE (S left) (S right)
102102
103−implementation Uninhabited (LTE (S n) Z) where
103+Uninhabited (LTE (S n) Z) where
104104 uninhabited LTEZero impossible
105105
106106||| Greater than or equal to
@@ -187,34 +187,34 @@ toIntNat n = toIntNat' n 0 where
187187-- Type class implementations
188188--------------------------------------------------------------------------------
189189
190−implementation Eq Nat where
190+Eq Nat where
191191 Z == Z = True
192192 (S l) == (S r) = l == r
193193 _ == _ = False
194194
195−implementation Cast Nat Integer where
195+Cast Nat Integer where
196196 cast = toIntegerNat
197197
198−implementation Ord Nat where
198+Ord Nat where
199199 compare Z Z = EQ
200200 compare Z (S k) = LT
201201 compare (S k) Z = GT
202202 compare (S x) (S y) = compare x y
203203
204−implementation Num Nat where
204+Num Nat where
205205 (+) = plus
206206 (*) = mult
207207
208208 fromInteger = fromIntegerNat
209209
210−implementation MinBound Nat where
210+MinBound Nat where
211211 minBound = Z
212212
213213||| Casts negative `Integers` to 0.
214−implementation Cast Integer Nat where
214+Cast Integer Nat where
215215 cast = fromInteger
216216
217−implementation Cast String Nat where
217+Cast String Nat where
218218 cast str = cast (the Integer (cast str))
219219
220220||| A wrapper for Nat that specifies the semigroup and monad implementations that use (*)
@@ -227,7 +227,7 @@ record Additive where
227227 constructor GetAdditive
228228 _ : Nat
229229
230−implementation Semigroup Multiplicative where
230+Semigroup Multiplicative where
231231 (<+>) left right = GetMultiplicative $ left' * right'
232232 where
233233 left' : Nat
@@ -240,7 +240,7 @@ implementation Semigroup Multiplicative where
240240 case right of
241241 GetMultiplicative m => m
242242
243−implementation Semigroup Additive where
243+Semigroup Additive where
244244 left <+> right = GetAdditive $ left' + right'
245245 where
246246 left' : Nat
@@ -253,20 +253,20 @@ implementation Semigroup Additive where
253253 case right of
254254 GetAdditive m => m
255255
256−implementation Monoid Multiplicative where
256+Monoid Multiplicative where
257257 neutral = GetMultiplicative $ S Z
258258
259−implementation Monoid Additive where
259+Monoid Additive where
260260 neutral = GetAdditive Z
261261
262262||| Casts negative `Ints` to 0.
263−implementation Cast Int Nat where
263+Cast Int Nat where
264264 cast i = fromInteger (cast i)
265265
266−implementation Cast Nat Int where
266+Cast Nat Int where
267267 cast = toIntNat
268268
269−implementation Cast Nat Double where
269+Cast Nat Double where
270270 cast = cast . toIntegerNat
271271
272272--------------------------------------------------------------------------------
@@ -341,7 +341,7 @@ partial
341341divCeil : Nat -> Nat -> Nat
342342divCeil x (S y) = divCeilNZ x (S y) SIsNotZ
343343
344−implementation Integral Nat where
344+Integral Nat where
345345 div = divNat
346346 mod = modNat
347347
libs/prelude/Prelude/Providers.idr+3−3
@@ -15,16 +15,16 @@ data Provider : (a : Type) -> Type where
1515 ||| @ msg the error message
1616 Error : (msg : String) -> Provider a
1717
18−implementation Functor Provider where
18+Functor Provider where
1919 map f (Provide a) = Provide (f a)
2020 map f (Error err) = Error err
2121
22−implementation Applicative Provider where
22+Applicative Provider where
2323 (Provide f) <*> (Provide x) = Provide (f x)
2424 (Provide f) <*> (Error err) = Error err
2525 (Error err) <*> _ = Error err
2626 pure = Provide
2727
28−implementation Monad Provider where
28+Monad Provider where
2929 (Provide x) >>= f = f x
3030 (Error err) >>= _ = Error err
libs/prelude/Prelude/Show.idr+20−20
@@ -29,11 +29,11 @@ precCon (User n) = 4
2929precCon PrefixMinus = 5
3030precCon App = 6
3131
32−implementation Eq Prec where
32+Eq Prec where
3333 (==) (User m) (User n) = m == n
3434 (==) x y = precCon x == precCon y
3535
36−implementation Ord Prec where
36+Ord Prec where
3737 compare (User m) (User n) = compare m n
3838 compare x y = compare (precCon x) (precCon y)
3939
@@ -78,7 +78,7 @@ showParens True s = "(" ++ s ++ ")"
7878||| ```
7979||| data Ann a = MkAnn String a
8080|||
81−||| implementation Show a => Show (Ann a) where
81+||| Show a => Show (Ann a) where
8282||| showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x
8383||| ```
8484showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String
@@ -100,13 +100,13 @@ firstCharIs p s with (strM s)
100100primNumShow : (a -> String) -> Prec -> a -> String
101101primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str
102102
103−implementation Show Int where
103+Show Int where
104104 showPrec = primNumShow prim__toStrInt
105105
106−implementation Show Integer where
106+Show Integer where
107107 showPrec = primNumShow prim__toStrBigInt
108108
109−implementation Show Double where
109+Show Double where
110110 showPrec = primNumShow prim__floatToStr
111111
112112protectEsc : (Char -> Bool) -> String -> String -> String
@@ -144,52 +144,52 @@ showLitString [] = id
144144showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs
145145showLitString (c ::cs) = showLitChar c . showLitString cs
146146
147−implementation Show Char where
147+Show Char where
148148 show '\'' = "'\\''"
149149 show c = strCons '\'' (showLitChar c "'")
150150
151−implementation Show String where
151+Show String where
152152 show cs = strCons '"' (showLitString (cast cs) "\"")
153153
154−implementation Show Nat where
154+Show Nat where
155155 show n = show (the Integer (cast n))
156156
157−implementation Show Bool where
157+Show Bool where
158158 show True = "True"
159159 show False = "False"
160160
161−implementation Show () where
161+Show () where
162162 show () = "()"
163163
164−implementation Show Bits8 where
164+Show Bits8 where
165165 show b = b8ToString b
166166
167−implementation Show Bits16 where
167+Show Bits16 where
168168 show b = b16ToString b
169169
170−implementation Show Bits32 where
170+Show Bits32 where
171171 show b = b32ToString b
172172
173−implementation Show Bits64 where
173+Show Bits64 where
174174 show b = b64ToString b
175175
176−implementation (Show a, Show b) => Show (a, b) where
176+(Show a, Show b) => Show (a, b) where
177177 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"
178178
179−implementation Show a => Show (List a) where
179+Show a => Show (List a) where
180180 show xs = "[" ++ show' "" xs ++ "]" where
181181 show' acc [] = acc
182182 show' acc [x] = acc ++ show x
183183 show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs
184184
185−implementation Show a => Show (Maybe a) where
185+Show a => Show (Maybe a) where
186186 showPrec d Nothing = "Nothing"
187187 showPrec d (Just x) = showCon d "Just" $ showArg x
188188
189−implementation (Show a, Show b) => Show (Either a b) where
189+(Show a, Show b) => Show (Either a b) where
190190 showPrec d (Left x) = showCon d "Left" $ showArg x
191191 showPrec d (Right x) = showCon d "Right" $ showArg x
192192
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
194194 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"
195195
libs/prelude/Prelude/Stream.idr+3−3
@@ -22,7 +22,7 @@ codata Stream : Type -> Type where
2222-- Usage hints for erasure analysis
2323%used Stream.(::) e
2424
25−implementation Functor Stream where
25+Functor Stream where
2626 map f (x::xs) = f x :: map f xs
2727
2828||| The first element of an infinite stream
@@ -121,10 +121,10 @@ cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs
121121 cycle' [] = x :: cycle' xs
122122 cycle' (y :: ys) = y :: cycle' ys
123123
124−implementation Applicative Stream where
124+Applicative Stream where
125125 pure = repeat
126126 (<*>) = zipWith apply
127127
128−implementation Monad Stream where
128+Monad Stream where
129129 s >>= f = diag (map f s)
130130
libs/prelude/Prelude/Strings.idr+5−5
@@ -143,19 +143,19 @@ pack = foldr strCons ""
143143singleton : Char -> String
144144singleton c = strCons c ""
145145
146−implementation Cast String (List Char) where
146+Cast String (List Char) where
147147 cast = unpack
148148
149−implementation Cast (List Char) String where
149+Cast (List Char) String where
150150 cast = pack
151151
152−implementation Cast Char String where
152+Cast Char String where
153153 cast = singleton
154154
155−implementation Semigroup String where
155+Semigroup String where
156156 (<+>) = (++)
157157
158−implementation Monoid String where
158+Monoid String where
159159 neutral = ""
160160
161161||| Splits the string into a part before the predicate
libs/prelude/Prelude/Uninhabited.idr+1−1
@@ -11,7 +11,7 @@ interface Uninhabited t where
1111 ||| @ t the uninhabited type
1212 total uninhabited : t -> Void
1313
14−implementation Uninhabited Void where
14+Uninhabited Void where
1515 uninhabited a = a
1616
1717||| Use an absurd assumption to discharge a proof obligation
src/Idris/ParseExpr.hs+1−1
@@ -1118,7 +1118,7 @@ constraintList1 syn = try (do lchar '('
11181118 return (n, fc, e))
11191119 <|> do e <- expr syn
11201120 return (defname, NoFC, e)
1121− defname = sMN 0 "constrarg"
1121+ defname = sMN 0 "constraint"
11221122
11231123{- | Parses a type declaration list
11241124@
src/Idris/Parser.hs+14−10
@@ -211,13 +211,14 @@ internalDecl syn
211211 declBody continue)
212212 <|> fail "End of readable input"
213213 where declBody :: Bool -> IdrisParser [PDecl]
214− declBody b = declBody' b
214+ declBody b =
215+ try (instance_ True syn)
216+ <|> declBody' b
215217 <|> using_ syn
216218 <|> params syn
217219 <|> mutual syn
218220 <|> namespace syn
219221 <|> class_ syn
220− <|> instance_ syn
221222 <|> do d <- dsl syn; return [d]
222223 <|> directive syn
223224 <|> provider syn
@@ -798,7 +799,7 @@ instanceBlock syn = do reservedHL "where"
798799 ds <- many (fnDecl syn)
799800 closeBlock
800801 return (concat ds)
801− <?> "instance block"
802+ <?> "implementation block"
802803
803804{- | Parses a methods and instances block (for type classes)
804805
@@ -825,7 +826,7 @@ classBlock syn = do reservedHL "where"
825826 ist <- get
826827 let cd' = annotate syn ist cd
827828
828− ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn)
829+ ds <- many (notEndBlock >> try (instance_ True syn) <|> fnDecl syn)
829830 closeBlock
830831 return (cn, cd', concat ds)
831832 <?> "class block"
@@ -901,9 +902,12 @@ class_ syn = do (doc, argDocs, acc)
901902InstanceName ::= '[' Name ']';
902903@
903904-}
904−instance_ :: SyntaxInfo -> IdrisParser [PDecl]
905−instance_ syn = do (doc, argDocs)
906− <- try (docstring syn <* instanceKeyword)
905+instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]
906+instance_ kwopt syn
907+ = do (doc, argDocs)
908+ <- try (docstring syn <* if kwopt then optional instanceKeyword
909+ else do instanceKeyword
910+ return (Just ()))
907911 fc <- getFC
908912 en <- optional instanceName
909913 cs <- constraintList syn
@@ -912,14 +916,14 @@ instance_ syn = do (doc, argDocs)
912916 args <- many (simpleExpr syn)
913917 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)
914918 let t = bindList (PPi constraint) cs sc
915− ds <- option [] (instanceBlock syn)
919+ ds <- instanceBlock syn
916920 return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]
917− <?> "instance declaration"
921+ <?> "implementation declaration"
918922 where instanceName :: IdrisParser Name
919923 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'
920924 let n = expandNS syn n_in
921925 return n
922− <?> "instance name"
926+ <?> "implementation name"
923927 instanceKeyword :: IdrisParser ()
924928 instanceKeyword = reservedHL "implementation"
925929 <|> do reservedHL "instance"