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
|
(*
** For writing ATS code
** that translates into Python
*)
(* ****** ****** *)
//
// HX-2014-08:
// prefix for external names
//
#define
ATS_EXTERN_PREFIX "ats2pypre_"
//
(* ****** ****** *)
//
fun
bool2int0
(b: bool):<> natLt(2) = "mac#%"
fun
bool2int1
{b:bool}
(b: bool(b)):<> int(bool2int(b)) = "mac#%"
//
symintr bool2int
overload bool2int with bool2int0 of 100
overload bool2int with bool2int1 of 110
//
(* ****** ****** *)
//
fun
int2bool0 (i: int):<> bool = "mac#%"
fun
int2bool1
{i:int}(i: int(i)):<> bool(i != 0) = "mac#%"
//
symintr int2bool
overload int2bool with int2bool0 of 100
overload int2bool with int2bool1 of 110
//
(* ****** ****** *)
//
fun
neg_bool0
: bool -> bool = "mac#%"
fun
neg_bool1
: {b:bool} bool(b) -> bool(~b) = "mac#%"
//
overload ~ with neg_bool0 of 100
overload ~ with neg_bool1 of 110
//
overload not with neg_bool0 of 100
overload not with neg_bool1 of 110
//
(* ****** ****** *)
fun
add_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
overload + with add_bool0_bool0 of 100
fun
add_bool0_bool1
{b2:bool}
(
b1: bool, b2: bool b2
) :<> [b1:bool] bool(b1 || b2) = "mac#%"
overload + with add_bool0_bool1 of 110
fun
add_bool1_bool0
{b1:bool}
(
b1: bool b1, b2: bool
) :<> [b2:bool] bool(b1 || b2) = "mac#%"
overload + with add_bool1_bool0 of 110
fun
add_bool1_bool1
{b1,b2:bool}
(b1: bool b1, b2: bool b2):<> bool(b1 || b2) = "mac#%"
overload + with add_bool1_bool1 of 120
(* ****** ****** *)
fun
mul_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
overload * with mul_bool0_bool0 of 100
fun
mul_bool0_bool1
{b2:bool}
(
b1: bool, b2: bool b2
) :<> [b1:bool] bool(b1 && b2) = "mac#%"
overload * with mul_bool0_bool1 of 110
fun
mul_bool1_bool0
{b1:bool}
(
b1: bool b1, b2: bool
) :<> [b2:bool] bool(b1 && b2) = "mac#%"
overload * with mul_bool1_bool0 of 110
fun
mul_bool1_bool1
{b1,b2:bool}
(b1: bool b1, b2: bool b2):<> bool(b1 && b2) = "mac#%"
overload * with mul_bool1_bool1 of 120
(* ****** ****** *)
//
fun
eq_bool0_bool0 : (bool, bool) -> bool = "mac#%"
fun
neq_bool0_bool0 : (bool, bool) -> bool = "mac#%"
//
fun
eq_bool1_bool1 :
{b1,b2:bool}(bool(b1), bool(b2)) -> bool(b1 == b2) = "mac#%"
fun
neq_bool1_bool1 :
{b1,b2:bool}(bool(b1), bool(b2)) -> bool(b1 != b2) = "mac#%"
//
overload = with eq_bool0_bool0 of 100
overload = with eq_bool1_bool1 of 120
//
overload != with neq_bool0_bool0 of 100
overload != with neq_bool1_bool1 of 120
//
(* ****** ****** *)
(* end of [bool.sats] *)
|
