Line data Source code
1 : // Author(s): Jan Friso Groote
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/sort_specification.h
10 : /// \brief This file describes the a sort_specification,
11 : // which contains declared sorts and sort aliases.
12 :
13 : #ifndef MCRL2_DATA_SORT_SPECIFICATION_H
14 : #define MCRL2_DATA_SORT_SPECIFICATION_H
15 :
16 : #include "mcrl2/data/alias.h"
17 : #include "mcrl2/data/structured_sort.h"
18 :
19 : namespace mcrl2
20 : {
21 : namespace data
22 : {
23 :
24 : /// \cond INTERNAL_DOC
25 : namespace detail
26 : {
27 :
28 : template < typename Container, typename T >
29 : inline
30 16 : void remove(Container& container, const T& t)
31 : {
32 16 : typename Container::iterator i = std::find(container.begin(), container.end(), t);
33 16 : if(i != container.end())
34 : {
35 13 : container.erase(i);
36 : }
37 16 : }
38 :
39 : } // end namespace detail
40 : /// \endcond
41 :
42 : class sort_specification;
43 : sort_expression normalize_sorts(const sort_expression& x, const data::sort_specification& sortspec);
44 :
45 : class sort_specification
46 : {
47 : protected:
48 :
49 : /// \brief This boolean indicates whether the variables
50 : /// m_normalised_constructors, m_mappings, m_equations, m_normalised_sorts,
51 : /// m_normalised_aliases are up to date with respect to changes of this sort specification.
52 : mutable bool m_normalised_sorts_are_up_to_date;
53 :
54 : /// \brief The variable below indicates whether a surrounding
55 : /// data specification is up to data with respect to
56 : /// sort normalisation and available sorts. This is set to false if
57 : /// an alias or a new sort is added.
58 : mutable bool m_normalised_data_is_up_to_date;
59 :
60 : /// \brief The basic sorts and structured sorts in the specification.
61 : basic_sort_vector m_user_defined_sorts;
62 :
63 : /// \brief Set containing all the sorts, including the system defined ones.
64 : mutable std::set<sort_expression> m_normalised_sorts;
65 :
66 : /// \brief The sorts that occur are needed in this sort specification but are
67 : /// not explicitly defined as user defined sorts. An example is the sort Nat
68 : /// when declaring the use of a sort List(Nat).
69 : /// The normalised sorts, constructors, mappings and equations are complete
70 : /// with respect to these sorts.
71 : std::set< sort_expression > m_sorts_in_context;
72 :
73 : /// \brief The basic sorts and structured sorts in the specification.
74 : alias_vector m_user_defined_aliases;
75 :
76 : /// \brief Table containing how sorts should be mapped to normalised sorts.
77 : mutable std::map< sort_expression, sort_expression > m_normalised_aliases;
78 :
79 : public:
80 :
81 : /// \brief Default constructor
82 30779 : sort_specification()
83 30779 : : m_normalised_sorts_are_up_to_date(false),
84 30779 : m_normalised_data_is_up_to_date(false)
85 : {
86 30779 : add_predefined_basic_sorts();
87 30779 : }
88 :
89 73 : sort_specification(const basic_sort_vector& sorts, const alias_vector& aliases)
90 73 : : m_normalised_sorts_are_up_to_date(false),
91 73 : m_normalised_data_is_up_to_date(false)
92 : {
93 73 : add_predefined_basic_sorts();
94 :
95 76 : for(const basic_sort& sort: sorts)
96 : {
97 3 : add_sort(sort);
98 : }
99 130 : for(const alias& a: aliases)
100 : {
101 57 : add_alias(a);
102 : }
103 73 : }
104 :
105 :
106 : /// \brief Adds a sort to this specification
107 : /// \param[in] s A sort expression.
108 207 : void add_sort(const basic_sort& s)
109 : {
110 207 : if (std::find(m_user_defined_sorts.begin(),m_user_defined_sorts.end(),s)==m_user_defined_sorts.end())
111 : {
112 207 : m_user_defined_sorts.push_back(s);
113 207 : import_system_defined_sort(s);
114 207 : sorts_are_not_necessarily_normalised_anymore();
115 : }
116 207 : }
117 :
118 : /// \brief Adds a sort to this specification, and marks it as system
119 : /// defined
120 : ///
121 : /// \param[in] s A sort expression.
122 : /// \pre s does not yet occur in this specification.
123 : /// \post is_system_defined(s) = true
124 : /// \note this operation does not invalidate iterators of sorts_const_range
125 61704 : void add_system_defined_sort(const sort_expression& s)
126 : {
127 61704 : import_system_defined_sort(s);
128 61704 : }
129 :
130 : ///\brief Adds the sort s to the context sorts
131 : /// \param[in] s a sort expression. It is
132 : /// added to m_sorts_in_context. For this sort standard functions are generated
133 : /// automatically (if, <,<=,==,!=,>=,>) and if the sort is a standard sort,
134 : /// the necessary constructors, mappings and equations are added to the data type.
135 27275 : void add_context_sort(const sort_expression& s)
136 : {
137 27275 : import_system_defined_sort(s);
138 27275 : sorts_are_not_necessarily_normalised_anymore();
139 27275 : }
140 :
141 : ///\brief Adds the sorts in c to the context sorts
142 : /// \param[in] c a container of sort expressions. These are
143 : /// added to m_sorts_in_context. For these sorts standard functions are generated
144 : /// automatically (if, <,<=,==,!=,>=,>) and if the sorts are standard sorts,
145 : /// the necessary constructors, mappings and equations are added to the data type.
146 : template <typename Container>
147 4455 : void add_context_sorts(const Container& c, typename atermpp::enable_if_container<Container>::type* = nullptr)
148 : {
149 31548 : for(typename Container::const_iterator i=c.begin(); i!=c.end(); ++i)
150 : {
151 27093 : add_context_sort(*i);
152 : }
153 4455 : }
154 :
155 : /// \brief Removes sort from the user defined sorts in the specification.
156 : /// Note that this does not remove aliases for the sort, and it does not remove
157 : /// constructors, mappings and equations, and also keeps the sort as
158 : /// defined in the context.
159 : /// \param[in] s A sort expression.
160 : /// \post s does not occur in this specification.
161 2 : void remove_sort(const sort_expression& s)
162 : {
163 2 : detail::remove(m_user_defined_sorts,s);
164 2 : sorts_are_not_necessarily_normalised_anymore();
165 2 : }
166 :
167 : /// \brief Gets the normalised sort declarations including those that are system defined.
168 : /// This is the set with all sorts that occur in a data_specification, or that
169 : /// have been registered as sorts used in the context.
170 : ///
171 : /// \details The time complexity of this operation is constant, except when
172 : /// the data specification has been changed, in which case it can be that
173 : /// the sorts must be renormalised. This operation is linear in the size of
174 : /// the specification.
175 : /// \return The sort normalised using the aliases occurring in this specification,
176 : /// including the built in sorts such as Bool and Nat, and complex
177 : /// sorts that are used in the user defined aliases and sorts, but
178 : /// also that are registered as sorts used in the context of the specification.
179 : inline
180 14330 : const std::set<sort_expression>& sorts() const
181 : {
182 14330 : normalise_sort_specification_if_required();
183 14330 : return m_normalised_sorts;
184 : }
185 :
186 : /// \brief Return the user defined context sorts of the current specification.
187 : /// \details Time complexity is constant.
188 : /// \return The set with sorts used in the context.
189 186 : const std::set<sort_expression>& context_sorts() const
190 : {
191 186 : return m_sorts_in_context;
192 : }
193 :
194 : /// \brief Gets all sorts defined by a user (excluding the system defined sorts).
195 : ///
196 : /// \details The time complexity of this operation is constant.
197 : /// \return The user defined sort declaration.
198 : inline
199 33471 : const basic_sort_vector& user_defined_sorts() const
200 : {
201 33471 : return m_user_defined_sorts;
202 : }
203 :
204 : /// \brief Adds an alias (new name for a sort) to this specification
205 : /// \param[in] a an alias
206 2029 : void add_alias(const alias& a)
207 : {
208 2029 : if (std::find(m_user_defined_aliases.begin(),m_user_defined_aliases.end(),a)==m_user_defined_aliases.end())
209 : {
210 2025 : m_user_defined_aliases.push_back(a);
211 2025 : import_system_defined_sort(a.name());
212 2025 : import_system_defined_sort(a.reference());
213 2025 : sorts_are_not_necessarily_normalised_anymore();
214 : }
215 2029 : }
216 :
217 :
218 : /// \brief Removes a user defined //alias from specification.
219 : /// \details This also removes the defined sort of this alias from the set of user defined sorts.
220 : /// This routine does not check whether the alias, or name was in the user defined sets.
221 : void remove_alias(const alias& a)
222 : {
223 : detail::remove(m_user_defined_sorts, a.name());
224 : detail::remove(m_user_defined_aliases, a);
225 : sorts_are_not_necessarily_normalised_anymore();
226 : }
227 :
228 :
229 : /// \brief Gets the user defined aliases.
230 : /// \details The time complexity is constant.
231 : inline
232 46996 : const alias_vector& user_defined_aliases() const
233 : {
234 46996 : return m_user_defined_aliases;
235 : }
236 :
237 :
238 : /// \brief Gets a normalisation mapping that maps each sort to its unique normalised sort
239 : /// \details Sorts that are mapped to itself are not include in the mapping.
240 : /// This map is required in functions with the name normalize_sorts.
241 : /// When in a specification sort aliases are used, like sort A=B or
242 : /// sort Tree=struct leaf | node(Tree,Tree) then there are different representations
243 : /// for each sort. The normalisation mapping maps each sort to a unique representant.
244 : /// Moreover, it is this unique sort that it provides in internal mappings.
245 4767099 : const std::map< sort_expression, sort_expression >& sort_alias_map() const
246 : {
247 4767099 : normalise_sort_specification_if_required();
248 4767099 : return m_normalised_aliases;
249 : }
250 :
251 7 : bool operator==(const sort_specification& other) const
252 : {
253 7 : return m_user_defined_sorts==other.m_user_defined_sorts &&
254 14 : m_sorts_in_context == other.m_sorts_in_context &&
255 14 : m_user_defined_aliases==other.m_user_defined_aliases;
256 : }
257 :
258 : // Below are auxiliary functions for this class.
259 : protected:
260 111072 : void sorts_are_not_necessarily_normalised_anymore() const
261 : {
262 111072 : m_normalised_sorts_are_up_to_date=false;
263 111072 : data_is_not_necessarily_normalised_anymore();
264 111072 : }
265 :
266 122472 : void data_is_not_necessarily_normalised_anymore() const
267 : {
268 122472 : m_normalised_data_is_up_to_date=false;
269 122472 : }
270 :
271 4781429 : void normalise_sort_specification_if_required() const
272 : {
273 4781429 : if (!m_normalised_sorts_are_up_to_date)
274 : {
275 11400 : m_normalised_sorts_are_up_to_date=true;
276 11400 : m_normalised_sorts.clear();
277 11400 : reconstruct_m_normalised_aliases();
278 74837 : for (const sort_expression& s: m_sorts_in_context)
279 : {
280 63437 : m_normalised_sorts.insert(normalize_sorts(s,*this));
281 : }
282 11641 : for (const sort_expression& s: m_user_defined_sorts)
283 : {
284 241 : m_normalised_sorts.insert(normalize_sorts(s,*this));
285 : }
286 11400 : data_is_not_necessarily_normalised_anymore();
287 : }
288 4781429 : }
289 :
290 : void add_predefined_basic_sorts();
291 :
292 : template <class CONTAINER>
293 11506 : void import_system_defined_sorts(const CONTAINER& sorts)
294 : {
295 49794 : for(const sort_expression& sort: sorts)
296 : {
297 29002 : import_system_defined_sort(sort);
298 : }
299 11506 : }
300 :
301 : /// \brief Adds the system defined sorts in a sequence.
302 : /// The second argument is used to check which sorts are added, to prevent
303 : /// useless repetitions of additions of sorts.
304 : /// \details The function normalise_sorts imports for the given sort_expression sort all sorts, constructors,
305 : /// mappings and equations that belong to this sort to the `normalised' sets in this
306 : /// data type. E.g. for the sort Nat of natural numbers, it is required that Pos
307 : /// (positive numbers) are defined.
308 : void import_system_defined_sort(const sort_expression& sort);
309 :
310 : // The function below recalculates m_normalised_aliases, such that
311 : // it forms a confluent terminating rewriting system using which
312 : // sorts can be normalised.
313 : void reconstruct_m_normalised_aliases() const;
314 :
315 : // The function below checks whether there is an alias loop, e.g. aliases
316 : // of the form A=B; B=A; or more complex A=B->C; B=Set(D); D=List(A); Loops
317 : // through structured sorts are allowed. If a loop is detected, an exception
318 : // is thrown.
319 : void check_for_alias_loop(
320 : const sort_expression& s,
321 : std::set<sort_expression> sorts_already_seen,
322 : const bool toplevel=true) const;
323 :
324 :
325 : }
326 : ;
327 :
328 : } // namespace data
329 :
330 : } // namespace mcrl2
331 :
332 : #endif // MCRL2_DATA_SORT_SPECIFICATION_H
|
