0 | module Prelude.Num
  1 |
  2 | import Prelude.Basics
  3 | import Prelude.EqOrd
  4 |
  5 | %default total
  6 |
  7 | ------------------------
  8 | -- NUMERIC INTERFACES --
  9 | ------------------------
 10 |
 11 | %integerLit fromInteger
 12 |
 13 | ||| The Num interface defines basic numerical arithmetic.
 14 | public export
 15 | interface Num ty where
 16 |   constructor MkNum
 17 |   (+) : ty -> ty -> ty
 18 |   (*) : ty -> ty -> ty
 19 |   ||| Conversion from Integer.
 20 |   fromInteger : Integer -> ty
 21 |
 22 | %allow_overloads fromInteger
 23 |
 24 | ||| The `Neg` interface defines operations on numbers which can be negative.
 25 | public export
 26 | interface Num ty => Neg ty where
 27 |   constructor MkNeg
 28 |   ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
 29 |   negate : ty -> ty
 30 |   (-) : ty -> ty -> ty
 31 |
 32 | ||| A convenience alias for `(-)`, this function enables partial application of subtraction on the
 33 | ||| right-hand operand as
 34 | ||| ```idris example
 35 | ||| (`subtract` 1)
 36 | ||| ```
 37 | ||| This contrasts with `(- 1)`, which is parsed as `-1`.
 38 | export
 39 | subtract : Neg ty => ty -> ty -> ty
 40 | subtract = (-)
 41 |
 42 | ||| Numbers for which the absolute value is defined should implement `Abs`.
 43 | public export
 44 | interface Num ty => Abs ty where
 45 |   constructor MkAbs
 46 |   ||| Absolute value.
 47 |   abs : ty -> ty
 48 |
 49 | public export
 50 | interface Num ty => Fractional ty where
 51 |   constructor MkFractional
 52 |   partial
 53 |   (/) : ty -> ty -> ty
 54 |   partial
 55 |   recip : ty -> ty
 56 |
 57 |   recip x = 1 / x
 58 |
 59 | public export
 60 | interface Num ty => Integral ty where
 61 |   constructor MkIntegral
 62 |   partial
 63 |   div : ty -> ty -> ty
 64 |   partial
 65 |   mod : ty -> ty -> ty
 66 |
 67 | ----- Instances for primitives
 68 |
 69 | -- Integer
 70 |
 71 | %inline
 72 | public export
 73 | Num Integer where
 74 |   (+) = prim__add_Integer
 75 |   (*) = prim__mul_Integer
 76 |   fromInteger = id
 77 |
 78 | %inline
 79 | public export
 80 | Neg Integer where
 81 |   negate x = prim__sub_Integer 0 x
 82 |   (-) = prim__sub_Integer
 83 |
 84 | public export
 85 | Abs Integer where
 86 |   abs x = if x < 0 then -x else x
 87 |
 88 | public export
 89 | Integral Integer where
 90 |   div x y
 91 |       = case y == 0 of
 92 |              False => prim__div_Integer x y
 93 |   mod x y
 94 |       = case y == 0 of
 95 |              False => prim__mod_Integer x y
 96 |
 97 | -- This allows us to pick integer as a default at the end of elaboration if
 98 | -- all other possibilities fail. I don't plan to provide a nicer syntax for
 99 | -- this...
