Line data Source code
1 : // Author(s): Aad Mathijssen, Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 :
10 : #define BOOST_TEST_MODULE typecheck_test
11 :
12 : // Some tests rely on type check failures, so we have to set this flag.
13 : #define MCRL2_DISABLE_TYPECHECK_ASSERTIONS
14 :
15 : #include <boost/test/included/unit_test.hpp>
16 :
17 : #include "mcrl2/data/data_io.h"
18 : #include "mcrl2/data/experimental/type_check_tree.h"
19 : #include "mcrl2/data/print.h"
20 :
21 : using namespace mcrl2;
22 :
23 : inline
24 26 : data::sort_expression pos()
25 : {
26 26 : return data::sort_pos::pos();
27 : }
28 :
29 : inline
30 18 : data::sort_expression nat()
31 : {
32 18 : return data::sort_nat::nat();
33 : }
34 :
35 : inline
36 9 : data::sort_expression list(const data::sort_expression& x)
37 : {
38 9 : return data::sort_list::list(x);
39 : }
40 :
41 : inline
42 55 : data::variable var(const std::string& name, const data::sort_expression& sort)
43 : {
44 55 : return data::variable(name, sort);
45 : }
46 :
47 : // Expected failures, these are not going to be fixed in the current
48 : // implementation of the type checker
49 : //BOOST_AUTO_TEST_CASE_EXPECTED_FAILURES(test_multiple_variables, 1)
50 : //BOOST_AUTO_TEST_CASE_EXPECTED_FAILURES(test_multiple_variables_reversed, 1)
51 : //BOOST_AUTO_TEST_CASE_EXPECTED_FAILURES(test_matching_ambiguous, 1) // Fails because of reordering in type checker / pretty printer
52 : //BOOST_AUTO_TEST_CASE_EXPECTED_FAILURES(test_matching_ambiguous_rhs, 1) // Fails because of reordering in type checker / pretty printer
53 : //BOOST_AUTO_TEST_CASE_EXPECTED_FAILURES(test_ambiguous_function_application4, 1) // Fails because of reordering in type checker / pretty printer
54 : //BOOST_AUTO_TEST_CASE_EXPECTED_FAILURES(test_ambiguous_function_application4a, 1) // Fails because of reordering in type checker / pretty printer
55 :
56 : // Parse functions that do not change any context (i.e. do not typecheck and
57 : // normalise sorts).
58 83 : data::sort_expression parse_sort_expression(const std::string& de_in)
59 : {
60 83 : data::sort_expression result;
61 : try {
62 83 : result = data::detail::parse_sort_expression(de_in);
63 83 : std::string de_out = data::pp(result);
64 83 : if (de_in != de_out)
65 : {
66 0 : std::clog << "aterm : " << result << std::endl;
67 0 : std::clog << "de_in : " << de_in << std::endl;
68 0 : std::clog << "de_out: " << de_out << std::endl;
69 0 : std::clog << "The following sort expressions should be the same:" << std::endl << " " << de_in << std::endl << " " << de_out << std::endl;
70 0 : BOOST_CHECK_EQUAL(de_in, de_out);
71 : }
72 83 : }
73 0 : catch (...)
74 : {
75 0 : BOOST_CHECK(false);
76 0 : }
77 83 : return result;
78 0 : }
79 :
80 120 : data::data_expression parse_data_expression(const std::string& de_in)
81 : {
82 120 : data::data_expression result;
83 : try {
84 120 : result = data::detail::parse_data_expression(de_in);
85 : #ifdef MCRL2_ENABLE_TYPECHECK_PP_TESTS
86 : std::string de_out = data::pp(result);
87 : if (de_in != de_out)
88 : {
89 : std::clog << "aterm : " << result << std::endl;
90 : std::clog << "de_in : " << de_in << std::endl;
91 : std::clog << "de_out: " << de_out << std::endl;
92 : std::clog << "The following data expressions should be the same:" << std::endl << " " << de_in << std::endl << " " << de_out << std::endl;
93 : BOOST_CHECK_EQUAL(de_in, de_out);
94 : }
95 : #endif
96 : }
97 0 : catch (mcrl2::runtime_error& e)
98 : {
99 0 : BOOST_CHECK(false);
100 0 : }
101 120 : return result;
102 0 : }
103 :
104 71 : data::data_specification parse_data_specification(const std::string& de_in, bool expect_success = true)
105 : {
106 71 : data::data_specification result;
107 : try {
108 71 : result = data::detail::parse_data_specification_new(de_in);
109 71 : std::string de_out = data::pp(result);
110 :
111 71 : std::string input = utilities::trim_copy(de_in);
112 71 : std::string output = utilities::trim_copy(de_out);
113 71 : if (input != output)
114 : {
115 0 : std::clog << "aterm : " << data::detail::data_specification_to_aterm(result) << std::endl;
116 0 : std::clog << "de_in : " << de_in << std::endl;
117 0 : std::clog << "de_out: " << de_out << std::endl;
118 0 : std::clog << "The following data specifications should be the same:" << std::endl << " " << de_in << std::endl << " " << de_out << std::endl;
119 0 : BOOST_CHECK_EQUAL(input, output);
120 : }
121 71 : }
122 0 : catch (...)
123 : {
124 0 : BOOST_CHECK(!expect_success);
125 0 : }
126 71 : return result;
127 0 : }
128 :
129 70 : void test_data_expression(const std::string& de_in,
130 : const data::variable_vector& variable_context,
131 : bool expect_success = true,
132 : const std::string& expected_sort = "",
133 : bool test_type_checker = true)
134 : {
135 70 : std::clog << std::endl
136 70 : << "==========================================" << std::endl;
137 70 : data::data_expression x(parse_data_expression(de_in));
138 70 : std::clog << "Testing type checking of data expression: " << std::endl
139 70 : << " de_in: " << de_in << std::endl
140 70 : << " de_out: " << pp(x) << std::endl
141 70 : << " expect success: " << (expect_success?("yes"):("no")) << std::endl
142 70 : << " expected type: " << expected_sort << std::endl
143 70 : << " detected type: " << pp(x.sort()) << " (before typechecking) " << std::endl;
144 :
145 :
146 70 : if (test_type_checker)
147 : {
148 70 : if (expect_success)
149 : {
150 54 : BOOST_CHECK_NO_THROW(x = data::typecheck_data_expression(x, variable_context));
151 54 : BOOST_CHECK_NE(x, data::data_expression());
152 :
153 54 : std::string de_out = data::pp(x);
154 : //std::clog << "The following data expressions should be the same:" << std::endl << " " << de_in << std::endl << " " << de_out << std::endl;
155 : //#ifdef MCRL2_ENABLE_TYPECHECK_PP_TESTS
156 54 : BOOST_CHECK_EQUAL(de_in, de_out);
157 : //#endif
158 : // TODO: this check should be uncommented
159 : //BOOST_CHECK(!search_sort_expression(x.sort(), data::untyped_sort()));
160 54 : if (expected_sort != "")
161 : {
162 44 : BOOST_CHECK_EQUAL(x.sort(), parse_sort_expression(expected_sort));
163 44 : std::clog << " expression x in internal format: " << x << std::endl;
164 : }
165 : else
166 : {
167 10 : std::clog << " failed to typecheck" << std::endl;
168 : }
169 54 : }
170 : else
171 : {
172 48 : BOOST_CHECK_THROW(x = data::typecheck_data_expression(x), mcrl2::runtime_error);
173 : }
174 : }
175 70 : }
176 :
177 53 : void test_data_expression(const std::string& de_in,
178 : bool expect_success = true,
179 : const std::string& expected_sort = "",
180 : bool test_type_checker = true)
181 : {
182 53 : data::variable_vector v;
183 53 : test_data_expression(de_in, v, expect_success, expected_sort, test_type_checker);
184 53 : }
185 :
186 2 : BOOST_AUTO_TEST_CASE(test_true)
187 : {
188 : //test boolean data expressions
189 1 : test_data_expression("true", true, "Bool");
190 1 : }
191 :
192 2 : BOOST_AUTO_TEST_CASE(test_if)
193 : {
194 1 : test_data_expression("if(true, true, false)", true, "Bool");
195 1 : }
196 :
197 2 : BOOST_AUTO_TEST_CASE(test_not)
198 : {
199 1 : test_data_expression("!true", true, "Bool");
200 1 : }
201 :
202 2 : BOOST_AUTO_TEST_CASE(test_and)
203 : {
204 1 : test_data_expression("true && false", true, "Bool");
205 1 : }
206 :
207 2 : BOOST_AUTO_TEST_CASE(test_zero)
208 : {
209 1 : test_data_expression("0", true, "Nat");
210 1 : }
211 :
212 2 : BOOST_AUTO_TEST_CASE(test_minus_one)
213 : {
214 1 : test_data_expression("-1", true, "Int");
215 1 : }
216 :
217 2 : BOOST_AUTO_TEST_CASE(test_zero_plus_one)
218 : {
219 1 : test_data_expression("0 + 1", true, "Pos");
220 1 : }
221 :
222 2 : BOOST_AUTO_TEST_CASE(test_one_plus_zero)
223 : {
224 1 : test_data_expression("1 + 0", true, "Pos");
225 1 : }
226 :
227 2 : BOOST_AUTO_TEST_CASE(test_zero_plus_zero)
228 : {
229 1 : test_data_expression("0 + 0", true, "Nat");
230 1 : }
231 :
232 2 : BOOST_AUTO_TEST_CASE(test_one_plus_one)
233 : {
234 1 : test_data_expression("1 + 1", true, "Pos");
235 1 : }
236 :
237 2 : BOOST_AUTO_TEST_CASE(test_one_times_two_plus_three)
238 : {
239 1 : test_data_expression("1 * 2 + 3", true, "Pos");
240 1 : }
241 :
242 2 : BOOST_AUTO_TEST_CASE(test_empty_list)
243 : {
244 1 : test_data_expression("[]", true); // List unknown
245 1 : }
246 :
247 2 : BOOST_AUTO_TEST_CASE(test_empty_list_concat)
248 : {
249 1 : test_data_expression("[] ++ []", true); // List unknown
250 1 : }
251 :
252 2 : BOOST_AUTO_TEST_CASE(test_empty_list_size)
253 : {
254 1 : test_data_expression("#[]", true, "Nat");
255 1 : }
256 :
257 2 : BOOST_AUTO_TEST_CASE(test_empty_list_in)
258 : {
259 1 : test_data_expression("true in []", true, "Bool");
260 1 : }
261 :
262 2 : BOOST_AUTO_TEST_CASE(test_list_true_false)
263 : {
264 1 : test_data_expression("[true, false]", true, "List(Bool)");
265 1 : }
266 :
267 2 : BOOST_AUTO_TEST_CASE(test_list_zero)
268 : {
269 1 : test_data_expression("[0]", true, "List(Nat)");
270 1 : }
271 :
272 2 : BOOST_AUTO_TEST_CASE(test_list_one_two)
273 : {
274 1 : test_data_expression("[1, 2]", true, "List(Pos)");
275 1 : }
276 :
277 2 : BOOST_AUTO_TEST_CASE(test_list_zero_concat_one_two)
278 : {
279 1 : test_data_expression("[0] ++ [1, 2]", true, "List(Nat)");
280 1 : }
281 :
282 2 : BOOST_AUTO_TEST_CASE(test_list_nat_pos)
283 : {
284 1 : test_data_expression("[0, 1, 2]", true, "List(Nat)");
285 1 : }
286 :
287 2 : BOOST_AUTO_TEST_CASE(test_list_pos_nat)
288 : {
289 1 : test_data_expression("[1, 0, 2]", true, "List(Nat)");
290 1 : }
291 :
292 2 : BOOST_AUTO_TEST_CASE(test_list_nat_concat_one_two)
293 : {
294 2 : test_data_expression("l ++ [1, 2]", { var("l", list(nat())) }, true, "List(Nat)");
295 1 : }
296 :
297 2 : BOOST_AUTO_TEST_CASE(test_list_pos_concat_one_two)
298 : {
299 :
300 2 : test_data_expression("l ++ [1, 2]", { var("l", list(pos())) }, true, "List(Pos)");
301 1 : }
302 :
303 2 : BOOST_AUTO_TEST_CASE(test_list_zero_concat_list_pos)
304 : {
305 2 : test_data_expression("[0] ++ l", { var("l", list(pos())) }, false);
306 1 : }
307 :
308 2 : BOOST_AUTO_TEST_CASE(test_list_zero_concat_list_nat)
309 : {
310 2 : test_data_expression("[0] ++ l", { var("l", list(nat())) }, true, "List(Nat)");
311 1 : }
312 :
313 2 : BOOST_AUTO_TEST_CASE(test_list_pos_concat_list_nat)
314 : {
315 3 : test_data_expression("x ++ y", { var("x", list(pos())), var("y", list(nat())) }, false);
316 1 : }
317 :
318 2 : BOOST_AUTO_TEST_CASE(test_list_is_list_nat)
319 : {
320 3 : test_data_expression("x == y", { var("x", list(pos())), var("y", list(nat())) }, false);
321 1 : }
322 :
323 2 : BOOST_AUTO_TEST_CASE(test_emptyset)
324 : {
325 1 : test_data_expression("{}", true);
326 1 : }
327 :
328 2 : BOOST_AUTO_TEST_CASE(test_emptyset_complement)
329 : {
330 1 : test_data_expression("!{}", true);
331 1 : }
332 :
333 2 : BOOST_AUTO_TEST_CASE(test_emptyset_complement_subset)
334 : {
335 1 : test_data_expression("!{} <= {}", true);
336 1 : }
337 :
338 2 : BOOST_AUTO_TEST_CASE(test_emptyset_complement_subset_reverse)
339 : {
340 1 : test_data_expression("{} <= !{}", true);
341 1 : }
342 :
343 2 : BOOST_AUTO_TEST_CASE(test_set_true_false)
344 : {
345 1 : test_data_expression("{ true, false }", true, "FSet(Bool)");
346 1 : }
347 :
348 2 : BOOST_AUTO_TEST_CASE(test_set_numbers)
349 : {
350 1 : test_data_expression("{ 1, 2, -7 }", true, "FSet(Int)");
351 1 : }
352 :
353 2 : BOOST_AUTO_TEST_CASE(test_set_comprehension)
354 : {
355 1 : test_data_expression("{ x: Nat | x mod 2 == 0 }", true, "Set(Nat)");
356 1 : }
357 :
358 2 : BOOST_AUTO_TEST_CASE(test_emptybag)
359 : {
360 1 : test_data_expression("{:}", true);
361 1 : }
362 :
363 2 : BOOST_AUTO_TEST_CASE(test_emptybag_complement)
364 : {
365 1 : test_data_expression("!{:}", false);
366 1 : }
367 2 : BOOST_AUTO_TEST_CASE(test_bag_true_false)
368 : {
369 1 : test_data_expression("{ true: 1, false: 2 }", true, "FBag(Bool)");
370 1 : }
371 :
372 2 : BOOST_AUTO_TEST_CASE(test_bag_numbers)
373 : {
374 1 : test_data_expression("{ 1: 1, 2: 2, -8: 8 }", true, "FBag(Int)");
375 1 : }
376 :
377 2 : BOOST_AUTO_TEST_CASE(test_bag_comprehension)
378 : {
379 1 : test_data_expression("{ x: Nat | (lambda y: Nat. y * y)(x) }", true, "Bag(Nat)");
380 1 : }
381 :
382 2 : BOOST_AUTO_TEST_CASE(test_function_updates)
383 : {
384 : //test function updates
385 1 : test_data_expression("(lambda x: Bool. x)[true -> false]", true);
386 1 : test_data_expression("(lambda x: Bool. x)[0 -> false]", false);
387 1 : test_data_expression("(lambda x: Bool. x)[true -> false][false -> true]", true);
388 1 : test_data_expression("(lambda n: Nat. n mod 2 == 0)[0 -> false]", true);
389 1 : }
390 :
391 2 : BOOST_AUTO_TEST_CASE(test_inline_struct_recogniser)
392 : {
393 1 : test_data_expression("lambda x: struct t?is_t. x == t", false);
394 1 : }
395 :
396 2 : BOOST_AUTO_TEST_CASE(test_inline_struct)
397 : {
398 1 : test_data_expression("lambda x: struct t. x == t", false);
399 1 : }
400 :
401 2 : BOOST_AUTO_TEST_CASE(test_inline_structs_compare)
402 : {
403 1 : test_data_expression("lambda x,y: struct t. x == y", true, "struct t # struct t -> Bool");
404 1 : }
405 :
406 2 : BOOST_AUTO_TEST_CASE(test_inline_structs_compare_recogniser)
407 : {
408 1 : test_data_expression("lambda x: struct t?is_t, y: struct t. x == y", false);
409 1 : }
410 :
411 2 : BOOST_AUTO_TEST_CASE(test_lambda_aliasing)
412 : {
413 1 : test_data_expression("lambda f: Nat. lambda f: Nat -> Bool. f(f)", false);
414 1 : }
415 :
416 2 : BOOST_AUTO_TEST_CASE(test_forall_structs_compare)
417 : {
418 1 : test_data_expression("forall x,y: struct t. x == y", true, "Bool");
419 1 : }
420 :
421 2 : BOOST_AUTO_TEST_CASE(test_forall_simple)
422 : {
423 1 : test_data_expression("forall n: Nat. n >= 0", true, "Bool");
424 1 : }
425 :
426 2 : BOOST_AUTO_TEST_CASE(test_forall_simple_nat_vs_int)
427 : {
428 1 : test_data_expression("forall n: Nat. n > -1", true, "Bool");
429 1 : }
430 :
431 2 : BOOST_AUTO_TEST_CASE(test_exists_structs_compare)
432 : {
433 1 : test_data_expression("exists x,y: struct t. x == y", true, "Bool");
434 1 : }
435 :
436 2 : BOOST_AUTO_TEST_CASE(test_exists_simple)
437 : {
438 1 : test_data_expression("exists n: Nat. n > 481", true, "Bool");
439 1 : }
440 :
441 2 : BOOST_AUTO_TEST_CASE(test_equal_context)
442 : {
443 3 : test_data_expression("x == y", { var("x", parse_sort_expression("struct t?is_t")), var("y", parse_sort_expression("struct t?is_t")) }, true, "Bool");
444 1 : }
445 :
446 2 : BOOST_AUTO_TEST_CASE(test_not_equal_context)
447 : {
448 3 : test_data_expression("x == y", { var("x", parse_sort_expression("struct t")), var("y", parse_sort_expression("struct t?is_t")) }, false);
449 1 : }
450 :
451 2 : BOOST_AUTO_TEST_CASE(test_where)
452 : {
453 1 : test_data_expression("x + y whr x = 3, y = 10 end", true, "Pos");
454 1 : }
455 :
456 2 : BOOST_AUTO_TEST_CASE(test_where_var_one_occurs_in_two)
457 : {
458 1 : test_data_expression("x + y whr x = 3, y = x + 10 end", false);
459 1 : }
460 :
461 2 : BOOST_AUTO_TEST_CASE(test_where_var_one_and_two_occur_in_two)
462 : {
463 1 : test_data_expression("x + y whr x = 3, y = x + y + 10 end", false);
464 1 : }
465 :
466 2 : BOOST_AUTO_TEST_CASE(test_where_var_two_occurs_in_one)
467 : {
468 1 : test_data_expression("x + y whr x = y + 10, y = 3 end", false);
469 1 : }
470 :
471 2 : BOOST_AUTO_TEST_CASE(test_where_var_one_occurs_in_two_and_vice_versa)
472 : {
473 1 : test_data_expression("x + y whr x = y + 10, y = x + 3 end", false);
474 1 : }
475 :
476 2 : BOOST_AUTO_TEST_CASE(test_where_in_context)
477 : {
478 3 : test_data_expression("x + y whr x = 3, y = 0 end", { var("x", pos()), var("y", nat()) }, true, "Pos");
479 1 : }
480 :
481 2 : BOOST_AUTO_TEST_CASE(test_where_var_one_occurs_in_two_in_context)
482 : {
483 3 : test_data_expression("x + y whr x = 3, y = x + 10 end", { var("x", pos()), var("y", pos()) }, true, "Pos");
484 1 : }
485 :
486 2 : BOOST_AUTO_TEST_CASE(test_where_var_one_and_two_occur_in_two_in_context)
487 : {
488 3 : test_data_expression("x + y whr x = 3, y = x + y + 10 end", { var("x", pos()), var("y", pos()) }, true, "Pos");
489 1 : }
490 :
491 2 : BOOST_AUTO_TEST_CASE(test_where_var_two_occurs_in_one_in_context)
492 : {
493 3 : test_data_expression("x + y whr x = y + 10, y = 0 end", { var("x", pos()), var("y", nat()) }, true, "Pos");
494 1 : }
495 :
496 2 : BOOST_AUTO_TEST_CASE(test_where_var_one_occurs_in_two_and_vice_versa_in_context)
497 : {
498 3 : test_data_expression("x + y whr x = y + 10, y = x + 3 end", { var("x", pos()), var("y", pos()) }, true, "Pos");
499 1 : }
500 :
501 2 : BOOST_AUTO_TEST_CASE(test_where_mix_nat_pos_list)
502 : {
503 3 : test_data_expression("x ++ y whr x = [0, y], y = [x] end", { var("x", pos()), var("y", nat()) }, false);
504 1 : }
505 :
506 2 : BOOST_AUTO_TEST_CASE(test_where_mix_nat_list)
507 : {
508 3 : test_data_expression("x1 ++ y whr x1 = [0, z], y = [x] end", { var("x", nat()), var("z", nat()) }, true, "List(Nat)");
509 1 : }
510 :
511 2 : BOOST_AUTO_TEST_CASE(test_upcast_pos2nat)
512 : {
513 3 : test_data_expression("x + y", { var("x", pos()), var("y", nat()) }, true, "Pos");
514 3 : test_data_expression("x == y", { var("x", pos()), var("y", nat()) }, true, "Bool");
515 1 : }
516 :
517 21 : void test_data_specification(const std::string& ds_in,
518 : bool expect_success = true,
519 : bool test_type_checker = true)
520 : {
521 21 : data::data_specification ds(parse_data_specification(ds_in, expect_success));
522 :
523 21 : if (test_type_checker)
524 : {
525 :
526 21 : if (expect_success)
527 : {
528 11 : data::typecheck_data_specification(ds);
529 : //Cannot pretty print a data specification anymore.
530 : //std::string ds_out = data::pp(ds);
531 : //BOOST_CHECK_EQUAL(ds_in, ds_out);
532 : }
533 : else
534 : {
535 20 : BOOST_CHECK_THROW(data::typecheck_data_specification(ds), mcrl2::runtime_error);
536 : }
537 : }
538 21 : }
539 :
540 2 : BOOST_AUTO_TEST_CASE(test_data_specification_struct_with_projection)
541 : {
542 : //test data specification involving structured sorts
543 : //in which projection functions are reused
544 1 : test_data_specification(
545 : "sort S = struct c(p: Bool) | d(p: Bool, q: S);\n"
546 : );
547 1 : }
548 :
549 : // What is the desired result here? I would expect an exception (JK)
550 2 : BOOST_AUTO_TEST_CASE(test_duplicate_sort)
551 : {
552 1 : test_data_specification(
553 : "sort S = struct c;\n"
554 : " S = Nat;\n",
555 : false
556 : );
557 1 : }
558 :
559 2 : BOOST_AUTO_TEST_CASE(test_data_specification_constructor_same_signature)
560 : {
561 : //test data specification involving multiple constructors/functions with
562 : //different signatures
563 1 : test_data_specification(
564 : "sort S;\n"
565 : " T;\n"
566 : "\n"
567 : "cons f: S;\n"
568 : " f: T;\n",
569 : false
570 : );
571 1 : }
572 :
573 2 : BOOST_AUTO_TEST_CASE(test_data_specification_constructor_map_same_signature)
574 : {
575 : //test data specification involving multiple constructors/functions with
576 : //different signatures
577 1 : test_data_specification(
578 : "sort S;\n"
579 : " T;\n"
580 : "\n"
581 : "cons f: S;\n"
582 : "\n"
583 : "map f: T;\n",
584 : false
585 : );
586 1 : }
587 :
588 2 : BOOST_AUTO_TEST_CASE(test_data_specification_constructor_different_signature)
589 : {
590 1 : test_data_specification(
591 : "sort S;\n"
592 : " T;\n"
593 : "\n"
594 : "cons f: S;\n"
595 : " f: S -> T;\n"
596 : );
597 1 : }
598 :
599 2 : BOOST_AUTO_TEST_CASE(test_data_specification_nested_struct)
600 : {
601 1 : test_data_specification(
602 : "sort S = struct t(struct e(Nat));\n"
603 : );
604 1 : }
605 :
606 : //BOOST_AUTO_TEST_CASE(test_multiple_variables)
607 : //{
608 : // test_data_specification(
609 : // "sort S;\n\n"
610 : // "var x: Nat;\n"
611 : // " x: S;\n"
612 : // "eqn x == x + 1 = true;\n",
613 : // false
614 : // );
615 : //}
616 : //
617 : //BOOST_AUTO_TEST_CASE(test_multiple_variables_reversed)
618 : //{
619 : // test_data_specification(
620 : // "sort S;\n\n"
621 : // "var x: S;\n"
622 : // " x: Nat;\n"
623 : // "eqn x == x + 1 = true;\n",
624 : // false
625 : // );
626 : //}
627 :
628 2 : BOOST_AUTO_TEST_CASE(test_sort_as_variable)
629 : {
630 1 : test_data_specification(
631 : "sort S;\n\n"
632 : "map S: S -> Bool;\n\n"
633 : "var S: S;\n"
634 : "eqn S(S) = S == S;\n",
635 : false
636 : );
637 1 : }
638 :
639 : /* BOOST_AUTO_TEST_CASE(test_predefined_aliases) // This test case leads to a parse error, not a typecheck error.
640 : {
641 : test_data_specification(
642 : "sort Nat = Int;\n",
643 : false, // parse error
644 : false // so do not test type checker
645 : );
646 : } */
647 :
648 : /* BOOST_AUTO_TEST_CASE(test_conflicting_aliases) // This test case leads to a parse error, due to the use of Nat.
649 : // This is not a typecheck error. Therefore this case is outcommented.
650 : {
651 : test_data_specification(
652 : "sort S = Nat;\n"
653 : " S = T;\n"
654 : " T = Int;\n",
655 : false
656 : );
657 : } */
658 :
659 : /* BOOST_AUTO_TEST_CASE(test_conflicting_aliases_predefined_left) // This test case leads to a parse error, due to the use of Nat.
660 : {
661 : test_data_specification(
662 : "sort Nat = S;\n"
663 : " S = T;\n"
664 : " T = Int;\n",
665 : false, // parse error
666 : false // so do not test type checker
667 : );
668 : } */
669 :
670 2 : BOOST_AUTO_TEST_CASE(test_cyclic_aliases)
671 : {
672 1 : test_data_specification(
673 : "sort S = U;\n"
674 : " U = S;\n",
675 : false
676 : );
677 1 : }
678 :
679 2 : BOOST_AUTO_TEST_CASE(test_cyclic_aliases_indirect)
680 : {
681 1 : test_data_specification(
682 : "sort S = U;\n"
683 : " U = T;\n"
684 : " T = S;\n",
685 : false
686 : );
687 1 : }
688 :
689 2 : BOOST_AUTO_TEST_CASE(test_matching)
690 : {
691 1 : test_data_specification(
692 : "map f: Pos # Nat -> Bool;\n\n"
693 : "var x: Pos;\n"
694 : " y: Nat;\n"
695 : "eqn f(x, y) = true;\n",
696 : true
697 : );
698 1 : }
699 :
700 2 : BOOST_AUTO_TEST_CASE(test_matching_non_strict)
701 : {
702 1 : test_data_specification(
703 : "map f: Pos # Nat -> Bool;\n\n"
704 : "var x: Pos;\n"
705 : " y: Nat;\n"
706 : "eqn f(x, x) = true;\n",
707 : true
708 : );
709 1 : }
710 :
711 : //BOOST_AUTO_TEST_CASE(test_matching_ambiguous)
712 : //{
713 : // test_data_specification(
714 : // "map f: Pos # Nat -> Bool;\n"
715 : // " f: Nat # Nat -> Bool;\n\n"
716 : // "var x: Pos;\n"
717 : // " y: Nat;\n"
718 : // "eqn f(x, y) = false;\n\n"
719 : // "var x: Pos;\n"
720 : // " y: Nat;\n"
721 : // "eqn f(y, y) = true;\n",
722 : // true
723 : // );
724 : //}
725 : //
726 : //BOOST_AUTO_TEST_CASE(test_matching_ambiguous_rhs)
727 : //{
728 : // test_data_specification(
729 : // "map f: Int;\n\n"
730 : // "var x: Pos;\n"
731 : // "eqn f(x) = -5;\n\n"
732 : // "var x: Pos;\n"
733 : // "eqn f(x) = 3;\n",
734 : // false
735 : // );
736 : //}
737 :
738 2 : BOOST_AUTO_TEST_CASE(test_function_alias)
739 : {
740 1 : test_data_specification(
741 : "sort Array = Nat -> Nat;\n\n"
742 : "map update: Nat # Nat # Array -> Array;\n\n"
743 : "var i,n: Nat;\n"
744 : " f: Array;\n"
745 : "eqn update(i, n, f) = lambda j: Nat. if(i == j, n, f(j));\n",
746 : true
747 : );
748 1 : }
749 :
750 : // Test case for bug #787
751 2 : BOOST_AUTO_TEST_CASE(test_eqn_set_where)
752 : {
753 1 : test_data_specification(
754 : "map f_dot: Set(Bool);\n\n"
755 : "eqn f_dot = if(true, {}, { o: Bool | true whr z=true end });\n",
756 : true
757 : );
758 1 : }
759 :
760 2 : BOOST_AUTO_TEST_CASE(test_recursive_function_sort)
761 : {
762 1 : test_data_specification(
763 : "sort G;\n"
764 : " F = F -> G;\n",
765 : false
766 : );
767 1 : }
768 :
769 2 : BOOST_AUTO_TEST_CASE(test_recursive_function_sort_reverse)
770 : {
771 1 : test_data_specification(
772 : "sort G;\n"
773 : " F = G -> F;\n",
774 : false
775 : );
776 1 : }
777 :
778 2 : BOOST_AUTO_TEST_CASE(test_recursive_struct_no_base)
779 : {
780 1 : test_data_specification(
781 : "sort D = struct f(D);\n",
782 : false
783 : );
784 1 : }
785 :
786 2 : BOOST_AUTO_TEST_CASE(test_recursive_struct_via_function)
787 : {
788 1 : test_data_specification(
789 : "sort G = struct f(Nat -> G);\n",
790 : false
791 : );
792 1 : }
793 :
794 2 : BOOST_AUTO_TEST_CASE(test_recursive_struct_list)
795 : {
796 1 : test_data_specification(
797 : "sort P = struct b(x: List(P));\n",
798 : true
799 : );
800 1 : }
801 :
802 2 : BOOST_AUTO_TEST_CASE(test_recursive_struct_list_indirect)
803 : {
804 1 : test_data_specification(
805 : "sort LP = List(P);\n"
806 : " P = struct b(x: LP);\n",
807 : true
808 : );
809 1 : }
810 :
811 2 : BOOST_AUTO_TEST_CASE(test_alias_loop) // This is a correct declaration, Typical elements of sort B are [], [f([])].
812 : {
813 1 : test_data_specification(
814 : "sort B = List(struct f(B));\n",
815 : true
816 : );
817 1 : }
818 :
819 2 : BOOST_AUTO_TEST_CASE(test_alias_loop_extended)
820 : {
821 1 : test_data_specification(
822 : "sort B = List(struct f(B) | c);\n",
823 : true
824 : );
825 1 : }
826 :
827 :
828 50 : void test_data_expression_in_specification_context(const std::string& de_in,
829 : const std::string& ds_in,
830 : const data::variable_vector& variable_context,
831 : bool expect_success = true,
832 : const std::string& expected_sort = "",
833 : bool test_type_checker = true)
834 : {
835 50 : data::data_specification ds(parse_data_specification(ds_in));
836 :
837 50 : if (test_type_checker)
838 : {
839 50 : data::typecheck_data_specification(ds);
840 50 : std::string ds_out = data::pp(ds);
841 50 : if (utilities::trim_copy(ds_in) != utilities::trim_copy(ds_out))
842 : {
843 0 : std::clog << "Warning, ds_in != ds_out; [" << utilities::trim_copy(ds_in) << " != " << utilities::trim_copy(ds_out) << "]" << std::endl;
844 : }
845 50 : BOOST_CHECK_EQUAL(utilities::trim_copy(ds_in), utilities::trim_copy(ds_out));
846 50 : }
847 :
848 50 : data::data_expression de(parse_data_expression(de_in));
849 :
850 50 : if (test_type_checker)
851 : {
852 50 : if (expect_success)
853 : {
854 36 : de = data::typecheck_data_expression(de, variable_context, ds);
855 :
856 36 : std::string de_out = data::pp(de);
857 :
858 36 : BOOST_CHECK_EQUAL(de_in, de_out);
859 36 : if (expected_sort != "")
860 : {
861 35 : BOOST_CHECK_EQUAL(de.sort(), parse_sort_expression(expected_sort));
862 : }
863 36 : }
864 : else
865 : {
866 28 : BOOST_CHECK_THROW(de = data::typecheck_data_expression(de, variable_context, ds), mcrl2::runtime_error);
867 : }
868 : }
869 50 : }
870 :
871 23 : void test_data_expression_in_specification_context(const std::string& de_in,
872 : const std::string& ds_in,
873 : bool expect_success = true,
874 : const std::string& expected_sort = "",
875 : bool test_type_checker = true)
876 : {
877 23 : data::variable_vector v;
878 23 : test_data_expression_in_specification_context(de_in, ds_in, v, expect_success, expected_sort, test_type_checker);
879 23 : }
880 :
881 2 : BOOST_AUTO_TEST_CASE(test_data_expressions_different_signature)
882 : {
883 1 : test_data_expression_in_specification_context(
884 : "f(f)",
885 : "sort S;\n"
886 : " T;\n"
887 : "\n"
888 : "cons f: S;\n"
889 : " f: S -> T;\n",
890 : true,
891 : "T"
892 : );
893 1 : }
894 :
895 2 : BOOST_AUTO_TEST_CASE(test_data_expressions_struct)
896 : {
897 4 : test_data_expression_in_specification_context(
898 : "x == t(e(3))",
899 : "sort S = struct t(struct e(Nat));\n",
900 2 : { var("x", data::basic_sort("S")) },
901 : true,
902 : "Bool"
903 : );
904 1 : }
905 :
906 2 : BOOST_AUTO_TEST_CASE(test_lambda_variable_aliasing)
907 : {
908 4 : test_data_expression_in_specification_context(
909 : "lambda x: S. x(x)",
910 : "sort S;\n"
911 : " T;\n",
912 2 : { var("x", make_function_sort_(data::basic_sort("S"), data::basic_sort("T"))) },
913 : false);
914 1 : }
915 :
916 2 : BOOST_AUTO_TEST_CASE(test_lambda_anonymous_struct)
917 : {
918 1 : test_data_expression_in_specification_context(
919 : "lambda x: struct t. f(x)",
920 : "map f: struct t -> Bool;\n",
921 : true,
922 : "struct t -> Bool"
923 : );
924 1 : }
925 :
926 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_application)
927 : {
928 1 : test_data_expression_in_specification_context(
929 : "f(f)",
930 : "map f: Nat -> Bool;\n"
931 : " f: Nat;\n",
932 : true,
933 : "Bool"
934 : );
935 1 : }
936 :
937 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_different_arity)
938 : {
939 1 : test_data_expression_in_specification_context(
940 : "f",
941 : "map f: Nat -> Bool;\n"
942 : " f: Nat;\n",
943 : true,
944 : "Nat"
945 : );
946 1 : }
947 :
948 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_different_arity_reverse)
949 : {
950 1 : test_data_expression_in_specification_context(
951 : "f",
952 : "map f: Nat;\n"
953 : " f: Nat -> Bool;\n",
954 : true,
955 : "Nat"
956 : );
957 1 : }
958 :
959 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_different_arity_larger)
960 : {
961 1 : test_data_expression_in_specification_context(
962 : "f",
963 : "map f: Nat -> Bool;\n"
964 : " f: Nat # Nat -> Bool;\n",
965 : false
966 : );
967 1 : }
968 :
969 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_different_arity_horrible)
970 : {
971 1 : test_data_expression_in_specification_context(
972 : "f",
973 : "map f: Nat -> Bool;\n"
974 : " f: Nat # Nat -> Bool;\n"
975 : " f: Nat;\n",
976 : true,
977 : "Nat"
978 : );
979 1 : }
980 :
981 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_different_arity_horrible_app1)
982 : {
983 1 : test_data_expression_in_specification_context(
984 : "f(f)",
985 : "map f: Nat -> Bool;\n"
986 : " f: Nat # Nat -> Bool;\n"
987 : " f: Nat;\n",
988 : true,
989 : "Bool"
990 : );
991 1 : }
992 :
993 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_different_arity_horrible_app2)
994 : {
995 1 : test_data_expression_in_specification_context(
996 : "f(f, f)",
997 : "map f: Nat -> Bool;\n"
998 : " f: Nat # Nat -> Bool;\n"
999 : " f: Nat;\n",
1000 : true,
1001 : "Bool"
1002 : );
1003 1 : }
1004 :
1005 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_different_arity_horrible_abs)
1006 : {
1007 1 : test_data_expression_in_specification_context(
1008 : "f((lambda x: Bool. f)(f(f, f)))",
1009 : "map f: Nat -> Bool;\n"
1010 : " f: Nat # Nat -> Bool;\n"
1011 : " f: Nat;\n",
1012 : true,
1013 : "Bool"
1014 : );
1015 1 : }
1016 :
1017 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_different_arity_functional)
1018 : {
1019 1 : test_data_expression_in_specification_context(
1020 : "f",
1021 : "map f: Nat -> Nat -> Bool;\n"
1022 : " f: Nat -> Bool;\n",
1023 : false
1024 : );
1025 1 : }
1026 :
1027 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_same_arity)
1028 : {
1029 1 : test_data_expression_in_specification_context(
1030 : "f",
1031 : "map f: Pos -> Nat;\n"
1032 : " f: Nat -> Pos;\n",
1033 : false
1034 : );
1035 1 : }
1036 :
1037 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_same_arity_application_nat_constant)
1038 : {
1039 1 : test_data_expression_in_specification_context(
1040 : "f(0)",
1041 : "map f: Pos -> Nat;\n"
1042 : " f: Nat -> Pos;\n",
1043 : true,
1044 : "Pos"
1045 : );
1046 1 : }
1047 :
1048 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_same_arity_application_pos_constant)
1049 : {
1050 1 : test_data_expression_in_specification_context(
1051 : "f(1)",
1052 : "map f: Pos -> Nat;\n"
1053 : " f: Nat -> Pos;\n",
1054 : true,
1055 : "Nat"
1056 : );
1057 1 : }
1058 :
1059 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_same_arity_application_nat_variable)
1060 : {
1061 4 : test_data_expression_in_specification_context(
1062 : "f(x)",
1063 : "map f: Pos -> Nat;\n"
1064 : " f: Nat -> Pos;\n",
1065 2 : { var("x", nat()) },
1066 : true,
1067 : "Pos"
1068 : );
1069 1 : }
1070 :
1071 2 : BOOST_AUTO_TEST_CASE(test_duplicate_function_same_arity_application_pos_variable)
1072 : {
1073 4 : test_data_expression_in_specification_context(
1074 : "f(x)",
1075 : "map f: Pos -> Nat;\n"
1076 : " f: Nat -> Pos;\n",
1077 2 : { var("x", pos()) },
1078 : true,
1079 : "Nat"
1080 : );
1081 1 : }
1082 :
1083 2 : BOOST_AUTO_TEST_CASE(test_function_symbol)
1084 : {
1085 1 : test_data_expression_in_specification_context(
1086 : "f",
1087 : "map f: Nat -> Bool;\n",
1088 : true,
1089 : "Nat -> Bool"
1090 : );
1091 1 : }
1092 :
1093 2 : BOOST_AUTO_TEST_CASE(test_function_application_pos_constant)
1094 : {
1095 1 : test_data_expression_in_specification_context(
1096 : "f(1)",
1097 : "map f: Nat -> Bool;\n",
1098 : true,
1099 : "Bool"
1100 : );
1101 1 : }
1102 :
1103 2 : BOOST_AUTO_TEST_CASE(test_function_application_nat_constant)
1104 : {
1105 1 : test_data_expression_in_specification_context(
1106 : "f(0)",
1107 : "map f: Nat -> Bool;\n",
1108 : true,
1109 : "Bool"
1110 : );
1111 1 : }
1112 :
1113 2 : BOOST_AUTO_TEST_CASE(test_function_application_int_constant)
1114 : {
1115 1 : test_data_expression_in_specification_context(
1116 : "f(-1)",
1117 : "map f: Nat -> Bool;\n",
1118 : false
1119 : );
1120 1 : }
1121 :
1122 2 : BOOST_AUTO_TEST_CASE(test_function_application_pos_variable)
1123 : {
1124 4 : test_data_expression_in_specification_context(
1125 : "f(x)",
1126 : "map f: Nat -> Bool;\n",
1127 2 : { var("x", pos()) },
1128 : true,
1129 : "Bool"
1130 : );
1131 1 : }
1132 :
1133 2 : BOOST_AUTO_TEST_CASE(test_function_application_nat_variable)
1134 : {
1135 4 : test_data_expression_in_specification_context(
1136 : "f(x)",
1137 : "map f: Nat -> Bool;\n",
1138 2 : { var("x", nat()) },
1139 : true,
1140 : "Bool"
1141 : );
1142 1 : }
1143 :
1144 2 : BOOST_AUTO_TEST_CASE(test_function_application_int_variable)
1145 : {
1146 3 : test_data_expression_in_specification_context(
1147 : "f(x)",
1148 : "map f: Nat -> Bool;\n",
1149 1 : { var("x", data::sort_int::int_()) },
1150 : false
1151 : );
1152 1 : }
1153 :
1154 2 : BOOST_AUTO_TEST_CASE(test_struct_constructor)
1155 : {
1156 1 : test_data_expression_in_specification_context(
1157 : "c",
1158 : "sort S = struct c(Nat);\n",
1159 : true,
1160 : "Nat -> S"
1161 : );
1162 1 : }
1163 :
1164 2 : BOOST_AUTO_TEST_CASE(test_struct_constructor_application_pos_constant)
1165 : {
1166 1 : test_data_expression_in_specification_context(
1167 : "c(1)",
1168 : "sort S = struct c(Nat);\n",
1169 : true,
1170 : "S"
1171 : );
1172 1 : }
1173 :
1174 2 : BOOST_AUTO_TEST_CASE(test_struct_constructor_application_nat_constant)
1175 : {
1176 1 : test_data_expression_in_specification_context(
1177 : "c(0)",
1178 : "sort S = struct c(Nat);\n",
1179 : true,
1180 : "S"
1181 : );
1182 1 : }
1183 :
1184 2 : BOOST_AUTO_TEST_CASE(test_struct_constructor_application_int_constant)
1185 : {
1186 1 : test_data_expression_in_specification_context(
1187 : "c(-1)",
1188 : "sort S = struct c(Nat);\n",
1189 : false
1190 : );
1191 1 : }
1192 :
1193 2 : BOOST_AUTO_TEST_CASE(test_struct_constructor_application_pos_variable)
1194 : {
1195 4 : test_data_expression_in_specification_context(
1196 : "c(x)",
1197 : "sort S = struct c(Nat);\n",
1198 2 : { var("x", pos()) },
1199 : true,
1200 : "S"
1201 : );
1202 1 : }
1203 :
1204 2 : BOOST_AUTO_TEST_CASE(test_struct_constructor_application_nat_variable)
1205 : {
1206 4 : test_data_expression_in_specification_context(
1207 : "c(x)",
1208 : "sort S = struct c(Nat);\n",
1209 2 : { var("x", nat()) },
1210 : true,
1211 : "S"
1212 : );
1213 1 : }
1214 :
1215 2 : BOOST_AUTO_TEST_CASE(test_struct_constructor_application_int_variable)
1216 : {
1217 3 : test_data_expression_in_specification_context(
1218 : "c(x)",
1219 : "sort S = struct c(Nat);\n",
1220 1 : { var("x", data::sort_int::int_()) },
1221 : false
1222 : );
1223 1 : }
1224 :
1225 2 : BOOST_AUTO_TEST_CASE(test_ambiguous_function)
1226 : {
1227 1 : test_data_expression_in_specification_context(
1228 : "f",
1229 : "sort U;\n"
1230 : " S;\n"
1231 : " T;\n\n"
1232 : "map f: Pos;\n"
1233 : " f: Pos # Nat -> U;\n"
1234 : " f: Pos # Pos -> S;\n"
1235 : " f: Nat # Pos -> T;\n",
1236 : true,
1237 : "Pos"
1238 : );
1239 1 : }
1240 :
1241 2 : BOOST_AUTO_TEST_CASE(test_ambiguous_function_application1)
1242 : {
1243 7 : test_data_expression_in_specification_context(
1244 : "f(x, x)",
1245 : "sort U;\n"
1246 : " S;\n"
1247 : " T;\n\n"
1248 : "map f: Pos;\n"
1249 : " f: Pos # Nat -> U;\n"
1250 : " f: Pos # Pos -> S;\n"
1251 : " f: Nat # Pos -> T;\n",
1252 4 : { var("x", pos()), var("y", nat()) },
1253 : true,
1254 : "S"
1255 : );
1256 1 : }
1257 :
1258 2 : BOOST_AUTO_TEST_CASE(test_ambiguous_function_application2)
1259 : {
1260 7 : test_data_expression_in_specification_context(
1261 : "f(x, y)",
1262 : "sort U;\n"
1263 : " S;\n"
1264 : " T;\n\n"
1265 : "map f: Pos;\n"
1266 : " f: Pos # Nat -> U;\n"
1267 : " f: Pos # Pos -> S;\n"
1268 : " f: Nat # Pos -> T;\n",
1269 4 : { var("x", pos()), var("y", nat()) },
1270 : true,
1271 : "U"
1272 : );
1273 1 : }
1274 :
1275 2 : BOOST_AUTO_TEST_CASE(test_ambiguous_function_application3)
1276 : {
1277 7 : test_data_expression_in_specification_context(
1278 : "f(y, x)",
1279 : "sort U;\n"
1280 : " S;\n"
1281 : " T;\n\n"
1282 : "map f: Pos;\n"
1283 : " f: Pos # Nat -> U;\n"
1284 : " f: Pos # Pos -> S;\n"
1285 : " f: Nat # Pos -> T;\n",
1286 4 : { var("x", pos()), var("y", nat()) },
1287 : true,
1288 : "T"
1289 : );
1290 1 : }
1291 :
1292 : //BOOST_AUTO_TEST_CASE(test_ambiguous_function_application4)
1293 : //{
1294 : // test_data_expression_in_specification_context(
1295 : // "f(x, x)",
1296 : // "sort S;\n"
1297 : // " T;\n"
1298 : // " U;\n\n"
1299 : // "map f: Pos;\n"
1300 : // " f: Pos # Nat -> U;\n"
1301 : // " f: Nat # Nat -> S;\n"
1302 : // " f: Nat # Pos -> T;\n",
1303 : // { var("x", pos()), var("y", nat()) },
1304 : // true,
1305 : // "S"
1306 : // );
1307 : //}
1308 : //
1309 : //BOOST_AUTO_TEST_CASE(test_ambiguous_function_application4a)
1310 : //{
1311 : // test_data_expression_in_specification_context(
1312 : // "f(x, x)",
1313 : // "sort U;\n"
1314 : // " S;\n"
1315 : // " T;\n\n"
1316 : // "map f: Pos;\n"
1317 : // " f: Pos # Nat -> U;\n"
1318 : // " f: Nat # Nat -> S;\n"
1319 : // " f: Nat # Pos -> T;\n",
1320 : // { var("x", pos()), var("y", nat()) },
1321 : // true,
1322 : // "S"
1323 : // );
1324 : //}
1325 :
1326 2 : BOOST_AUTO_TEST_CASE(test_ambiguous_function_application5)
1327 : {
1328 7 : test_data_expression_in_specification_context(
1329 : "f(x, x)",
1330 : "sort S;\n"
1331 : " T;\n"
1332 : " U;\n\n"
1333 : "map f: Pos;\n"
1334 : " f: Nat # Nat -> S;\n"
1335 : " f: Nat # Pos -> T;\n"
1336 : " f: Pos # Nat -> U;\n",
1337 4 : { var("x", pos()), var("y", nat()) },
1338 : true,
1339 : "S"
1340 : );
1341 1 : }
1342 :
1343 2 : BOOST_AUTO_TEST_CASE(test_ambiguous_function_application_recursive)
1344 : {
1345 4 : test_data_expression_in_specification_context(
1346 : "g(f(x))",
1347 : "map g: Int -> Bool;\n"
1348 : " f: Pos -> Nat;\n"
1349 : " f: Pos -> Int;\n",
1350 2 : { var("x", pos()) },
1351 : false
1352 : );
1353 1 : }
1354 :
1355 2 : BOOST_AUTO_TEST_CASE(test_ambiguous_function_application_recursive2)
1356 : {
1357 4 : test_data_expression_in_specification_context(
1358 : "g(f(x))",
1359 : "map g: Int -> Bool;\n"
1360 : " f: Pos -> Nat;\n"
1361 : " f: Pos -> Int;\n"
1362 : " g: Int -> Int;\n",
1363 2 : { var("x", pos()) },
1364 : false
1365 : );
1366 1 : }
1367 :
1368 2 : BOOST_AUTO_TEST_CASE(test_ambiguous_function_application_recursive3)
1369 : {
1370 4 : test_data_expression_in_specification_context(
1371 : "g(f(x))",
1372 : "map g: Int -> Bool;\n"
1373 : " f: Pos -> Nat;\n"
1374 : " f,g: Int -> Int;\n",
1375 2 : { var("x", pos()) },
1376 : false,
1377 : "Bool"
1378 : );
1379 1 : }
1380 :
1381 2 : BOOST_AUTO_TEST_CASE(test_ambiguous_function_application_recursive4)
1382 : {
1383 4 : test_data_expression_in_specification_context(
1384 : "g(f(x))",
1385 : "map g: Int -> Bool;\n"
1386 : " f: Pos -> Nat;\n"
1387 : " f: Pos -> Int;\n"
1388 : " g: Nat -> Int;\n",
1389 2 : { var("x", pos()) },
1390 : false
1391 : );
1392 1 : }
1393 :
1394 2 : BOOST_AUTO_TEST_CASE(test_aliases)
1395 : {
1396 7 : test_data_expression_in_specification_context(
1397 : "f == g",
1398 : "sort B;\n"
1399 : " A = List(List(B));\n"
1400 : " C = List(B);\n",
1401 4 : { var("f", data::basic_sort("A")), var("g", list(data::basic_sort("C"))) },
1402 : true
1403 : );
1404 1 : }
1405 :
1406 2 : BOOST_AUTO_TEST_CASE(test_bag_with_pos_as_argument)
1407 : {
1408 1 : test_data_expression_in_specification_context(
1409 : "{ n: Pos | n + 1 }",
1410 : "sort dummy;\n",
1411 : { },
1412 : true,
1413 : "Bag(Pos)"
1414 : );
1415 1 : }
1416 :
1417 2 : BOOST_AUTO_TEST_CASE(test_bag_with_nat_as_argument1)
1418 : {
1419 1 : test_data_expression_in_specification_context(
1420 : "{ n: Pos | 0 }",
1421 : "sort dummy;\n",
1422 : { },
1423 : true,
1424 : "Bag(Pos)"
1425 : );
1426 1 : }
1427 :
1428 2 : BOOST_AUTO_TEST_CASE(test_bag_with_nat_as_argument2)
1429 : {
1430 1 : test_data_expression_in_specification_context(
1431 : "{ n: Nat | n }",
1432 : "sort dummy;\n",
1433 : { },
1434 : true,
1435 : "Bag(Nat)"
1436 : );
1437 1 : }
1438 :
1439 2 : BOOST_AUTO_TEST_CASE(test_bag_with_real_as_argument)
1440 : {
1441 3 : test_data_expression_in_specification_context(
1442 : "{ n: Pos | 2 / 3 }",
1443 : "sort dummy;\n",
1444 2 : data::variable_vector(),
1445 : false
1446 : );
1447 1 : }
1448 :
1449 : /* The test below shows an ambiguous projection function that
1450 : * cannot be resolved with the current typechecker. This test should
1451 : * be enabled with a new typechecker. */
1452 2 : BOOST_AUTO_TEST_CASE(test_ambiguous_projection_function)
1453 : {
1454 4 : test_data_expression_in_specification_context(
1455 : "R(pi_1(p)) && IS_T1(p)",
1456 : "sort S;\n"
1457 : " T = struct T0 | T1(pi_1: T)?IS_T1 | T2(pi_1: S)?IS_T2;\n\n"
1458 : "map R: T -> Bool;\n",
1459 2 : { var("p", data::basic_sort("T")) },
1460 : false // <-------------- Should be set to true with a new typechecker ---------------------------------------
1461 : );
1462 1 : }
1463 :
1464 :
1465 2 : BOOST_AUTO_TEST_CASE(test_lambda_term_with_wrong_number_of_arguments)
1466 : {
1467 : /* The typechecker couldn't catch the wrongly typed term below in november 2012,
1468 : which led to a core dump */
1469 1 : test_data_expression("((lambda x: Nat. x)(1, 2) > 0)",false);
1470 1 : }
1471 :
1472 : /* The example below has the nasty feature that the sort of
1473 : # in the expression below can be #:List(Nat)->Nat,
1474 : List(Int)->Nat and List(Real)->Nat. In version 10169 of
1475 : the toolset the type of # became List(PossibleTypes([Nat, Int, Real])
1476 : causing confusion in the other tools */
1477 2 : BOOST_AUTO_TEST_CASE(test_avoidance_of_possible_types)
1478 : {
1479 1 : test_data_expression_in_specification_context(
1480 : "#[0, 1] == -1",
1481 : "sort dummy;\n",
1482 : { },
1483 : true,
1484 : "Bool"
1485 : );
1486 1 : }
1487 :
1488 : /* The next example checks whether Int2Pos is properly typed. */
1489 2 : BOOST_AUTO_TEST_CASE(test_proper_use_of_int2pos)
1490 : {
1491 1 : test_data_expression_in_specification_context(
1492 : "f(Int2Pos(-1))",
1493 : "map f: Pos -> Bool;\n",
1494 : { },
1495 : true,
1496 : "Bool"
1497 : );
1498 1 : }
1499 :
1500 : /* This example checks whether explicit transformations among
1501 : * numbers are properly typable.*/
1502 2 : BOOST_AUTO_TEST_CASE(test_proper_use_of_int2pos1)
1503 : {
1504 1 : test_data_expression_in_specification_context(
1505 : "fpos(Nat2Pos(0)) && fpos(Int2Pos(-1)) && fpos(Real2Pos(1 / 2)) && "
1506 : "fnat(Int2Nat(-1)) && fnat(Real2Nat(1 / 2)) && "
1507 : "fint(Real2Int(1 / 2))",
1508 : "map fpos: Pos -> Bool;\n"
1509 : " fnat: Nat -> Bool;\n"
1510 : " fint: Int -> Bool;\n",
1511 : { },
1512 : true,
1513 : "Bool"
1514 : );
1515 1 : }
1516 :
1517 : class testable_sort_type_checker: public data::sort_type_checker
1518 : {
1519 : public:
1520 15 : std::pair<bool, bool> check_alias(const data::alias& x)
1521 : {
1522 : // search for the alias x
1523 : // auto x_iter = m_normalized_aliases.end();
1524 : // for (auto i = m_normalized_aliases.begin(); i != m_normalized_aliases.end(); ++i)
1525 15 : bool found=false;
1526 120 : for (const data::alias& a: get_sort_specification().user_defined_aliases())
1527 : {
1528 120 : if (a == x)
1529 : {
1530 15 : found=true;
1531 15 : break;
1532 : }
1533 : }
1534 : // if (x_iter == m_normalized_aliases.end())
1535 15 : if (!found)
1536 : {
1537 0 : throw mcrl2::runtime_error("could not find alias " + data::pp(x));
1538 : }
1539 :
1540 15 : std::map < data::basic_sort, data::sort_expression > alias_map;
1541 240 : for(const data::alias& a: get_sort_specification().user_defined_aliases())
1542 : {
1543 225 : alias_map[a.name()]=a.reference();
1544 : }
1545 15 : std::set<data::basic_sort> sort_already_seen;
1546 :
1547 : bool first, second;
1548 : try
1549 : {
1550 15 : first = true;
1551 :
1552 : // check_alias_recursion(x.name(), x.reference());
1553 15 : check_for_sort_alias_loop_through_function_sort(x.name(),x.reference(),sort_already_seen, false, alias_map);
1554 10 : assert(sort_already_seen.size()==0);
1555 : }
1556 5 : catch (mcrl2::runtime_error& e)
1557 : {
1558 5 : mCRL2log(log::debug) << e.what() << std::endl;
1559 5 : first = false;
1560 5 : }
1561 : try
1562 : {
1563 15 : second = true;
1564 : // check_alias_circularity(x.name(), x.reference());
1565 23 : check_alias_circularity(x.name(), x.reference(),sort_already_seen, alias_map);
1566 7 : assert(sort_already_seen.size()==0);
1567 : }
1568 8 : catch (mcrl2::runtime_error& e)
1569 : {
1570 8 : mCRL2log(log::debug) << e.what() << std::endl;
1571 8 : second = false;
1572 8 : }
1573 30 : return std::make_pair(first, second);
1574 15 : }
1575 :
1576 : /// \brief constructs a sort expression checker.
1577 1 : testable_sort_type_checker(const data::sort_specification& sort_spec)
1578 1 : : data::sort_type_checker(sort_spec, false)
1579 1 : {}
1580 :
1581 : };
1582 :
1583 2 : BOOST_AUTO_TEST_CASE(test_sort_aliases)
1584 : {
1585 : std::pair<data::basic_sort_vector, data::alias_vector> sortspec = data::parse_sort_specification(
1586 : "sort \n"
1587 : " A; \n"
1588 : " B; \n"
1589 : " C; \n"
1590 : " A1 = A1; \n"
1591 : " A2 = List(A2); \n"
1592 : " A3 = Set(A3); \n"
1593 : " A4 = Bag(A4); \n"
1594 : " A5 = A5 -> B; \n"
1595 : " A6 = B -> A6; \n"
1596 : " A7 = struct f(A7); \n"
1597 : " A8 = struct f(Nat -> A8); \n"
1598 : " A9 = struct f(x: List(A9)); \n"
1599 : " A10 = List(struct f(A10)); \n"
1600 : " A11 = struct A11 | B; \n"
1601 : " A12 = FSet(A12); \n"
1602 : " A13 = FBag(A13); \n"
1603 : " A14 = struct f(FSet(A14)) | c;\n"
1604 : " A15 = struct f(FSet(A15)) | g(FBag(A15)) | c;\n"
1605 2 : );
1606 :
1607 : std::string expected_results(
1608 : " A1 true false \n"
1609 : " A2 true false \n"
1610 : " A3 false false \n"
1611 : " A4 false false \n"
1612 : " A5 false false \n"
1613 : " A6 false false \n"
1614 : " A7 true true \n"
1615 : " A8 false true \n"
1616 : " A9 true true \n"
1617 : " A10 true true \n"
1618 : " A11 true true \n"
1619 : " A12 true false \n"
1620 : " A13 true false \n"
1621 : " A14 true true \n"
1622 : " A15 true true \n"
1623 1 : );
1624 :
1625 1 : std::map<std::string, std::pair<bool, bool> > expected_result_map;
1626 16 : for (const std::string& line: utilities::regex_split(expected_results, "\\n"))
1627 : {
1628 30 : auto words = utilities::regex_split(utilities::trim_copy(line), "\\s+");
1629 15 : if (words.size() == 3)
1630 : {
1631 15 : std::string name = words[0];
1632 15 : bool result1 = words[1] == "true";
1633 15 : bool result2 = words[2] == "true";
1634 15 : expected_result_map[name] = std::make_pair(result1, result2);
1635 15 : }
1636 16 : }
1637 :
1638 1 : data::sort_specification sp(sortspec.first,sortspec.second);
1639 1 : testable_sort_type_checker checker(sp);
1640 16 : for (const data::alias& a: sortspec.second)
1641 : {
1642 15 : std::pair<bool, bool> result = checker.check_alias(a);
1643 15 : std::string name = core::pp(a.name().name());
1644 15 : std::pair<bool, bool> expected_result = expected_result_map[name];
1645 15 : if (result != expected_result)
1646 : {
1647 0 : std::clog << "ERROR: alias " << a
1648 0 : << " result = " << std::boolalpha << result.first << " " << std::boolalpha << result.second
1649 0 : << " expected result = " << std::boolalpha << expected_result.first << " " << std::boolalpha << expected_result.second
1650 0 : << std::endl;
1651 : }
1652 15 : BOOST_CHECK(result == expected_result);
1653 15 : }
1654 1 : }
1655 :
|
