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
|