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/translate_user_notation.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_TRANSLATE_USER_NOTATION_H
13 : #define MCRL2_DATA_TRANSLATE_USER_NOTATION_H
14 :
15 : #include "mcrl2/data/builder.h"
16 : #include "mcrl2/data/standard_container_utility.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace data
22 : {
23 :
24 : namespace detail
25 : {
26 :
27 : template <typename Derived>
28 : class translate_user_notation_builder: public data_expression_builder<Derived>
29 : {
30 : public:
31 : typedef data_expression_builder<Derived> super;
32 :
33 : using super::enter;
34 : using super::leave;
35 : using super::apply;
36 : using super::update;
37 :
38 : inline
39 155638 : Derived& derived()
40 : {
41 155638 : return static_cast<Derived&>(*this);
42 : }
43 :
44 : template <class T>
45 254 : void apply(T& result, const abstraction& x)
46 : {
47 254 : const variable_list& bound_variables = x.variables();
48 :
49 254 : if (is_set_comprehension(x))
50 : {
51 17 : sort_expression element_sort(x.variables().begin()->sort());
52 17 : data_expression body;
53 17 : derived().apply(body, x.body());
54 17 : result = sort_set::constructor(element_sort, lambda(bound_variables, body),
55 : sort_fset::empty(element_sort));
56 17 : return;
57 17 : }
58 237 : else if (is_bag_comprehension(x))
59 : {
60 4 : sort_expression element_sort(x.variables().begin()->sort());
61 4 : data_expression body;
62 4 : derived().apply(body, x.body());
63 4 : result = sort_bag::constructor(element_sort, lambda(bound_variables, body),
64 : sort_fbag::empty(element_sort));
65 4 : return;
66 4 : }
67 233 : data_expression body;
68 233 : derived().apply(body, x.body());
69 233 : result = abstraction(x.binding_operator(), bound_variables, body);
70 233 : }
71 :
72 : template <class T>
73 32952 : void apply(T& result, const function_symbol& x)
74 : {
75 32952 : derived().enter(x);
76 32952 : result = x;
77 32952 : std::string name(x.name());
78 32952 : if (is_system_defined(x.sort()) && (name.find_first_not_of("-/0123456789") == std::string::npos)) // crude but efficient
79 : {
80 5378 : result = number(x.sort(), name);
81 : }
82 32952 : derived().leave(x);
83 32952 : }
84 :
85 : template <class T>
86 17570 : void apply(T& result, const application& x)
87 : {
88 17570 : derived().enter(x);
89 17570 : if (is_function_symbol(x.head()))
90 : {
91 15636 : function_symbol head(x.head());
92 :
93 15636 : if (head.name() == sort_list::list_enumeration_name())
94 : {
95 : // convert to snoc list
96 116 : sort_expression element_sort(*function_sort(head.sort()).domain().begin());
97 :
98 : // result = sort_list::list(element_sort, derived().apply(data_expression_list(x.begin(), x.end())));
99 116 : result = sort_list::list(element_sort,
100 232 : data_expression_list(
101 : x.begin(),
102 : x.end(),
103 242 : [&](const data_expression& t) { data_expression r; derived().apply(r, t); return r;} ));
104 116 : return;
105 116 : }
106 15520 : else if (head.name() == sort_set::set_enumeration_name())
107 : {
108 : // convert to finite set
109 193 : sort_expression element_sort(*function_sort(head.sort()).domain().begin());
110 193 : result = sort_fset::fset(element_sort,
111 386 : data_expression_list(
112 : x.begin(),
113 : x.end(),
114 289 : [&](const data_expression& t) { data_expression r; derived().apply(r, t); return r;} ));
115 193 : return;
116 193 : }
117 15327 : else if (head.name() == sort_bag::bag_enumeration_name())
118 : {
119 : // convert to finite bag
120 186 : sort_expression element_sort(*function_sort(head.sort()).domain().begin());
121 186 : result = sort_fbag::fbag(element_sort,
122 372 : data_expression_list(
123 : x.begin(),
124 : x.end(),
125 512 : [&](const data_expression& t) { data_expression r; derived().apply(r, t); return r;} ));
126 186 : return;
127 186 : }
128 15636 : }
129 :
130 17075 : make_application(result,
131 : x.head(),
132 : x.begin(),
133 : x.end(),
134 53792 : [&](data_expression& r, const data_expression& t){ return derived().apply(r, t); }
135 : );
136 17075 : derived().leave(x);
137 : }
138 : };
139 :
140 : struct translate_user_notation_function
141 : {
142 : using argument_type = data_expression;
143 : using result_type = data_expression;
144 :
145 22495 : data_expression operator()(const data_expression& x) const
146 : {
147 22495 : data_expression result;
148 22495 : core::make_apply_builder<translate_user_notation_builder>().apply(result, x);
149 22495 : return result;
150 0 : }
151 : };
152 :
153 : } // namespace detail
154 :
155 : template <typename T>
156 : void translate_user_notation(T& x,
157 : typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type* = 0
158 : )
159 : {
160 : core::make_update_apply_builder<data::data_expression_builder>(detail::translate_user_notation_function()).update(x);
161 : }
162 :
163 : template <typename T>
164 4489 : T translate_user_notation(const T& x,
165 : typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
166 : )
167 : {
168 4489 : T result;
169 4489 : core::make_update_apply_builder<data::data_expression_builder>(detail::translate_user_notation_function()).apply(result, x);
170 4489 : return result;
171 0 : }
172 :
173 : namespace detail
174 : {
175 : // added to avoid circular header problems in data_specification.h
176 : inline
177 : data_equation translate_user_notation_data_equation(const data_equation& x)
178 : {
179 : return translate_user_notation(x);
180 : }
181 : } // namespace detail
182 :
183 : } // namespace data
184 :
185 : } // namespace mcrl2
186 :
187 : #endif // MCRL2_DATA_TRANSLATE_USER_NOTATION_H
|
