This file is indexed.

/usr/lib/ats2-postiats-0.1.3/prelude/DATS/integer.dats is in ats2-lang 0.1.3-1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)

(*
** Source:
** $PATSHOME/prelude/DATS/CODEGEN/integer.atxt
** Time of generation: Fri Sep 26 22:20:54 2014
*)

(* ****** ****** *)

(* Author: Hongwei Xi *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: May, 2012 *)

(* ****** ****** *)

#define ATS_DYNLOADFLAG 0 // no dynloading at run-time

(* ****** ****** *)
//
//
(* ****** ****** *)
//
staload UN = "prelude/SATS/unsafe.sats"
//
(* ****** ****** *)

implement
g0int2int<intknd,intknd> = g0int2int_int_int
implement
g0int2int<intknd,lintknd> = g0int2int_int_lint
implement
g0int2int<intknd,llintknd> = g0int2int_int_llint
implement
g0int2int<intknd,ssizeknd> = g0int2int_int_ssize

(* ****** ****** *)

implement g0int_neg<intknd> = g0int_neg_int
implement g0int_abs<intknd> = g0int_abs_int
implement g0int_succ<intknd> = g0int_succ_int
implement g0int_pred<intknd> = g0int_pred_int
implement g0int_half<intknd> = g0int_half_int
implement g0int_add<intknd> = g0int_add_int
implement g0int_sub<intknd> = g0int_sub_int
implement g0int_mul<intknd> = g0int_mul_int
implement g0int_div<intknd> = g0int_div_int
implement g0int_mod<intknd> = g0int_mod_int
implement g0int_asl<intknd> = g0int_asl_int
implement g0int_asr<intknd> = g0int_asr_int
implement g0int_isltz<intknd> = g0int_isltz_int
implement g0int_isltez<intknd> = g0int_isltez_int
implement g0int_isgtz<intknd> = g0int_isgtz_int
implement g0int_isgtez<intknd> = g0int_isgtez_int
implement g0int_iseqz<intknd> = g0int_iseqz_int
implement g0int_isneqz<intknd> = g0int_isneqz_int
implement g0int_lt<intknd> = g0int_lt_int
implement g0int_lte<intknd> = g0int_lte_int
implement g0int_gt<intknd> = g0int_gt_int
implement g0int_gte<intknd> = g0int_gte_int
implement g0int_eq<intknd> = g0int_eq_int
implement g0int_neq<intknd> = g0int_neq_int
implement g0int_compare<intknd> = g0int_compare_int
implement g0int_max<intknd> = g0int_max_int
implement g0int_min<intknd> = g0int_min_int
//
implement fprint_val<int> (out, x) = fprint_int (out, x)
//
implement g0int_neg<lintknd> = g0int_neg_lint
implement g0int_abs<lintknd> = g0int_abs_lint
implement g0int_succ<lintknd> = g0int_succ_lint
implement g0int_pred<lintknd> = g0int_pred_lint
implement g0int_half<lintknd> = g0int_half_lint
implement g0int_add<lintknd> = g0int_add_lint
implement g0int_sub<lintknd> = g0int_sub_lint
implement g0int_mul<lintknd> = g0int_mul_lint
implement g0int_div<lintknd> = g0int_div_lint
implement g0int_mod<lintknd> = g0int_mod_lint
implement g0int_asl<lintknd> = g0int_asl_lint
implement g0int_asr<lintknd> = g0int_asr_lint
implement g0int_isltz<lintknd> = g0int_isltz_lint
implement g0int_isltez<lintknd> = g0int_isltez_lint
implement g0int_isgtz<lintknd> = g0int_isgtz_lint
implement g0int_isgtez<lintknd> = g0int_isgtez_lint
implement g0int_iseqz<lintknd> = g0int_iseqz_lint
implement g0int_isneqz<lintknd> = g0int_isneqz_lint
implement g0int_lt<lintknd> = g0int_lt_lint
implement g0int_lte<lintknd> = g0int_lte_lint
implement g0int_gt<lintknd> = g0int_gt_lint
implement g0int_gte<lintknd> = g0int_gte_lint
implement g0int_eq<lintknd> = g0int_eq_lint
implement g0int_neq<lintknd> = g0int_neq_lint
implement g0int_compare<lintknd> = g0int_compare_lint
implement g0int_max<lintknd> = g0int_max_lint
implement g0int_min<lintknd> = g0int_min_lint
//
implement fprint_val<lint> (out, x) = fprint_lint (out, x)
//
implement g0int_neg<llintknd> = g0int_neg_llint
implement g0int_abs<llintknd> = g0int_abs_llint
implement g0int_succ<llintknd> = g0int_succ_llint
implement g0int_pred<llintknd> = g0int_pred_llint
implement g0int_half<llintknd> = g0int_half_llint
implement g0int_add<llintknd> = g0int_add_llint
implement g0int_sub<llintknd> = g0int_sub_llint
implement g0int_mul<llintknd> = g0int_mul_llint
implement g0int_div<llintknd> = g0int_div_llint
implement g0int_mod<llintknd> = g0int_mod_llint
implement g0int_asl<llintknd> = g0int_asl_llint
implement g0int_asr<llintknd> = g0int_asr_llint
implement g0int_isltz<llintknd> = g0int_isltz_llint
implement g0int_isltez<llintknd> = g0int_isltez_llint
implement g0int_isgtz<llintknd> = g0int_isgtz_llint
implement g0int_isgtez<llintknd> = g0int_isgtez_llint
implement g0int_iseqz<llintknd> = g0int_iseqz_llint
implement g0int_isneqz<llintknd> = g0int_isneqz_llint
implement g0int_lt<llintknd> = g0int_lt_llint
implement g0int_lte<llintknd> = g0int_lte_llint
implement g0int_gt<llintknd> = g0int_gt_llint
implement g0int_gte<llintknd> = g0int_gte_llint
implement g0int_eq<llintknd> = g0int_eq_llint
implement g0int_neq<llintknd> = g0int_neq_llint
implement g0int_compare<llintknd> = g0int_compare_llint
implement g0int_max<llintknd> = g0int_max_llint
implement g0int_min<llintknd> = g0int_min_llint
//
implement fprint_val<llint> (out, x) = fprint_llint (out, x)
//
implement g0int_neg<ssizeknd> = g0int_neg_ssize
implement g0int_abs<ssizeknd> = g0int_abs_ssize
implement g0int_succ<ssizeknd> = g0int_succ_ssize
implement g0int_pred<ssizeknd> = g0int_pred_ssize
implement g0int_half<ssizeknd> = g0int_half_ssize
implement g0int_add<ssizeknd> = g0int_add_ssize
implement g0int_sub<ssizeknd> = g0int_sub_ssize
implement g0int_mul<ssizeknd> = g0int_mul_ssize
implement g0int_div<ssizeknd> = g0int_div_ssize
implement g0int_mod<ssizeknd> = g0int_mod_ssize
implement g0int_asl<ssizeknd> = g0int_asl_ssize
implement g0int_asr<ssizeknd> = g0int_asr_ssize
implement g0int_isltz<ssizeknd> = g0int_isltz_ssize
implement g0int_isltez<ssizeknd> = g0int_isltez_ssize
implement g0int_isgtz<ssizeknd> = g0int_isgtz_ssize
implement g0int_isgtez<ssizeknd> = g0int_isgtez_ssize
implement g0int_iseqz<ssizeknd> = g0int_iseqz_ssize
implement g0int_isneqz<ssizeknd> = g0int_isneqz_ssize
implement g0int_lt<ssizeknd> = g0int_lt_ssize
implement g0int_lte<ssizeknd> = g0int_lte_ssize
implement g0int_gt<ssizeknd> = g0int_gt_ssize
implement g0int_gte<ssizeknd> = g0int_gte_ssize
implement g0int_eq<ssizeknd> = g0int_eq_ssize
implement g0int_neq<ssizeknd> = g0int_neq_ssize
implement g0int_compare<ssizeknd> = g0int_compare_ssize
implement g0int_max<ssizeknd> = g0int_max_ssize
implement g0int_min<ssizeknd> = g0int_min_ssize
//
implement fprint_val<ssize_t> (out, x) = fprint_ssize (out, x)
//
(* ****** ****** *)

