mCRL2
Loading...
Searching...
No Matches
typecheck.h
Go to the documentation of this file.
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//
11
12#ifndef MCRL2_DATA_TYPECHECK_H
13#define MCRL2_DATA_TYPECHECK_H
14
19
20namespace mcrl2
21{
22
23namespace data
24{
25
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)
36
37 public:
43 data_type_checker(const data_specification& data_spec);
44
52 void operator()(const variable& v, const detail::variable_context& context) const;
53
61 void operator()(const variable_list& l, const detail::variable_context& context) const;
62
67 const data_specification operator()() const;
68
74
76 const sort_expression& expected_sort,
77 const detail::variable_context& variable_context
78 )
79 {
80 data_expression x1 = x;
81 TraverseVarConsTypeD(variable_context, x1, expected_sort);
83 if (x1.sort() != expected_sort)
84 {
85 x1 = upcast_numeric_type(x1, expected_sort, variable_context);
86 }
87 return x1;
88 }
89
91 {
93 data_expression rhs = typecheck_data_expression(x.rhs(), x.lhs().sort(), variable_context);
94 return assignment(x.lhs(), rhs);
95 }
96
98 {
99 // check for name clashes
100 std::set<core::identifier_string> names;
101 for (const assignment& a: assignments)
102 {
103 const core::identifier_string& name = a.lhs().name();
104 if (names.find(name) != names.end())
105 {
106 throw mcrl2::runtime_error("duplicate variable names in assignments: " + data::pp(assignments) + ")");
107 }
108 names.insert(name);
109 }
110
111 // typecheck the assignments
112 assignment_vector result;
113 for (const assignment& a: assignments)
114 {
115 result.push_back(typecheck_assignment(a, variable_context));
116 }
117 return assignment_list(result.begin(), result.end());
118 }
119
121 {
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:
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);
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>
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
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
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;
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;
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;
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;
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
261 const sort_expression& expected_sort,
262 const detail::variable_context& variable_context
263 )
264 {
265 try
266 {
267 data_expression x1 = x;
268 UpCastNumericType(expected_sort, x.sort(), x1, variable_context, false, false, false);
270 }
271 catch (mcrl2::runtime_error& e)
272 {
273 throw mcrl2::runtime_error(std::string(e.what()) + "\ncannot (up)cast " + data::pp(x) + " to type " + data::pp(expected_sort));
274 }
275 }
276
277};
278
285inline
286void 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());
292 type_checker(sort_expr);
293 }
294 catch (mcrl2::runtime_error& e)
295 {
296 throw mcrl2::runtime_error(std::string(e.what()) + "\nCould not type check sort " + pp(sort_expr));
297 }
298}
299
307template <typename VariableContainer>
309 const VariableContainer& variables,
310 const data_specification& dataspec = data_specification()
311 )
312{
313 try
314 {
315 data_type_checker typechecker(dataspec);
316 detail::variable_context variable_context;
317 variable_context.add_context_variables(variables, typechecker);
318 return typechecker.typecheck_data_expression(x, untyped_sort(), variable_context);
319 }
320 catch (mcrl2::runtime_error& e)
321 {
322 throw mcrl2::runtime_error(std::string(e.what()) + "\nCould not type check data expression " + data::pp(x));
323 }
324}
325
332inline
334{
335 return typecheck_data_expression(x, variable_list(), dataspec);
336}
337
343inline
345{
347 data_spec=type_checker();
348}
349
350inline
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 if (parameters.empty())
359 {
360 return typechecker.typecheck_data_expression(untyped_identifier(name), expected_sort, variable_context);
361 }
362 else
363 {
364 return typechecker.typecheck_data_expression(application(untyped_identifier(name), parameters), expected_sort, variable_context);
365 }
366}
367
369
370} // namespace data
371
372} // namespace mcrl2
373
374#endif // MCRL2_DATA_TYPECHECK_H
Term containing a string.
Iterator for term_list.
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
An application of a data expression to a number of arguments.
\brief Assignment of a data expression to a variable
Definition assignment.h:91
const data_expression & rhs() const
Definition assignment.h:122
const variable & lhs() const
Definition assignment.h:117
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
bool IsNotInferredL(sort_expression_list TypeList) const
bool TypeMatchL(const sort_expression_list &TypeList, const sort_expression_list &PosTypeList, sort_expression_list &result) const
bool UnFBag(sort_expression PosType, sort_expression &result) const
std::map< core::identifier_string, sort_expression_list > system_functions
Definition typecheck.h:32
bool MatchIf(const function_sort &type, sort_expression &result) const
sort_expression TraverseVarConsTypeD(const detail::variable_context &DeclaredVars, data_expression &DataTerm, const sort_expression &PosType, const bool strictly_ambiguous=true, const bool warn_upcasting=false, const bool print_cast_error=true) const
bool MatchFalseFunction(const function_sort &type, sort_expression &result) const
bool MatchListOpCons(const function_sort &type, sort_expression &result) const
std::map< core::identifier_string, sort_expression_list > system_constants
Definition typecheck.h:31
bool UnifyMinType(const sort_expression &Type1, const sort_expression &Type2, sort_expression &result) const
bool MatchListOpEltAt(const function_sort &type, sort_expression &result) const
const data_specification operator()() const
Yields a type checked data specification, provided typechecking was successful. If not successful an ...
bool EqTypesA(const sort_expression &Type1, const sort_expression &Type2) const
std::map< core::identifier_string, sort_expression_list > user_functions
Definition typecheck.h:34
sort_expression UpCastNumericType(sort_expression NeededType, sort_expression Type, data_expression &Par, const detail::variable_context &DeclaredVars, const bool strictly_ambiguous, bool warn_upcasting=false, const bool print_cast_error=false) const
bool MatchListSetBagOpIn(const function_sort &type, sort_expression &result) const
bool match_fbag_cinsert(const function_sort &type, sort_expression &result) const
bool MatchSqrt(const function_sort &type, sort_expression &result) const
bool MatchBagOpBag2Set(const function_sort &type, sort_expression &result) const
void read_constructors_and_mappings(const function_symbol_vector &constructors, const function_symbol_vector &mappings, const function_symbol_vector &normalized_constructors)
bool MatchEqNeqComparison(const function_sort &type, sort_expression &result) const
bool InTypesL(const sort_expression_list &Type, atermpp::term_list< sort_expression_list > Types) const
bool MatchSetBagOpUnionDiffIntersect(const function_sort &type, sort_expression &result) const
sort_expression UnwindType(const sort_expression &Type) const
bool strict_type_check(const data_expression &d) const
Definition typecheck.cpp:84
bool MatchBagConstructor(const function_sort &type, sort_expression &result) const
bool MatchBagOpBagCount(const function_sort &type, sort_expression &result) const
assignment_list typecheck_assignment_list(const assignment_list &assignments, const detail::variable_context &variable_context)
Definition typecheck.h:97
sort_expression ExpandNumTypesUp(sort_expression Type) const
sort_expression ExpandNumTypesDown(sort_expression Type) const
sort_expression_list ExpandNumTypesUpL(const sort_expression_list &type_list) const
void add_constant(const data::function_symbol &f, const std::string &msg)
bool MatchListOpSnoc(const function_sort &type, sort_expression &result) const
bool UnFSet(sort_expression PosType, sort_expression &result) const
bool MatchListOpConcat(const function_sort &type, sort_expression &result) const
void add_system_function(const data::function_symbol &f)
void ErrorMsgCannotCast(sort_expression CandidateType, data_expression_list Arguments, sort_expression_list ArgumentTypes, std::string previous_reason) const
void TransformVarConsTypeData(data_specification &data_spec)
void add_system_constants_and_functions(const std::vector< data::function_symbol > &v)
bool IsTypeAllowedA(const sort_expression &Type, const sort_expression &PosType) const
data_expression typecheck_data_expression(const data_expression &x, const sort_expression &expected_sort, const detail::variable_context &variable_context)
Definition typecheck.h:75
assignment typecheck_assignment(const assignment &x, const detail::variable_context &variable_context)
Definition typecheck.h:90
bool MatchSetOpSetCompl(const function_sort &type, sort_expression &result) const
void initialise_system_defined_functions(void)
bool InTypesA(const sort_expression &Type, sort_expression_list Types) const
bool MaximumType(const sort_expression &Type1, const sort_expression &Type2, sort_expression &result) const
std::map< core::identifier_string, sort_expression > user_constants
Definition typecheck.h:33
bool UnList(sort_expression PosType, sort_expression &result) const
bool MatchFuncUpdate(const function_sort &type, sort_expression &result) const
void add_system_constant(const data::function_symbol &f)
bool MatchSetOpSet2Bag(const function_sort &type, sort_expression &result) const
std::pair< bool, sort_expression_list > AdjustNotInferredList(const sort_expression_list &PosTypeList, const atermpp::term_list< sort_expression_list > &TypeListList) const
bool EqTypesL(sort_expression_list Type1, sort_expression_list Type2) const
sort_expression determine_allowed_type(const data_expression &d, const sort_expression &proposed_type) const
data_expression upcast_numeric_type(const data_expression &x, const sort_expression &expected_sort, const detail::variable_context &variable_context)
Definition typecheck.h:260
void add_function(const data::function_symbol &f, const std::string &msg, bool allow_double_decls=false)
sort_expression_list GetNotInferredList(const atermpp::term_list< sort_expression_list > &TypeListList) const
void read_sort(const sort_expression &SortExpr)
const data_specification & typechecked_data_specification() const
Definition typecheck.h:120
bool MatchListOpHead(const function_sort &type, sort_expression &result) const
bool match_fset_insert(const function_sort &type, sort_expression &result) const
sort_expression TraverseVarConsTypeDN(const detail::variable_context &DeclaredVars, data_expression &DataTerm, sort_expression PosType, const bool strictly_ambiguous=true, const std::size_t nFactPars=std::string::npos, const bool warn_upcasting=false, const bool print_cast_error=true) const
sort_expression_list InsertType(const sort_expression_list &TypeList, const sort_expression &Type) const
bool UnArrowProd(const sort_expression_list &ArgTypes, sort_expression PosType, sort_expression &result) const
bool TypeMatchA(const sort_expression &Type_in, const sort_expression &PosType_in, sort_expression &result) const
bool IsTypeAllowedL(const sort_expression_list &TypeList, const sort_expression_list &PosTypeList) const
bool MatchSetConstructor(const function_sort &type, sort_expression &result) const
data_specification type_checked_data_spec
Definition typecheck.h:35
bool MatchListOpTail(const function_sort &type, sort_expression &result) const
atermpp::term_list< T > UnwindType(const atermpp::term_list< T > &l)
Definition typecheck.h:173
void add_context_variables(const VariableContainer &variables)
\brief A function sort
\brief A function symbol
\brief A sort expression
const sort_specification & get_sort_specification() const
void check_sort_is_declared(const sort_expression &x) const
\brief An untyped identifier
\brief Unknown sort expression
\brief A data variable
Definition variable.h:28
const sort_expression & sort() const
Definition variable.h:43
Standard exception class for reporting runtime errors.
Definition exception.h:27
The class data_specification.
std::vector< assignment > assignment_vector
\brief vector of assignments
Definition assignment.h:149
void typecheck_sort_expression(const sort_expression &sort_expr, const data_specification &data_spec)
Type check a sort expression. Throws an exception if something went wrong.
Definition typecheck.h:286
atermpp::term_list< sort_expression_list > sorts_list
Definition typecheck.h:368
void typecheck_data_specification(data_specification &data_spec)
Type check a parsed mCRL2 data specification. Throws an exception if something went wrong.
Definition typecheck.h:344
data_expression typecheck_data_expression(const data_expression &x, const VariableContainer &variables, const data_specification &dataspec=data_specification())
Type check a data expression. Throws an exception if something went wrong.
Definition typecheck.h:308
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
std::string pp(const abstraction &x)
Definition data.cpp:39
data_expression typecheck_untyped_data_parameter(data_type_checker &typechecker, const core::identifier_string &name, const data_expression_list &parameters, const data::sort_expression &expected_sort, const detail::variable_context &variable_context)
Definition typecheck.h:351
atermpp::term_list< variable > variable_list
\brief list of variables
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
add your file description here.
add your file description here.