100 | %defaulthint
101 | %inline
102 | public export
103 | defaultInteger : Num Integer
104 | defaultInteger = %search
105 |
106 | -- Int
107 |
108 | %inline
109 | public export
110 | Num Int where
111 |   (+) = prim__add_Int
112 |   (*) = prim__mul_Int
113 |   fromInteger = prim__cast_IntegerInt
114 |
115 | %inline
116 | public export
117 | Neg Int where
118 |   negate x = prim__sub_Int 0 x
119 |   (-) = prim__sub_Int
120 |
121 | public export
122 | Abs Int where
123 |   abs x = if x < 0 then -x else x
124 |
125 | public export
126 | Integral Int where
127 |   div x y
128 |       = case y == 0 of
129 |              False => prim__div_Int x y
130 |   mod x y
131 |       = case y == 0 of
132 |              False => prim__mod_Int x y
133 |
134 | -- Int8
135 |
136 | %inline
137 | public export
138 | Num Int8 where
139 |   (+) = prim__add_Int8
140 |   (*) = prim__mul_Int8
141 |   fromInteger = prim__cast_IntegerInt8
142 |
143 | %inline
144 | public export
145 | Neg Int8 where
146 |   negate x = prim__sub_Int8 0 x
147 |   (-) = prim__sub_Int8
148 |
149 | public export
150 | Abs Int8 where
151 |   abs x = if x < 0 then -x else x
152 |
153 | public export
154 | Integral Int8 where
155 |   div x y
156 |       = case y == 0 of
157 |              False => prim__div_Int8 x y
158 |   mod x y
159 |       = case y == 0 of
160 |              False => prim__mod_Int8 x y
161 |
162 | -- Int16
163 |
164 | %inline
165 | public export
166 | Num Int16 where
167 |   (+) = prim__add_Int16
168 |   (*) = prim__mul_Int16
169 |   fromInteger = prim__cast_IntegerInt16
170 |
171 | %inline
172 | public export
173 | Neg Int16 where
174 |   negate x = prim__sub_Int16 0 x
175 |   (-) = prim__sub_Int16
176 |
177 | public export
178 | Abs Int16 where
179 |   abs x = if x < 0 then -x else x
180 |
181 | public export
182 | Integral Int16 where
183 |   div x y
184 |       = case y == 0 of
185 |              False => prim__div_Int16 x y
186 |   mod x y
187 |       = case y == 0 of
188 |              False => prim__mod_Int16 x y
189 |
190 | -- Int32
191 |
192 | %inline
193 | public export
194 | Num Int32 where
195 |   (+) = prim__add_Int32
196 |   (*) = prim__mul_Int32
197 |   fromInteger = prim__cast_IntegerInt32
198 |
199 | %inline
200 | public export
201 | Neg Int32 where
202 |   negate x = prim__sub_Int32 0 x
203 |   (-) = prim__sub_Int32
204 |
205 | public export
206 | Abs Int32 where
207 |   abs x = if x < 0 then -x else x
208 |
209 | public export
210 | Integral Int32 where
211 |   div x y
212 |       = case y == 0 of
213 |              False => prim__div_Int32 x y
214 |   mod x y
215 |       = case y == 0 of
216 |              False => prim__mod_Int32 x y
217 |
218 | -- Int64
219 |
220 | %inline
221 | public export
222 | Num Int64 where
223 |   (+) = prim__add_Int64
224 |   (*) = prim__mul_Int64
225 |   fromInteger = prim__cast_IntegerInt64
226 |
227 | %inline
228 | public export
229 | Neg Int64 where
230 |   negate x = prim__sub_Int64 0 x
231 |   (-) = prim__sub_Int64
232 |
233 | public export
234 | Abs Int64 where
235 |   abs x = if x < 0 then -x else x
236 |
237 | public export
238 | Integral Int64 where
239 |   div x y
240 |       = case y == 0 of
241 |              False => prim__div_Int64 x y
242 |   mod x y
243 |       = case y == 0 of
244 |              False => prim__mod_Int64 x y
245 |
246 | -- Bits8
247 |
248 | %inline
249 | public export
250 | Num Bits8 where
251 |   (+) = prim__add_Bits8
252 |   (*) = prim__mul_Bits8
253 |   fromInteger = prim__cast_IntegerBits8
254 |
255 | %inline
256 | public export
257 | Neg Bits8 where
258 |   negate x = prim__sub_Bits8 0 x
259 |   (-) = prim__sub_Bits8
260 |
261 | public export
262 | Abs Bits8 where
263 |   abs x = if x < 0 then -x else x
264 |
265 | public export
266 | Integral Bits8 where
267 |   div x y
268 |       = case y == 0 of
269 |              False => prim__div_Bits8 x y
270 |   mod x y
271 |       = case y == 0 of
272 |              False => prim__mod_Bits8 x y
273 |
274 | -- Bits16
275 |
276 | %inline
277 | public export
278 | Num Bits16 where
279 |   (+) = prim__add_Bits16
280 |   (*) = prim__mul_Bits16
281 |   fromInteger = prim__cast_IntegerBits16
282 |
283 | %inline
284 | public export
285 | Neg Bits16 where
286 |   negate x = prim__sub_Bits16 0 x
287 |   (-) = prim__sub_Bits16
288 |
289 | public export
290 | Abs Bits16 where
291 |   abs x = if x < 0 then -x else x
292 |
293 | public export
294 | Integral Bits16 where
295 |   div x y
296 |       = case y == 0 of
297 |              False => prim__div_Bits16 x y
298 |   mod x y
299 |       = case y == 0 of
300 |              False => prim__mod_Bits16 x y
301 |
302 | -- Bits32
303 |
304 | %inline
305 | public export
306 | Num Bits32 where
307 |   (+) = prim__add_Bits32
308 |   (*) = prim__mul_Bits32
309 |   fromInteger = prim__cast_IntegerBits32
310 |
311 | %inline
312 | public export
313 | Neg Bits32 where
314 |   negate x = prim__sub_Bits32 0 x
315 |   (-) = prim__sub_Bits32
316 |
317 | public export
318 | Abs Bits32 where
319 |   abs x = if x < 0 then -x else x
320 |
321 | public export
322 | Integral Bits32 where
323 |   div x y
324 |       = case y == 0 of
325 |              False => prim__div_Bits32 x y
326 |   mod x y
327 |       = case y == 0 of
328 |              False => prim__mod_Bits32 x y
329 |
330 | -- Bits64
331 |
332 | %inline
333 | public export
334 | Num Bits64 where
335 |   (+) = prim__add_Bits64
336 |   (*) = prim__mul_Bits64
337 |   fromInteger = prim__cast_IntegerBits64
338 |
339 | %inline
340 | public export
341 | Neg Bits64 where
342 |   negate x = prim__sub_Bits64 0 x
343 |   (-) = prim__sub_Bits64
344 |
345 | public export
346 | Abs Bits64 where
347 |   abs x = if x < 0 then -x else x
348 |
349 | public export
350 | Integral Bits64 where
351 |   div x y
352 |       = case y == 0 of
353 |              False => prim__div_Bits64 x y
354 |   mod x y
355 |       = case y == 0 of
356 |              False => prim__mod_Bits64 x y
357 |
358 | -- Double
359 |
360 | public export
361 | Num Double where
362 |   (+) = prim__add_Double
363 |   (*) = prim__mul_Double
364 |   fromInteger = prim__cast_IntegerDouble
365 |
366 | %inline
367 | public export
368 | Neg Double where
369 |   negate x = prim__negate_Double x
370 |   (-) = prim__sub_Double
371 |
372 | public export
373 | Abs Double where
374 |   abs x = if x < 0 then -x else x
375 |
376 | public export
377 | Fractional Double where
378 |   (/) = prim__div_Double
379 |