implement{} mul_int1_size0 (i, j) = i2sz(i) * j
implement{} mul_size0_int1 (i, j) = i * i2sz(j)

(* ****** ****** *)

implement
g1int2int<intknd,intknd> = g1int2int_int_int
implement
g1int2int<intknd,lintknd> = g1int2int_int_lint
implement
g1int2int<intknd,llintknd> = g1int2int_int_llint
implement
g1int2int<intknd,ssizeknd> = g1int2int_int_ssize

(* ****** ****** *)

implement g1int_neg<intknd> = g1int_neg_int
implement g1int_abs<intknd> = g1int_abs_int
implement g1int_succ<intknd> = g1int_succ_int
implement g1int_pred<intknd> = g1int_pred_int
implement g1int_half<intknd> = g1int_half_int
implement g1int_add<intknd> = g1int_add_int
implement g1int_sub<intknd> = g1int_sub_int
implement g1int_mul<intknd> = g1int_mul_int
implement g1int_div<intknd> = g1int_div_int
implement g1int_nmod<intknd> = g1int_nmod_int
implement g1int_isltz<intknd> = g1int_isltz_int
implement g1int_isltez<intknd> = g1int_isltez_int
implement g1int_isgtz<intknd> = g1int_isgtz_int
implement g1int_isgtez<intknd> = g1int_isgtez_int
implement g1int_iseqz<intknd> = g1int_iseqz_int
implement g1int_isneqz<intknd> = g1int_isneqz_int
implement g1int_lt<intknd> = g1int_lt_int
implement g1int_lte<intknd> = g1int_lte_int
implement g1int_gt<intknd> = g1int_gt_int
implement g1int_gte<intknd> = g1int_gte_int
implement g1int_eq<intknd> = g1int_eq_int
implement g1int_neq<intknd> = g1int_neq_int
implement g1int_compare<intknd> = g1int_compare_int
implement g1int_max<intknd> = g1int_max_int
implement g1int_min<intknd> = g1int_min_int
//
implement g1int_neg<lintknd> = g1int_neg_lint
implement g1int_abs<lintknd> = g1int_abs_lint
implement g1int_succ<lintknd> = g1int_succ_lint
implement g1int_pred<lintknd> = g1int_pred_lint
implement g1int_half<lintknd> = g1int_half_lint
implement g1int_add<lintknd> = g1int_add_lint
implement g1int_sub<lintknd> = g1int_sub_lint
implement g1int_mul<lintknd> = g1int_mul_lint
implement g1int_div<lintknd> = g1int_div_lint
implement g1int_nmod<lintknd> = g1int_nmod_lint
implement g1int_isltz<lintknd> = g1int_isltz_lint
implement g1int_isltez<lintknd> = g1int_isltez_lint
implement g1int_isgtz<lintknd> = g1int_isgtz_lint
implement g1int_isgtez<lintknd> = g1int_isgtez_lint
implement g1int_iseqz<lintknd> = g1int_iseqz_lint
implement g1int_isneqz<lintknd> = g1int_isneqz_lint
implement g1int_lt<lintknd> = g1int_lt_lint
implement g1int_lte<lintknd> = g1int_lte_lint
implement g1int_gt<lintknd> = g1int_gt_lint
implement g1int_gte<lintknd> = g1int_gte_lint
implement g1int_eq<lintknd> = g1int_eq_lint
implement g1int_neq<lintknd> = g1int_neq_lint
implement g1int_compare<lintknd> = g1int_compare_lint
implement g1int_max<lintknd> = g1int_max_lint
implement g1int_min<lintknd> = g1int_min_lint
//
implement g1int_neg<llintknd> = g1int_neg_llint
implement g1int_abs<llintknd> = g1int_abs_llint
implement g1int_succ<llintknd> = g1int_succ_llint
implement g1int_pred<llintknd> = g1int_pred_llint
implement g1int_half<llintknd> = g1int_half_llint
implement g1int_add<llintknd> = g1int_add_llint
implement g1int_sub<llintknd> = g1int_sub_llint
implement g1int_mul<llintknd> = g1int_mul_llint
implement g1int_div<llintknd> = g1int_div_llint
implement g1int_nmod<llintknd> = g1int_nmod_llint
implement g1int_isltz<llintknd> = g1int_isltz_llint
implement g1int_isltez<llintknd> = g1int_isltez_llint
implement g1int_isgtz<llintknd> = g1int_isgtz_llint
implement g1int_isgtez<llintknd> = g1int_isgtez_llint
implement g1int_iseqz<llintknd> = g1int_iseqz_llint
implement g1int_isneqz<llintknd> = g1int_isneqz_llint
implement g1int_lt<llintknd> = g1int_lt_llint
implement g1int_lte<llintknd> = g1int_lte_llint
implement g1int_gt<llintknd> = g1int_gt_llint
implement g1int_gte<llintknd> = g1int_gte_llint
implement g1int_eq<llintknd> = g1int_eq_llint
implement g1int_neq<llintknd> = g1int_neq_llint
implement g1int_compare<llintknd> = g1int_compare_llint
implement g1int_max<llintknd> = g1int_max_llint
implement g1int_min<llintknd> = g1int_min_llint
//
implement g1int_neg<ssizeknd> = g1int_neg_ssize
implement g1int_abs<ssizeknd> = g1int_abs_ssize
implement g1int_succ<ssizeknd> = g1int_succ_ssize
implement g1int_pred<ssizeknd> = g1int_pred_ssize
implement g1int_half<ssizeknd> = g1int_half_ssize
implement g1int_add<ssizeknd> = g1int_add_ssize
implement g1int_sub<ssizeknd> = g1int_sub_ssize
implement g1int_mul<ssizeknd> = g1int_mul_ssize
implement g1int_div<ssizeknd> = g1int_div_ssize
implement g1int_nmod<ssizeknd> = g1int_nmod_ssize
implement g1int_isltz<ssizeknd> = g1int_isltz_ssize
implement g1int_isltez<ssizeknd> = g1int_isltez_ssize
implement g1int_isgtz<ssizeknd> = g1int_isgtz_ssize
implement g1int_isgtez<ssizeknd> = g1int_isgtez_ssize
implement g1int_iseqz<ssizeknd> = g1int_iseqz_ssize
implement g1int_isneqz<ssizeknd> = g1int_isneqz_ssize
implement g1int_lt<ssizeknd> = g1int_lt_ssize
implement g1int_lte<ssizeknd> = g1int_lte_ssize
implement g1int_gt<ssizeknd> = g1int_gt_ssize
implement g1int_gte<ssizeknd> = g1int_gte_ssize
implement g1int_eq<ssizeknd> = g1int_eq_ssize
implement g1int_neq<ssizeknd> = g1int_neq_ssize
implement g1int_compare<ssizeknd> = g1int_compare_ssize
implement g1int_max<ssizeknd> = g1int_max_ssize
implement g1int_min<ssizeknd> = g1int_min_ssize
//
(* ****** ****** *)

