Line data Source code
1 : // Author(s): Jan Friso Groote, 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/typecheck.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_TYPECHECK_H
13 : #define MCRL2_DATA_TYPECHECK_H
14 :
15 : #include "mcrl2/atermpp/aterm_io.h"
16 : #include "mcrl2/data/data_specification.h"
17 : #include "mcrl2/data/detail/variable_context.h"
18 : #include "mcrl2/data/sort_type_checker.h"
19 :
20 : namespace mcrl2
21 : {
22 :
23 : namespace data
24 : {
25 :
26 : class data_type_checker: public sort_type_checker
27 : {
28 : protected:
29 : mutable bool was_warning_upcasting; // This variable is used to limit the number of upcasting warnings.
30 :
31 : std::map<core::identifier_string,sort_expression_list> system_constants; //name -> Set(sort expression)
32 : std::map<core::identifier_string,sort_expression_list> system_functions; //name -> Set(sort expression)
33 : std::map<core::identifier_string,sort_expression> user_constants; //name -> sort expression
34 : std::map<core::identifier_string,sort_expression_list> user_functions; //name -> Set(sort expression)
35 : data_specification type_checked_data_spec;
36 :
37 : public:
38 : /** \brief make a data type checker.
39 : * Throws a mcrl2::runtime_error exception if the data_specification is not well typed.
40 : * \param[in] data_spec A data specification that does not need to have been type checked.
41 : * \return A data expression where all untyped identifiers have been replace by typed ones.
42 : **/
43 : data_type_checker(const data_specification& data_spec);
44 :
45 : /** \brief Type checks a variable.
46 : * Throws an mcrl2::runtime_error exception if the variable is not well typed.
47 : * \details A variable is not well typed if its name clashes with the name of a declared function, when its sort does not exist, or when
48 : * the variable is used in its context with a different sort.
49 : * \param[in] v A variables that is to be type checked.
50 : * \param[in] context Information about the context of the variable.
51 : **/
52 : void operator()(const variable& v, const detail::variable_context& context) const;
53 :
54 : /** \brief Type checks a variable list.
55 : * Throws an mcrl2::runtime_error exception if the variables are not well typed.
56 : * \details A variable is not well typed if its name clashes with the name of a declared function, when its sort does not exist, or when
57 : * a variable occurs in the context. Furthermore, variables cannot occur multiple times in a variable list.
58 : * \param[in] l A list of variables that must be type checked.
59 : * \param[in] context Information about the context of the variables in the list.
60 : **/
61 : void operator()(const variable_list& l, const detail::variable_context& context) const;
62 :
63 : /** \brief Yields a type checked data specification, provided typechecking was successful.
64 : * If not successful an exception is thrown.
65 : * \return a data specification where all untyped identifiers have been replace by typed ones.
66 : **/
67 : const data_specification operator()() const;
68 :
69 : /** \brief Yields a type checked equation list, and sets the types in the equations right.
70 : * If not successful an exception is thrown.
71 : * \param[in] eqns The list of equations that is type checked and updated.
72 : **/
73 : void operator()(data_equation_vector& eqns);
74 :
75 12882 : data_expression typecheck_data_expression(const data_expression& x,
76 : const sort_expression& expected_sort,
77 : const detail::variable_context& variable_context
78 : )
79 : {
80 12882 : data_expression x1 = x;
81 12882 : TraverseVarConsTypeD(variable_context, x1, expected_sort);
82 12553 : x1 = data::normalize_sorts(x1, get_sort_specification());
83 12553 : if (x1.sort() != expected_sort)
84 : {
85 779 : x1 = upcast_numeric_type(x1, expected_sort, variable_context);
86 : }
87 12553 : return x1;
88 329 : }
89 :
90 15 : assignment typecheck_assignment(const assignment& x, const detail::variable_context& variable_context)
91 : {
92 15 : sort_type_checker::check_sort_is_declared(x.lhs().sort());
93 15 : data_expression rhs = typecheck_data_expression(x.rhs(), x.lhs().sort(), variable_context);
94 30 : return assignment(x.lhs(), rhs);
95 15 : }
96 :
97 168 : assignment_list typecheck_assignment_list(const assignment_list& assignments, const detail::variable_context& variable_context)
98 : {
99 : // check for name clashes
100 168 : std::set<core::identifier_string> names;
101 183 : for (const assignment& a: assignments)
102 : {
103 15 : const core::identifier_string& name = a.lhs().name();
104 15 : if (names.find(name) != names.end())
105 : {
106 0 : throw mcrl2::runtime_error("duplicate variable names in assignments: " + data::pp(assignments) + ")");
107 : }
108 15 : names.insert(name);
109 : }
110 :
111 : // typecheck the assignments
112 168 : assignment_vector result;
113 183 : for (const assignment& a: assignments)
114 : {
115 15 : result.push_back(typecheck_assignment(a, variable_context));
116 : }
117 336 : return assignment_list(result.begin(), result.end());
118 168 : }
119 :
120 3404 : const data_specification& typechecked_data_specification() const
121 : {
122 3404 : return type_checked_data_spec;
123 : }
124 :
125 : void print_context() const
126 : {
127 : auto const& sortspec = get_sort_specification();
128 : std::cout << "--- basic sorts ---" << std::endl;
129 : for (auto const& x: sortspec.user_defined_sorts())
130 : {
131 : std::cout << x << std::endl;
132 : }
133 : std::cout << "--- aliases ---" << std::endl;
134 : for (auto const& x: sortspec.user_defined_aliases())
135 : {
136 : std::cout << x << std::endl;
137 : }
138 : std::cout << "--- user constants ---" << std::endl;
139 : for (const auto& user_constant: user_constants)
140 : {
141 : std::cout << user_constant.first << " -> " << user_constant.second << std::endl;
142 : }
143 : std::cout << "--- user functions ---" << std::endl;
144 : for (const auto& user_function: user_functions)
145 : {
146 : std::cout << user_function.first << " -> " << user_function.second << std::endl;
147 : }
148 : }
149 :
150 : protected:
151 : /** \brief Type check a data expression.
152 : * Throws a mcrl2::runtime_error exception if the expression is not well typed.
153 : * \param[in] data_expr A data expression that has not been type checked.
154 : * \param[in] context The variable context in which this term must be typechecked.
155 : * \return a data expression where all untyped identifiers have been replace by typed ones.
156 : **/
157 : data_expression operator()(const data_expression& data_expr,
158 : const detail::variable_context& context) const;
159 :
160 : void read_sort(const sort_expression& SortExpr);
161 : void read_constructors_and_mappings(const function_symbol_vector& constructors, const function_symbol_vector& mappings, const function_symbol_vector& normalized_constructors);
162 : void add_function(const data::function_symbol& f, const std::string& msg, bool allow_double_decls=false);
163 : void add_constant(const data::function_symbol& f, const std::string& msg);
164 : void initialise_system_defined_functions(void);
165 : void add_system_constant(const data::function_symbol& f);
166 : void add_system_function(const data::function_symbol& f);
167 : void add_system_constants_and_functions(const std::vector<data::function_symbol>& v);
168 : bool TypeMatchA(const sort_expression& Type_in, const sort_expression& PosType_in, sort_expression& result) const;
169 : bool TypeMatchL(const sort_expression_list& TypeList, const sort_expression_list& PosTypeList, sort_expression_list& result) const;
170 : sort_expression UnwindType(const sort_expression& Type) const;
171 : variable UnwindType(const variable& v) const;
172 : template <class T>
173 : atermpp::term_list<T> UnwindType(const atermpp::term_list<T>& l)
174 : {
175 : std::vector<T> result;
176 : for(typename atermpp::term_list<T>::const_iterator i=l.begin(); i!=l.end(); ++i)
177 : {
178 : result.push_back(UnwindType(*i));
179 : }
180 : return atermpp::term_list<T>(result.begin(),result.end());
181 : }
182 :
183 : sort_expression TraverseVarConsTypeD(
184 : const detail::variable_context& DeclaredVars,
185 : data_expression& DataTerm,
186 : const sort_expression& PosType,
187 : const bool strictly_ambiguous=true,
188 : const bool warn_upcasting=false,
189 : const bool print_cast_error=true) const;
190 :
191 : /* sort_expression TraverseVarConsTypeD(const std::map<core::identifier_string,sort_expression>& DeclaredVars,
192 : data_expression& t1,
193 : const sort_expression& t2); */
194 :
195 : sort_expression TraverseVarConsTypeDN(
196 : const detail::variable_context& DeclaredVars,
197 : data_expression& DataTerm,
198 : sort_expression PosType,
199 : const bool strictly_ambiguous=true,
200 : const std::size_t nFactPars=std::string::npos,
201 : const bool warn_upcasting=false,
202 : const bool print_cast_error=true) const;
203 :
204 : bool InTypesA(const sort_expression& Type, sort_expression_list Types) const;
205 : bool EqTypesA(const sort_expression& Type1, const sort_expression& Type2) const;
206 : bool InTypesL(const sort_expression_list& Type, atermpp::term_list<sort_expression_list> Types) const;
207 : bool EqTypesL(sort_expression_list Type1, sort_expression_list Type2) const;
208 : bool MaximumType(const sort_expression& Type1, const sort_expression& Type2, sort_expression& result) const;
209 : sort_expression ExpandNumTypesUp(sort_expression Type) const;
210 : sort_expression_list ExpandNumTypesUpL(const sort_expression_list& type_list) const;
211 : sort_expression ExpandNumTypesDown(sort_expression Type) const;
212 : bool UnifyMinType(const sort_expression& Type1, const sort_expression& Type2, sort_expression& result) const;
213 : sort_expression determine_allowed_type(const data_expression& d, const sort_expression& proposed_type) const;
214 : bool MatchIf(const function_sort& type, sort_expression& result) const;
215 : bool MatchEqNeqComparison(const function_sort& type, sort_expression& result) const;
216 : bool MatchSqrt(const function_sort& type, sort_expression& result) const;
217 : bool MatchListOpCons(const function_sort& type, sort_expression& result) const;
218 : bool MatchListOpSnoc(const function_sort& type, sort_expression& result) const;
219 : bool MatchListOpConcat(const function_sort& type, sort_expression& result) const;
220 : bool MatchListOpEltAt(const function_sort& type, sort_expression& result) const;
221 : bool MatchListOpHead(const function_sort& type, sort_expression& result) const;
222 : bool MatchListOpTail(const function_sort& type, sort_expression& result) const;
223 : bool MatchSetOpSet2Bag(const function_sort& type, sort_expression& result) const;
224 : bool MatchFalseFunction(const function_sort& type, sort_expression& result) const;
225 : bool MatchListSetBagOpIn(const function_sort& type, sort_expression& result) const;
226 : bool match_fset_insert(const function_sort& type, sort_expression& result) const;
227 : bool match_fbag_cinsert(const function_sort& type, sort_expression& result) const;
228 : bool MatchSetBagOpUnionDiffIntersect(const function_sort& type, sort_expression& result) const;
229 : bool MatchSetOpSetCompl(const function_sort& type, sort_expression& result) const;
230 : bool MatchBagOpBag2Set(const function_sort& type, sort_expression& result) const;
231 : bool MatchBagOpBagCount(const function_sort& type, sort_expression& result) const;
232 : bool MatchFuncUpdate(const function_sort& type, sort_expression& result) const;
233 : bool MatchSetConstructor(const function_sort& type, sort_expression& result) const;
234 : bool MatchBagConstructor(const function_sort& type, sort_expression& result) const;
235 : bool UnArrowProd(const sort_expression_list& ArgTypes, sort_expression PosType, sort_expression& result) const;
236 : bool UnFSet(sort_expression PosType, sort_expression& result) const;
237 : bool UnFBag(sort_expression PosType, sort_expression& result) const;
238 : bool UnList(sort_expression PosType, sort_expression& result) const;
239 : void ErrorMsgCannotCast(sort_expression CandidateType, data_expression_list Arguments, sort_expression_list ArgumentTypes,std::string previous_reason) const;
240 : sort_expression UpCastNumericType(
241 : sort_expression NeededType,
242 : sort_expression Type,
243 : data_expression& Par,
244 : const detail::variable_context& DeclaredVars,
245 : const bool strictly_ambiguous,
246 : bool warn_upcasting=false,
247 : const bool print_cast_error=false) const;
248 : void TransformVarConsTypeData(data_specification& data_spec);
249 : sort_expression_list GetNotInferredList(const atermpp::term_list<sort_expression_list>& TypeListList) const;
250 : sort_expression_list InsertType(const sort_expression_list& TypeList, const sort_expression& Type) const;
251 : std::pair<bool,sort_expression_list> AdjustNotInferredList(
252 : const sort_expression_list& PosTypeList,
253 : const atermpp::term_list<sort_expression_list>& TypeListList) const;
254 : bool IsTypeAllowedA(const sort_expression& Type, const sort_expression& PosType) const;
255 : bool IsTypeAllowedL(const sort_expression_list& TypeList, const sort_expression_list& PosTypeList) const;
256 : bool IsNotInferredL(sort_expression_list TypeList) const;
257 : bool strict_type_check(const data_expression& d) const;
258 :
259 : // for example Pos -> Nat, or Nat -> Int
260 779 : data_expression upcast_numeric_type(const data_expression& x,
261 : const sort_expression& expected_sort,
262 : const detail::variable_context& variable_context
263 : )
264 : {
265 : try
266 : {
267 779 : data_expression x1 = x;
268 779 : UpCastNumericType(expected_sort, x.sort(), x1, variable_context, false, false, false);
269 1558 : return data::normalize_sorts(x1, get_sort_specification());
270 779 : }
271 0 : catch (mcrl2::runtime_error& e)
272 : {
273 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\ncannot (up)cast " + data::pp(x) + " to type " + data::pp(expected_sort));
274 0 : }
275 : }
276 :
277 : };
278 :
279 : /** \brief Type check a sort expression.
280 : * Throws an exception if something went wrong.
281 : * \param[in] sort_expr A sort expression that has not been type checked.
282 : * \param[in] data_spec The data specification to use as context.
283 : * \post sort_expr is type checked.
284 : **/
285 : inline
286 29 : void typecheck_sort_expression(const sort_expression& sort_expr, const data_specification& data_spec)
287 : {
288 : try
289 : {
290 : // sort_type_checker type_checker(data_spec.user_defined_sorts(), data_spec.user_defined_aliases());
291 29 : sort_type_checker type_checker(data_spec);
292 29 : type_checker(sort_expr);
293 29 : }
294 0 : catch (mcrl2::runtime_error& e)
295 : {
296 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nCould not type check sort " + pp(sort_expr));
297 0 : }
298 29 : }
299 :
300 : /** \brief Type check a data expression.
301 : * Throws an exception if something went wrong.
302 : * \param[in] x A data expression that has not been type checked.
303 : * \param[in] variables A container with variables that can occur in the data expression.
304 : * \param[in] dataspec The data specification that is used for type checking.
305 : * \post data_expr is type checked.
306 : **/
307 : template <typename VariableContainer>
308 809 : data_expression typecheck_data_expression(const data_expression& x,
309 : const VariableContainer& variables,
310 : const data_specification& dataspec = data_specification()
311 : )
312 : {
313 : try
314 : {
315 809 : data_type_checker typechecker(dataspec);
316 809 : detail::variable_context variable_context;
317 809 : variable_context.add_context_variables(variables, typechecker);
318 2397 : return typechecker.typecheck_data_expression(x, untyped_sort(), variable_context);
319 839 : }
320 60 : catch (mcrl2::runtime_error& e)
321 : {
322 30 : throw mcrl2::runtime_error(std::string(e.what()) + "\nCould not type check data expression " + data::pp(x));
323 : }
324 : }
325 :
326 : /** \brief Type check a data expression.
327 : * Throws an exception if something went wrong.
328 : * \param[in] x A data expression that has not been type checked.
329 : * \param[in] dataspec Data specification to be used as context.
330 : * \post data_expr is type checked.
331 : **/
332 : inline
333 16 : data_expression typecheck_data_expression(const data_expression& x, const data_specification& dataspec = data_specification())
334 : {
335 16 : return typecheck_data_expression(x, variable_list(), dataspec);
336 : }
337 :
338 : /** \brief Type check a parsed mCRL2 data specification.
339 : * Throws an exception if something went wrong.
340 : * \param[in] data_spec A data specification that has not been type checked.
341 : * \post data_spec is type checked.
342 : **/
343 : inline
344 158 : void typecheck_data_specification(data_specification& data_spec)
345 : {
346 158 : data_type_checker type_checker(data_spec);
347 146 : data_spec=type_checker();
348 146 : }
349 :
350 : inline
351 165 : data_expression typecheck_untyped_data_parameter(data_type_checker& typechecker,
352 : const core::identifier_string& name,
353 : const data_expression_list& parameters,
354 : const data::sort_expression& expected_sort,
355 : const detail::variable_context& variable_context
356 : )
357 : {
358 165 : if (parameters.empty())
359 : {
360 190 : return typechecker.typecheck_data_expression(untyped_identifier(name), expected_sort, variable_context);
361 : }
362 : else
363 : {
364 140 : return typechecker.typecheck_data_expression(application(untyped_identifier(name), parameters), expected_sort, variable_context);
365 : }
366 : }
367 :
368 : typedef atermpp::term_list<sort_expression_list> sorts_list;
369 :
370 : } // namespace data
371 :
372 : } // namespace mcrl2
373 :
374 : #endif // MCRL2_DATA_TYPECHECK_H
|