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
|
(*
** For writing ATS code
** that translates into Python
*)
(* ****** ****** *)
//
// HX-2014-08:
// prefix for external names
//
#define
ATS_EXTERN_PREFIX "ats2pypre_"
//
(* ****** ****** *)
//
fun double2int (x: double): int = "mac#%"
fun int_of_double (x: double): int = "mac#%"
//
fun int2double (x: int): double = "mac#%"
fun double_of_int (x: int): double = "mac#%"
//
(* ****** ****** *)
fun abs_double : (double) -> double = "mac#%"
fun neg_double : (double) -> double = "mac#%"
(* ****** ****** *)
overload abs with abs_double of 100
overload neg with neg_double of 100
(* ****** ****** *)
fun succ_double : (double) -> double = "mac#%"
fun pred_double : (double) -> double = "mac#%"
(* ****** ****** *)
overload succ with succ_double of 100
overload pred with pred_double of 100
(* ****** ****** *)
//
fun add_int_double
: (int, double) -<fun> double = "mac#%"
fun add_double_int
: (double, int) -<fun> double = "mac#%"
//
fun sub_int_double
: (int, double) -<fun> double = "mac#%"
fun sub_double_int
: (double, int) -<fun> double = "mac#%"
//
fun mul_int_double
: (int, double) -<fun> double = "mac#%"
fun mul_double_int
: (double, int) -<fun> double = "mac#%"
//
fun div_int_double
: (int, double) -<fun> double = "mac#%"
fun div_double_int
: (double, int) -<fun> double = "mac#%"
//
(* ****** ****** *)
overload + with add_int_double of 100
overload + with add_double_int of 100
overload - with sub_int_double of 100
overload - with sub_double_int of 100
overload * with mul_int_double of 100
overload * with mul_double_int of 100
overload / with div_int_double of 100
overload / with div_double_int of 100
(* ****** ****** *)
typedef
float_aop_type = (double, double) -> double
(* ****** ****** *)
//
fun add_double_double : float_aop_type = "mac#%"
fun sub_double_double : float_aop_type = "mac#%"
fun mul_double_double : float_aop_type = "mac#%"
fun div_double_double : float_aop_type = "mac#%"
//
(* ****** ****** *)
//
overload + with add_double_double of 100
overload - with sub_double_double of 100
overload * with mul_double_double of 100
overload / with div_double_double of 100
//
(* ****** ****** *)
//
fun lt_int_double
: (int, double) -<fun> bool = "mac#%"
fun lte_int_double
: (int, double) -<fun> bool = "mac#%"
fun gt_int_double
: (int, double) -<fun> bool = "mac#%"
fun gte_int_double
: (int, double) -<fun> bool = "mac#%"
//
fun lt_double_int
: (double, int) -<fun> bool = "mac#%"
fun lte_double_int
: (double, int) -<fun> bool = "mac#%"
fun gt_double_int
: (double, int) -<fun> bool = "mac#%"
fun gte_double_int
: (double, int) -<fun> bool = "mac#%"
//
(* ****** ****** *)
typedef
float_cmp_type = (double, double) -<fun> bool
(* ****** ****** *)
//
fun lt_double_double : float_cmp_type = "mac#%"
fun lte_double_double : float_cmp_type = "mac#%"
//
fun gt_double_double : float_cmp_type = "mac#%"
fun gte_double_double : float_cmp_type = "mac#%"
//
fun eq_double_double : float_cmp_type = "mac#%"
fun neq_double_double : float_cmp_type = "mac#%"
//
(* ****** ****** *)
//
fun
compare_double_double : (double, double) -<fun> int
//
(* ****** ****** *)
//
overload < with lt_double_double of 100
overload <= with lte_double_double of 100
overload > with gt_double_double of 100
overload >= with gte_double_double of 100
overload = with eq_double_double of 100
overload != with neq_double_double of 100
overload <> with neq_double_double of 100
//
overload compare with compare_double_double of 100
//
(* ****** ****** *)
(* end of [float.sats] *)
|