implement{tk}
g1int_sgn (x) = compare_g1int_int<tk> (x, 0)

(* ****** ****** *)
//
implement{
} add_size1_int1
  {i,j}(i, j) = $UN.cast{size_t(i+j)}(i+g0i2u(j))
implement{
} add_int1_size1
  {i,j}(i, j) = $UN.cast{size_t(i+j)}(g0i2u(i)+j)
//
implement{
} sub_size1_int1
  {i,j}(i, j) = $UN.cast{size_t(i-j)}(i-g0i2u(j))
//
(* ****** ****** *)

implement{tk}
g1int_mul2 {i,j} (x, y) = let
  prval pf = mul_make {i,j} () in (pf | g1int_mul<tk> (x, y))
end // end of [let] // end of [g1int_mul2]

(* ****** ****** *)
//
implement{
} mul_int1_size1
  {i,j}(i, j) = $UN.cast{size_t(i*j)}(g0i2u(i)*j)
implement{
} mul_size1_int1
  {i,j}(i, j) = $UN.cast{size_t(i*j)}(i*g0i2u(j))
//
(* ****** ****** *)

implement{tk}
g1int_ndiv {i,j} (x, y) = let
  val q = g1int_div (x, y) in $UN.cast{g1int(tk,ndiv(i,j))}(q)
