Line data Source code
1 : // Author(s): Jan Friso Groote
2 : // Wieger Wesselink 2015 -
3 : // Copyright: see the accompanying file COPYING or copy at
4 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
5 : //
6 : // Distributed under the Boost Software License, Version 1.0.
7 : // (See accompanying file LICENSE_1_0.txt or copy at
8 : // http://www.boost.org/LICENSE_1_0.txt)
9 : //
10 : /// \file mcrl2/process/typecheck.h
11 : /// \brief add your file description here.
12 :
13 : #ifndef MCRL2_PROCESS_TYPECHECK_H
14 : #define MCRL2_PROCESS_TYPECHECK_H
15 :
16 : #include <algorithm>
17 : #include "mcrl2/process/detail/match_action_parameters.h"
18 : #include "mcrl2/process/detail/process_context.h"
19 : #include "mcrl2/process/normalize_sorts.h"
20 :
21 : namespace mcrl2
22 : {
23 :
24 : namespace process
25 : {
26 :
27 : inline
28 3082 : action typecheck_action(const core::identifier_string& name,
29 : const data::data_expression_list& parameters,
30 : data::data_type_checker& typechecker,
31 : const data::detail::variable_context& variable_context,
32 : const detail::action_context& action_context
33 : )
34 : {
35 3082 : std::string msg = "action";
36 3082 : data::sorts_list parameter_list = action_context.matching_action_sorts(name, parameters);
37 3082 : auto p = process::detail::match_action_parameters(parameters, parameter_list, variable_context, name, msg, typechecker);
38 9243 : return action(action_label(name, p.second), p.first);
39 3083 : }
40 :
41 : // returns the intersection of the 2 type list lists
42 : inline
43 390 : data::sorts_list sorts_list_intersection(const data::sorts_list& sorts1, const data::sorts_list& sorts2)
44 : {
45 390 : data::sorts_list result;
46 852 : for (const data::sort_expression_list& s: sorts2)
47 : {
48 462 : if (std::find(sorts1.begin(), sorts1.end(), s) != sorts1.end())
49 : {
50 462 : result.push_front(s);
51 : }
52 : }
53 780 : return atermpp::reverse(result);
54 390 : }
55 :
56 : inline
57 : std::ostream& operator<<(std::ostream& out, const data::sorts_list& x)
58 : {
59 : out << "[";
60 : for (auto i = x.begin(); i != x.end(); ++i)
61 : {
62 : if (i != x.begin())
63 : {
64 : out << ", ";
65 : }
66 : out << *i;
67 : }
68 : return out;
69 : }
70 :
71 : namespace detail
72 : {
73 :
74 : bool equal_multi_actions(core::identifier_string_list a1, core::identifier_string_list a2);
75 :
76 : // returns true if a is in A
77 : inline
78 182 : bool multi_actions_contains(const core::identifier_string_list& a, const action_name_multiset_list& A)
79 : {
80 567 : for (const action_name_multiset& i: A)
81 : {
82 385 : if (equal_multi_actions(a, i.names()))
83 : {
84 0 : return true;
85 : }
86 : }
87 182 : return false;
88 : }
89 :
90 : // returns true if the two multiactions are equal.
91 : inline
92 385 : bool equal_multi_actions(core::identifier_string_list a1, core::identifier_string_list a2)
93 : {
94 385 : if (a1.size() != a2.size())
95 : {
96 1 : return false;
97 : }
98 384 : if (a1.empty())
99 : {
100 0 : return true;
101 : }
102 384 : core::identifier_string Act1 = a1.front();
103 384 : a1 = a1.tail();
104 :
105 : //remove Act1 once from a2. if not there -- return ATfalse.
106 384 : core::identifier_string_list NewMAct2;
107 768 : for (; !a2.empty(); a2 = a2.tail())
108 : {
109 384 : core::identifier_string Act2 = a2.front();
110 384 : if (Act1 == Act2)
111 : {
112 0 : a2 = atermpp::reverse(NewMAct2) + a2.tail();
113 0 : return equal_multi_actions(a1, a2);
114 : }
115 : else
116 : {
117 384 : NewMAct2.push_front(Act2);
118 : }
119 384 : }
120 384 : return false;
121 384 : }
122 :
123 : inline
124 : std::ostream& operator<<(std::ostream& out, const std::pair<core::identifier_string, data::sort_expression_list>& x)
125 : {
126 : return out << "(" << x.first << ", " << x.second << ")";
127 : }
128 :
129 : struct typecheck_builder: public process_expression_builder<typecheck_builder>
130 : {
131 : typedef process_expression_builder<typecheck_builder> super;
132 : using super::apply;
133 :
134 : data::data_type_checker& m_data_type_checker;
135 : data::detail::variable_context m_variable_context;
136 : const detail::process_context& m_process_context;
137 : const detail::action_context& m_action_context;
138 : const process_identifier* m_current_equation;
139 :
140 2293 : typecheck_builder(data::data_type_checker& data_typechecker,
141 : const data::detail::variable_context& variable_context,
142 : const detail::process_context& process_context,
143 : const detail::action_context& action_context,
144 : const process_identifier* current_equation = nullptr
145 : )
146 2293 : : m_data_type_checker(data_typechecker),
147 2293 : m_variable_context(variable_context),
148 2293 : m_process_context(process_context),
149 2293 : m_action_context(action_context),
150 2293 : m_current_equation(current_equation)
151 2293 : {}
152 :
153 585 : data::sorts_list action_sorts(const core::identifier_string& name)
154 : {
155 585 : return m_action_context.matching_action_sorts(name);
156 : }
157 :
158 24 : void check_action_declared(const core::identifier_string& a, const process_expression& x)
159 : {
160 24 : if (!m_action_context.is_declared(a))
161 : {
162 0 : throw mcrl2::runtime_error("Undefined action " + core::pp(a) + " (typechecking " + core::pp(x) + ")");
163 : }
164 24 : }
165 :
166 24 : void check_actions_declared(const core::identifier_string_list& act_list, const process_expression& x)
167 : {
168 24 : std::set<core::identifier_string> actions;
169 48 : for (const core::identifier_string& a: act_list)
170 : {
171 24 : check_action_declared(a, x);
172 24 : if (!actions.insert(a).second) // The action was already in the set.
173 : {
174 0 : mCRL2log(log::warning) << "Used action " << a << " twice (typechecking " << x << ")" << std::endl;
175 : }
176 : }
177 24 : }
178 :
179 : template <typename Container>
180 216 : void check_not_empty(const Container& c, const std::string& msg, const process_expression& x)
181 : {
182 216 : if (c.empty())
183 : {
184 0 : mCRL2log(log::warning) << msg << " (typechecking " << x << ")" << std::endl;
185 : }
186 216 : }
187 :
188 : template <typename T>
189 0 : void check_not_equal(const T& first, const T& second, const std::string& msg, const process_expression& x)
190 : {
191 0 : if (first == second)
192 : {
193 0 : mCRL2log(log::warning) << msg << " " << first << "(typechecking " << x << ")" << std::endl;
194 : }
195 0 : }
196 :
197 0 : static bool has_empty_intersection(const data::sorts_list& s1, const data::sorts_list& s2)
198 : {
199 0 : std::set<data::sort_expression_list> v1(s1.begin(), s1.end());
200 0 : std::set<data::sort_expression_list> v2(s2.begin(), s2.end());
201 0 : return utilities::detail::has_empty_intersection(v1, v2);
202 0 : }
203 :
204 0 : void check_rename_common_type(const core::identifier_string& a, const core::identifier_string& b, const process_expression& x)
205 : {
206 0 : if (has_empty_intersection(action_sorts(a), action_sorts(b)))
207 : {
208 0 : throw mcrl2::runtime_error("renaming action " + core::pp(a) + " into action " + core::pp(b) + ": these two have no common type (typechecking " + process::pp(x) + ")");
209 : }
210 0 : }
211 :
212 441 : static std::map<core::identifier_string, data::data_expression> make_assignment_map(const data::untyped_identifier_assignment_list& assignments)
213 : {
214 441 : std::map<core::identifier_string, data::data_expression> result;
215 1403 : for (const data::untyped_identifier_assignment& a: assignments)
216 : {
217 963 : auto i = result.find(a.lhs());
218 963 : if (i != result.end()) // An data::assignment of the shape x := t already exists, this is not OK.
219 : {
220 1 : throw mcrl2::runtime_error("Double data::assignment to data::variable " + core::pp(a.lhs()) + " (detected assigned values are " + data::pp(i->second) + " and " + core::pp(a.rhs()) + ")");
221 : }
222 962 : result[a.lhs()]=a.rhs();
223 : }
224 440 : return result;
225 1 : }
226 :
227 5009 : bool is_action_name(const core::identifier_string& name)
228 : {
229 5009 : return m_action_context.is_declared(name);
230 : }
231 :
232 2573 : bool is_process_name(const core::identifier_string& name)
233 : {
234 2573 : return m_process_context.is_declared(name);
235 : }
236 :
237 2883 : action typecheck_action(const core::identifier_string& name, const data::data_expression_list& parameters)
238 : {
239 2883 : return process::typecheck_action(name, parameters, m_data_type_checker, m_variable_context, m_action_context);
240 : }
241 :
242 2132 : process_instance typecheck_process_instance(const core::identifier_string& name, const data::data_expression_list& parameters)
243 : {
244 2132 : std::string msg = "process";
245 2132 : data::sorts_list parameter_list = m_process_context.matching_process_sorts(name, parameters);
246 2132 : auto p = process::detail::match_action_parameters(parameters, parameter_list, m_variable_context, name, msg, m_data_type_checker);
247 4264 : return m_process_context.make_process_instance(name, p.second, p.first);
248 2132 : }
249 :
250 0 : std::string print_untyped_process_assignment(const untyped_process_assignment& x) const
251 : {
252 0 : if (x.assignments().empty())
253 : {
254 0 : return core::pp(x.name()) + "()";
255 : }
256 : else
257 : {
258 0 : return core::pp(x.name()) + core::detail::print_arguments(x.assignments());
259 : }
260 : }
261 :
262 : // Checks if in the equation P(..) = Q(assignments) all formal parameters of Q have been assigned a value,
263 : // either directly via an assignment in assignments, or indirectly via a formal parameter of P.
264 423 : void check_assignments(const process_identifier& P, const process_identifier& Q, const std::vector<data::assignment>& assignments, const untyped_process_assignment& x) const
265 : {
266 423 : std::set<data::variable> Q_variables;
267 1359 : for (const data::assignment& a: assignments)
268 : {
269 936 : Q_variables.insert(a.lhs());
270 : }
271 2811 : for (const data::variable& v: P.variables())
272 : {
273 2388 : Q_variables.insert(v);
274 : }
275 2811 : for (const data::variable& v: Q.variables())
276 : {
277 2388 : if (Q_variables.find(v) == Q_variables.end())
278 : {
279 0 : throw mcrl2::runtime_error("Process parameter " + core::pp(v.name()) + " has not been assigned a value in the process call with short-hand assignments " + print_untyped_process_assignment(x) + ".");
280 : }
281 : }
282 423 : }
283 :
284 : template <class T>
285 441 : void apply(T& result, const untyped_process_assignment& x)
286 : {
287 441 : mCRL2log(log::debug) << "typechecking a process call with short-hand assignments " << x << "" << std::endl;
288 441 : if (!is_process_name(x.name()))
289 : {
290 0 : throw mcrl2::runtime_error("Could not find a matching declaration for action or process expression " + print_untyped_process_assignment(x) + ".");
291 : }
292 :
293 441 : process_identifier P = m_process_context.match_untyped_process_instance_assignment(x);
294 441 : const data::variable_list& formal_parameters = P.variables();
295 :
296 : // This checks for duplicate left hand sides.
297 441 : std::map<core::identifier_string, data::data_expression> assignment_map = make_assignment_map(x.assignments());
298 :
299 440 : std::map<core::identifier_string, data::variable> formal_parameter_map;
300 3294 : for (const data::variable& v: formal_parameters)
301 : {
302 2414 : formal_parameter_map[v.name()] = v;
303 : }
304 :
305 : // Typecheck the right hand sides of the assignments
306 440 : std::vector<data::assignment> assignments;
307 1841 : for (const data::untyped_identifier_assignment& a: x.assignments())
308 : {
309 : try
310 : {
311 961 : data::variable v = formal_parameter_map[a.lhs()];
312 961 : formal_parameter_map.erase(v.name());
313 961 : data::data_expression e = m_data_type_checker.typecheck_data_expression(a.rhs(), v.sort(), m_variable_context);
314 961 : assignments.emplace_back(v, e);
315 961 : }
316 0 : catch (const mcrl2::runtime_error& e)
317 : {
318 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nType error occurred while typechecking the process call with short-hand assignments " + process::pp(x));
319 : }
320 : }
321 :
322 : // Check if all formal parameters have been assigned a value
323 440 : if (m_current_equation)
324 : {
325 423 : check_assignments(*m_current_equation, P, assignments, x);
326 : }
327 :
328 : // Check that for any non explicitly stated assignment x:=x, the rhs is well defined.
329 1892 : for (const auto& [name, var]: formal_parameter_map)
330 : {
331 : try
332 : {
333 1453 : m_data_type_checker.typecheck_data_expression(var, var.sort(), m_variable_context);
334 : }
335 2 : catch (const mcrl2::runtime_error& e)
336 : {
337 1 : throw mcrl2::runtime_error(std::string(e.what()) + "\nIn implicitly stated assignment " + pp(var) + "=" + pp(var) + " in process " + pp(P) + "(" + data::pp(assignments) + ")\n");
338 : }
339 : }
340 :
341 439 : make_process_instance_assignment(result, P, data::assignment_list(assignments.begin(), assignments.end()));
342 444 : }
343 :
344 : template <class T>
345 5009 : void apply(T& result, const data::untyped_data_parameter& x)
346 : {
347 5009 : if (is_action_name(x.name()))
348 : {
349 2877 : result = typecheck_action(x.name(), x.arguments());
350 : }
351 2132 : else if (is_process_name(x.name()))
352 : {
353 2132 : result = typecheck_process_instance(x.name(), x.arguments());
354 : }
355 : else
356 : {
357 0 : throw mcrl2::runtime_error("Could not find a matching declaration for action or process expression " + core::pp(x.name()) + core::detail::print_arguments(x.arguments()) + ".");
358 : }
359 5008 : }
360 :
361 : // This case is necessary for actionrename
362 : template <class T>
363 6 : void apply(T& result, const process::action& x)
364 : {
365 6 : result = typecheck_action(x.label().name(), x.arguments());
366 6 : }
367 :
368 : template <class T>
369 24 : void apply(T& result, const process::hide& x)
370 : {
371 24 : check_not_empty(x.hide_set(), "Hiding empty set of actions", x);
372 24 : check_actions_declared(x.hide_set(), x);
373 72 : process::make_hide(result,
374 24 : x.hide_set(),
375 24 : [&](process_expression& result){ (*this).apply(result, x.operand()); } );
376 24 : }
377 :
378 : template <class T>
379 0 : void apply(T& result, const process::block& x)
380 : {
381 0 : check_not_empty(x.block_set(), "Blocking empty set of actions", x);
382 0 : check_actions_declared(x.block_set(), x);
383 0 : make_block(result, x.block_set(), [&]( process_expression& result){ (*this).apply(result, x.operand()); });
384 0 : }
385 :
386 : template <class T>
387 0 : void apply(T& result, const process::rename& x)
388 : {
389 0 : check_not_empty(x.rename_set(), "Renaming empty set of actions", x);
390 :
391 0 : std::set<core::identifier_string> actions;
392 0 : for (const rename_expression& r: x.rename_set())
393 : {
394 0 : check_not_equal(r.source(), r.target(), "Renaming action into itself:", x);
395 0 : check_action_declared(r.source(), x);
396 0 : check_action_declared(r.target(), x);
397 0 : check_rename_common_type(r.source(), r.target(), x);
398 0 : if (!actions.insert(r.source()).second) // The element was already in the set.
399 : {
400 0 : throw mcrl2::runtime_error("renaming action " + core::pp(r.source()) + " twice (typechecking " + process::pp(x) + ")");
401 : }
402 : }
403 0 : make_rename(result, x.rename_set(), [&](process_expression& r){ (*this).apply(r, x.operand()); } );
404 0 : }
405 :
406 : //comm: like renaming multiactions (with the same parameters) to action/tau
407 : template <class T>
408 122 : void apply(T& result, const process::comm& x)
409 : {
410 122 : check_not_empty(x.comm_set(), "synchronizing empty set of (multi)actions", x);
411 :
412 122 : std::multiset<core::identifier_string> left_hand_side_actions;
413 439 : for (const communication_expression& c: x.comm_set())
414 : {
415 195 : const core::identifier_string_list& cnames = c.action_name().names();
416 195 : assert(!cnames.empty());
417 :
418 195 : if (cnames.size() == 1)
419 : {
420 0 : throw mcrl2::runtime_error("using synchronization as renaming/hiding of action " + core::pp(cnames.front()) + " into " + core::pp(c.name()) + " (typechecking " + process::pp(x) + ")");
421 : }
422 :
423 : //Actions must be declared
424 195 : data::sorts_list c_sorts;
425 195 : if (!m_action_context.is_declared(c.name()))
426 : {
427 0 : throw mcrl2::runtime_error("synchronizing to an undefined action " + core::pp(c.name()) + " (typechecking " + process::pp(x) + ")");
428 : }
429 195 : c_sorts = action_sorts(c.name());
430 :
431 780 : for (const core::identifier_string& a: cnames)
432 : {
433 390 : if (!m_action_context.is_declared(a))
434 : {
435 0 : throw mcrl2::runtime_error("synchronizing an undefined action " + core::pp(a) + " in (multi)action " + core::pp(cnames) + " (typechecking " + process::pp(x) + ")");
436 : }
437 390 : c_sorts = sorts_list_intersection(c_sorts, action_sorts(a));
438 390 : if (c_sorts.empty())
439 : {
440 0 : throw mcrl2::runtime_error("synchronizing action " + core::pp(a) + " from (multi)action " + core::pp(cnames) +
441 : " into action " + core::pp(c.name()) + ": these have no common type (typechecking " + process::pp(x) + ")");
442 : }
443 : }
444 :
445 : //the multiactions in the lhss of comm should not intersect.
446 : //but there can be multiple of the same actions in cnames.
447 195 : std::set < core::identifier_string > this_left_hand_sides;
448 780 : for (const core::identifier_string& a: cnames)
449 : {
450 390 : if (this_left_hand_sides.count(a)==0 && left_hand_side_actions.find(a) != left_hand_side_actions.end())
451 : {
452 0 : throw mcrl2::runtime_error("synchronizing action " + core::pp(a) + " in different ways (typechecking " + process::pp(x) + ")");
453 : }
454 : else
455 : {
456 390 : left_hand_side_actions.insert(a);
457 390 : this_left_hand_sides.insert(a);
458 : }
459 : }
460 : }
461 :
462 : //the multiactions in the rhs of comm should not intersect with an action in the a lhs of
463 : //all other rules. So, {a|a->a} is allowed, but {a|b->c, c|a->d} is not.
464 439 : for (const communication_expression& c: x.comm_set())
465 : {
466 : // Count how many actions in the rhs occur at the left
467 195 : std::size_t number_of_rhs_in_lhs=0;
468 780 : for (const core::identifier_string& lhs_action: c.action_name().names())
469 : {
470 390 : if (lhs_action==c.name())
471 : {
472 12 : number_of_rhs_in_lhs++;
473 : }
474 : }
475 195 : assert(left_hand_side_actions.count(c.name())>=number_of_rhs_in_lhs);
476 195 : if (left_hand_side_actions.count(c.name())-number_of_rhs_in_lhs>0) // There are more actions x.name() in the lhss than just in this lhs.
477 : {
478 0 : throw mcrl2::runtime_error("action " + core::pp(c.name()) +
479 : " occurs at the left and the right in a communication (typechecking " + process::pp(x) + ")");
480 : }
481 : }
482 244 : make_comm(result, x.comm_set(), [&](process_expression& r){ (*this).apply(r, x.operand()); } );
483 122 : }
484 :
485 : template <class T>
486 70 : void apply(T& result, const process::allow& x)
487 : {
488 70 : check_not_empty(x.allow_set(), "Allowing empty set of (multi) actions", x);
489 70 : action_name_multiset_list MActs;
490 322 : for (const action_name_multiset& A: x.allow_set())
491 : {
492 : //Actions must be declared
493 577 : for (const core::identifier_string& a: A.names())
494 : {
495 213 : if (!m_action_context.is_declared(a))
496 : {
497 0 : throw mcrl2::runtime_error("allowing an undefined action " + core::pp(a) + " in (multi)action " + core::pp(A.names()) + " (typechecking " + process::pp(x) + ")");
498 : }
499 : }
500 182 : if (multi_actions_contains(A.names(), MActs))
501 : {
502 0 : mCRL2log(log::warning) << "allowing (multi)action " << A.names() << " twice (typechecking " << x << ")" << std::endl;
503 : }
504 : else
505 : {
506 182 : MActs.push_front(mcrl2::process::action_name_multiset(A.names()));
507 : }
508 : }
509 140 : make_allow(result, x.allow_set(), [&](process_expression& r){ (*this).apply(r, x.operand()); } );
510 70 : }
511 :
512 : template <class T>
513 342 : void apply(T& result, const process::at& x)
514 : {
515 342 : data::data_expression new_time = m_data_type_checker.typecheck_data_expression(x.time_stamp(), data::sort_real::real_(), m_variable_context);
516 684 : make_at(result, [&](process_expression& r){ (*this).apply(r, x.operand()); }, new_time);
517 342 : }
518 :
519 : template <class T>
520 672 : void apply(T& result, const process::if_then& x)
521 : {
522 672 : data::data_expression condition = m_data_type_checker.typecheck_data_expression(x.condition(), data::sort_bool::bool_(), m_variable_context);
523 1342 : make_if_then(result, condition, [&](process_expression& r){ (*this).apply(r, x.then_case()); } );
524 671 : }
525 :
526 : template <class T>
527 125 : void apply(T& result, const process::if_then_else& x)
528 : {
529 125 : data::data_expression condition = m_data_type_checker.typecheck_data_expression(x.condition(), data::sort_bool::bool_(), m_variable_context);
530 125 : make_if_then_else(result,
531 : condition,
532 125 : [&](process_expression& r){ (*this).apply(r, x.then_case()); },
533 125 : [&](process_expression& r){ (*this).apply(r, x.else_case()); } );
534 125 : }
535 :
536 : template <class T>
537 618 : void apply(T& result, const process::sum& x)
538 : {
539 : try
540 : {
541 618 : auto m_variable_context_copy = m_variable_context;
542 618 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
543 618 : process_expression operand;
544 618 : (*this).apply(operand, x.operand());
545 618 : m_variable_context = m_variable_context_copy;
546 618 : make_sum(result, x.variables(), operand);
547 618 : }
548 0 : catch (mcrl2::runtime_error& e)
549 : {
550 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + process::pp(x));
551 : }
552 618 : }
553 :
554 : template <class T>
555 136 : void apply(T& result, const process::stochastic_operator& x)
556 : {
557 : try
558 : {
559 136 : auto m_variable_context_copy = m_variable_context;
560 136 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
561 136 : data::data_expression distribution = m_data_type_checker.typecheck_data_expression(x.distribution(), data::sort_real::real_(), m_variable_context);
562 136 : process_expression operand;
563 136 : (*this).apply(operand, x.operand());
564 136 : m_variable_context = m_variable_context_copy;
565 136 : make_stochastic_operator(result, x.variables(), distribution, operand);
566 136 : }
567 0 : catch (mcrl2::runtime_error& e)
568 : {
569 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + process::pp(x));
570 : }
571 136 : }
572 : };
573 :
574 : inline
575 2293 : typecheck_builder make_typecheck_builder(
576 : data::data_type_checker& data_typechecker,
577 : const data::detail::variable_context& variables,
578 : const detail::process_context& process_identifiers,
579 : const detail::action_context& action_context,
580 : const process_identifier* current_equation = nullptr
581 : )
582 : {
583 2293 : return typecheck_builder(data_typechecker, variables, process_identifiers, action_context, current_equation);
584 : }
585 :
586 : } // namespace detail
587 :
588 : class process_type_checker
589 : {
590 : protected:
591 : data::data_type_checker m_data_type_checker;
592 : detail::action_context m_action_context;
593 : detail::process_context m_process_context;
594 : data::detail::variable_context m_variable_context;
595 :
596 1136 : static std::vector<process_identifier> equation_identifiers(const std::vector<process_equation>& equations)
597 : {
598 1136 : std::vector<process_identifier> result;
599 2281 : for (const process_equation& eqn: equations)
600 : {
601 1145 : result.push_back(eqn.identifier());
602 : }
603 1136 : return result;
604 0 : }
605 :
606 : public:
607 : template <typename VariableContainer, typename ActionLabelContainer, typename ProcessIdentifierContainer>
608 13 : process_type_checker(const data::data_specification& dataspec,
609 : const VariableContainer& variables,
610 : const ActionLabelContainer& action_labels,
611 : const ProcessIdentifierContainer& process_identifiers
612 : )
613 13 : : m_data_type_checker(dataspec)
614 : {
615 13 : m_action_context.add_context_action_labels(action_labels, m_data_type_checker);
616 13 : m_variable_context.add_context_variables(variables, m_data_type_checker);
617 13 : m_process_context.add_process_identifiers(process_identifiers, m_action_context, m_data_type_checker);
618 13 : }
619 :
620 : /// \brief Default constructor
621 1152 : explicit process_type_checker(const data::data_specification& dataspec = data::data_specification())
622 1152 : : m_data_type_checker(dataspec)
623 1152 : {}
624 :
625 : /** \brief Type check a process expression.
626 : * Throws a mcrl2::runtime_error exception if the expression is not well typed.
627 : * \param[in] x A process expression that has not been type checked.
628 : * \return a process expression where all untyped identifiers have been replace by typed ones.
629 : **/ /// \brief Typecheck the pbes pbesspec
630 13 : process_expression operator()(const process_expression& x, const process_identifier* current_equation = nullptr)
631 : {
632 26 : return typecheck_process_expression(m_variable_context, process::normalize_sorts(x, m_data_type_checker.typechecked_data_specification()), current_equation);
633 : }
634 :
635 : /// \brief Typecheck the process specification procspec
636 1152 : void operator()(process_specification& procspec)
637 : {
638 1152 : mCRL2log(log::verbose) << "type checking process specification..." << std::endl;
639 :
640 : // reset the context
641 1152 : m_data_type_checker = data::data_type_checker(procspec.data());
642 :
643 1136 : process::normalize_sorts(procspec, m_data_type_checker.typechecked_data_specification());
644 :
645 1136 : m_action_context.clear();
646 1136 : m_variable_context.clear();
647 1136 : m_process_context.clear();
648 1136 : m_action_context.add_context_action_labels(procspec.action_labels(), m_data_type_checker);
649 1136 : m_variable_context.add_context_variables(procspec.global_variables(), m_data_type_checker);
650 1136 : m_process_context.add_process_identifiers(equation_identifiers(procspec.equations()), m_action_context, m_data_type_checker);
651 :
652 : // typecheck the equations
653 2280 : for (process_equation& eqn: procspec.equations())
654 : {
655 1145 : data::detail::variable_context variable_context = m_variable_context;
656 1145 : variable_context.add_context_variables(eqn.identifier().variables(), m_data_type_checker);
657 1145 : eqn = process_equation(eqn.identifier(), eqn.formal_parameters(), typecheck_process_expression(variable_context, eqn.expression(), &eqn.identifier()));
658 1145 : }
659 :
660 : // typecheck the initial state
661 1135 : procspec.init() = typecheck_process_expression(m_variable_context, procspec.init());
662 :
663 : // typecheck the data specification
664 1132 : procspec.data() = m_data_type_checker.typechecked_data_specification();
665 1132 : procspec.data().translate_user_notation();
666 :
667 :
668 1132 : mCRL2log(log::debug) << "type checking process specification finished" << std::endl;
669 1132 : }
670 :
671 : protected:
672 2293 : process_expression typecheck_process_expression(const data::detail::variable_context& variables, const process_expression& x, const process_identifier* current_equation = nullptr)
673 : {
674 2293 : process_expression result;
675 2297 : detail::make_typecheck_builder(m_data_type_checker, variables, m_process_context, m_action_context, current_equation).apply(result, x);
676 2289 : return result;
677 4 : }
678 : };
679 :
680 : /** \brief Type check a parsed mCRL2 process specification.
681 : * Throws an exception if something went wrong.
682 : * \param[in] proc_spec A process specification that has not been type checked.
683 : * \post proc_spec is type checked.
684 : **/
685 :
686 : inline
687 1152 : void typecheck_process_specification(process_specification& proc_spec)
688 : {
689 1152 : process_type_checker type_checker;
690 1152 : type_checker(proc_spec);
691 1152 : }
692 :
693 : /// \brief Typecheck a process expression
694 : /// \param x An untyped process expression
695 : /// \param variables A sequence of data variables
696 : /// \param dataspec A data specification
697 : /// \param action_labels A sequence of action labels
698 : /// \param process_identifiers A sequence of process identifiers
699 : /// \param current_equation A pointer to the current equation. If this pointer is set, a check will be done it
700 : /// process instance assignments assign values to all their parameters.
701 : template <typename VariableContainer, typename ActionLabelContainer, typename ProcessIdentifierContainer>
702 13 : process_expression typecheck_process_expression(const process_expression& x,
703 : const VariableContainer& variables = VariableContainer(),
704 : const data::data_specification& dataspec = data::data_specification(),
705 : const ActionLabelContainer& action_labels = ActionLabelContainer(),
706 : const ProcessIdentifierContainer& process_identifiers = ProcessIdentifierContainer(),
707 : const process_identifier* current_equation = nullptr
708 : )
709 : {
710 13 : process_type_checker type_checker(dataspec, variables, action_labels, process_identifiers);
711 26 : return type_checker(x, current_equation);
712 13 : }
713 :
714 : } // namespace process
715 :
716 : } // namespace mcrl2
717 :
718 : #endif // MCRL2_PROCESS_TYPECHECK_H
|
