Line data Source code
1 : // Author(s): 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 : /// \file type_check_tree_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE type_check_tree_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/data/experimental/type_check_tree.h"
16 : #include "mcrl2/data/print.h"
17 :
18 :
19 : using namespace mcrl2;
20 :
21 71 : void test_data_expression(const std::string& text, const std::string& variable_context = "", const std::string& expected_sort = "", bool expected_result = true)
22 : {
23 71 : std::cout << "--------------------------------------------------------------------" << std::endl;
24 71 : std::cout << "text = " << text << std::endl;
25 71 : std::cout << "variables = " << variable_context << std::endl;
26 71 : std::cout << "expected sort = " << expected_sort << std::endl;
27 71 : std::cout << "expected result = " << std::boolalpha << expected_result << std::endl;
28 71 : data::data_specification dataspec;
29 71 : core::parser p(parser_tables_mcrl2, core::detail::ambiguity_fn, core::detail::syntax_error_fn);
30 71 : unsigned int start_symbol_index = p.start_symbol_index("DataExpr");
31 71 : bool partial_parses = false;
32 71 : core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
33 71 : core::warn_and_or(node);
34 71 : data::type_check_context context;
35 71 : data::variable_list variables = data::parse_variables(variable_context);
36 71 : data::type_check_node_ptr tnode = data::type_check_tree_generator(context, p).parse_DataExpr(node);
37 71 : context.add_context_variables(variables);
38 71 : tnode->set_constraint(context);
39 71 : data::print_node(tnode);
40 71 : context.remove_context_variables(variables);
41 71 : }
42 :
43 15 : void test_data_expression_fail(const std::string& text, const std::string& variable_context = "", const std::string& expected_sort = "")
44 : {
45 15 : test_data_expression(text, variable_context, expected_sort, false);
46 15 : }
47 :
48 2 : BOOST_AUTO_TEST_CASE(data_expressions_test)
49 : {
50 1 : test_data_expression("x" , "x: Pos;" , "Pos" );
51 1 : test_data_expression("true" , "" , "Bool" );
52 1 : test_data_expression("if(true, true, false)" , "" , "Bool" );
53 1 : test_data_expression("!true" , "" , "Bool" );
54 1 : test_data_expression("true && false" , "" , "Bool" );
55 1 : test_data_expression("0" , "" , "Nat" );
56 1 : test_data_expression("-1" , "" , "Int" );
57 1 : test_data_expression("0 + 1" , "" , "Pos" );
58 1 : test_data_expression("1 + 0" , "" , "Pos" );
59 1 : test_data_expression("0 + 0" , "" , "Nat" );
60 1 : test_data_expression("1 + 1" , "" , "Pos" );
61 1 : test_data_expression("1 * 2 + 3" , "" , "Pos" );
62 1 : test_data_expression("[]" , "" , "" );
63 1 : test_data_expression("[] ++ []" , "" , "" );
64 1 : test_data_expression("#[]" , "" , "Nat" );
65 1 : test_data_expression("true in []" , "" , "Bool" );
66 1 : test_data_expression("[true, false]" , "" , "List(Bool)" );
67 1 : test_data_expression("[0]" , "" , "List(Nat)" );
68 1 : test_data_expression("[1, 2]" , "" , "List(Pos)" );
69 1 : test_data_expression("[0] ++ [1, 2]" , "" , "List(Nat)" );
70 1 : test_data_expression("[0, 1, 2]" , "" , "List(Nat)" );
71 1 : test_data_expression("[1, 0, 2]" , "" , "List(Nat)" );
72 1 : test_data_expression("l ++ [1, 2]" , "l: List(Nat);" , "List(Nat)" );
73 1 : test_data_expression("l ++ [1, 2]" , "l: List(Pos);" , "List(Pos)" );
74 1 : test_data_expression("[0] ++ l" , "l: List(Nat);" , "List(Nat)" );
75 1 : test_data_expression("{}" , "" , "" );
76 1 : test_data_expression("!{}" , "" , "" );
77 1 : test_data_expression("!{} <= {}" , "" , "" );
78 1 : test_data_expression("{} <= !{}" , "" , "" );
79 1 : test_data_expression("{ true, false }" , "" , "FSet(Bool)" );
80 1 : test_data_expression("{ 1, 2, -7 }" , "" , "FSet(Int)" );
81 1 : test_data_expression("{ x: Nat | x mod 2 == 0 }" , "" , "Set(Nat)" );
82 1 : test_data_expression("{:}" , "" , "" );
83 1 : test_data_expression("{ true: 1, false: 2 }" , "" , "FBag(Bool)" );
84 1 : test_data_expression("{ 1: 1, 2: 2, -8: 8 }" , "" , "FBag(Int)" );
85 1 : test_data_expression("{ x: Nat | (lambda y: Nat. y * y)(x) }" , "" , "Bag(Nat)" );
86 1 : test_data_expression("(lambda x: Bool. x)[true -> false]" , "" , "" );
87 1 : test_data_expression("(lambda x: Bool. x)[true -> false][false -> true]" , "" , "" );
88 1 : test_data_expression("(lambda n: Nat. n mod 2 == 0)[0 -> false]" , "" , "" );
89 1 : test_data_expression("lambda x,y: struct t. x == y" , "" , "struct t # struct t -> Bool");
90 1 : test_data_expression("forall x,y: struct t. x == y" , "" , "Bool" );
91 1 : test_data_expression("forall n: Nat. n >= 0" , "" , "Bool" );
92 1 : test_data_expression("forall n: Nat. n > -1" , "" , "Bool" );
93 1 : test_data_expression("exists x,y: struct t. x == y" , "" , "Bool" );
94 1 : test_data_expression("exists n: Nat. n > 481" , "" , "Bool" );
95 1 : test_data_expression("x == y" , "x: struct t?is_t; y: struct t?is_t;", "Bool" );
96 1 : test_data_expression("x whr x = 3 end" , "x: Nat;" , "Nat" );
97 1 : test_data_expression("x + y whr x = 3, y = 10 end" , "" , "Pos" );
98 1 : test_data_expression("x + y whr x = 3, y = 10 end" , "x: Pos; y: Nat;" , "Pos" );
99 1 : test_data_expression("x + y whr x = 3, y = x + 10 end" , "x: Pos; y: Nat;" , "Pos" );
100 1 : test_data_expression("x + y whr x = 3, y = x + y + 10 end" , "x: Pos; y: Nat;" , "Pos" );
101 1 : test_data_expression("x + y whr x = y + 10, y = 3 end" , "x: Pos; y: Nat;" , "Pos" );
102 1 : test_data_expression("x + y whr x = y + 10, y = x + 3 end" , "x: Pos; y: Nat;" , "Pos" );
103 1 : test_data_expression("x ++ y whr x = [0, y], y = [x] end" , "x: Nat; y: Nat;" , "List(Nat)" );
104 1 : test_data_expression("x + y" , "x: Pos; y: Nat;" , "Pos" );
105 1 : test_data_expression("x == y" , "x: Pos; y: Nat;" , "Bool" );
106 :
107 1 : test_data_expression_fail("[0] ++ l" , "l: List(Pos);" );
108 1 : test_data_expression_fail("x ++ y" , "x: List(Pos); y: List(Pos);" );
109 1 : test_data_expression_fail("x == y" , "x: List(Pos); y: List(Nat);" );
110 1 : test_data_expression_fail("!{:}" , "" );
111 1 : test_data_expression_fail("(lambda x: Bool. x)[0 -> false]" , "" );
112 1 : test_data_expression_fail("lambda x: struct t?is_t. x == t" , "" );
113 1 : test_data_expression_fail("lambda x: struct t. x == t" , "" );
114 1 : test_data_expression_fail("lambda x: struct t?is_t, y: struct t. x == y" , "" );
115 1 : test_data_expression_fail("lambda f: Nat. lambda f: Nat -> Bool. f(f)" , "" );
116 1 : test_data_expression_fail("x == y" , "x: struct t; y: struct t?is_t;");
117 1 : test_data_expression_fail("x + y whr x = 3, y = x + 10 end" , "" );
118 1 : test_data_expression_fail("x + y whr x = 3, y = x + y + 10 end" , "" );
119 1 : test_data_expression_fail("x + y whr x = y + 10, y = 3 end" , "" );
120 1 : test_data_expression_fail("x + y whr x = y + 10, y = x + 3 end" , "" );
121 1 : test_data_expression_fail("x ++ y whr x = [0, y], y = [x] end" , "x: Pos; y: Nat;" );
122 1 : }
123 :
124 2 : BOOST_AUTO_TEST_CASE(replace_untyped_sort_test)
125 : {
126 : using namespace mcrl2::data;
127 1 : const sort_expression& B = sort_bool::bool_();
128 1 : const sort_expression& U = untyped_sort();
129 2 : data_expression s1 = sort_set::intersection(U, sort_fset::fset(U), sort_fset::fset(U));
130 2 : data_expression s2 = sort_set::intersection(B, sort_fset::fset(B), sort_fset::fset(B));
131 1 : BOOST_CHECK(has_untyped_sort(s1));
132 1 : BOOST_CHECK(!has_untyped_sort(s2));
133 1 : BOOST_CHECK(replace_untyped_sort(s1, B) == s2);
134 1 : }
135 :
|