end // end of [let] // end of [g1int_ndiv]

(* ****** ****** *)

implement{tk}
g1int_ndiv2 {i,j} (x, y) = let
  val [q:int] q = g1int_div (x, y)
  prval [q2:int,r:int] pf = divmod_istot{i,j}()
  prval EQINT() = $UN.castview0{EQINT(q,q2)}(0)
in
  (pf | q)
end // end of [let] // end of [g1int_ndiv2]

(* ****** ****** *)

implement{tk}
g1int_nmod2 {i,j} (x, y) = let
  val [r:int] r = g1int_nmod (x, y)
  prval [q:int,r2:int] pf = divmod_istot{i,j}()
  prval EQINT() = $UN.castview0{EQINT(r,r2)}(0)
in
  (pf | r)
end // end of [let] // end of [g1int_nmod2]

(* ****** ****** *)

implement
nmod_g1int_int1<intknd> (x, y) = g1i2i(g1int_nmod (x, g1i2i(y)))
implement
nmod_g1int_int1<lintknd> (x, y) = g1i2i(g1int_nmod (x, g1i2i(y)))
implement
nmod_g1int_int1<llintknd> (x, y) = g1i2i(g1int_nmod (x, g1i2i(y)))

(* ****** ****** *)

implement{tk}
g1int_ngcd (x, y) = let
//
fun loop{i,j:nat} .<j>.
(
  x: g1int (tk, i), y: g1int (tk, j)
) :<> [r:nat] g1int (tk, r) = let
in
//
if y > 0 then loop (y, g1int_nmod (x, y)) else x
//
end // end of [loop]
//
in
  loop (x, y)
end // end of [g1int_ngcd]

(* ****** ****** *)
//
// HX: int -> uint
//
implement
g0int2uint<intknd,uintknd> = g0int2uint_int_uint
implement
g0int2uint<intknd,ulintknd> = g0int2uint_int_ulint
implement
g0int2uint<intknd,ullintknd> = g0int2uint_int_ullint
implement
g0int2uint<intknd,sizeknd> = g0int2uint_int_size
//
implement
g0int2uint<lintknd,ulintknd> = g0int2uint_lint_ulint
implement
g0int2uint<lintknd,ullintknd> = g0int2uint_lint_ullint
implement
g0int2uint<lintknd,sizeknd> = g0int2uint_lint_size
//
implement
g0int2uint<llintknd,ullintknd> = g0int2uint_llint_ullint
//
implement
g0int2uint<ssizeknd,sizeknd> = g0int2uint_ssize_size

(* ****** ****** *)
//
// HX: uint -> int
//
implement
g0uint2int<uintknd,intknd> = g0uint2int_uint_int
implement
g0uint2int<uintknd,lintknd> = g0uint2int_uint_lint
implement
g0uint2int<uintknd,llintknd> = g0uint2int_uint_llint
implement
g0uint2int<uintknd,ssizeknd> = g0uint2int_uint_ssize
//
implement
g0uint2int<sizeknd,intknd> = g0uint2int_size_int
implement
g0uint2int<sizeknd,lintknd> = g0uint2int_size_lint
implement
g0uint2int<sizeknd,llintknd> = g0uint2int_size_llint
implement
g0uint2int<sizeknd,ssizeknd> = g0uint2int_size_ssize
//
(* ****** ****** *)
//
// HX: uint -> uint
//
implement
g0uint2uint<uintknd,uintknd> = g0uint2uint_uint_uint
implement
g0uint2uint<uintknd,ulintknd> = g0uint2uint_uint_ulint
implement
g0uint2uint<uintknd,ullintknd> = g0uint2uint_uint_ullint
implement
g0uint2uint<uintknd,sizeknd> = g0uint2uint_uint_size

(* ****** ****** *)

implement
g0uint2uint<sizeknd,ulintknd> = g0uint2uint_size_ulint
implement
g0uint2uint<sizeknd,ullintknd> = g0uint2uint_size_ullint
implement
g0uint2uint<sizeknd,sizeknd> = g0uint2uint_size_size

