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
|
(*
** For writing ATS code
** that translates into Python
*)
(* ****** ****** *)
//
// HX-2014-08:
// prefix for external names
//
#define
ATS_EXTERN_PREFIX "ats2pypre_"
//
(* ****** ****** *)
//
fun
abs_int0 : int -<fun> int = "mac#%"
//
overload abs with abs_int0 of 100
//
(* ****** ****** *)
//
fun
neg_int0 : int -<fun> int = "mac#%"
//
fun neg_int1
: {i:int} int(i) -<fun> int(~i) = "mac#%"
//
overload ~ with neg_int0 of 100
overload ~ with neg_int1 of 110
overload neg with neg_int0 of 100
overload neg with neg_int1 of 110
//
(* ****** ****** *)
//
fun succ_int0 : int -<fun> int = "mac#%"
fun pred_int0 : int -<fun> int = "mac#%"
//
fun succ_int1
: {i:int} int(i) -<fun> int(i+1) = "mac#%"
fun pred_int1
: {i:int} int(i) -<fun> int(i-1) = "mac#%"
//
overload succ with succ_int0 of 100
overload pred with pred_int0 of 100
//
overload succ with succ_int1 of 110
overload pred with pred_int1 of 110
//
(* ****** ****** *)
//
fun half_int0 : int -<fun> int = "mac#%"
fun half_int1 : {i:int} int(i) -<fun> int(i/2) = "mac#%"
//
overload half with half_int0 of 100
overload half with half_int1 of 110
//
(* ****** ****** *)
//
fun add_int0_int0 : (int, int) -<fun> int = "mac#%"
fun sub_int0_int0 : (int, int) -<fun> int = "mac#%"
fun mul_int0_int0 : (int, int) -<fun> int = "mac#%"
fun div_int0_int0 : (int, int) -<fun> int = "mac#%"
fun mod_int0_int0 : (int, int) -<fun> int = "mac#%"
//
fun add_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> int(i+j) = "mac#%"
fun sub_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> int(i-j) = "mac#%"
fun mul_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> int(i*j) = "mac#%"
fun div_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> int(i/j) = "mac#%"
//
(* ****** ****** *)
//
overload + with add_int0_int0 of 100
overload - with sub_int0_int0 of 100
overload * with mul_int0_int0 of 100
overload / with div_int0_int0 of 100
overload % with mod_int0_int0 of 100
overload mod with mod_int0_int0 of 100
//
overload + with add_int1_int1 of 120
overload - with sub_int1_int1 of 120
overload * with mul_int1_int1 of 120
overload / with div_int1_int1 of 120
//
(* ****** ****** *)
//
fun
nmod_int1_int1
{ i,j:int
| i >= 0; j > 0
} (i: int(i), j: int(j)):<fun> int(nmod(i, j)) = "mac#%"
//
(* ****** ****** *)
//
fun lt_int0_int0 : (int, int) -<fun> bool = "mac#%"
fun lte_int0_int0 : (int, int) -<fun> bool = "mac#%"
fun gt_int0_int0 : (int, int) -<fun> bool = "mac#%"
fun gte_int0_int0 : (int, int) -<fun> bool = "mac#%"
//
fun eq_int0_int0 : (int, int) -<fun> bool = "mac#%"
fun neq_int0_int0 : (int, int) -<fun> bool = "mac#%"
//
fun compare_int0_int0: (int, int) -<fun> int = "mac#%"
//
(* ****** ****** *)
//
fun lt_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> bool(i < j) = "mac#%"
fun lte_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> bool(i <= j) = "mac#%"
fun gt_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> bool(i > j) = "mac#%"
fun gte_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> bool(i >= j) = "mac#%"
//
fun eq_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> bool(i == j) = "mac#%"
fun neq_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> bool(i != j) = "mac#%"
//
(* ****** ****** *)
//
overload < with lt_int0_int0 of 100
overload <= with lte_int0_int0 of 100
overload > with gt_int0_int0 of 100
overload >= with gte_int0_int0 of 100
overload = with eq_int0_int0 of 100
overload != with neq_int0_int0 of 100
overload <> with neq_int0_int0 of 100
//
overload compare with compare_int0_int0 of 100
//
(* ****** ****** *)
//
overload < with lt_int1_int1 of 120
overload <= with lte_int1_int1 of 120
overload > with gt_int1_int1 of 120
overload >= with gte_int1_int1 of 120
overload = with eq_int1_int1 of 120
overload != with neq_int1_int1 of 120
overload <> with neq_int1_int1 of 120
//
(* ****** ****** *)
//
fun max_int0_int0: (int, int) -<fun> int = "mac#%"
fun min_int0_int0: (int, int) -<fun> int = "mac#%"
//
fun max_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> int(max(i,j)) = "mac#%"
fun min_int1_int1
: {i,j:int} (int(i), int(j)) -<fun> int(min(i,j)) = "mac#%"
//
(* ****** ****** *)
//
overload max with max_int0_int0 of 100
overload min with min_int0_int0 of 100
//
overload max with max_int1_int1 of 120
overload min with min_int1_int1 of 120
//
(* ****** ****** *)
(* end of [integer.sats] *)
|
