This repository has been archived by the owner on May 18, 2023. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathstatic_tc_tests.ml
331 lines (323 loc) · 10.7 KB
/
static_tc_tests.ml
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
(* some int Items*)
let i0 = CstInt(0);;
let i1 = CstInt(1);;
let i2 = CstInt(-2);;
let i3 = CstInt(3);;
let i4 = CstInt(100);;
(* some float Items*)
let f0 = CstFloat(0.);;
let f1 = CstFloat(1.);;
let f2 = CstFloat(-2.);;
let f3 = CstFloat(3.);;
let f4 = CstFloat(100.);;
(* some boolean Items *)
let b0 = CstFalse;;
let b1 = CstTrue;;
(* some string Items*)
let s0 = CstString("");;
let s1 = CstString("aaaa");;
let s2 = CstString("bbb");;
let s3 = CstString("123456789");;
print_string "testing set constructors: ";;
print_string "Set 0: ";;
let set0 = Empty(TFloat);;
typecheck set0 tEmptyEnv;;
print_string "Set 1: ";;
let set1 = Singleton(i3);;
typecheck set1 tEmptyEnv;;
print_string "Set 2: ";;
let set2 = OfOpt(TBool, Empty);;
typecheck set2 tEmptyEnv;;
print_string "Set 3: ";;
let set3 = OfOpt(TInt,Empty);;
typecheck set3 tEmptyEnv;;
print_string "Set 6: ";;
let set6 = Singleton(f3);;
typecheck set6 tEmptyEnv;;
print_string "Set 7: ";;
let set7 = Singleton(s3);;
typecheck set7 tEmptyEnv;;
print_string "Set 8: ";;
let set8 = Singleton(b0);;
typecheck set8 tEmptyEnv;;
print_string "Set 9: ";;
let set9 = OfOpt(TInt,
Item(i0,Item(i1,Item(i2,Item(i3,Item(i4,Empty))))));;
typecheck set9 tEmptyEnv;;
print_string "Set 10: ";;
let set10 = OfOpt(TInt, Item(i0,Empty)) ;;
typecheck set10 tEmptyEnv;;
print_string "Set 11: ";;
let set11 = Singleton(i0) ;;
typecheck set11 tEmptyEnv;;
print_string "testing if Set 10 and 11 are different: ";;
let b = set10<>set11;;
(typecheck (set10) tEmptyEnv)<>(typecheck (set11) tEmptyEnv);;
print_string "testing operations for integers: ";;
print_string "testing the sum: ";;
let op0 = Sum(i3,i2);;
typecheck op0 tEmptyEnv;;
print_string "testing the subtraction: ";;
let op1 = Sub(i0,i2);;
typecheck op1 tEmptyEnv;;
print_string "testing the negation: ";;
let op3 = Neg(i2);;
typecheck op3 tEmptyEnv;;
print_string "testing the multiplication: ";;
let op4 = Times(i2,i4);;
typecheck op4 tEmptyEnv;;
print_string "testing the division: ";;
let op5 = Div(i4,Neg(i2));;
typecheck op5 tEmptyEnv;;
print_string "testing the equality: ";;
let op6 = Eq(i0,i0);;
typecheck op6 tEmptyEnv;;
let op7 = Eq(i0,i3);;
typecheck op7 tEmptyEnv;;
print_string "testing < and >: ";;
let op8 = BiggerThan(i2,i0);;
typecheck op8 tEmptyEnv;;
let op9 = BiggerThan(i0,i2);;
typecheck op9 tEmptyEnv;;
let op1 = LessThan(i0,i2);;
typecheck op1 tEmptyEnv;;
print_string "testing IsZero: ";;
let op2 = IsZero(i0);;
typecheck op2 tEmptyEnv;;
let op3 = IsZero(i1);;
typecheck op3 tEmptyEnv;;
print_string "testing the modulus: ";;
let op0 = Mod(i4,i3);;
typecheck op0 tEmptyEnv;;
print_string "testing operations for floats: ";;
print_string "testing the sum: ";;
let op0 = Sum(f3,f2);;
typecheck op0 tEmptyEnv;;
print_string "testing the subtraction: ";;
let op1 = Sub(f0,f2);;
typecheck op1 tEmptyEnv;;
print_string "testing the negation: ";;
let op3 = Neg(f2);;
typecheck op3 tEmptyEnv;;
print_string "testing the multiplication: ";;
let op4 = Times(f2,f4);;
typecheck op4 tEmptyEnv;;
print_string "testing the division: ";;
let op5 = Div(f4,Neg(f2));;
typecheck op5 tEmptyEnv;;
print_string "testing the equality: ";;
let op6 = Eq(f0,f0);;
typecheck op6 tEmptyEnv;;
let op7 = Eq(f0,f3);;
typecheck op7 tEmptyEnv;;
print_string "testing < and >: ";;
let op8 = BiggerThan(f2,f0);;
typecheck op8 tEmptyEnv;;
let op9 = BiggerThan(f0,f2);;
typecheck op9 tEmptyEnv;;
let op1 = LessThan(f0,f2);;
typecheck op1 tEmptyEnv;;
print_string "testing operations for booleans: ";;
print_string "testing the negation: ";;
let op0 = Not(b1);;
typecheck op0 tEmptyEnv;;
print_string "testing the and: ";;
let op1 = And(op0, b1);;
typecheck op1 tEmptyEnv;;
print_string "testing the and the negation: ";;
let op2 = And(Not(op1), b1);;
typecheck op2 tEmptyEnv;;
print_string "testing the or: ";;
let op3 = Or(op0, b0);;
typecheck op3 tEmptyEnv;;
print_string "testing operations for strings: ";;
print_string "testing the equality: ";;
let op0 = Eq(s1,s1);;
typecheck op0 tEmptyEnv;;
let op1 = Eq(s1, s0);;
typecheck op1 tEmptyEnv;;
print_string "testing < and >: ";;
let op2 = BiggerThan(s2, s1);;
typecheck op2 tEmptyEnv;;
let op3 = BiggerThan(s1, s2);;
typecheck op3 tEmptyEnv;;
let op4 = LessThan(s0,s2);;
typecheck op4 tEmptyEnv;;
let op5 = LessThan(s2,s0);;
typecheck op5 tEmptyEnv;;
let op6 = LessThan(s0,s0);;
typecheck op6 tEmptyEnv;;
print_string "testing the concatenation: ";;
let op7 = Concat(s1,s2);;
typecheck op7 tEmptyEnv;;
let op8 = Concat(op7,s3);;
typecheck op8 tEmptyEnv;;
print_string "testing operations for sets: ";;
print_string "testing the union: ";;
let op1 = Union(set9, Add(Add(set1,CstInt(189)), CstInt(22)));;
typecheck op1 tEmptyEnv;;
let op2 = Union(set3, set1);;
typecheck op2 tEmptyEnv;;
let op3 = Union(set6, set0);;
typecheck op3 tEmptyEnv;;
print_string "testing the intersection: ";;
let op4 = Intersection(set0,set6);;
typecheck op4 tEmptyEnv;;
let op5 = Intersection(set6,set0);;
typecheck op5 tEmptyEnv;;
let op6 = Intersection(set9, Add(Add(set10, i3), CstInt(22)));;
typecheck op6 tEmptyEnv;;
let op7 = Intersection(set8,set8);;
typecheck op7 tEmptyEnv;;
let op8 = Intersection(set9,set11);;
typecheck op8 tEmptyEnv;;
print_string "testing the difference: ";;
let op8 = Difference(set9,set11);;
typecheck op8 tEmptyEnv;;
let op9 = Difference(set6,set0);;
typecheck op9 tEmptyEnv;;
let op1 = Difference(set0,set6);;
typecheck op1 tEmptyEnv;;
print_string "testing the insertion: ";;
let op2 = Add(set7, s2);;
typecheck op2 tEmptyEnv;;
let op3 = Add(set9, CstInt(77));;
typecheck op3 tEmptyEnv;;
let op5 = Add(set0,f1);;
typecheck op5 tEmptyEnv;;
print_string "testing the removal: ";;
let op2 = Remove(set7, s3);;
typecheck op2 tEmptyEnv;;
let op3 = Remove(set9, i4);;
typecheck op3 tEmptyEnv;;
print_string "testing the minimum and maximum: ";;
let op0 = GetMin(set9);;
typecheck op0 tEmptyEnv;;
let op1 = GetMax(set9);;
typecheck op1 tEmptyEnv;;
let op2 = GetMin(set0);;
typecheck op2 tEmptyEnv;;
let op3 = GetMax(set0);;
typecheck op3 tEmptyEnv;;
let op4 = GetMin(set1);;
typecheck op4 tEmptyEnv;;
let op5 = GetMax(set1);;
typecheck op5 tEmptyEnv;;
print_string "testing IsEmpty: ";;
let op0 = IsEmpty(set0);;
typecheck op0 tEmptyEnv;;
let op1 = IsEmpty(set9);;
typecheck op1 tEmptyEnv;;
print_string "testing IsInside: ";;
let op0 = IsInside((Empty(TString), s0));;
typecheck op0 tEmptyEnv;;
let op1 = IsInside(set9, i0);;
typecheck op1 tEmptyEnv;;
let op2 = IsInside(set9, CstInt(33));;
typecheck op2 tEmptyEnv;;
print_string "testing IsSubset: ";;
let op0 = IsSubset(set0, set0);;
typecheck op0 tEmptyEnv;;
let op3 = IsSubset(Empty(TInt),set9);;
typecheck op3 tEmptyEnv;;
let op4 = IsSubset((Add(Empty(TInt),CstInt 0)),set9);;
typecheck op4 tEmptyEnv;;
let op5 = IsSubset(set1, set9);;
typecheck op5 tEmptyEnv;;
let op6 = IsSubset(set9, set1);;
typecheck op6 tEmptyEnv;;
print_string "testing functions: ";;
print_string "testing recursion by implementig the factorial function: ";;
let fact = Letrec("fact", "x",TInt,TInt,
Ifthenelse(Eq(Den("x"), CstInt(0)), CstInt(1), Times(Den("x"),
Apply(Den("fact"), Sub(Den("x"), CstInt(1))))),
Apply(Den("fact"), CstInt(3)));;
typecheck fact tEmptyEnv;;
(* tests with pred = even, with pred = odd and finally with pred = neg*)
let pred_even = Fun("x",TInt,Ifthenelse(Eq(Mod(Den("x"),
CstInt(2)),CstInt(0)),CstTrue,CstFalse));;
let pred_odd = Fun("x",TInt,Ifthenelse(Not(Eq(Mod(Den("x"),
CstInt(2)),CstInt(0))),CstTrue,CstFalse));;
let pred_neg = Fun("x", TInt, Neg(Den("x")))
let make_even = Fun("x",TInt,Times(Den("x"),CstInt(2)));;
print_string "testing ForAll: ";;
let forall_even=ForAll(pred_even,set9);;
typecheck forall_even tEmptyEnv;;
let forall_odd=ForAll(pred_odd,set9);;
typecheck forall_odd tEmptyEnv;;
let forall_odd=ForAll(pred_odd,set1);;
typecheck forall_odd tEmptyEnv;;
print_string "testing Exists: ";;
let exists_even=Exists(pred_even,set9);;
typecheck exists_even tEmptyEnv;;
let exists_odd=Exists(pred_odd,set9);;
typecheck exists_odd tEmptyEnv;;
let exists_even=Exists(pred_even,set1);;
typecheck exists_even tEmptyEnv;;
print_string "testing Filter: ";;
let filter_even=Filter(pred_even,set9);;
let filter_odd=Filter(pred_odd,set9);;
typecheck filter_even tEmptyEnv;;
typecheck filter_odd tEmptyEnv;;
print_string "testing Map: ";;
let map_make_even=Map(make_even,set9);;
typecheck map_make_even tEmptyEnv;;
let str = OfOpt(TString,Item(CstString("0:"),
Item(CstString("1:"),Item(CstString("2:"),
Item(CstString("3:"),Item(CstString("4:"),Empty))))));;
let pred_concat = Fun("x", TString, Concat(Den("x"), s1)) ;;
let map_concat= Map(pred_concat,str);;
typecheck map_concat tEmptyEnv;;
print_string "the mapping function can change types of the resulting set: ";;
let map_turn_to_one = Map(Fun("x", TInt,CstInt(1)), set7) ;;
typecheck map_turn_to_one tEmptyEnv ;;
let map_neg = Map(pred_neg, set9);;
typecheck map_neg tEmptyEnv ;;
print_string "------------------------------------------------------------";;
print_string "testing failures: ";;
print_string "testing type mismatch: ";;
print_string "Set 4: ";;
let set4 = OfOpt(TInt,
Item(f0,Item(i1,Item(i0,Item(i2,Item(i3,Empty))))));;
typecheck set4 tEmptyEnv;;
print_string "on the union: ";;
let op0 = Union(set0,set1);;
typecheck op0 tEmptyEnv;;
print_string "on the insertion: ";;
let op4 = Add(set7,b0);;
typecheck op4 tEmptyEnv;;
print_string "on IsInside: ";;
let op3 = IsInside(set9, b1);;
typecheck op3 tEmptyEnv;;
print_string "on IsSubset: ";;
let op1 = IsSubset(set9, set0);;
typecheck op1 tEmptyEnv;;
let op2 = IsSubset(set0, set9);;
typecheck op2 tEmptyEnv;;
print_string "testing set consistency: ";;
print_string "on the insertion: ";;
let op5 = Add(set9,Empty(TInt));;
typecheck op5 tEmptyEnv;;
print_string "testing if the predicate is a boolean: ";;
print_string "on the ForAll: ";;
let forall_failure = ForAll(pred_neg, set9);;
typecheck forall_failure tEmptyEnv;;
print_string "on the Exists: ";;
let exists_failure = Exists(pred_neg, set9);;
typecheck exists_failure tEmptyEnv ;;
print_string "on the Filter: ";;
let filter_failure = Filter(pred_neg, set9);;
typecheck filter_failure tEmptyEnv ;;
print_string "testing if the pred in f(pred,set) is actually a predicate: ";;
print_string "on the ForAll: ";;
let forall_failure = ForAll(CstInt(3), set9);;
typecheck forall_failure tEmptyEnv;;
print_string "on the Exists: ";;
let exists_failure = Exists(CstInt(3), set9);;
typecheck exists_failure tEmptyEnv ;;
print_string "on the Filter: ";;
let filter_failure = Filter(CstInt(3), set9);;
typecheck filter_failure tEmptyEnv ;;
print_string "on the Map: ";;
let pred_map_failure = Map(CstInt(3),set9) ;;
typecheck pred_map_failure tEmptyEnv;;