(* ****** ****** *)

implement g0uint_succ<uintknd> = g0uint_succ_uint
implement g0uint_pred<uintknd> = g0uint_pred_uint
implement g0uint_half<uintknd> = g0uint_half_uint
implement g0uint_add<uintknd> = g0uint_add_uint
implement g0uint_sub<uintknd> = g0uint_sub_uint
implement g0uint_mul<uintknd> = g0uint_mul_uint
implement g0uint_div<uintknd> = g0uint_div_uint
implement g0uint_mod<uintknd> = g0uint_mod_uint
implement g0uint_lsl<uintknd> = g0uint_lsl_uint
implement g0uint_lsr<uintknd> = g0uint_lsr_uint
implement g0uint_lnot<uintknd> = g0uint_lnot_uint
implement g0uint_lor<uintknd> = g0uint_lor_uint
implement g0uint_lxor<uintknd> = g0uint_lxor_uint
implement g0uint_land<uintknd> = g0uint_land_uint
implement g0uint_isgtz<uintknd> = g0uint_isgtz_uint
implement g0uint_iseqz<uintknd> = g0uint_iseqz_uint
implement g0uint_isneqz<uintknd> = g0uint_isneqz_uint
implement g0uint_lt<uintknd> = g0uint_lt_uint
implement g0uint_lte<uintknd> = g0uint_lte_uint
implement g0uint_gt<uintknd> = g0uint_gt_uint
implement g0uint_gte<uintknd> = g0uint_gte_uint
implement g0uint_eq<uintknd> = g0uint_eq_uint
implement g0uint_neq<uintknd> = g0uint_neq_uint
implement g0uint_compare<uintknd> = g0uint_compare_uint
implement g0uint_max<uintknd> = g0uint_max_uint
implement g0uint_min<uintknd> = g0uint_min_uint
//
implement fprint_val<uint> (out, x) = fprint_uint (out, x)
//
implement g0uint_succ<ulintknd> = g0uint_succ_ulint
implement g0uint_pred<ulintknd> = g0uint_pred_ulint
implement g0uint_half<ulintknd> = g0uint_half_ulint
implement g0uint_add<ulintknd> = g0uint_add_ulint
implement g0uint_sub<ulintknd> = g0uint_sub_ulint
implement g0uint_mul<ulintknd> = g0uint_mul_ulint
implement g0uint_div<ulintknd> = g0uint_div_ulint
implement g0uint_mod<ulintknd> = g0uint_mod_ulint
implement g0uint_lsl<ulintknd> = g0uint_lsl_ulint
implement g0uint_lsr<ulintknd> = g0uint_lsr_ulint
implement g0uint_lnot<ulintknd> = g0uint_lnot_ulint
implement g0uint_lor<ulintknd> = g0uint_lor_ulint
implement g0uint_lxor<ulintknd> = g0uint_lxor_ulint
implement g0uint_land<ulintknd> = g0uint_land_ulint
implement g0uint_isgtz<ulintknd> = g0uint_isgtz_ulint
implement g0uint_iseqz<ulintknd> = g0uint_iseqz_ulint
implement g0uint_isneqz<ulintknd> = g0uint_isneqz_ulint
implement g0uint_lt<ulintknd> = g0uint_lt_ulint
implement g0uint_lte<ulintknd> = g0uint_lte_ulint
implement g0uint_gt<ulintknd> = g0uint_gt_ulint
implement g0uint_gte<ulintknd> = g0uint_gte_ulint
implement g0uint_eq<ulintknd> = g0uint_eq_ulint
implement g0uint_neq<ulintknd> = g0uint_neq_ulint
implement g0uint_compare<ulintknd> = g0uint_compare_ulint
implement g0uint_max<ulintknd> = g0uint_max_ulint
implement g0uint_min<ulintknd> = g0uint_min_ulint
//
implement fprint_val<ulint> (out, x) = fprint_ulint (out, x)
//
implement g0uint_succ<ullintknd> = g0uint_succ_ullint
implement g0uint_pred<ullintknd> = g0uint_pred_ullint
implement g0uint_half<ullintknd> = g0uint_half_ullint
implement g0uint_add<ullintknd> = g0uint_add_ullint
implement g0uint_sub<ullintknd> = g0uint_sub_ullint
implement g0uint_mul<ullintknd> = g0uint_mul_ullint
implement g0uint_div<ullintknd> = g0uint_div_ullint
implement g0uint_mod<ullintknd> = g0uint_mod_ullint
implement g0uint_lsl<ullintknd> = g0uint_lsl_ullint
implement g0uint_lsr<ullintknd> = g0uint_lsr_ullint
implement g0uint_lnot<ullintknd> = g0uint_lnot_ullint
implement g0uint_lor<ullintknd> = g0uint_lor_ullint
implement g0uint_lxor<ullintknd> = g0uint_lxor_ullint
implement g0uint_land<ullintknd> = g0uint_land_ullint
implement g0uint_isgtz<ullintknd> = g0uint_isgtz_ullint
implement g0uint_iseqz<ullintknd> = g0uint_iseqz_ullint
implement g0uint_isneqz<ullintknd> = g0uint_isneqz_ullint
implement g0uint_lt<ullintknd> = g0uint_lt_ullint
implement g0uint_lte<ullintknd> = g0uint_lte_ullint
implement g0uint_gt<ullintknd> = g0uint_gt_ullint
implement g0uint_gte<ullintknd> = g0uint_gte_ullint
implement g0uint_eq<ullintknd> = g0uint_eq_ullint
implement g0uint_neq<ullintknd> = g0uint_neq_ullint
implement g0uint_compare<ullintknd> = g0uint_compare_ullint
implement g0uint_max<ullintknd> = g0uint_max_ullint
implement g0uint_min<ullintknd> = g0uint_min_ullint
//
implement fprint_val<ullint> (out, x) = fprint_ullint (out, x)
//
implement g0uint_succ<sizeknd> = g0uint_succ_size
implement g0uint_pred<sizeknd> = g0uint_pred_size
implement g0uint_half<sizeknd> = g0uint_half_size
implement g0uint_add<sizeknd> = g0uint_add_size
implement g0uint_sub<sizeknd> = g0uint_sub_size
implement g0uint_mul<sizeknd> = g0uint_mul_size
implement g0uint_div<sizeknd> = g0uint_div_size
implement g0uint_mod<sizeknd> = g0uint_mod_size
implement g0uint_lsl<sizeknd> = g0uint_lsl_size
implement g0uint_lsr<sizeknd> = g0uint_lsr_size
implement g0uint_lnot<sizeknd> = g0uint_lnot_size
implement g0uint_lor<sizeknd> = g0uint_lor_size
implement g0uint_lxor<sizeknd> = g0uint_lxor_size
implement g0uint_land<sizeknd> = g0uint_land_size
implement g0uint_isgtz<sizeknd> = g0uint_isgtz_size
implement g0uint_iseqz<sizeknd> = g0uint_iseqz_size
implement g0uint_isneqz<sizeknd> = g0uint_isneqz_size
implement g0uint_lt<sizeknd> = g0uint_lt_size
implement g0uint_lte<sizeknd> = g0uint_lte_size
implement g0uint_gt<sizeknd> = g0uint_gt_size
implement g0uint_gte<sizeknd> = g0uint_gte_size
implement g0uint_eq<sizeknd> = g0uint_eq_size
implement g0uint_neq<sizeknd> = g0uint_neq_size
implement g0uint_compare<sizeknd> = g0uint_compare_size
implement g0uint_max<sizeknd> = g0uint_max_size
implement g0uint_min<sizeknd> = g0uint_min_size
//
implement fprint_val<size_t> (out, x) = fprint_size (out, x)
//
(* ****** ****** *)
//
// HX: int -> uint
//
implement
g1int2uint<intknd,uintknd> = g1int2uint_int_uint
implement
g1int2uint<intknd,ulintknd> = g1int2uint_int_ulint
implement
g1int2uint<intknd,ullintknd> = g1int2uint_int_ullint
implement
g1int2uint<intknd,sizeknd> = g1int2uint_int_size
//
implement
g1int2uint<ssizeknd,sizeknd> = g1int2uint_ssize_size

