LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - parse_impl.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 248 259 95.8 %
Date: 2024-03-08 02:52:28 Functions: 48 48 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 mcrl2/data/parse_impl.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_PARSE_IMPL_H
      13             : #define MCRL2_DATA_PARSE_IMPL_H
      14             : 
      15             : #include <climits>
      16             : #include <fstream>
      17             : #include "mcrl2/core/parser_utility.h"
      18             : #include "mcrl2/data/function_update.h"
      19             : #include "mcrl2/data/standard_container_utility.h"
      20             : #include "mcrl2/data/typecheck.h"
      21             : #include "mcrl2/data/untyped_data_specification.h"
      22             : 
      23             : namespace mcrl2 {
      24             : 
      25             : namespace data {
      26             : 
      27             : namespace detail {
      28             : 
      29             : struct sort_expression_actions: public core::default_parser_actions
      30             : {
      31        3112 :   explicit sort_expression_actions(const core::parser& parser_)
      32        3112 :     : core::default_parser_actions(parser_)
      33        3112 :   {}
      34             : 
      35       12886 :   data::sort_expression parse_SortExpr(const core::parse_node& node, data::sort_expression_list* product=nullptr) const
      36             :   {
      37       12886 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Bool")) { return sort_bool::bool_(); }
      38        9466 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Pos")) { return sort_pos::pos(); }
      39        7841 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Nat")) { return sort_nat::nat(); }
      40        3774 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Int")) { return sort_int::int_(); }
      41        3659 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Real")) { return sort_real::real_(); }
      42        3567 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "List") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "SortExpr") && (symbol_name(node.child(3)) == ")")) { return sort_list::list(parse_SortExpr(node.child(2))); }
      43        3195 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "Set") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "SortExpr") && (symbol_name(node.child(3)) == ")")) { return sort_set::set_(parse_SortExpr(node.child(2))); }
      44        3125 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "FSet") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "SortExpr") && (symbol_name(node.child(3)) == ")")) { return sort_fset::fset(parse_SortExpr(node.child(2))); }
      45        3111 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "Bag") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "SortExpr") && (symbol_name(node.child(3)) == ")")) { return sort_bag::bag(parse_SortExpr(node.child(2))); }
      46        3093 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "FBag") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "SortExpr") && (symbol_name(node.child(3)) == ")")) { return sort_fbag::fbag(parse_SortExpr(node.child(2))); }
      47        3087 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Id")) { return basic_sort(parse_Id(node.child(0))); }
      48        1511 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "SortExpr") && (symbol_name(node.child(2)) == ")")) { return parse_SortExpr(node.child(1), product); }
      49        1441 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "struct") && (symbol_name(node.child(1)) == "ConstrDeclList")) { return structured_sort(parse_ConstrDeclList(node.child(1))); }
      50        1006 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "SortExpr") && (node.child(1).string() == "->") && (symbol_name(node.child(2)) == "SortExpr")) { return function_sort(parse_SortExpr_as_SortProduct(node.child(0)), parse_SortExpr(node.child(2))); }
      51         442 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "SortExpr") && (node.child(1).string() == "#") && (symbol_name(node.child(2)) == "SortExpr"))
      52             :     {
      53         442 :       if (product != nullptr)
      54             :       {
      55         438 :         data::sort_expression new_element = parse_SortExpr(node.child(2), product);
      56         438 :         if (new_element != data::sort_expression())
      57             :         {
      58         438 :           product->push_front(new_element);
      59             :         }
      60         438 :         new_element = parse_SortExpr(node.child(0), product);
      61         438 :         if (new_element != data::sort_expression())
      62             :         {
      63         334 :           product->push_front(new_element);
      64             :         }
      65         438 :         return data::sort_expression();
      66         438 :       }
      67             :       else
      68             :       {
      69           4 :         throw core::parse_node_exception(node.child(1), "Sort product is only allowed on the left "
      70           8 :                                                         "hand side of ->, and when declaring actions.");
      71             :       }
      72             :     }
      73           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
      74             :   }
      75             : 
      76        1307 :   data::sort_expression_list parse_SortExpr_as_SortProduct(const core::parse_node& node) const
      77             :   {
      78        1307 :     data::sort_expression_list result;
      79        1307 :     data::sort_expression new_element = parse_SortExpr(node, &result);
      80        1307 :     if (new_element != data::sort_expression())
      81             :     {
      82         973 :       result.push_front(new_element);
      83             :     }
      84        2614 :     return result;
      85        1307 :   }
      86             : 
      87         745 :   data::sort_expression_list parse_SortProduct(const core::parse_node& node) const
      88             :   {
      89         745 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "SortExpr"))
      90             :     {
      91        1490 :       return parse_SortExpr_as_SortProduct(node.child(0));
      92             :     }
      93           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
      94             :   }
      95             : 
      96         842 :   data::structured_sort_constructor parse_ConstrDecl(const core::parse_node& node) const
      97             :   {
      98         842 :     core::identifier_string name = parse_Id(node.child(0));
      99         842 :     data::structured_sort_constructor_argument_list arguments;
     100         842 :     core::identifier_string recogniser = atermpp::empty_string();
     101         842 :     if (node.child(1))
     102             :     {
     103         842 :       arguments = parse_ProjDeclList(node.child(1));
     104             :     }
     105         842 :     if (node.child(2))
     106             :     {
     107         842 :       core::parse_node u = node.child(2);
     108         842 :       if (u.child(0))
     109             :       {
     110          62 :         recogniser = parse_Id(node.child(2).child(0).child(1));
     111             :       }
     112         842 :     }
     113        1684 :     return structured_sort_constructor(name, arguments, recogniser);
     114         842 :   }
     115             : 
     116         436 :   data::structured_sort_constructor_list parse_ConstrDeclList(const core::parse_node& node) const
     117             :   {
     118        1278 :     return parse_list<data::structured_sort_constructor>(node, "ConstrDecl", [&](const core::parse_node& node) { return parse_ConstrDecl(node); });
     119             :   }
     120             : 
     121         165 :   data::structured_sort_constructor_argument parse_ProjDecl(const core::parse_node& node) const
     122             :   {
     123         165 :     core::identifier_string name = atermpp::empty_string();
     124         165 :     sort_expression sort = parse_SortExpr(node.child(1));
     125         165 :     if (node.child(0).child(0))
     126             :     {
     127             :       // TODO: check if this nesting depth is correct
     128          89 :       name = parse_Id(node.child(0).child(0).child(0));
     129             :     }
     130         330 :     return structured_sort_constructor_argument(name, sort);
     131         165 :   }
     132             : 
     133         842 :   data::structured_sort_constructor_argument_list parse_ProjDeclList(const core::parse_node& node) const
     134             :   {
     135        1007 :     return parse_list<data::structured_sort_constructor_argument>(node, "ProjDecl", [&](const core::parse_node& node) { return parse_ProjDecl(node); });
     136             :   }
     137             : };
     138             : 
     139             : struct data_expression_actions: public sort_expression_actions
     140             : {
     141        3112 :   data_expression_actions(const core::parser& parser_)
     142        3112 :     : sort_expression_actions(parser_)
     143        3112 :   {}
     144             : 
     145          29 :   data_expression make_untyped_set_or_bag_comprehension(const variable& v, const data_expression& x) const
     146             :   {
     147          58 :     return abstraction(untyped_set_or_bag_comprehension_binder(), { v }, x);
     148             :   }
     149             : 
     150         116 :   data_expression make_list_enumeration(const data_expression_list& x) const
     151             :   {
     152         116 :     assert(!x.empty());
     153         232 :     return sort_list::list_enumeration(untyped_sort(),x);
     154             :   }
     155             : 
     156         174 :   data_expression make_set_enumeration(const data_expression_list& x) const
     157             :   {
     158         174 :     assert(!x.empty());
     159         348 :     return sort_set::set_enumeration(untyped_sort(),x);
     160             :   }
     161             : 
     162         188 :   data_expression make_bag_enumeration(const data_expression_list& x) const
     163             :   {
     164         188 :     assert(!x.empty());
     165         376 :     return sort_bag::bag_enumeration(untyped_sort(),x);
     166             :   }
     167             : 
     168          29 :   data_expression make_function_update(const data_expression& x, const data_expression& y, const data_expression& z) const
     169             :   {
     170          29 :     return application(function_symbol(mcrl2::data::function_update_name(),untyped_sort()), x, y, z);
     171             :   }
     172             : 
     173             :   template <typename ExpressionContainer>
     174             :   data::sort_expression_list get_sorts(const ExpressionContainer& x) const
     175             :   {
     176             :     data::sort_expression_vector result;
     177             :     for (auto i = x.begin(); i != x.end(); ++i)
     178             :     {
     179             :       result.push_back(i->sort());
     180             :     }
     181             :     return data::sort_expression_list(result.begin(), result.end());
     182             :   }
     183             : 
     184          31 :   data::variable parse_VarDecl(const core::parse_node& node) const
     185             :   {
     186          62 :     return variable(parse_Id(node.child(0)), parse_SortExpr(node.child(2)));
     187             :   }
     188             : 
     189       39618 :   bool callback_VarsDecl(const core::parse_node& node, variable_vector& result) const
     190             :   {
     191       39618 :     if (symbol_name(node) == "VarsDecl")
     192             :     {
     193        8212 :       core::identifier_string_list names = parse_IdList(node.child(0));
     194        8212 :       data::sort_expression sort = parse_SortExpr(node.child(2));
     195       17102 :       for (const core::identifier_string& name: names)
     196             :       {
     197        8890 :         result.push_back(variable(name, sort));
     198             :       }
     199        8212 :       return true;
     200        8212 :     }
     201       31406 :     return false;
     202             :   };
     203             : 
     204        6158 :   data::variable_list parse_VarsDeclList(const core::parse_node& node) const
     205             :   {
     206        6158 :     variable_vector result;
     207       45776 :     traverse(node, [&](const core::parse_node& node) { return callback_VarsDecl(node, result); });
     208       12316 :     return data::variable_list(result.begin(), result.end());
     209        6158 :   }
     210             : 
     211       25190 :   data::data_expression parse_DataExpr(const core::parse_node& node) const
     212             :   {
     213       25190 :     assert(symbol_name(node) == "DataExpr");
     214       25190 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Id")) { return untyped_identifier(parse_Id(node.child(0))); }
     215       14264 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Number")) { return untyped_identifier(parse_Number(node.child(0))); }
     216        9123 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "true")) { return untyped_identifier(parse_Id(node.child(0))); }
     217        8344 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "false")) { return untyped_identifier(parse_Id(node.child(0))); }
     218        7840 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "[") && (symbol_name(node.child(1)) == "]")) { return untyped_identifier("[]"); }
     219        7622 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "{") && (symbol_name(node.child(1)) == "}")) { return untyped_identifier("{}"); }
     220        7596 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "{") && (symbol_name(node.child(1)) == ":") && (symbol_name(node.child(2)) == "}")) { return untyped_identifier("{:}"); }
     221        7697 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "[") && (symbol_name(node.child(1)) == "DataExprList") && (symbol_name(node.child(2)) == "]")) { return make_list_enumeration(parse_DataExprList(node.child(1))); }
     222        7653 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "{") && (symbol_name(node.child(1)) == "BagEnumEltList") && (symbol_name(node.child(2)) == "}")) { return make_bag_enumeration(parse_BagEnumEltList(node.child(1))); }
     223        7306 :     else if ((node.child_count() == 5) && (symbol_name(node.child(0)) == "{") && (symbol_name(node.child(1)) == "VarDecl") && (symbol_name(node.child(2)) == "|") && (symbol_name(node.child(3)) == "DataExpr") && (symbol_name(node.child(4)) == "}")) { return make_untyped_set_or_bag_comprehension(parse_VarDecl(node.child(1)), parse_DataExpr(node.child(3))); }
     224        7422 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "{") && (symbol_name(node.child(1)) == "DataExprList") && (symbol_name(node.child(2)) == "}")) { return make_set_enumeration(parse_DataExprList(node.child(1))); }
     225        7532 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "DataExpr") && (symbol_name(node.child(2)) == ")")) { return parse_DataExpr(node.child(1)); }
     226        6645 :     else if ((node.child_count() == 6) && (symbol_name(node.child(0)) == "DataExpr") && (symbol_name(node.child(1)) == "[") && (symbol_name(node.child(2)) == "DataExpr") && (symbol_name(node.child(3)) == "->") && (symbol_name(node.child(4)) == "DataExpr") && (symbol_name(node.child(5)) == "]")) { return make_function_update(parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2)), parse_DataExpr(node.child(4))); }
     227        6587 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "DataExpr") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "DataExprList") && (symbol_name(node.child(3)) == ")")) { return application(parse_DataExpr(node.child(0)), parse_DataExprList(node.child(2))); }
     228        4769 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "!") && (symbol_name(node.child(1)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(0))), parse_DataExpr(node.child(1))); }
     229        4298 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "-") && (symbol_name(node.child(1)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(0))), parse_DataExpr(node.child(1))); }
     230        4253 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "#") && (symbol_name(node.child(1)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(0))), parse_DataExpr(node.child(1))); }
     231        4200 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "forall") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "DataExpr")) { return forall(parse_VarsDeclList(node.child(1)), parse_DataExpr(node.child(3))); }
     232        4148 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "exists") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "DataExpr")) { return exists(parse_VarsDeclList(node.child(1)), parse_DataExpr(node.child(3))); }
     233        4089 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "lambda") && (symbol_name(node.child(1)) == "VarsDeclList") && (symbol_name(node.child(2)) == ".") && (symbol_name(node.child(3)) == "DataExpr")) { return lambda(parse_VarsDeclList(node.child(1)), parse_DataExpr(node.child(3))); }
     234        4019 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "=>") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     235        3998 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "&&") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     236        3426 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "||") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     237        3314 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "==") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     238        1914 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "!=") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     239        1878 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "<") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     240        1408 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "<=") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     241        1296 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == ">=") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     242        1268 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == ">") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     243        1097 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "in") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     244        1052 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "|>") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     245         870 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "<|") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     246         850 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "++") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     247         838 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "+") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     248         461 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "-") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     249         341 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "/") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     250         167 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "div") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     251         157 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "mod") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     252         112 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == "*") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     253          71 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "DataExpr") && (node.child(1).string() == ".") && (symbol_name(node.child(2)) == "DataExpr")) { return application(untyped_identifier(parse_Id(node.child(1))), parse_DataExpr(node.child(0)), parse_DataExpr(node.child(2))); }
     254          43 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "DataExpr") && (symbol_name(node.child(1)) == "whr") && (symbol_name(node.child(2)) == "AssignmentList") && (symbol_name(node.child(3)) == "end")) { return where_clause(parse_DataExpr(node.child(0)), parse_AssignmentList(node.child(2))); }
     255           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
     256             :   }
     257             : 
     258        1149 :   data::data_expression parse_DataExprUnit(const core::parse_node& node) const
     259             :   {
     260        1149 :     if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Id")) { return untyped_identifier(parse_Id(node.child(0))); }
     261        1064 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "Number")) { return untyped_identifier(parse_Number(node.child(0))); }
     262         738 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "true")) { return untyped_identifier(parse_Id(node.child(0))); }
     263         708 :     else if ((node.child_count() == 1) && (symbol_name(node.child(0)) == "false")) { return untyped_identifier(parse_Id(node.child(0))); }
     264        1397 :     else if ((node.child_count() == 3) && (symbol_name(node.child(0)) == "(") && (symbol_name(node.child(1)) == "DataExpr") && (symbol_name(node.child(2)) == ")")) { return parse_DataExpr(node.child(1)); }
     265           9 :     else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "DataExprUnit") && (symbol_name(node.child(1)) == "(") && (symbol_name(node.child(2)) == "DataExprList") && (symbol_name(node.child(3)) == ")")) { return application(parse_DataExprUnit(node.child(0)), parse_DataExprList(node.child(2))); }
     266           7 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "!") && (symbol_name(node.child(1)) == "DataExprUnit")) { return application(untyped_identifier(parse_Id(node.child(0))), parse_DataExprUnit(node.child(1))); }
     267           0 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "-") && (symbol_name(node.child(1)) == "DataExprUnit")) { return application(untyped_identifier(parse_Id(node.child(0))), parse_DataExprUnit(node.child(1))); }
     268           0 :     else if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "#") && (symbol_name(node.child(1)) == "DataExprUnit")) { return application(untyped_identifier(parse_Id(node.child(0))), parse_DataExprUnit(node.child(1))); }
     269           0 :     throw core::parse_node_unexpected_exception(m_parser, node);
     270             :   }
     271             : 
     272         710 :   data::data_expression parse_DataValExpr(const core::parse_node& node) const
     273             :   {
     274        1420 :     return parse_DataExpr(node.child(2));
     275             :   }
     276             : 
     277        1020 :   data::untyped_identifier_assignment parse_Assignment(const core::parse_node& node) const
     278             :   {
     279        2040 :     return untyped_identifier_assignment(parse_Id(node.child(0)), parse_DataExpr(node.child(2)));
     280             :   }
     281             : 
     282         484 :   data::untyped_identifier_assignment_list parse_AssignmentList(const core::parse_node& node) const
     283             :   {
     284        1504 :     return parse_list<data::untyped_identifier_assignment>(node, "Assignment", [&](const core::parse_node& node) { return parse_Assignment(node); });
     285             :   }
     286             : 
     287        8867 :   data::data_expression_list parse_DataExprList(const core::parse_node& node) const
     288             :   {
     289       18333 :     return parse_list<data::data_expression>(node, "DataExpr", [&](const core::parse_node& node) { return parse_DataExpr(node); });
     290             :   }
     291             : 
     292         188 :   data::data_expression_list parse_BagEnumEltList(const core::parse_node& node) const
     293             :   {
     294         188 :     return parse_DataExprList(node);
     295             :   }
     296             : };
     297             : 
     298             : struct data_specification_actions: public data_expression_actions
     299             : {
     300        2119 :   explicit data_specification_actions(const core::parser& parser_)
     301        2119 :     : data_expression_actions(parser_)
     302        2119 :   {}
     303             : 
     304        1025 :   bool callback_SortDecl(const core::parse_node& node, std::vector<atermpp::aterm_appl>& result) const
     305             :   {
     306        1025 :     if (symbol_name(node) == "SortDecl")
     307             :     {
     308         633 :       if ((node.child_count() == 2) && (symbol_name(node.child(0)) == "IdList") && (symbol_name(node.child(1)) == ";"))
     309             :       {
     310          74 :         core::identifier_string_list ids = parse_IdList(node.child(0));
     311         149 :         for (const core::identifier_string& id: ids)
     312             :         {
     313          75 :           result.push_back(basic_sort(id));
     314             :         }
     315          74 :       }
     316         559 :       else if ((node.child_count() == 4) && (symbol_name(node.child(0)) == "Id") && (symbol_name(node.child(1)) == "=") && (symbol_name(node.child(2)) == "SortExpr") && (symbol_name(node.child(3)) == ";"))
     317             :       {
     318         559 :         result.push_back(alias(basic_sort(parse_Id(node.child(0))), parse_SortExpr(node.child(2))));
     319             :       }
     320             :       else
     321             :       {
     322           0 :         throw core::parse_node_unexpected_exception(m_parser, node);
     323             :       }
     324         633 :       return true;
     325             :     }
     326         392 :     return false;
     327             :   }
     328             : 
     329         392 :   std::vector<atermpp::aterm_appl> parse_SortDeclList(const core::parse_node& node) const
     330             :   {
     331         392 :     std::vector<atermpp::aterm_appl> result;
     332        1417 :     traverse(node, [&](const core::parse_node& node) { return callback_SortDecl(node, result); });
     333         392 :     return result;
     334           0 :   }
     335             : 
     336         392 :   std::vector<atermpp::aterm_appl> parse_SortSpec(const core::parse_node& node) const
     337             :   {
     338         784 :     return parse_SortDeclList(node.child(1));
     339             :   }
     340             : 
     341        2433 :   bool callback_IdsDecl(const core::parse_node& node, function_symbol_vector& result) const
     342             :   {
     343        2433 :     if (symbol_name(node) == "IdsDecl")
     344             :     {
     345         527 :       core::identifier_string_list names = parse_IdList(node.child(0));
     346         527 :       data::sort_expression sort = parse_SortExpr(node.child(2));
     347        1083 :       for (const core::identifier_string& name: names)
     348             :       {
     349         556 :         result.push_back(function_symbol(name, sort));
     350             :       }
     351         527 :       return true;
     352         527 :     }
     353        1906 :     return false;
     354             :   }
     355             : 
     356         284 :   data::function_symbol_vector parse_IdsDeclList(const core::parse_node& node) const
     357             :   {
     358         284 :     function_symbol_vector result;
     359        2717 :     traverse(node, [&](const core::parse_node& node) { return callback_IdsDecl(node, result); });
     360         284 :     return result;
     361           0 :   }
     362             : 
     363          25 :   data::function_symbol_vector parse_ConsSpec(const core::parse_node& node) const
     364             :   {
     365          25 :     return parse_IdsDeclList(node);
     366             :   }
     367             : 
     368         259 :   data::function_symbol_vector parse_MapSpec(const core::parse_node& node) const
     369             :   {
     370         259 :     return parse_IdsDeclList(node);
     371             :   }
     372             : 
     373         505 :   data::variable_list parse_GlobVarSpec(const core::parse_node& node) const
     374             :   {
     375         505 :     return parse_VarsDeclList(node);
     376             :   }
     377             : 
     378         329 :   data::variable_list parse_VarSpec(const core::parse_node& node) const
     379             :   {
     380         329 :     return parse_VarsDeclList(node);
     381             :   }
     382             : 
     383         728 :   bool callback_EqnDecl(const core::parse_node& node, const variable_list& variables, data_equation_vector& result) const
     384             :   {
     385         728 :     if (symbol_name(node) == "EqnDecl")
     386             :     {
     387         548 :       data_expression condition = sort_bool::true_();
     388             :       // TODO: check if this is the correct nesting depth
     389         548 :       if (node.child(0).child(0))
     390             :       {
     391         102 :         condition = parse_DataExpr(node.child(0).child(0).child(0));
     392             :       }
     393         548 :       result.push_back(data_equation(variables, condition, parse_DataExpr(node.child(1)), parse_DataExpr(node.child(3))));
     394         548 :       return true;
     395         548 :     }
     396         180 :     return false;
     397             :   }
     398             : 
     399         180 :   data::data_equation_vector parse_EqnDeclList(const core::parse_node& node, const variable_list& variables) const
     400             :   {
     401         180 :     data_equation_vector result;
     402         908 :     traverse(node, [&](const core::parse_node& node) { return callback_EqnDecl(node, variables, result); });
     403         180 :     return result;
     404           0 :   }
     405             : 
     406         180 :   data::data_equation_vector parse_EqnSpec(const core::parse_node& node) const
     407             :   {
     408         180 :     assert(symbol_name(node) == "EqnSpec");
     409         180 :     variable_list variables = parse_VarSpec(node.child(0));
     410         540 :     return parse_EqnDeclList(node.child(2), variables);
     411         180 :   }
     412             : 
     413        2033 :   bool callback_DataSpecElement(const core::parse_node& node, untyped_data_specification& result) const
     414             :   {
     415        2033 :     if (symbol_name(node) == "SortSpec")
     416             :     {
     417         391 :       std::vector<atermpp::aterm_appl> sorts = parse_SortSpec(node);
     418        1007 :       for (const atermpp::aterm_appl& t: sorts)
     419             :       {
     420         616 :         if (is_alias(t))
     421             :         {
     422         544 :           result.add_alias(alias(t));
     423             :         }
     424             :         else
     425             :         {
     426          72 :           result.add_sort(basic_sort(t));
     427             :         }
     428             :       }
     429         391 :       return true;
     430         391 :     }
     431        1642 :     else if (symbol_name(node) == "ConsSpec")
     432             :     {
     433          25 :       function_symbol_vector functions = parse_ConsSpec(node);
     434          70 :       for (const function_symbol& f: functions)
     435             :       {
     436          45 :         result.add_constructor(f);
     437             :       }
     438          25 :       return true;
     439          25 :     }
     440        1617 :     else if (symbol_name(node) == "MapSpec")
     441             :     {
     442         259 :       function_symbol_vector functions = parse_MapSpec(node);
     443         770 :       for (const function_symbol& f: functions)
     444             :       {
     445         511 :         result.add_mapping(f);
     446             :       }
     447         259 :       return true;
     448         259 :     }
     449        1358 :     else if (symbol_name(node) == "EqnSpec")
     450             :     {
     451         180 :       data_equation_vector equations = parse_EqnSpec(node);
     452         728 :       for (const data_equation& eq: equations)
     453             :       {
     454         548 :         result.add_equation(eq);
     455             :       }
     456         180 :       return true;
     457         180 :     }
     458        1178 :     return false;
     459             :   }
     460             : 
     461         625 :   untyped_data_specification parse_DataSpec(const core::parse_node& node) const
     462             :   {
     463         625 :     untyped_data_specification result;
     464        2156 :     traverse(node, [&](const core::parse_node& node) { return callback_DataSpecElement(node, result); });
     465         625 :     return result;
     466           0 :   }
     467             : };
     468             : 
     469             : } // namespace detail
     470             : 
     471             : } // namespace data
     472             : 
     473             : } // namespace mcrl2
     474             : 
     475             : #endif // MCRL2_DATA_PARSE_IMPL_H

Generated by: LCOV version 1.14