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/pbes/typecheck.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_TYPECHECK_H
13 : #define MCRL2_PBES_TYPECHECK_H
14 :
15 : #include "mcrl2/data/consistency.h"
16 : #include "mcrl2/pbes/detail/pbes_context.h"
17 : #include "mcrl2/pbes/normalize_sorts.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace pbes_system
23 : {
24 :
25 : namespace detail
26 : {
27 :
28 : struct typecheck_builder: public pbes_expression_builder<typecheck_builder>
29 : {
30 : typedef pbes_expression_builder<typecheck_builder> super;
31 : using super::apply;
32 :
33 : data::data_type_checker& m_data_type_checker;
34 : data::detail::variable_context m_variable_context;
35 : const detail::pbes_context& m_pbes_context;
36 :
37 3331 : typecheck_builder(data::data_type_checker& data_typechecker,
38 : const data::detail::variable_context& variables,
39 : const detail::pbes_context& pbes_context
40 : )
41 3331 : : m_data_type_checker(data_typechecker),
42 3331 : m_variable_context(variables),
43 3331 : m_pbes_context(pbes_context)
44 3331 : { }
45 :
46 : template <class T>
47 3054 : void apply(T& result, const data::data_expression& x)
48 : {
49 3054 : result = m_data_type_checker.typecheck_data_expression(x, data::bool_(), m_variable_context);
50 3054 : }
51 :
52 : template <class T>
53 219 : void apply(T& result, const forall& x)
54 : {
55 : try
56 : {
57 219 : data::detail::check_duplicate_variable_names(x.variables(), "quantifier variable");
58 219 : auto m_variable_context_copy = m_variable_context;
59 219 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
60 219 : pbes_expression body;
61 219 : (*this).apply(body, x.body());
62 219 : m_variable_context = m_variable_context_copy;
63 219 : result = forall(x.variables(), body);
64 219 : }
65 0 : catch (mcrl2::runtime_error& e)
66 : {
67 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + pbes_system::pp(x));
68 : }
69 219 : }
70 :
71 : template <class T>
72 119 : void apply(T& result, const exists& x)
73 : {
74 : try
75 : {
76 119 : data::detail::check_duplicate_variable_names(x.variables(), "quantifier variable");
77 119 : auto m_variable_context_copy = m_variable_context;
78 119 : m_variable_context.add_context_variables(x.variables(), m_data_type_checker);
79 119 : pbes_expression body;
80 119 : (*this).apply(body, x.body());
81 119 : m_variable_context = m_variable_context_copy;
82 119 : result = exists(x.variables(), body);
83 119 : }
84 0 : catch (mcrl2::runtime_error& e)
85 : {
86 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nwhile typechecking " + pbes_system::pp(x));
87 : }
88 119 : }
89 :
90 : template <class T>
91 467 : void apply(T& result, const propositional_variable_instantiation& x)
92 : {
93 467 : const core::identifier_string& name = x.name();
94 467 : if (!m_pbes_context.is_declared(name))
95 : {
96 0 : throw mcrl2::runtime_error("propositional variable " + core::pp(name) + " not declared");
97 : }
98 :
99 467 : data::sort_expression_list equation_sorts = m_pbes_context.propositional_variable_sorts(name);
100 467 : std::vector<data::data_expression> x_parameters(x.parameters().begin(), x.parameters().end());
101 :
102 467 : if (x_parameters.size() != equation_sorts.size())
103 : {
104 0 : throw mcrl2::runtime_error("propositional variable " + pbes_system::pp(x) + " has the wrong number of parameters");
105 : }
106 :
107 467 : auto ei = equation_sorts.begin();
108 467 : auto xi = x_parameters.begin();
109 714 : for (; ei != equation_sorts.end(); ++ei, ++xi)
110 : {
111 : try
112 : {
113 247 : *xi = m_data_type_checker.typecheck_data_expression(*xi, *ei, m_variable_context);
114 : }
115 0 : catch (mcrl2::runtime_error& e)
116 : {
117 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\ncannot typecheck " + data::pp(*xi) + " as type " + data::pp(*ei) + " (while typechecking " + pbes_system::pp(x) + ")");
118 : }
119 : }
120 467 : make_propositional_variable_instantiation(result, name, data::data_expression_list(x_parameters.begin(), x_parameters.end()));
121 467 : }
122 :
123 : template <class T>
124 787 : void apply(T& result, const data::untyped_data_parameter& x)
125 : {
126 787 : const core::identifier_string& name = x.name();
127 787 : if (!m_pbes_context.is_declared(name))
128 : {
129 0 : result = data::typecheck_untyped_data_parameter(m_data_type_checker, x.name(), x.arguments(), data::bool_(), m_variable_context);
130 0 : return;
131 : }
132 :
133 787 : data::sort_expression_list equation_sorts = m_pbes_context.propositional_variable_sorts(name);
134 787 : std::vector<data::data_expression> x_parameters(x.arguments().begin(), x.arguments().end());
135 :
136 787 : if (x_parameters.size() != equation_sorts.size())
137 : {
138 0 : throw mcrl2::runtime_error("propositional variable " + data::pp(x) + " has the wrong number of parameters");
139 : }
140 :
141 787 : auto ei = equation_sorts.begin();
142 787 : auto xi = x_parameters.begin();
143 1899 : for (; ei != equation_sorts.end(); ++ei, ++xi)
144 : {
145 : try
146 : {
147 1112 : *xi = m_data_type_checker.typecheck_data_expression(*xi, *ei, m_variable_context);
148 : }
149 0 : catch (mcrl2::runtime_error& e)
150 : {
151 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\ncannot typecheck " + data::pp(*xi) + " as type " + data::pp(*ei) + " (while typechecking " + data::pp(x) + ")");
152 : }
153 : }
154 787 : make_propositional_variable_instantiation(result, name, data::data_expression_list(x_parameters.begin(), x_parameters.end()));
155 787 : }
156 : };
157 :
158 : inline
159 3331 : typecheck_builder make_typecheck_builder(
160 : data::data_type_checker& data_typechecker,
161 : const data::detail::variable_context& variables,
162 : const detail::pbes_context& propositional_variables
163 : )
164 : {
165 3331 : return typecheck_builder(data_typechecker, variables, propositional_variables);
166 : }
167 :
168 : } // namespace detail
169 :
170 : class pbes_type_checker
171 : {
172 : protected:
173 : data::data_type_checker m_data_type_checker;
174 : data::detail::variable_context m_variable_context;
175 : detail::pbes_context m_pbes_context;
176 :
177 467 : std::vector<propositional_variable> equation_variables(const std::vector<pbes_equation>& equations)
178 : {
179 467 : std::vector<propositional_variable> result;
180 3330 : for (const pbes_equation& eqn: equations)
181 : {
182 2863 : result.push_back(eqn.variable());
183 : }
184 467 : return result;
185 0 : }
186 :
187 : public:
188 : /// \brief Default constructor
189 467 : pbes_type_checker(const data::data_specification& dataspec = data::data_specification())
190 467 : : m_data_type_checker(dataspec)
191 467 : {}
192 :
193 : /// \brief Constructor
194 : template <typename VariableContainer, typename PropositionalVariableContainer>
195 1 : pbes_type_checker(const data::data_specification& dataspec, const VariableContainer& global_variables, const PropositionalVariableContainer& propositional_variables)
196 1 : : m_data_type_checker(dataspec)
197 : {
198 1 : m_variable_context.add_context_variables(global_variables, m_data_type_checker);
199 1 : m_pbes_context.add_propositional_variables(propositional_variables, m_data_type_checker);
200 1 : }
201 :
202 : /// \brief Typecheck the pbes pbesspec
203 467 : void operator()(pbes& pbesspec)
204 : {
205 467 : mCRL2log(log::verbose) << "type checking PBES specification..." << std::endl;
206 :
207 467 : pbes_system::normalize_sorts(pbesspec, m_data_type_checker.typechecked_data_specification());
208 :
209 : // reset the context
210 467 : m_data_type_checker = data::data_type_checker(pbesspec.data());
211 467 : m_variable_context.clear();
212 467 : m_pbes_context.clear();
213 467 : m_variable_context.add_context_variables(pbesspec.global_variables(), m_data_type_checker);
214 467 : m_pbes_context.add_propositional_variables(equation_variables(pbesspec.equations()), m_data_type_checker);
215 :
216 : // typecheck the equations
217 3330 : for (pbes_equation& eqn: pbesspec.equations())
218 : {
219 2863 : data::detail::variable_context variable_context = m_variable_context;
220 : try
221 : {
222 2863 : data::detail::check_duplicate_variable_names(eqn.variable().parameters(), "propositional variable parameter");
223 : }
224 0 : catch (mcrl2::runtime_error& e)
225 : {
226 0 : throw mcrl2::runtime_error(std::string(e.what()) + " while typechecking " + pbes_system::pp(eqn.variable()));
227 0 : }
228 2863 : variable_context.add_context_variables(eqn.variable().parameters(), m_data_type_checker);
229 2863 : pbes_expression formula;
230 2863 : detail::make_typecheck_builder(m_data_type_checker, variable_context, m_pbes_context).apply(formula, eqn.formula());
231 2863 : eqn.formula() = formula;
232 2863 : }
233 :
234 : // typecheck the initial state
235 467 : propositional_variable_instantiation initial_state;
236 467 : detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_pbes_context).apply(initial_state, pbesspec.initial_state());
237 467 : pbesspec.initial_state() = initial_state;
238 :
239 : // typecheck the data specification
240 467 : pbesspec.data() = m_data_type_checker.typechecked_data_specification();
241 467 : pbesspec.data().translate_user_notation();
242 467 : }
243 :
244 : /** \brief Type check a process expression.
245 : * Throws a mcrl2::runtime_error exception if the expression is not well typed.
246 : * \param[in] x A process expression that has not been type checked.
247 : * \return a process expression where all untyped identifiers have been replace by typed ones.
248 : **/
249 1 : pbes_expression operator()(const pbes_expression& x)
250 : {
251 1 : pbes_expression result;
252 1 : detail::make_typecheck_builder(m_data_type_checker, m_variable_context, m_pbes_context).
253 1 : apply(result,pbes_system::normalize_sorts(x, m_data_type_checker.typechecked_data_specification()));
254 1 : return result;
255 0 : }
256 :
257 : protected:
258 : pbes_expression typecheck(const pbes_expression& x, const data::variable_list& parameters)
259 : {
260 : data::detail::variable_context variable_context = m_variable_context;
261 : variable_context.add_context_variables(parameters, m_data_type_checker);
262 : pbes_expression result;
263 : detail::make_typecheck_builder(m_data_type_checker, variable_context, m_pbes_context).apply(result, x);
264 : return result;
265 : }
266 : };
267 :
268 : /** \brief Type check a parsed mCRL2 pbes specification.
269 : * Throws an exception if something went wrong.
270 : * \param[in] pbesspec A process specification that has not been type checked.
271 : * \post pbesspec is type checked.
272 : **/
273 :
274 : inline
275 467 : void typecheck_pbes(pbes& pbesspec)
276 : {
277 467 : pbes_type_checker type_checker;
278 : try
279 : {
280 467 : type_checker(pbesspec);
281 : }
282 0 : catch (mcrl2::runtime_error &e)
283 : {
284 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\nCould not type check " + pbes_system::pp(pbesspec));
285 0 : }
286 467 : }
287 :
288 : /** \brief Type check a parsed mCRL2 propositional variable.
289 : * Throws an exception if something went wrong.
290 : * \param[in] x A propositional variable.
291 : * \param[in] variables A sequence of data variables that may appear in x.
292 : * \param[in] dataspec A data specification.
293 : * \return the type checked expression
294 : **/
295 : template <typename VariableContainer>
296 2 : propositional_variable typecheck_propositional_variable(const propositional_variable& x,
297 : const VariableContainer& variables,
298 : const data::data_specification& dataspec = data::data_specification()
299 : )
300 : {
301 : // This function should be implemented using the PBES type checker, but it is not immediately clear how to do that.
302 : try
303 : {
304 2 : const data::variable_list& parameters = x.parameters();
305 2 : std::vector<data::variable> typed_parameters;
306 7 : for (const data::variable& parameter: parameters)
307 : {
308 3 : data::variable d = atermpp::down_cast<data::variable>(data::typecheck_data_expression(parameter, variables, dataspec));
309 3 : typed_parameters.push_back(d);
310 : }
311 6 : return propositional_variable(x.name(), data::variable_list(typed_parameters.begin(), typed_parameters.end()));
312 2 : }
313 0 : catch (mcrl2::runtime_error &e)
314 : {
315 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not type check " + pbes_system::pp(x));
316 : }
317 : }
318 :
319 : /** \brief Type check a parsed mCRL2 pbes expression.
320 : * Throws an exception if something went wrong.
321 : * \param[in] x A pbes expression.
322 : * \param[in] variables A sequence of data variables that may appear in x.
323 : * \param[in] propositional_variables A sequence of propositional variables that may appear in x.
324 : * \param[in] dataspec A data specification.
325 : * \return the type checked expression
326 : **/
327 : template <typename VariableContainer, typename PropositionalVariableContainer>
328 1 : pbes_expression typecheck_pbes_expression(pbes_expression& x,
329 : const VariableContainer& variables,
330 : const PropositionalVariableContainer& propositional_variables,
331 : const data::data_specification& dataspec = data::data_specification()
332 : )
333 : {
334 : try
335 : {
336 1 : pbes_type_checker type_checker(dataspec, variables, propositional_variables);
337 2 : return type_checker(x);
338 1 : }
339 0 : catch (mcrl2::runtime_error &e)
340 : {
341 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not type check " + pbes_system::pp(x));
342 : }
343 : }
344 :
345 : } // namespace pbes_system
346 :
347 : } // namespace mcrl2
348 :
349 : #endif // MCRL2_PBES_TYPECHECK_H
|