mCRL2
Loading...
Searching...
No Matches
type_checker.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_DATA_TYPE_CHECKER_H
13#define MCRL2_DATA_TYPE_CHECKER_H
14
15#include "mcrl2/data/parse_impl.h"
16
17namespace mcrl2 {
18
19namespace data {
20
21namespace detail {
22
23inline
24bool is_pos(const core::identifier_string& Number)
25{
26 char c = Number.function().name()[0];
27 return isdigit(c) && c > '0';
28}
29
30inline
31bool is_nat(const core::identifier_string& Number)
32{
33 return isdigit(Number.function().name()[0]) != 0;
34}
35
36inline
37function_sort make_function_sort_(const sort_expression& domain, const sort_expression& codomain)
38{
39 return function_sort({ domain }, codomain);
40}
41
42template <typename Function, typename T>
43atermpp::term_list<T> transform_aterm_list(const Function& f, const atermpp::term_list<T>& x)
44{
45 atermpp::term_list<T> result;
46 for (const T& t: x)
47 {
48 result.push_front(f(t));
49 }
50 return atermpp::reverse(result);
51}
52
53inline
54sort_expression unwind_sort_expression(const sort_expression& x, const alias_vector& aliases)
55{
56 if (is_container_sort(x))
57 {
58 const container_sort& cs = atermpp::down_cast<const container_sort>(x);
59 return container_sort(cs.container_name(), unwind_sort_expression(cs.element_sort(), aliases));
60 }
61 else if (is_function_sort(x))
62 {
63 const function_sort& fs = atermpp::down_cast<function_sort>(x);
64 auto new_arguments = detail::transform_aterm_list([&](const sort_expression& s) { return unwind_sort_expression(s, aliases); }, fs.domain());
65 return function_sort(new_arguments, unwind_sort_expression(fs.codomain(), aliases));
66 }
67 else if (is_basic_sort(x))
68 {
69 const basic_sort& bs = atermpp::down_cast<const basic_sort>(x);
70 for(const alias& a: aliases)
71 {
72 if (bs == a.name())
73 {
74 return unwind_sort_expression(a.reference(), aliases);
75 }
76 return x;
77 }
78 }
79 return x;
80}
81
82inline
83bool is_numeric_type(const sort_expression& x)
84{
85 if (data::is_untyped_sort(x))
86 {
87 return false;
88 }
89 return sort_bool::is_bool(x) ||
90 sort_pos::is_pos(x) ||
91 sort_nat::is_nat(x) ||
92 sort_int::is_int(x) ||
93 sort_real::is_real(x);
94}
95
96} // namespace detail
97
98class type_checker: public sort_type_checker
99{
100 protected:
101 std::map<core::identifier_string, sort_expression_list> m_system_constants;
102 std::map<core::identifier_string, function_sort_list> m_system_functions;
103 std::map<core::identifier_string, sort_expression> m_user_constants;
104 std::map<core::identifier_string, function_sort_list> m_user_functions;
105
106 void add_system_constant(const data::function_symbol& f)
107 {
108 // append the Type to the entry of the Name of the OpId in system constants table
109 auto i = m_system_constants.find(f.name());
110 sort_expression_list sorts;
111 if (i != m_system_constants.end())
112 {
113 sorts = i->second;
114 }
115 sorts = push_back(sorts, f.sort());
116 m_system_constants[f.name()] = sorts;
117 }
118
119 void add_system_function(const data::function_symbol& f)
120 {
121 m_system_functions[f.name()] = m_system_functions[f.name()] + function_sort_list({ atermpp::down_cast<function_sort>(f.sort()) });
122 }
123
124 sort_expression unwind_sort_expression(const sort_expression& x) const
125 {
126 return detail::unwind_sort_expression(x, get_sort_specification().user_defined_aliases());
127 }
128
129 bool equal_types(const sort_expression& x1, const sort_expression& x2) const
130 {
131 if (x1 == x2)
132 {
133 return true;
134 }
135 return unwind_sort_expression(x1) == unwind_sort_expression(x2);
136 }
137
138 bool find_sort(const sort_expression& x, const function_sort_list& sorts) const
139 {
140 return std::any_of(sorts.begin(), sorts.end(), [&](const function_sort& s) { return equal_types(x, s); });
141 }
142
143 void initialise_system_defined_functions()
144 {
145 //Creation of operation identifiers for system defined operations.
146 //Bool
147 add_system_constant(sort_bool::true_());
148 add_system_constant(sort_bool::false_());
149 add_system_function(sort_bool::not_());
150 add_system_function(sort_bool::and_());
151 add_system_function(sort_bool::or_());
152 add_system_function(sort_bool::implies());
153 add_system_function(equal_to(data::untyped_sort()));
154 add_system_function(not_equal_to(data::untyped_sort()));
155 add_system_function(if_(data::untyped_sort()));
156 add_system_function(less(data::untyped_sort()));
157 add_system_function(less_equal(data::untyped_sort()));
158 add_system_function(greater_equal(data::untyped_sort()));
159 add_system_function(greater(data::untyped_sort()));
160 //Numbers
161 add_system_function(sort_nat::pos2nat());
162#ifndef MCRL2_ENABLE_MACHINENUMBERS
163 add_system_function(sort_nat::cnat());
164#endif
165 add_system_function(sort_real::pos2real());
166 add_system_function(sort_nat::nat2pos());
167 add_system_function(sort_int::nat2int());
168 add_system_function(sort_int::cint());
169 add_system_function(sort_real::nat2real());
170 add_system_function(sort_int::int2pos());
171 add_system_function(sort_int::int2nat());
172 add_system_function(sort_real::int2real());
173 add_system_function(sort_real::creal());
174 add_system_function(sort_real::real2pos());
175 add_system_function(sort_real::real2nat());
176 add_system_function(sort_real::real2int());
177 add_system_constant(sort_pos::c1());
178 //Square root for the natural numbers.
179 add_system_function(sort_nat::sqrt());
180 //more about numbers
181 add_system_function(sort_real::maximum(sort_pos::pos(),sort_pos::pos()));
182 add_system_function(sort_real::maximum(sort_pos::pos(),sort_nat::nat()));
183 add_system_function(sort_real::maximum(sort_nat::nat(),sort_pos::pos()));
184 add_system_function(sort_real::maximum(sort_nat::nat(),sort_nat::nat()));
185 add_system_function(sort_real::maximum(sort_pos::pos(),sort_int::int_()));
186 add_system_function(sort_real::maximum(sort_int::int_(),sort_pos::pos()));
187 add_system_function(sort_real::maximum(sort_nat::nat(),sort_int::int_()));
188 add_system_function(sort_real::maximum(sort_int::int_(),sort_nat::nat()));
189 add_system_function(sort_real::maximum(sort_int::int_(),sort_int::int_()));
190 add_system_function(sort_real::maximum(sort_real::real_(),sort_real::real_()));
191 //more
192 add_system_function(sort_real::minimum(sort_pos::pos(), sort_pos::pos()));
193 add_system_function(sort_real::minimum(sort_nat::nat(), sort_nat::nat()));
194 add_system_function(sort_real::minimum(sort_int::int_(), sort_int::int_()));
195 add_system_function(sort_real::minimum(sort_real::real_(), sort_real::real_()));
196 //more
197 // add_system_function(sort_real::abs(sort_pos::pos()));
198 // add_system_function(sort_real::abs(sort_nat::nat()));
199 add_system_function(sort_real::abs(sort_int::int_()));
200 add_system_function(sort_real::abs(sort_real::real_()));
201 //more
202 add_system_function(sort_real::negate(sort_pos::pos()));
203 add_system_function(sort_real::negate(sort_nat::nat()));
204 add_system_function(sort_real::negate(sort_int::int_()));
205 add_system_function(sort_real::negate(sort_real::real_()));
206 add_system_function(sort_real::succ(sort_pos::pos()));
207 add_system_function(sort_real::succ(sort_nat::nat()));
208 add_system_function(sort_real::succ(sort_int::int_()));
209 add_system_function(sort_real::succ(sort_real::real_()));
210 add_system_function(sort_real::pred(sort_pos::pos()));
211 add_system_function(sort_real::pred(sort_nat::nat()));
212 add_system_function(sort_real::pred(sort_int::int_()));
213 add_system_function(sort_real::pred(sort_real::real_()));
214 add_system_function(sort_real::plus(sort_pos::pos(),sort_pos::pos()));
215 add_system_function(sort_real::plus(sort_pos::pos(),sort_nat::nat()));
216 add_system_function(sort_real::plus(sort_nat::nat(),sort_pos::pos()));
217 add_system_function(sort_real::plus(sort_nat::nat(),sort_nat::nat()));
218 add_system_function(sort_real::plus(sort_int::int_(),sort_int::int_()));
219 add_system_function(sort_real::plus(sort_real::real_(),sort_real::real_()));
220 //more
221 add_system_function(sort_real::minus(sort_pos::pos(), sort_pos::pos()));
222 add_system_function(sort_real::minus(sort_nat::nat(), sort_nat::nat()));
223 add_system_function(sort_real::minus(sort_int::int_(), sort_int::int_()));
224 add_system_function(sort_real::minus(sort_real::real_(), sort_real::real_()));
225 add_system_function(sort_real::times(sort_pos::pos(), sort_pos::pos()));
226 add_system_function(sort_real::times(sort_nat::nat(), sort_nat::nat()));
227 add_system_function(sort_real::times(sort_int::int_(), sort_int::int_()));
228 add_system_function(sort_real::times(sort_real::real_(), sort_real::real_()));
229 //more
230 // add_system_function(sort_int::div(sort_pos::pos(), sort_pos::pos()));
231 add_system_function(sort_int::div(sort_nat::nat(), sort_pos::pos()));
232 add_system_function(sort_int::div(sort_int::int_(), sort_pos::pos()));
233 // add_system_function(sort_int::mod(sort_pos::pos(), sort_pos::pos()));
234 add_system_function(sort_int::mod(sort_nat::nat(), sort_pos::pos()));
235 add_system_function(sort_int::mod(sort_int::int_(), sort_pos::pos()));
236 add_system_function(sort_real::divides(sort_pos::pos(), sort_pos::pos()));
237 add_system_function(sort_real::divides(sort_nat::nat(), sort_nat::nat()));
238 add_system_function(sort_real::divides(sort_int::int_(), sort_int::int_()));
239 add_system_function(sort_real::divides(sort_real::real_(), sort_real::real_()));
240 add_system_function(sort_real::exp(sort_pos::pos(), sort_nat::nat()));
241 add_system_function(sort_real::exp(sort_nat::nat(), sort_nat::nat()));
242 add_system_function(sort_real::exp(sort_int::int_(), sort_nat::nat()));
243 add_system_function(sort_real::exp(sort_real::real_(), sort_int::int_()));
244 add_system_function(sort_real::floor());
245 add_system_function(sort_real::ceil());
246 add_system_function(sort_real::round());
247 //Lists
248 add_system_constant(sort_list::empty(data::untyped_sort()));
249 add_system_function(sort_list::cons_(data::untyped_sort()));
250 add_system_function(sort_list::count(data::untyped_sort()));
251 add_system_function(sort_list::snoc(data::untyped_sort()));
252 add_system_function(sort_list::concat(data::untyped_sort()));
253 add_system_function(sort_list::element_at(data::untyped_sort()));
254 add_system_function(sort_list::head(data::untyped_sort()));
255 add_system_function(sort_list::tail(data::untyped_sort()));
256 add_system_function(sort_list::rhead(data::untyped_sort()));
257 add_system_function(sort_list::rtail(data::untyped_sort()));
258 add_system_function(sort_list::in(data::untyped_sort()));
259
260 //Sets
261
262 add_system_function(sort_bag::set2bag(data::untyped_sort()));
263 add_system_function(sort_set::in(data::untyped_sort(), data::untyped_sort(), sort_fset::fset(data::untyped_sort())));
264 add_system_function(sort_set::in(data::untyped_sort(), data::untyped_sort(), sort_set::set_(data::untyped_sort())));
265 add_system_function(sort_set::union_(data::untyped_sort(), sort_fset::fset(data::untyped_sort()), sort_fset::fset(data::untyped_sort())));
266 add_system_function(sort_set::union_(data::untyped_sort(), sort_set::set_(data::untyped_sort()), sort_set::set_(data::untyped_sort())));
267 add_system_function(sort_set::difference(data::untyped_sort(), sort_fset::fset(data::untyped_sort()), sort_fset::fset(data::untyped_sort())));
268 add_system_function(sort_set::difference(data::untyped_sort(), sort_set::set_(data::untyped_sort()), sort_set::set_(data::untyped_sort())));
269 add_system_function(sort_set::intersection(data::untyped_sort(), sort_fset::fset(data::untyped_sort()), sort_fset::fset(data::untyped_sort())));
270 add_system_function(sort_set::intersection(data::untyped_sort(), sort_set::set_(data::untyped_sort()), sort_set::set_(data::untyped_sort())));
271 add_system_function(sort_set::false_function(data::untyped_sort())); // Needed as it is used within the typechecker.
272 add_system_function(sort_set::constructor(data::untyped_sort())); // Needed as it is used within the typechecker.
273 //**** add_system_function(sort_bag::set2bag(data::untyped_sort()));
274 // add_system_constant(sort_set::empty(data::untyped_sort()));
275 // add_system_function(sort_set::in(data::untyped_sort()));
276 // add_system_function(sort_set::union_(data::untyped_sort()));
277 // add_system_function(sort_set::difference(data::untyped_sort()));
278 // add_system_function(sort_set::intersection(data::untyped_sort()));
279 add_system_function(sort_set::complement(data::untyped_sort()));
280
281 //FSets
282 add_system_constant(sort_fset::empty(data::untyped_sort()));
283 // add_system_function(sort_fset::in(data::untyped_sort()));
284 // add_system_function(sort_fset::union_(data::untyped_sort()));
285 // add_system_function(sort_fset::intersection(data::untyped_sort()));
286 // add_system_function(sort_fset::difference(data::untyped_sort()));
287 add_system_function(sort_fset::count(data::untyped_sort()));
288 add_system_function(sort_fset::insert(data::untyped_sort())); // Needed as it is used within the typechecker.
289
290 //Bags
291 add_system_function(sort_bag::bag2set(data::untyped_sort()));
292 add_system_function(sort_bag::in(data::untyped_sort(), data::untyped_sort(), sort_fbag::fbag(data::untyped_sort())));
293 add_system_function(sort_bag::in(data::untyped_sort(), data::untyped_sort(), sort_bag::bag(data::untyped_sort())));
294 add_system_function(sort_bag::union_(data::untyped_sort(), sort_fbag::fbag(data::untyped_sort()), sort_fbag::fbag(data::untyped_sort())));
295 add_system_function(sort_bag::union_(data::untyped_sort(), sort_bag::bag(data::untyped_sort()), sort_bag::bag(data::untyped_sort())));
296 add_system_function(sort_bag::difference(data::untyped_sort(), sort_fbag::fbag(data::untyped_sort()), sort_fbag::fbag(data::untyped_sort())));
297 add_system_function(sort_bag::difference(data::untyped_sort(), sort_bag::bag(data::untyped_sort()), sort_bag::bag(data::untyped_sort())));
298 add_system_function(sort_bag::intersection(data::untyped_sort(), sort_fbag::fbag(data::untyped_sort()), sort_fbag::fbag(data::untyped_sort())));
299 add_system_function(sort_bag::intersection(data::untyped_sort(), sort_bag::bag(data::untyped_sort()), sort_bag::bag(data::untyped_sort())));
300 add_system_function(sort_bag::count(data::untyped_sort(), data::untyped_sort(), sort_fbag::fbag(data::untyped_sort())));
301 add_system_function(sort_bag::count(data::untyped_sort(), data::untyped_sort(), sort_bag::bag(data::untyped_sort())));
302 // add_system_constant(sort_bag::empty(data::untyped_sort()));
303 // add_system_function(sort_bag::in(data::untyped_sort()));
304 //**** add_system_function(sort_bag::count(data::untyped_sort()));
305 // add_system_function(sort_bag::count(data::untyped_sort(), data::untyped_sort(), sort_fset::fset(data::untyped_sort())));
306 //add_system_function(sort_bag::join(data::untyped_sort()));
307 // add_system_function(sort_bag::difference(data::untyped_sort()));
308 // add_system_function(sort_bag::intersection(data::untyped_sort()));
309 add_system_function(sort_bag::zero_function(data::untyped_sort())); // Needed as it is used within the typechecker.
310 add_system_function(sort_bag::constructor(data::untyped_sort())); // Needed as it is used within the typechecker.
311
312 //FBags
313 add_system_constant(sort_fbag::empty(data::untyped_sort()));
314 // add_system_function(sort_fbag::count(data::untyped_sort()));
315 // add_system_function(sort_fbag::in(data::untyped_sort()));
316 // add_system_function(sort_fbag::union_(data::untyped_sort()));
317 // add_system_function(sort_fbag::intersection(data::untyped_sort()));
318 // add_system_function(sort_fbag::difference(data::untyped_sort()));
319 add_system_function(sort_fbag::count_all(data::untyped_sort()));
320 add_system_function(sort_fbag::cinsert(data::untyped_sort())); // Needed as it is used within the typechecker.
321
322 // function update
323 add_system_function(data::function_update(data::untyped_sort(),data::untyped_sort()));
324 }
325
326 void add_constant(const data::function_symbol& f, const std::string& msg)
327 {
328 if (m_user_constants.count(f.name()) > 0)
329 {
330 throw mcrl2::runtime_error("double declaration of " + msg + " " + core::pp(f.name()));
331 }
332 if (m_system_constants.count(f.name()) > 0 || m_system_functions.count(f.name()) > 0)
333 {
334 throw mcrl2::runtime_error("attempt to declare a constant with the name that is a built-in identifier (" + core::pp(f.name()) + ")");
335 }
336 m_user_constants[f.name()] = f.sort();
337 }
338
339 void add_function(const data::function_symbol& f, const std::string& msg, bool allow_double_decls = false)
340 {
341 if (m_system_constants.count(f.name()) > 0)
342 {
343 throw mcrl2::runtime_error("attempt to redeclare the system constant with a " + msg + " " + data::pp(f));
344 }
345
346 if (m_system_functions.count(f.name()) > 0)
347 {
348 throw mcrl2::runtime_error("attempt to redeclare a system function with a " + msg + " " + data::pp(f));
349 }
350
351 auto j = m_user_functions.find(f.name());
352 const function_sort& fsort = atermpp::down_cast<function_sort>(f.sort());
353
354 // the table m_user_functions contains a list of types for each
355 // function name. We need to check if there is already such a type
356 // in the list. If so -- error, otherwise -- add
357 if (j != m_user_functions.end())
358 {
359 auto& sorts = j->second;
360 if (find_sort(fsort, sorts))
361 {
362 if (!allow_double_decls)
363 {
364 throw mcrl2::runtime_error("double declaration of " + msg + " " + core::pp(f.name()));
365 }
366 }
367 }
368 m_user_functions[f.name()] = m_user_functions[f.name()] + function_sort_list({ fsort });
369 }
370
371 // Adds constants and functions corresponding to the sort x
372 void read_sort(const sort_expression& x)
373 {
374 if (is_basic_sort(x))
375 {
376 // This should be checked elsewhere
377 // check_basic_sort_is_declared(atermpp::down_cast<basic_sort>(x).name());
378 }
379 else if (is_container_sort(x))
380 {
381 read_sort(atermpp::down_cast<container_sort>(x).element_sort());
382 }
383 else if (is_function_sort(x))
384 {
385 const function_sort& fs = atermpp::down_cast<function_sort>(x);
386 read_sort(fs.codomain());
387 for (const sort_expression& sort: fs.domain())
388 {
389 read_sort(sort);
390 }
391 }
392 else if (is_structured_sort(x))
393 {
394 const structured_sort& struct_sort = atermpp::down_cast<structured_sort>(x);
395 for (const structured_sort_constructor& constructor: struct_sort.constructors())
396 {
397 // recognizer -- if present -- a function from SortExpr to Bool
398 core::identifier_string name = constructor.recogniser();
399 if (name != core::empty_identifier_string())
400 {
401 add_function(data::function_symbol(name, make_function_sort_(x, sort_bool::bool_())), "recognizer");
402 }
403
404 // constructor type and projections
405 structured_sort_constructor_argument_list arguments = constructor.arguments();
406 name = constructor.name();
407 if (arguments.empty())
408 {
409 add_constant(data::function_symbol(name, x), "constructor constant");
410 continue;
411 }
412
413 sort_expression_list sorts;
414 for (const structured_sort_constructor_argument& arg: arguments)
415 {
416 read_sort(arg.sort());
417 if (arg.name() != core::empty_identifier_string())
418 {
419 add_function(function_symbol(arg.name(), function_sort({ x }, arg.sort())), "projection", true);
420 }
421 sorts.push_front(arg.sort());
422 }
423 add_function(data::function_symbol(name, function_sort(atermpp::reverse(sorts), x)), "constructor");
424 }
425 }
426 // other sorts can be ignored
427 }
428
429 void read_constructors_and_mappings(const function_symbol_vector& constructors, const function_symbol_vector& mappings, const function_symbol_vector& normalized_constructors)
430 {
431 mCRL2log(log::debug) << "Start Read-in Func" << std::endl;
432
433 std::size_t constr_number=constructors.size();
434 function_symbol_vector functions_and_constructors=constructors;
435 functions_and_constructors.insert(functions_and_constructors.end(),mappings.begin(),mappings.end());
436 for (const function_symbol& f: functions_and_constructors)
437 {
438 sort_expression fsort = f.sort();
439
440 // This should be checked elsewhere
441 // check_sort_is_declared(fsort);
442
443 //if fsort is a defined function sort, unwind it
444 if (is_basic_sort(fsort))
445 {
446 const sort_expression s = unwind_sort_expression(fsort);
447 if (is_function_sort(s))
448 {
449 fsort = s;
450 }
451 }
452
453 if (is_function_sort(fsort))
454 {
455 add_function(data::function_symbol(f.name(), fsort), "function");
456 }
457 else
458 {
459 try
460 {
461 add_constant(data::function_symbol(f.name(), fsort), "constant");
462 }
463 catch (mcrl2::runtime_error& e)
464 {
465 throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not add constant");
466 }
467 }
468
469 if (constr_number)
470 {
471 constr_number--;
472
473 //Here checks for the constructors
474 sort_expression s = fsort;
475 if (is_function_sort(s))
476 {
477 s = atermpp::down_cast<function_sort>(s).codomain();
478 }
479 s = unwind_sort_expression(s);
480 if (!is_basic_sort(s) ||
481 sort_bool::is_bool(sort_expression(s)) ||
482 sort_pos::is_pos(sort_expression(s)) ||
483 sort_nat::is_nat(sort_expression(s)) ||
484 sort_int::is_int(sort_expression(s)) ||
485 sort_real::is_real(sort_expression(s))
486 )
487 {
488 throw mcrl2::runtime_error("Could not add constructor " + core::pp(f.name()) + " of sort " + data::pp(fsort) + ". Constructors of built-in sorts are not allowed.");
489 }
490 }
491
492 mCRL2log(log::debug) << "Read-in Func " << f.name() << ", Types " << fsort << "" << std::endl;
493 }
494
495 // Check that the constructors are defined such that they cannot generate an empty sort.
496 // E.g. in the specification sort D; cons f:D->D; the sort D must be necessarily empty, which is
497 // forbidden. The function below checks whether such malicious specifications occur.
498 check_for_empty_constructor_domains(normalized_constructors); // throws exception if not ok.
499 }
500
501 public:
502 type_checker(const data_specification& data_spec)
503 : sort_type_checker(data_spec)
504 {
505 initialise_system_defined_functions();
506 try
507 {
508 for (const alias& a: get_sort_specification().user_defined_aliases())
509 {
510 read_sort(a.reference());
511 }
512 read_constructors_and_mappings(data_spec.user_defined_constructors(),data_spec.user_defined_mappings(),data_spec.constructors());
513 }
514 catch (mcrl2::runtime_error& e)
515 {
516 throw mcrl2::runtime_error(std::string(e.what()) + "\ntype checking of data expression failed");
517 }
518 }
519
520 const std::map<core::identifier_string, sort_expression_list>& system_constants() const
521 {
522 return m_system_constants;
523 }
524
525 const std::map<core::identifier_string, function_sort_list>& system_functions() const
526 {
527 return m_system_functions;
528 }
529
530 const std::map<core::identifier_string, sort_expression>& user_constants() const
531 {
532 return m_user_constants;
533 }
534
535 const std::map<core::identifier_string, function_sort_list>& user_functions() const
536 {
537 return m_user_functions;
538 }
539};
540
541} // namespace data
542
543} // namespace mcrl2
544
545#endif // MCRL2_DATA_TYPE_CHECKER_H
546
atermpp::aterm_string
Term containing a string.
Definition aterm_string.h:20
atermpp::aterm::function
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
atermpp::function_symbol::name
const std::string & name() const
Return the name of the function_symbol.
Definition function_symbol.h:58
atermpp::term_list
A list of aterm objects.
Definition aterm_list.h:24
atermpp::term_list::end
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
atermpp::term_list::begin
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
atermpp::term_list::empty
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
atermpp::term_list::push_front
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
Definition aterm_list_implementation.h:30
mcrl2::data::alias
\brief A sort alias
Definition alias.h:26
mcrl2::data::basic_sort
\brief A basic sort
Definition basic_sort.h:26
mcrl2::data::basic_sort::name
const core::identifier_string & name() const
Definition basic_sort.h:57
mcrl2::data::container_sort
\brief A container sort
Definition container_sort.h:27
mcrl2::data::container_sort::container_name
const container_type & container_name() const
Definition container_sort.h:53
mcrl2::data::container_sort::element_sort
const sort_expression & element_sort() const
Definition container_sort.h:58
mcrl2::data::data_expression::sort
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
mcrl2::data::data_specification
data specification.
Definition data_specification.h:48
mcrl2::data::data_specification::user_defined_constructors
const function_symbol_vector & user_defined_constructors() const
Gets the constructors defined by the user, excluding those that are system defined.
Definition data_specification.h:345
mcrl2::data::data_specification::user_defined_mappings
const function_symbol_vector & user_defined_mappings() const
Gets all user defined mappings in this specification.
Definition data_specification.h:386
mcrl2::data::data_specification::constructors
const function_symbol_vector & constructors() const
Gets all constructors including those that are system defined.
Definition data_specification.h:335
mcrl2::data::function_sort
\brief A function sort
Definition function_sort.h:26
mcrl2::data::function_sort::codomain
const sort_expression & codomain() const
Definition function_sort.h:63
mcrl2::data::function_sort::domain
const sort_expression_list & domain() const
Definition function_sort.h:58
mcrl2::data::function_symbol
\brief A function symbol
Definition function_symbol.h:28
mcrl2::data::function_symbol::name
const core::identifier_string & name() const
Definition function_symbol.h:38
mcrl2::data::function_symbol::sort
const sort_expression & sort() const
Definition function_symbol.h:43
mcrl2::data::sort_expression
\brief A sort expression
Definition sort_expression.h:63
mcrl2::data::sort_specification::user_defined_aliases
const alias_vector & user_defined_aliases() const
Gets the user defined aliases.
Definition sort_specification.h:232
mcrl2::data::sort_type_checker
Definition sort_type_checker.h:25
mcrl2::data::sort_type_checker::get_sort_specification
const sort_specification & get_sort_specification() const
Definition sort_type_checker.h:42
mcrl2::data::sort_type_checker::check_for_empty_constructor_domains
void check_for_empty_constructor_domains(const function_symbol_vector &constructors)
Definition sort_type_checker.h:297
mcrl2::data::structured_sort_constructor_argument
\brief An argument of a constructor of a structured sort
Definition structured_sort_constructor_argument.h:26
mcrl2::data::structured_sort_constructor
\brief A constructor for a structured sort
Definition structured_sort_constructor.h:29
mcrl2::data::structured_sort
structured sort.
Definition structured_sort.h:56
mcrl2::data::structured_sort::constructors
const structured_sort_constructor_list & constructors() const
Definition structured_sort.h:88
mcrl2::data::type_checker
Definition type_checker.h:99
mcrl2::data::type_checker::unwind_sort_expression
sort_expression unwind_sort_expression(const sort_expression &x) const
Definition type_checker.h:124
mcrl2::data::type_checker::user_constants
const std::map< core::identifier_string, sort_expression > & user_constants() const
Definition type_checker.h:530
mcrl2::data::type_checker::add_system_function
void add_system_function(const data::function_symbol &f)
Definition type_checker.h:119
mcrl2::data::type_checker::type_checker
type_checker(const data_specification &data_spec)
Definition type_checker.h:502
mcrl2::data::type_checker::initialise_system_defined_functions
void initialise_system_defined_functions()
Definition type_checker.h:143
mcrl2::data::type_checker::add_constant
void add_constant(const data::function_symbol &f, const std::string &msg)
Definition type_checker.h:326
mcrl2::data::type_checker::system_constants
const std::map< core::identifier_string, sort_expression_list > & system_constants() const
Definition type_checker.h:520
mcrl2::data::type_checker::read_constructors_and_mappings
void read_constructors_and_mappings(const function_symbol_vector &constructors, const function_symbol_vector &mappings, const function_symbol_vector &normalized_constructors)
Definition type_checker.h:429
mcrl2::data::type_checker::m_system_functions
std::map< core::identifier_string, function_sort_list > m_system_functions
Definition type_checker.h:102
mcrl2::data::type_checker::read_sort
void read_sort(const sort_expression &x)
Definition type_checker.h:372
mcrl2::data::type_checker::equal_types
bool equal_types(const sort_expression &x1, const sort_expression &x2) const
Definition type_checker.h:129
mcrl2::data::type_checker::add_function
void add_function(const data::function_symbol &f, const std::string &msg, bool allow_double_decls=false)
Definition type_checker.h:339
mcrl2::data::type_checker::add_system_constant
void add_system_constant(const data::function_symbol &f)
Definition type_checker.h:106
mcrl2::data::type_checker::m_user_functions
std::map< core::identifier_string, function_sort_list > m_user_functions
Definition type_checker.h:104
mcrl2::data::type_checker::user_functions
const std::map< core::identifier_string, function_sort_list > & user_functions() const
Definition type_checker.h:535
mcrl2::data::type_checker::system_functions
const std::map< core::identifier_string, function_sort_list > & system_functions() const
Definition type_checker.h:525
mcrl2::data::type_checker::m_user_constants
std::map< core::identifier_string, sort_expression > m_user_constants
Definition type_checker.h:103
mcrl2::data::type_checker::find_sort
bool find_sort(const sort_expression &x, const function_sort_list &sorts) const
Definition type_checker.h:138
mcrl2::data::type_checker::m_system_constants
std::map< core::identifier_string, sort_expression_list > m_system_constants
Definition type_checker.h:101
mcrl2::data::untyped_sort
\brief Unknown sort expression
Definition untyped_sort.h:24
mcrl2::runtime_error
Standard exception class for reporting runtime errors.
Definition exception.h:27
parse_impl.h
add your file description here.
mCRL2log
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
atermpp::reverse
term_list< Term > reverse(const term_list< Term > &l)
Returns the list with the elements in reversed order.
Definition aterm_list_implementation.h:107
mcrl2::core::empty_identifier_string
identifier_string empty_identifier_string()
Provides the empty identifier string.
Definition identifier_string.h:67
mcrl2::core::pp
std::string pp(const identifier_string &x)
Definition core.cpp:26
mcrl2::data::detail::unwind_sort_expression
sort_expression unwind_sort_expression(const sort_expression &x, const alias_vector &aliases)
Definition type_checker.h:54
mcrl2::data::detail::is_nat
bool is_nat(const core::identifier_string &Number)
Definition type_checker.h:31
mcrl2::data::detail::make_function_sort_
function_sort make_function_sort_(const sort_expression &domain, const sort_expression &codomain)
Definition type_checker.h:37
mcrl2::data::detail::is_pos
bool is_pos(const core::identifier_string &Number)
Definition type_checker.h:24
mcrl2::data::detail::is_numeric_type
bool is_numeric_type(const sort_expression &x)
Definition type_checker.h:83
mcrl2::data::detail::transform_aterm_list
atermpp::term_list< T > transform_aterm_list(const Function &f, const atermpp::term_list< T > &x)
Definition type_checker.h:43
mcrl2::data::sort_bag::difference
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:612
mcrl2::data::sort_bag::bag2set
function_symbol bag2set(const sort_expression &s)
Constructor for function symbol Bag2Set.
Definition bag1.h:707
mcrl2::data::sort_bag::intersection
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:511
mcrl2::data::sort_bag::count
function_symbol count(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:298
mcrl2::data::sort_bag::set2bag
function_symbol set2bag(const sort_expression &s)
Constructor for function symbol Set2Bag.
Definition bag1.h:769
mcrl2::data::sort_bag::constructor
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @bag.
Definition bag1.h:78
mcrl2::data::sort_bag::in
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:362
mcrl2::data::sort_bag::union_
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:426
mcrl2::data::sort_bag::bag
container_sort bag(const sort_expression &s)
Constructor for sort expression Bag(S)
Definition bag1.h:44
mcrl2::data::sort_bag::zero_function
function_symbol zero_function(const sort_expression &s)
Constructor for function symbol @zero_.
Definition bag1.h:831
mcrl2::data::sort_bool::is_bool
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:54
mcrl2::data::sort_bool::bool_
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
mcrl2::data::sort_bool::implies
const function_symbol & implies()
Constructor for function symbol =>.
Definition bool.h:363
mcrl2::data::sort_bool::and_
const function_symbol & and_()
Constructor for function symbol &&.
Definition bool.h:235
mcrl2::data::sort_bool::false_
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
mcrl2::data::sort_bool::or_
const function_symbol & or_()
Constructor for function symbol ||.
Definition bool.h:299
mcrl2::data::sort_bool::not_
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:173
mcrl2::data::sort_bool::true_
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
mcrl2::data::sort_fbag::fbag
container_sort fbag(const sort_expression &s)
Constructor for sort expression FBag(S)
Definition fbag1.h:43
mcrl2::data::sort_fbag::count_all
function_symbol count_all(const sort_expression &s)
Constructor for function symbol #.
Definition fbag1.h:725
mcrl2::data::sort_fbag::empty
function_symbol empty(const sort_expression &s)
Constructor for function symbol {:}.
Definition fbag1.h:77
mcrl2::data::sort_fbag::cinsert
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fbag_cinsert.
Definition fbag1.h:277
mcrl2::data::sort_fset::insert
function_symbol insert(const sort_expression &s)
Constructor for function symbol @fset_insert.
Definition fset1.h:107
mcrl2::data::sort_fset::empty
function_symbol empty(const sort_expression &s)
Constructor for function symbol {}.
Definition fset1.h:75
mcrl2::data::sort_fset::count
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
Definition fset1.h:593
mcrl2::data::sort_fset::fset
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
Definition fset1.h:41
mcrl2::data::sort_int::int2nat
const function_symbol & int2nat()
Constructor for function symbol Int2Nat.
Definition int1.h:298
mcrl2::data::sort_int::is_int
bool is_int(const sort_expression &e)
Recogniser for sort expression Int.
Definition int1.h:57
mcrl2::data::sort_int::nat2int
const function_symbol & nat2int()
Constructor for function symbol Nat2Int.
Definition int1.h:236
mcrl2::data::sort_int::int2pos
const function_symbol & int2pos()
Constructor for function symbol Int2Pos.
Definition int1.h:422
mcrl2::data::sort_int::cint
const function_symbol & cint()
Constructor for function symbol @cInt.
Definition int1.h:80
mcrl2::data::sort_int::mod
function_symbol mod(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1261
mcrl2::data::sort_int::div
function_symbol div(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1184
mcrl2::data::sort_int::int_
const basic_sort & int_()
Constructor for sort expression Int.
Definition int1.h:47
mcrl2::data::sort_list::in
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition list1.h:208
mcrl2::data::sort_list::rtail
function_symbol rtail(const sort_expression &s)
Constructor for function symbol rtail.
Definition list1.h:712
mcrl2::data::sort_list::empty
function_symbol empty(const sort_expression &s)
Constructor for function symbol [].
Definition list1.h:76
mcrl2::data::sort_list::element_at
function_symbol element_at(const sort_expression &s)
Constructor for function symbol ..
Definition list1.h:462
mcrl2::data::sort_list::head
function_symbol head(const sort_expression &s)
Constructor for function symbol head.
Definition list1.h:526
mcrl2::data::sort_list::snoc
function_symbol snoc(const sort_expression &s)
Constructor for function symbol <|.
Definition list1.h:334
mcrl2::data::sort_list::count
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
Definition list1.h:272
mcrl2::data::sort_list::rhead
function_symbol rhead(const sort_expression &s)
Constructor for function symbol rhead.
Definition list1.h:650
mcrl2::data::sort_list::tail
function_symbol tail(const sort_expression &s)
Constructor for function symbol tail.
Definition list1.h:588
mcrl2::data::sort_list::cons_
function_symbol cons_(const sort_expression &s)
Constructor for function symbol |>.
Definition list1.h:108
mcrl2::data::sort_list::concat
function_symbol concat(const sort_expression &s)
Constructor for function symbol ++.
Definition list1.h:398
mcrl2::data::sort_nat::cnat
const function_symbol & cnat()
Constructor for function symbol @cNat.
Definition nat1.h:140
mcrl2::data::sort_nat::nat
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:46
mcrl2::data::sort_nat::is_nat
bool is_nat(const sort_expression &e)
Recogniser for sort expression Nat.
Definition nat1.h:56
mcrl2::data::sort_nat::sqrt
const function_symbol & sqrt()
Constructor for function symbol sqrt.
Definition nat1.h:1663
mcrl2::data::sort_nat::nat2pos
const function_symbol & nat2pos()
Constructor for function symbol Nat2Pos.
Definition nat1.h:362
mcrl2::data::sort_nat::pos2nat
const function_symbol & pos2nat()
Constructor for function symbol Pos2Nat.
Definition nat1.h:300
mcrl2::data::sort_pos::is_pos
bool is_pos(const sort_expression &e)
Recogniser for sort expression Pos.
Definition pos1.h:55
mcrl2::data::sort_pos::c1
const function_symbol & c1()
Constructor for function symbol @c1.
Definition pos1.h:78
mcrl2::data::sort_pos::pos
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
mcrl2::data::sort_real::minimum
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:650
mcrl2::data::sort_real::plus
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1059
mcrl2::data::sort_real::creal
const function_symbol & creal()
Constructor for function symbol @cReal.
Definition real1.h:107
mcrl2::data::sort_real::pos2real
const function_symbol & pos2real()
Constructor for function symbol Pos2Real.
Definition real1.h:171
mcrl2::data::sort_real::round
const function_symbol & round()
Constructor for function symbol round.
Definition real1.h:1597
mcrl2::data::sort_real::times
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1237
mcrl2::data::sort_real::divides
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1407
mcrl2::data::sort_real::real2nat
const function_symbol & real2nat()
Constructor for function symbol Real2Nat.
Definition real1.h:419
mcrl2::data::sort_real::ceil
const function_symbol & ceil()
Constructor for function symbol ceil.
Definition real1.h:1535
mcrl2::data::sort_real::succ
function_symbol succ(const sort_expression &s0)
Definition real1.h:893
mcrl2::data::sort_real::real2int
const function_symbol & real2int()
Constructor for function symbol Real2Int.
Definition real1.h:481
mcrl2::data::sort_real::pred
function_symbol pred(const sort_expression &s0)
Definition real1.h:976
mcrl2::data::sort_real::minus
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1152
mcrl2::data::sort_real::real_
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:48
mcrl2::data::sort_real::floor
const function_symbol & floor()
Constructor for function symbol floor.
Definition real1.h:1473
mcrl2::data::sort_real::is_real
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:58
mcrl2::data::sort_real::nat2real
const function_symbol & nat2real()
Constructor for function symbol Nat2Real.
Definition real1.h:233
mcrl2::data::sort_real::abs
function_symbol abs(const sort_expression &s0)
Definition real1.h:735
mcrl2::data::sort_real::negate
function_symbol negate(const sort_expression &s0)
Definition real1.h:810
mcrl2::data::sort_real::int2real
const function_symbol & int2real()
Constructor for function symbol Int2Real.
Definition real1.h:295
mcrl2::data::sort_real::exp
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1322
mcrl2::data::sort_real::real2pos
const function_symbol & real2pos()
Constructor for function symbol Real2Pos.
Definition real1.h:357
mcrl2::data::sort_real::maximum
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:541
mcrl2::data::sort_set::intersection
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:499
mcrl2::data::sort_set::set_
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
Definition set1.h:42
mcrl2::data::sort_set::constructor
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @set.
Definition set1.h:76
mcrl2::data::sort_set::false_function
function_symbol false_function(const sort_expression &s)
Constructor for function symbol @false_.
Definition set1.h:667
mcrl2::data::sort_set::in
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:296
mcrl2::data::sort_set::union_
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:422
mcrl2::data::sort_set::difference
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:584
mcrl2::data::sort_set::complement
function_symbol complement(const sort_expression &s)
Constructor for function symbol !.
Definition set1.h:362
mcrl2::data::function_sort_list
atermpp::term_list< function_sort > function_sort_list
list of function sorts
Definition function_sort.h:98
mcrl2::data::is_structured_sort
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
Definition sort_expression.h:43
mcrl2::data::less_equal
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:277
mcrl2::data::not_equal_to
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:163
mcrl2::data::alias_vector
std::vector< alias > alias_vector
\brief vector of aliass
Definition alias.h:75
mcrl2::data::less
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:240
mcrl2::data::is_untyped_sort
bool is_untyped_sort(const atermpp::aterm &x)
Returns true if the term t is the unknown sort.
Definition sort_expression.h:49
mcrl2::data::make_function_sort_
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
Definition function_sort.h:107
mcrl2::data::pp
std::string pp(const abstraction &x)
Definition data.cpp:39
mcrl2::data::greater_equal
function_symbol greater_equal(const sort_expression &s)
Constructor for function symbol >=.
Definition standard.h:351
mcrl2::data::is_container_sort
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
Definition sort_expression.h:37
mcrl2::data::is_basic_sort
bool is_basic_sort(const atermpp::aterm &x)
Returns true if the term t is a basic sort.
Definition sort_expression.h:25
mcrl2::data::is_function_sort
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
Definition sort_expression.h:31
mcrl2::data::equal_to
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
mcrl2::data::function_update
function_symbol function_update(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @func_update.
Definition function_update.h:73
mcrl2::data::function_symbol_vector
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
Definition function_symbol.h:91
mcrl2::data::if_
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
mcrl2::data::greater
function_symbol greater(const sort_expression &s)
Constructor for function symbol >
Definition standard.h:314
mcrl2
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72