(* ****** ****** *)
//
// HX: uint -> int
//
implement
g1uint2int<uintknd,intknd> = g1uint2int_uint_int
implement
g1uint2int<uintknd,lintknd> = g1uint2int_uint_lint
implement
g1uint2int<uintknd,llintknd> = g1uint2int_uint_llint
implement
g1uint2int<uintknd,ssizeknd> = g1uint2int_uint_ssize
//
implement
g1uint2int<sizeknd,intknd> = g1uint2int_size_int
implement
g1uint2int<sizeknd,lintknd> = g1uint2int_size_lint
implement
g1uint2int<sizeknd,llintknd> = g1uint2int_size_llint
implement
g1uint2int<sizeknd,ssizeknd> = g1uint2int_size_ssize

(* ****** ****** *)
//
// HX: uint -> uint
//
implement
g1uint2uint<uintknd,uintknd> = g1uint2uint_uint_uint
implement
g1uint2uint<uintknd,ulintknd> = g1uint2uint_uint_ulint
implement
g1uint2uint<uintknd,ullintknd> = g1uint2uint_uint_ullint
implement
g1uint2uint<uintknd,sizeknd> = g1uint2uint_uint_size
//
implement
g1uint2uint<sizeknd,uintknd> = g1uint2uint_size_uint
implement
g1uint2uint<sizeknd,ulintknd> = g1uint2uint_size_ulint
implement
g1uint2uint<sizeknd,ullintknd> = g1uint2uint_size_ullint
implement
g1uint2uint<sizeknd,sizeknd> = g1uint2uint_size_size

(* ****** ****** *)

