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/expression_traits.h
10 : /// \brief Contains term traits for data_expression.
11 :
12 : #ifndef MCRL2_DATA_EXPRESSION_TRAITS_H
13 : #define MCRL2_DATA_EXPRESSION_TRAITS_H
14 :
15 : #include "mcrl2/core/term_traits.h"
16 : #include "mcrl2/data/bool.h"
17 : #include "mcrl2/data/exists.h"
18 : #include "mcrl2/data/forall.h"
19 :
20 : namespace mcrl2
21 : {
22 :
23 : namespace core
24 : {
25 :
26 : /// \brief Contains type information for data expressions.
27 : template <>
28 : struct term_traits<data::data_expression>
29 : {
30 : /// \brief The term type
31 : typedef data::data_expression term_type;
32 :
33 : /// \brief The variable type
34 : typedef data::variable variable_type;
35 :
36 : /// \brief The variable sequence type
37 : typedef data::variable_list variable_sequence_type;
38 :
39 : /// \brief The value true
40 : /// \return The value true
41 : static inline
42 58 : const term_type& true_()
43 : {
44 58 : return data::sort_bool::true_();
45 : }
46 :
47 : /// \brief The value false
48 : /// \return The value false
49 : static inline
50 17 : const term_type& false_()
51 : {
52 17 : return data::sort_bool::false_();
53 : }
54 :
55 : /// \brief Operator not
56 : /// \param p A term
57 : /// \return Operator not applied to p
58 : static inline
59 : term_type not_(const term_type& p)
60 : {
61 : return data::sort_bool::not_(p);
62 : }
63 :
64 : /// \brief Operator not
65 : /// \param result Operator not applied to p
66 : /// \param p A term
67 : static inline
68 20 : void make_not_(term_type& result, const term_type& p)
69 : {
70 20 : data::sort_bool::make_not_(result, p);
71 20 : }
72 :
73 : /// \brief Operator and
74 : /// \param p A term
75 : /// \param q A term
76 : /// \return Operator and applied to p and q
77 : static inline
78 23 : term_type and_(const term_type& p, const term_type& q)
79 : {
80 23 : return data::sort_bool::and_(p, q);
81 : }
82 :
83 : /// \brief Operator and
84 : /// \param result Operator and applied to p and q
85 : /// \param p A term
86 : /// \param q A term
87 : static inline
88 400 : void make_and_(term_type& result, const term_type& p, const term_type& q)
89 : {
90 400 : data::sort_bool::make_and_(result, p, q);
91 400 : }
92 :
93 : /// \brief Operator or
94 : /// \param p A term
95 : /// \param q A term
96 : /// \return Operator or applied to p and q
97 : static inline
98 19 : term_type or_(const term_type& p, const term_type& q)
99 : {
100 19 : return data::sort_bool::or_(p, q);
101 : }
102 :
103 : /// \brief Operator or
104 : /// \param result Operator or applied to p and q
105 : /// \param p A term
106 : /// \param q A term
107 : static inline
108 7 : void make_or_(term_type& result, const term_type& p, const term_type& q)
109 : {
110 7 : data::sort_bool::make_or_(result, p, q);
111 7 : }
112 :
113 : /// \brief Operator imp
114 : /// \param p A term
115 : /// \param q A term
116 : /// \return Operator or applied to p and q
117 : static inline
118 : term_type imp(const term_type& p, const term_type& q)
119 : {
120 : return data::sort_bool::implies(p, q);
121 : }
122 :
123 : /// \brief Operator imp
124 : /// \param result Operator and applied to p and q
125 : /// \param p A term
126 : /// \param q A term
127 : static inline
128 0 : void make_imp(term_type& result, const term_type& p, const term_type& q)
129 : {
130 0 : data::sort_bool::make_implies(result, p, q);
131 0 : }
132 :
133 : /// \brief Operator forall
134 : /// \param d A sequence of variables
135 : /// \param p A term
136 : /// \return Operator forall applied to d and p
137 : static inline
138 : term_type forall(const variable_sequence_type& d, const term_type& p)
139 : {
140 : return data::forall(d, p);
141 : }
142 :
143 : /// \brief Construct a forall.
144 : /// \param result Place where the forall is put.
145 : /// \param d A sequence of variables
146 : /// \param p A term
147 : static inline
148 5 : void make_forall(term_type& result, const variable_sequence_type& d, const term_type& p)
149 : {
150 5 : return data::make_forall(result, d, p);
151 : }
152 :
153 : /// \brief Operator exists
154 : /// \param d A sequence of variables
155 : /// \param p A term
156 : /// \return Operator exists applied to d and p
157 : static inline
158 5 : term_type exists(const variable_sequence_type& d, const term_type& p)
159 : {
160 5 : return data::exists(d, p);
161 : }
162 :
163 : /// \brief Construct an exists.
164 : /// \param result Place where the forall is put.
165 : /// \param d A sequence of variables
166 : /// \param p A term
167 : static inline
168 : void make_exists(term_type& result, const variable_sequence_type& d, const term_type& p)
169 : {
170 : return data::make_exists(result, d, p);
171 : }
172 :
173 : /// \brief Test for value true
174 : /// \param t A term
175 : /// \return True if the term has the value true
176 : static inline
177 1363 : bool is_true(const term_type& t)
178 : {
179 1363 : return t == data::sort_bool::true_();
180 : }
181 :
182 : /// \brief Test for value false
183 : /// \param t A term
184 : /// \return True if the term has the value false
185 : static inline
186 983 : bool is_false(const term_type& t)
187 : {
188 983 : return t == data::sort_bool::false_();
189 : }
190 :
191 : /// \brief Test for operator not
192 : /// \param t A term
193 : /// \return True if the term is of type not
194 : static inline
195 22 : bool is_not(const term_type& t)
196 : {
197 22 : return data::sort_bool::is_not_application(t);
198 : }
199 :
200 : /// \brief Test for operator and
201 : /// \param t A term
202 : /// \return True if the term is of type and
203 : static inline
204 86 : bool is_and(const term_type& t)
205 : {
206 86 : return data::sort_bool::is_and_application(t);
207 : }
208 :
209 : /// \brief Test for operator or
210 : /// \param t A term
211 : /// \return True if the term is of type or
212 : static inline
213 23 : bool is_or(const term_type& t)
214 : {
215 23 : return data::sort_bool::is_or_application(t);
216 : }
217 :
218 : /// \brief Test for implication
219 : /// \param t A term
220 : /// \return True if the term is an implication
221 : static inline
222 : bool is_imp(const term_type& t)
223 : {
224 : return data::sort_bool::is_implies_application(t);
225 : }
226 :
227 : /// \brief Test for universal quantification
228 : /// \param t A term
229 : /// \return True if the term is an universal quantification
230 : static inline
231 : bool is_forall(const term_type& t)
232 : {
233 : return data::is_forall(t);
234 : }
235 :
236 : /// \brief Test for existential quantification
237 : /// \param t A term
238 : /// \return True if the term is an existential quantification
239 : static inline
240 : bool is_exists(const term_type& t)
241 : {
242 : return data::is_exists(t);
243 : }
244 :
245 : /// \brief Test for lambda abstraction
246 : /// \param t A term
247 : /// \return True if the term is a lambda expression
248 : static inline
249 : bool is_lambda(const term_type& t)
250 : {
251 : return data::is_lambda(t);
252 : }
253 :
254 : /// \brief Conversion from variable to term
255 : /// \param v A variable
256 : /// \return The converted variable
257 : static inline
258 : const term_type& variable2term(const variable_type& v)
259 : {
260 : return v;
261 : }
262 :
263 : /// \brief Test if a term is a variable
264 : /// \param t A term
265 : /// \return True if the term is a variable
266 : static inline
267 : bool is_variable(const term_type& t)
268 : {
269 : return data::is_variable(t);
270 : }
271 :
272 : /// \brief Get the n-th argument of a data expression, provided it is an application.
273 : /// \param t A term which is an application.
274 : /// \param n The index of the argument. The first index has number 0.
275 : /// \return the n-th argument of t.
276 : /// \details This function is linear in n.
277 : static inline
278 : const term_type& argument(const term_type& t, const std::size_t n)
279 : {
280 : assert(data::is_application(t));
281 : const data::application& a=atermpp::down_cast<data::application>(t);
282 : assert(a.size()>n);
283 : data::application::const_iterator i=a.begin();
284 : for(std::size_t j=0; j<n; ++j, ++i)
285 : {
286 : assert(i!=a.end());
287 : }
288 : assert(i!=a.end());
289 : return *i;
290 : }
291 :
292 : static inline
293 33 : const term_type& left(const term_type& t)
294 : {
295 33 : assert(data::is_application(t));
296 33 : const data::application& a=atermpp::down_cast<data::application>(t);
297 33 : assert(a.size() == 2);
298 33 : return *(a.begin());
299 : }
300 :
301 : static inline
302 33 : const term_type& right(const term_type& t)
303 : {
304 33 : assert(data::is_application(t));
305 33 : const data::application& a=atermpp::down_cast<data::application>(t);
306 33 : assert(a.size() == 2);
307 33 : return *(++(a.begin()));
308 : }
309 :
310 : static inline
311 1 : const term_type& not_arg(const term_type& t)
312 : {
313 1 : assert(is_not(t));
314 1 : assert(data::is_application(t));
315 1 : const data::application& a=atermpp::down_cast<data::application>(t);
316 1 : assert(a.size() == 1);
317 1 : return *(a.begin());
318 : }
319 :
320 : /// \brief Pretty print function
321 : /// \param t A term
322 : /// \return A pretty print representation of the term
323 : static inline
324 : std::string pp(const term_type& t)
325 : {
326 : return data::pp(t);
327 : }
328 : };
329 :
330 : } // namespace core
331 :
332 : namespace data
333 : {
334 : /// \brief expression traits (currently nothing more than core::term_traits)
335 : template < typename Expression >
336 : struct expression_traits : public core::term_traits< Expression >
337 : {
338 : // Type of expression that represents variables
339 : typedef mcrl2::data::variable variable_type;
340 :
341 : static bool is_true(const data_expression& e)
342 : {
343 : return sort_bool::is_true_function_symbol(e);
344 : }
345 :
346 : static bool is_false(const data_expression& e)
347 : {
348 : return sort_bool::is_false_function_symbol(e);
349 : }
350 :
351 : static bool is_application(const data_expression& e)
352 : {
353 : return data::is_application(e);
354 : }
355 :
356 : static bool is_abstraction(const data_expression& e)
357 : {
358 : return data::is_abstraction(e);
359 : }
360 :
361 : static const data_expression& head(const data_expression& e)
362 : {
363 : return atermpp::down_cast<mcrl2::data::application>(e).head();
364 : }
365 :
366 : static const data_expression_list& variables(const data_expression& a)
367 : {
368 : return atermpp::container_cast<data_expression_list>(atermpp::down_cast<abstraction>(a).variables());
369 : }
370 :
371 : static const data_expression& body(const data_expression& a)
372 : {
373 : return atermpp::down_cast<const abstraction>(a).body();
374 : }
375 :
376 : static data_expression replace_body(const data_expression& variable_binder, const data_expression& new_body)
377 : {
378 : const abstraction& a=atermpp::down_cast<const abstraction>(variable_binder);
379 : return abstraction(a.binding_operator(), a.variables(), new_body);
380 : }
381 :
382 : template < typename Container >
383 : static application application(const data_expression& e, const Container& arguments)
384 : {
385 : return application(e, arguments);
386 : }
387 :
388 : static const data_expression& false_()
389 : {
390 : return sort_bool::false_();
391 : }
392 :
393 : static const data_expression& true_()
394 : {
395 : return sort_bool::true_();
396 : }
397 :
398 : static data_expression and_(const data_expression& e1, const data_expression& e2)
399 : {
400 : return sort_bool::and_(e1, e2);
401 : }
402 :
403 : static data_expression or_(const data_expression& e1, const data_expression& e2)
404 : {
405 : return sort_bool::or_(e1, e2);
406 : }
407 : };
408 :
409 : } // namespace data
410 :
411 : } // namespace mcrl2
412 :
413 : #endif // MCRL2_DATA_EXPRESSION_TRAITS_H
|
