0 | module Prelude.Cast
  1 |
  2 | import Prelude.Basics
  3 | import Prelude.Num
  4 | import Prelude.Types
  5 |
  6 | %default total
  7 |
  8 | -----------
  9 | -- CASTS --
 10 | -----------
 11 |
 12 | -- Casts between primitives only here.  They might be lossy.
 13 |
 14 | ||| Interface for transforming an instance of a data type to another type.
 15 | public export
 16 | interface Cast from to where
 17 |   constructor MkCast
 18 |   ||| Perform a (potentially lossy!) cast operation.
 19 |   ||| @ orig The original type
 20 |   cast : (orig : from) -> to
 21 |
 22 | export %inline
 23 | Cast a a where
 24 |   cast = id
 25 |
 26 | -- To String
 27 |
 28 | export %inline
 29 | Cast Int String where
 30 |   cast = prim__cast_IntString
 31 |
 32 | export %inline
 33 | Cast Integer String where
 34 |   cast = prim__cast_IntegerString
 35 |
 36 | export %inline
 37 | Cast Char String where
 38 |   cast = prim__cast_CharString
 39 |
 40 | export %inline
 41 | Cast Double String where
 42 |   cast = prim__cast_DoubleString
 43 |
 44 | export %inline
 45 | Cast Nat String where
 46 |   cast = cast . natToInteger
 47 |
 48 | export %inline
 49 | Cast Int8 String where
 50 |   cast = prim__cast_Int8String
 51 |
 52 | export %inline
 53 | Cast Int16 String where
 54 |   cast = prim__cast_Int16String
 55 |
 56 | export %inline
 57 | Cast Int32 String where
 58 |   cast = prim__cast_Int32String
 59 |
 60 | export %inline
 61 | Cast Int64 String where
 62 |   cast = prim__cast_Int64String
 63 |
 64 | export %inline
 65 | Cast Bits8 String where
 66 |   cast = prim__cast_Bits8String
 67 |
 68 | export %inline
 69 | Cast Bits16 String where
 70 |   cast = prim__cast_Bits16String
 71 |
 72 | export %inline
 73 | Cast Bits32 String where
 74 |   cast = prim__cast_Bits32String
 75 |
 76 | export %inline
 77 | Cast Bits64 String where
 78 |   cast = prim__cast_Bits64String
 79 |
 80 | -- To Integer
 81 |
 82 | export %inline
 83 | Cast Int Integer where
 84 |   cast = prim__cast_IntInteger
 85 |
 86 | export %inline
 87 | Cast Char Integer where
 88 |   cast = prim__cast_CharInteger
 89 |
 90 | export %inline
 91 | Cast Double Integer where
 92 |   cast = prim__cast_DoubleInteger
 93 |
 94 | export %inline
 95 | Cast String Integer where
 96 |   cast = prim__cast_StringInteger
 97 |
 98 | export %inline
 99 | Cast Nat Integer where