implement g1uint_succ<uintknd> = g1uint_succ_uint
implement g1uint_pred<uintknd> = g1uint_pred_uint
implement g1uint_half<uintknd> = g1uint_half_uint
implement g1uint_add<uintknd> = g1uint_add_uint
implement g1uint_sub<uintknd> = g1uint_sub_uint
implement g1uint_mul<uintknd> = g1uint_mul_uint
implement g1uint_div<uintknd> = g1uint_div_uint
implement g1uint_mod<uintknd> = g1uint_mod_uint
implement g1uint_isgtz<uintknd> = g1uint_isgtz_uint
implement g1uint_iseqz<uintknd> = g1uint_iseqz_uint
implement g1uint_isneqz<uintknd> = g1uint_isneqz_uint
implement g1uint_lt<uintknd> = g1uint_lt_uint
implement g1uint_lte<uintknd> = g1uint_lte_uint
implement g1uint_gt<uintknd> = g1uint_gt_uint
implement g1uint_gte<uintknd> = g1uint_gte_uint
implement g1uint_eq<uintknd> = g1uint_eq_uint
implement g1uint_neq<uintknd> = g1uint_neq_uint
implement g1uint_compare<uintknd> = g1uint_compare_uint
implement g1uint_max<uintknd> = g1uint_max_uint
implement g1uint_min<uintknd> = g1uint_min_uint
//
implement g1uint_succ<ulintknd> = g1uint_succ_ulint
implement g1uint_pred<ulintknd> = g1uint_pred_ulint
implement g1uint_half<ulintknd> = g1uint_half_ulint
implement g1uint_add<ulintknd> = g1uint_add_ulint
implement g1uint_sub<ulintknd> = g1uint_sub_ulint
implement g1uint_mul<ulintknd> = g1uint_mul_ulint
implement g1uint_div<ulintknd> = g1uint_div_ulint
implement g1uint_mod<ulintknd> = g1uint_mod_ulint
implement g1uint_isgtz<ulintknd> = g1uint_isgtz_ulint
implement g1uint_iseqz<ulintknd> = g1uint_iseqz_ulint
implement g1uint_isneqz<ulintknd> = g1uint_isneqz_ulint
implement g1uint_lt<ulintknd> = g1uint_lt_ulint
implement g1uint_lte<ulintknd> = g1uint_lte_ulint
implement g1uint_gt<ulintknd> = g1uint_gt_ulint
implement g1uint_gte<ulintknd> = g1uint_gte_ulint
implement g1uint_eq<ulintknd> = g1uint_eq_ulint
implement g1uint_neq<ulintknd> = g1uint_neq_ulint
implement g1uint_compare<ulintknd> = g1uint_compare_ulint
implement g1uint_max<ulintknd> = g1uint_max_ulint
implement g1uint_min<ulintknd> = g1uint_min_ulint
//
implement g1uint_succ<ullintknd> = g1uint_succ_ullint
implement g1uint_pred<ullintknd> = g1uint_pred_ullint
implement g1uint_half<ullintknd> = g1uint_half_ullint
implement g1uint_add<ullintknd> = g1uint_add_ullint
implement g1uint_sub<ullintknd> = g1uint_sub_ullint
implement g1uint_mul<ullintknd> = g1uint_mul_ullint
implement g1uint_div<ullintknd> = g1uint_div_ullint
implement g1uint_mod<ullintknd> = g1uint_mod_ullint
implement g1uint_isgtz<ullintknd> = g1uint_isgtz_ullint
implement g1uint_iseqz<ullintknd> = g1uint_iseqz_ullint
implement g1uint_isneqz<ullintknd> = g1uint_isneqz_ullint
implement g1uint_lt<ullintknd> = g1uint_lt_ullint
implement g1uint_lte<ullintknd> = g1uint_lte_ullint
implement g1uint_gt<ullintknd> = g1uint_gt_ullint
implement g1uint_gte<ullintknd> = g1uint_gte_ullint
implement g1uint_eq<ullintknd> = g1uint_eq_ullint
implement g1uint_neq<ullintknd> = g1uint_neq_ullint
implement g1uint_compare<ullintknd> = g1uint_compare_ullint
implement g1uint_max<ullintknd> = g1uint_max_ullint
implement g1uint_min<ullintknd> = g1uint_min_ullint
//
implement g1uint_succ<sizeknd> = g1uint_succ_size
implement g1uint_pred<sizeknd> = g1uint_pred_size
implement g1uint_half<sizeknd> = g1uint_half_size
implement g1uint_add<sizeknd> = g1uint_add_size
implement g1uint_sub<sizeknd> = g1uint_sub_size
implement g1uint_mul<sizeknd> = g1uint_mul_size
implement g1uint_div<sizeknd> = g1uint_div_size
implement g1uint_mod<sizeknd> = g1uint_mod_size
implement g1uint_isgtz<sizeknd> = g1uint_isgtz_size
implement g1uint_iseqz<sizeknd> = g1uint_iseqz_size
implement g1uint_isneqz<sizeknd> = g1uint_isneqz_size
implement g1uint_lt<sizeknd> = g1uint_lt_size
implement g1uint_lte<sizeknd> = g1uint_lte_size
implement g1uint_gt<sizeknd> = g1uint_gt_size
implement g1uint_gte<sizeknd> = g1uint_gte_size
implement g1uint_eq<sizeknd> = g1uint_eq_size
implement g1uint_neq<sizeknd> = g1uint_neq_size
implement g1uint_compare<sizeknd> = g1uint_compare_size
implement g1uint_max<sizeknd> = g1uint_max_size
implement g1uint_min<sizeknd> = g1uint_min_size
//
(* ****** ****** *)

