LCOV - code coverage report
Current view: top level - data/test - type_check_tree_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 105 105 100.0 %
Date: 2024-03-08 02:52:28 Functions: 6 6 100.0 %
Legend: Lines: hit not hit

          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             : 

Generated by: LCOV version 1.14