100 |   cast = natToInteger
101 |
102 | export %inline
103 | Cast Bits8 Integer where
104 |   cast = prim__cast_Bits8Integer
105 |
106 | export %inline
107 | Cast Bits16 Integer where
108 |   cast = prim__cast_Bits16Integer
109 |
110 | export %inline
111 | Cast Bits32 Integer where
112 |   cast = prim__cast_Bits32Integer
113 |
114 | export %inline
115 | Cast Bits64 Integer where
116 |   cast = prim__cast_Bits64Integer
117 |
118 | export %inline
119 | Cast Int8 Integer where
120 |   cast = prim__cast_Int8Integer
121 |
122 | export %inline
123 | Cast Int16 Integer where
124 |   cast = prim__cast_Int16Integer
125 |
126 | export %inline
127 | Cast Int32 Integer where
128 |   cast = prim__cast_Int32Integer
129 |
130 | export %inline
131 | Cast Int64 Integer where
132 |   cast = prim__cast_Int64Integer
133 |
134 | -- To Int
135 |
136 | export %inline
137 | Cast Integer Int where
138 |   cast = prim__cast_IntegerInt
139 |
140 | export %inline
141 | Cast Char Int where
142 |   cast = prim__cast_CharInt
143 |
144 | export %inline
145 | Cast Double Int where
146 |   cast = prim__cast_DoubleInt
147 |
148 | export %inline
149 | Cast String Int where
150 |   cast = prim__cast_StringInt
151 |
152 | export %inline
153 | Cast Nat Int where
154 |   cast = fromInteger . natToInteger
155 |
156 | export %inline
157 | Cast Bits8 Int where
158 |   cast = prim__cast_Bits8Int
159 |
160 | export %inline
161 | Cast Bits16 Int where
162 |   cast = prim__cast_Bits16Int
163 |
164 | export %inline
165 | Cast Bits32 Int where
166 |   cast = prim__cast_Bits32Int
167 |
168 | export %inline
169 | Cast Bits64 Int where
170 |   cast = prim__cast_Bits64Int
171 |
172 | export %inline
173 | Cast Int8 Int where
174 |   cast = prim__cast_Int8Int
175 |
176 | export %inline
177 | Cast Int16 Int where
178 |   cast = prim__cast_Int16Int
179 |
180 | export %inline
181 | Cast Int32 Int where
182 |   cast = prim__cast_Int32Int
183 |
184 | export %inline
185 | Cast Int64 Int where
186 |   cast = prim__cast_Int64Int
187 |
188 | -- To Char
189 |
190 | export %inline
191 | Cast Int Char where
192 |   cast = prim__cast_IntChar
193 |
194 | export %inline
195 | Cast Integer Char where
196 |   cast = prim__cast_IntegerChar
197 |
198 | export %inline
199 | Cast Nat Char where
200 |   cast = cast . natToInteger
201 |
202 | export %inline
203 | Cast Bits8 Char where
204 |   cast = prim__cast_Bits8Char
205 |
206 | export %inline
207 | Cast Bits16 Char where
208 |   cast = prim__cast_Bits16Char
209 |
210 | export %inline
211 | Cast Bits32 Char where
212 |   cast = prim__cast_Bits32Char
213 |
214 | export %inline
215 | Cast Bits64 Char where
216 |   cast = prim__cast_Bits64Char
217 |
218 | export %inline
219 | Cast Int8 Char where
220 |   cast = prim__cast_Int8Char
221 |
222 | export %inline
223 | Cast Int16 Char where
224 |   cast = prim__cast_Int16Char
225 |
226 | export %inline
227 | Cast Int32 Char where
228 |   cast = prim__cast_Int32Char
229 |
230 | export %inline
231 | Cast Int64 Char where
232 |   cast = prim__cast_Int64Char
233 |
234 | -- To Double
235 |
236 | export %inline
237 | Cast Int Double where
238 |   cast = prim__cast_IntDouble
239 |
240 | export %inline
241 | Cast Integer Double where
242 |   cast = prim__cast_IntegerDouble
243 |
244 | export %inline
245 | Cast String Double where
246 |   cast = prim__cast_StringDouble
247 |
248 | export %inline
249 | Cast Nat Double where
250 |   cast = prim__cast_IntegerDouble . natToInteger
251 |
252 | export %inline
253 | Cast Bits8 Double where
254 |   cast = prim__cast_Bits8Double
255 |
256 | export %inline
257 | Cast Bits16 Double where
258 |   cast = prim__cast_Bits16Double
259 |
260 | export %inline
261 | Cast Bits32 Double where
262 |   cast = prim__cast_Bits32Double
263 |
264 | export %inline
265 | Cast Bits64 Double where
266 |   cast = prim__cast_Bits64Double
267 |
268 | export %inline
269 | Cast Int8 Double where
270 |   cast = prim__cast_Int8Double
271 |
272 | export %inline
273 | Cast Int16 Double where
274 |   cast = prim__cast_Int16Double
275 |
276 | export %inline
277 | Cast Int32 Double where
278 |   cast = prim__cast_Int32Double
279 |
280 | export %inline
281 | Cast Int64 Double where
282 |   cast = prim__cast_Int64Double
283 |
284 |
285 | -- To Bits8
286 |
287 | export %inline
288 | Cast Int Bits8 where
289 |   cast = prim__cast_IntBits8
290 |
291 | export %inline
292 | Cast Integer Bits8 where
293 |   cast = prim__cast_IntegerBits8
294 |
295 | export %inline
296 | Cast Bits16 Bits8 where
297 |   cast = prim__cast_Bits16Bits8
298 |
299 | export %inline
300 | Cast Bits32 Bits8 where
301 |   cast = prim__cast_Bits32Bits8
302 |
303 | export %inline
304 | Cast Bits64 Bits8 where
305 |   cast = prim__cast_Bits64Bits8
306 |
307 | export %inline
308 | Cast String Bits8 where
309 |   cast = prim__cast_StringBits8
310 |
311 | export %inline
312 | Cast Double Bits8 where
313 |   cast = prim__cast_DoubleBits8
314 |
315 | export %inline
316 | Cast Char Bits8 where
317 |   cast = prim__cast_CharBits8
318 |
319 | export %inline
320 | Cast Nat Bits8 where
321 |   cast = cast . natToInteger
322 |
323 | export %inline
324 | Cast Int8 Bits8 where
325 |   cast = prim__cast_Int8Bits8
326 |
327 | export %inline
328 | Cast Int16 Bits8 where
329 |   cast = prim__cast_Int16Bits8
330 |
331 | export %inline
332 | Cast Int32 Bits8 where
333 |   cast = prim__cast_Int32Bits8
334 |
335 | export %inline
336 | Cast Int64 Bits8 where
337 |   cast = prim__cast_Int64Bits8
338 |
339 |
340 | -- To Bits16
341 |
342 | export %inline
343 | Cast Int Bits16 where
344 |   cast = prim__cast_IntBits16
345 |
346 | export %inline
347 | Cast Integer Bits16 where
348 |   cast = prim__cast_IntegerBits16
349 |
350 | export %inline
351 | Cast Bits8 Bits16 where
352 |   cast = prim__cast_Bits8Bits16
353 |
354 | export %inline
355 | Cast Bits32 Bits16 where
356 |   cast = prim__cast_Bits32Bits16
357 |
358 | export %inline
359 | Cast Bits64 Bits16 where
360 |   cast = prim__cast_Bits64Bits16
361 |
362 | export %inline
363 | Cast String Bits16 where
364 |   cast = prim__cast_StringBits16
365 |
366 | export %inline
367 | Cast Double Bits16 where
368 |   cast = prim__cast_DoubleBits16
369 |
370 | export %inline
371 | Cast Char Bits16 where
372 |   cast = prim__cast_CharBits16
373 |
374 | export %inline
375 | Cast Nat Bits16 where
376 |   cast = cast . natToInteger
377 |
378 | export %inline
379 | Cast Int8 Bits16 where
380 |   cast = prim__cast_Int8Bits16
381 |
382 | export %inline
383 | Cast Int16 Bits16 where
384 |   cast = prim__cast_Int16Bits16
385 |
386 | export %inline
387 | Cast Int32 Bits16 where
388 |   cast = prim__cast_Int32Bits16
389 |
390 | export %inline
391 | Cast Int64 Bits16 where
392 |   cast = prim__cast_Int64Bits16
393 |
394 |
395 | -- To Bits32
396 |
397 | export %inline
398 | Cast Int Bits32 where
399 |   cast = prim__cast_IntBits32
400 |
401 | export %inline
402 | Cast Integer Bits32 where
403 |   cast = prim__cast_IntegerBits32
404 |
405 | export %inline
406 | Cast Bits8 Bits32 where
407 |   cast = prim__cast_Bits8Bits32
408 |
409 | export %inline
410 | Cast Bits16 Bits32 where
411 |   cast = prim__cast_Bits16Bits32
412 |
413 | export %inline
414 | Cast Bits64 Bits32 where
415 |   cast = prim__cast_Bits64Bits32
416 |
417 | export %inline
418 | Cast String Bits32 where
419 |   cast = prim__cast_StringBits32
420 |
421 | export %inline
422 | Cast Double Bits32 where
423 |   cast = prim__cast_DoubleBits32
424 |
425 | export %inline
426 | Cast Char Bits32 where
427 |   cast = prim__cast_CharBits32
428 |
429 | export %inline
430 | Cast Nat Bits32 where
431 |   cast = cast . natToInteger
432 |
433 | export %inline
434 | Cast Int8 Bits32 where
435 |   cast = prim__cast_Int8Bits32
436 |
437 | export %inline
438 | Cast Int16 Bits32 where
439 |   cast = prim__cast_Int16Bits32
440 |
441 | export %inline
442 | Cast Int32 Bits32 where
443 |   cast = prim__cast_Int32Bits32
444 |
445 | export %inline
446 | Cast Int64 Bits32 where
447 |   cast = prim__cast_Int64Bits32
448 |
449 | -- To Bits64
450 |
451 | export %inline
452 | Cast Int Bits64 where
453 |   cast = prim__cast_IntBits64
454 |
455 | export %inline
456 | Cast Integer Bits64 where
457 |   cast = prim__cast_IntegerBits64
458 |
459 | export %inline
460 | Cast Bits8 Bits64 where
461 |   cast = prim__cast_Bits8Bits64
462 |
463 | export %inline
464 | Cast Bits16 Bits64 where
465 |   cast = prim__cast_Bits16Bits64
466 |
467 | export %inline
468 | Cast Bits32 Bits64 where
469 |   cast = prim__cast_Bits32Bits64
470 |
471 | export %inline
472 | Cast String Bits64 where
473 |   cast = prim__cast_StringBits64
474 |
475 | export %inline
476 | Cast Double Bits64 where
477 |   cast = prim__cast_DoubleBits64
478 |
479 | export %inline
480 | Cast Char Bits64 where
481 |   cast = prim__cast_CharBits64
482 |
483 | export %inline
484 | Cast Nat Bits64 where
485 |   cast = cast . natToInteger
486 |
487 | export %inline
488 | Cast Int8 Bits64 where
489 |   cast = prim__cast_Int8Bits64
490 |
491 | export %inline
492 | Cast Int16 Bits64 where
493 |   cast = prim__cast_Int16Bits64
494 |
495 | export %inline
496 | Cast Int32 Bits64 where
497 |   cast = prim__cast_Int32Bits64
498 |
499 | export %inline
500 | Cast Int64 Bits64 where
501 |   cast = prim__cast_Int64Bits64
502 |
503 | -- To Int8
504 |
505 | export %inline
506 | Cast String Int8 where
507 |   cast = prim__cast_StringInt8
508 |
509 | export %inline
510 | Cast Double Int8 where
511 |   cast = prim__cast_DoubleInt8
512 |
513 | export %inline
514 | Cast Char Int8 where
515 |   cast = prim__cast_CharInt8
516 |
517 | export %inline
518 | Cast Int Int8 where
519 |   cast = prim__cast_IntInt8
520 |
521 | export %inline
522 | Cast Integer Int8 where
523 |   cast = prim__cast_IntegerInt8
524 |
525 | export %inline
526 | Cast Nat Int8 where
527 |   cast = cast . natToInteger
528 |
529 | export %inline
530 | Cast Bits8 Int8 where
531 |   cast = prim__cast_Bits8Int8
532 |
533 | export %inline
534 | Cast Bits16 Int8 where
535 |   cast = prim__cast_Bits16Int8
536 |
537 | export %inline
538 | Cast Bits32 Int8 where
539 |   cast = prim__cast_Bits32Int8
540 |
541 | export %inline
542 | Cast Bits64 Int8 where
543 |   cast = prim__cast_Bits64Int8
544 |
545 | export %inline
546 | Cast Int16 Int8 where
547 |   cast = prim__cast_Int16Int8
548 |
549 | export %inline
550 | Cast Int32 Int8 where
551 |   cast = prim__cast_Int32Int8
552 |
553 | export %inline
554 | Cast Int64 Int8 where
555 |   cast = prim__cast_Int64Int8
556 |
557 | -- To Int16
558 |
559 | export %inline
560 | Cast String Int16 where
561 |   cast = prim__cast_StringInt16
562 |
563 | export %inline
564 | Cast Double Int16 where
565 |   cast = prim__cast_DoubleInt16
566 |
567 | export %inline
568 | Cast Char Int16 where
569 |   cast = prim__cast_CharInt16
570 |
571 | export %inline
572 | Cast Int Int16 where
573 |   cast = prim__cast_IntInt16
574 |
575 | export %inline
576 | Cast Integer Int16 where
577 |   cast = prim__cast_IntegerInt16
578 |
579 | export %inline
580 | Cast Nat Int16 where
581 |   cast = cast . natToInteger
582 |
583 | export %inline
584 | Cast Bits8 Int16 where
585 |   cast = prim__cast_Bits8Int16
586 |
587 | export %inline
588 | Cast Bits16 Int16 where
589 |   cast = prim__cast_Bits16Int16
590 |
591 | export %inline
592 | Cast Bits32 Int16 where
593 |   cast = prim__cast_Bits32Int16
594 |
595 | export %inline
596 | Cast Bits64 Int16 where
597 |   cast = prim__cast_Bits64Int16
598 |
599 | export %inline
600 | Cast Int8 Int16 where
601 |   cast = prim__cast_Int8Int16
602 |
603 | export %inline
604 | Cast Int32 Int16 where
605 |   cast = prim__cast_Int32Int16
606 |
607 | export %inline
608 | Cast Int64 Int16 where
609 |   cast = prim__cast_Int64Int16
610 |
611 | -- To Int32
612 |
613 | export %inline
614 | Cast String Int32 where
615 |   cast = prim__cast_StringInt32
616 |
617 | export %inline
618 | Cast Double Int32 where
619 |   cast = prim__cast_DoubleInt32
620 |
621 | export %inline
622 | Cast Char Int32 where
623 |   cast = prim__cast_CharInt32
624 |
625 | export %inline
626 | Cast Int Int32 where
627 |   cast = prim__cast_IntInt32
628 |
629 | export %inline
630 | Cast Integer Int32 where
631 |   cast = prim__cast_IntegerInt32
632 |
633 | export %inline
634 | Cast Nat Int32 where
635 |   cast = cast . natToInteger
636 |
637 | export %inline
638 | Cast Bits8 Int32 where
639 |   cast = prim__cast_Bits8Int32
640 |
641 | export %inline
642 | Cast Bits16 Int32 where
643 |   cast = prim__cast_Bits16Int32
644 |
645 | export %inline
646 | Cast Bits32 Int32 where
647 |   cast = prim__cast_Bits32Int32
648 |
649 | export %inline
650 | Cast Bits64 Int32 where
651 |   cast = prim__cast_Bits64Int32
652 |
653 | export %inline
654 | Cast Int8 Int32 where
655 |   cast = prim__cast_Int8Int32
656 |
657 | export %inline
658 | Cast Int16 Int32 where
659 |   cast = prim__cast_Int16Int32
660 |
661 | export %inline
662 | Cast Int64 Int32 where
663 |   cast = prim__cast_Int64Int32
664 |
665 | -- To Int64
666 |
667 | export %inline
668 | Cast String Int64 where
669 |   cast = prim__cast_StringInt64
670 |
671 | export %inline
672 | Cast Double Int64 where
673 |   cast = prim__cast_DoubleInt64
674 |
675 | export %inline
676 | Cast Char Int64 where
677 |   cast = prim__cast_CharInt64
678 |
679 | export %inline
680 | Cast Int Int64 where
681 |   cast = prim__cast_IntInt64
682 |
683 | export %inline
684 | Cast Integer Int64 where
685 |   cast = prim__cast_IntegerInt64
686 |
687 | export %inline
688 | Cast Nat Int64 where
689 |   cast = cast . natToInteger
690 |
691 | export %inline
692 | Cast Bits8 Int64 where
693 |   cast = prim__cast_Bits8Int64
694 |
695 | export %inline
696 | Cast Bits16 Int64 where
697 |   cast = prim__cast_Bits16Int64
698 |
699 | export %inline
700 | Cast Bits32 Int64 where
701 |   cast = prim__cast_Bits32Int64
702 |
703 | export %inline
704 | Cast Bits64 Int64 where
705 |   cast = prim__cast_Bits64Int64
706 |
707 | export %inline
708 | Cast Int8 Int64 where
709 |   cast = prim__cast_Int8Int64
710 |
711 | export %inline
712 | Cast Int16 Int64 where
713 |   cast = prim__cast_Int16Int64
714 |
715 | export %inline
716 | Cast Int32 Int64 where
717 |   cast = prim__cast_Int32Int64
718 |
719 | -- To Nat
720 |
721 | export %inline
722 | Cast String Nat where
723 |   cast = integerToNat . cast
724 |
725 | export %inline
726 | Cast Double Nat where
727 |   cast = integerToNat . cast
728 |
729 | export %inline
730 | Cast Char Nat where
731 |   cast = integerToNat . cast {to = Integer}
732 |
733 | export %inline
734 | Cast Int Nat where
735 |   cast = integerToNat . cast
736 |
737 | export %inline
738 | Cast Integer Nat where
739 |   cast = integerToNat
740 |
741 | export %inline
742 | Cast Bits8 Nat where
743 |   cast = integerToNat . cast {to = Integer}
744 |
745 | export %inline
746 | Cast Bits16 Nat where
747 |   cast = integerToNat . cast {to = Integer}
748 |
749 | export %inline
750 | Cast Bits32 Nat where
751 |   cast = integerToNat . cast {to = Integer}
752 |
753 | export %inline
754 | Cast Bits64 Nat where
755 |   cast = integerToNat . cast {to = Integer}
756 |
757 | export %inline
758 | Cast Int8 Nat where
759 |   cast = integerToNat . cast
760 |
761 | export %inline
762 | Cast Int16 Nat where
763 |   cast = integerToNat . cast
764 |
765 | export %inline
766 | Cast Int32 Nat where
767 |   cast = integerToNat . cast
768 |
769 | export %inline
770 | Cast Int64 Nat where
771 |   cast = integerToNat . cast
772 |