implement
{tk}(*tmp*)
g1uint_div2 {i,j} (x, y) = let
//
  prval () = lemma_g1uint_param (x)
//
  val [q:int] q = g1uint_div (x, y)
  prval [q2:int,r:int] pf = divmod_istot{i,j}()
  prval EQINT() = $UN.castview0{EQINT(q,q2)}(0)
in
  (pf | q)
end // end of [let] // end of [g1uint_div2]

(* ****** ****** *)

implement
{tk}(*tmp*)
g1uint_mod2 {i,j} (x, y) = let
//
  prval () = lemma_g1uint_param (x)
//
  val [r:int] r = g1uint_mod (x, y)
  prval [q:int,r2:int] pf = divmod_istot{i,j}()
  prval EQINT() = $UN.castview0{EQINT(r,r2)}(0)
in
  (pf | r)
end // end of [let] // end of [g1uint_mod2]

(* ****** ****** *)
//
implement g0int2string<intknd> = g0int2string_int
implement g0int2string<lintknd> = g0int2string_lint
implement g0int2string<llintknd> = g0int2string_llint
(*
implement g0int2string<ssizeknd> = g0int2string_ssize
*)
//
(* ****** ****** *)
//
implement g0string2int<intknd> = g0string2int_int
implement g0string2int<lintknd> = g0string2int_lint
implement g0string2int<llintknd> = g0string2int_llint
implement g0string2int<ssizeknd> = g0string2int_ssize
//
implement g0string2uint<uintknd> = g0string2uint_uint
implement g0string2uint<ulintknd> = g0string2uint_ulint
implement g0string2uint<ullintknd> = g0string2uint_ullint
implement g0string2uint<sizeknd> = g0string2uint_size
//
(* ****** ****** *)

implement{tk}
g1string2int (str) = g1ofg0_int (g0string2int<tk> (str))
implement{tk}
g1string2uint (str) = g1ofg0_uint (g0string2uint<tk> (str))

(* ****** ****** *)

implement{tk}
lt_g0int_int (x, y) = g0int_lt<tk> (x, g0int2int (y))
implement{tk}
lte_g0int_int (x, y) = g0int_lte<tk> (x, g0int2int (y))
implement{tk}
gt_g0int_int (x, y) = g0int_gt<tk> (x, g0int2int (y))
implement{tk}
gte_g0int_int (x, y) = g0int_gte<tk> (x, g0int2int (y))
implement{tk}
eq_g0int_int (x, y) = g0int_eq<tk> (x, g0int2int (y))
implement{tk}
neq_g0int_int (x, y) = g0int_neq<tk> (x, g0int2int (y))

implement{tk}
compare_g0int_int (x, y) = g0int_compare<tk> (x, g0int2int (y))

(* ****** ****** *)

implement{tk}
lt_g1int_int (x, y) = g1int_lt<tk> (x, g1int2int (y))
implement{tk}
lte_g1int_int (x, y) = g1int_lte<tk> (x, g1int2int (y))
implement{tk}
gt_g1int_int (x, y) = g1int_gt<tk> (x, g1int2int (y))
implement{tk}
gte_g1int_int (x, y) = g1int_gte<tk> (x, g1int2int (y))
implement{tk}
eq_g1int_int (x, y) = g1int_eq<tk> (x, g1int2int (y))
implement{tk}
neq_g1int_int (x, y) = g1int_neq<tk> (x, g1int2int (y))

implement{tk}
compare_g1int_int (x, y) = g1int_compare<tk> (x, g1int2int (y))

(* ****** ****** *)

implement{tk}
lt_g0uint_int (x, y) = g0uint_lt<tk> (x, g0int2uint (y))
implement{tk}
lte_g0uint_int (x, y) = g0uint_lte<tk> (x, g0int2uint (y))
implement{tk}
gt_g0uint_int (x, y) = g0uint_gt<tk> (x, g0int2uint (y))
implement{tk}
gte_g0uint_int (x, y) = g0uint_gte<tk> (x, g0int2uint (y))
implement{tk}
eq_g0uint_int (x, y) = g0uint_eq<tk> (x, g0int2uint (y))
implement{tk}
neq_g0uint_int (x, y) = g0uint_neq<tk> (x, g0int2uint (y))

(* ****** ****** *)

implement{tk}
lt_g1uint_int (x, y) = g1uint_lt<tk> (x, g1int2uint (y))
implement{tk}
lte_g1uint_int (x, y) = g1uint_lte<tk> (x, g1int2uint (y))
implement{tk}
gt_g1uint_int (x, y) = g1uint_gt<tk> (x, g1int2uint (y))
implement{tk}
gte_g1uint_int (x, y) = g1uint_gte<tk> (x, g1int2uint (y))
implement{tk}
eq_g1uint_int (x, y) = g1uint_eq<tk> (x, g1int2uint (y))
implement{tk}
neq_g1uint_int (x, y) = g1uint_neq<tk> (x, g1int2uint (y))

(* ****** ****** *)

(* end of [integer.dats] *)