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