Line data Source code
1 : // Author(s): Jeroen Keiren, Jeroen van der Wulp
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/structured_sort_constructor.h
10 : /// \brief The classes structured_sort_constructor.
11 :
12 : #ifndef MCRL2_DATA_STRUCTURED_SORT_CONSTRUCTOR_H
13 : #define MCRL2_DATA_STRUCTURED_SORT_CONSTRUCTOR_H
14 :
15 : #include "mcrl2/data/bool.h"
16 : #include "mcrl2/data/structured_sort_constructor_argument.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace data
22 : {
23 :
24 : class structured_sort;
25 :
26 : //--- start generated class structured_sort_constructor ---//
27 : /// \\brief A constructor for a structured sort
28 : class structured_sort_constructor: public atermpp::aterm_appl
29 : {
30 : public:
31 : /// \\brief Default constructor.
32 0 : structured_sort_constructor()
33 0 : : atermpp::aterm_appl(core::detail::default_values::StructCons)
34 0 : {}
35 :
36 : /// \\brief Constructor.
37 : /// \\param term A term
38 : explicit structured_sort_constructor(const atermpp::aterm& term)
39 : : atermpp::aterm_appl(term)
40 : {
41 : assert(core::detail::check_term_StructCons(*this));
42 : }
43 :
44 : /// \\brief Constructor.
45 847 : structured_sort_constructor(const core::identifier_string& name, const structured_sort_constructor_argument_list& arguments, core::identifier_string& recogniser)
46 847 : : atermpp::aterm_appl(core::detail::function_symbol_StructCons(), name, arguments, recogniser)
47 847 : {}
48 :
49 : /// \\brief Constructor.
50 : template <typename Container>
51 40970 : structured_sort_constructor(const std::string& name, const Container& arguments, const std::string& recogniser, typename atermpp::enable_if_container<Container, structured_sort_constructor_argument>::type* = nullptr)
52 40970 : : atermpp::aterm_appl(core::detail::function_symbol_StructCons(), core::identifier_string(name), structured_sort_constructor_argument_list(arguments.begin(), arguments.end()), core::identifier_string(recogniser))
53 40970 : {}
54 :
55 : /// Move semantics
56 664 : structured_sort_constructor(const structured_sort_constructor&) noexcept = default;
57 48081 : structured_sort_constructor(structured_sort_constructor&&) noexcept = default;
58 : structured_sort_constructor& operator=(const structured_sort_constructor&) noexcept = default;
59 : structured_sort_constructor& operator=(structured_sort_constructor&&) noexcept = default;
60 :
61 124364 : const core::identifier_string& name() const
62 : {
63 124364 : return atermpp::down_cast<core::identifier_string>((*this)[0]);
64 : }
65 :
66 152538 : const structured_sort_constructor_argument_list& arguments() const
67 : {
68 152538 : return atermpp::down_cast<structured_sort_constructor_argument_list>((*this)[1]);
69 : }
70 :
71 92088 : const core::identifier_string& recogniser() const
72 : {
73 92088 : return atermpp::down_cast<core::identifier_string>((*this)[2]);
74 : }
75 : //--- start user section structured_sort_constructor ---//
76 : friend class structured_sort;
77 :
78 : private:
79 :
80 : struct get_argument_sort
81 : {
82 : sort_expression operator()(structured_sort_constructor_argument const& s) const
83 : {
84 : return s.sort();
85 : }
86 : };
87 :
88 : protected:
89 : /// \brief Returns the sorts of the arguments in an output iterator.
90 : ///
91 : template <typename OutIter>
92 63176 : void argument_sorts(OutIter out) const
93 : {
94 142416 : for(const auto & i : arguments())
95 : {
96 16064 : *out++ = i.sort();
97 : }
98 63176 : }
99 :
100 : public:
101 : /// \brief Constructor
102 328 : structured_sort_constructor(const core::identifier_string& name, const core::identifier_string& recogniser)
103 328 : : atermpp::aterm_appl(core::detail::function_symbol_StructCons(), name, structured_sort_constructor_argument_list(), recogniser)
104 328 : {}
105 :
106 : /// \brief Constructor.
107 561 : structured_sort_constructor(const std::string& name, const std::string& recogniser)
108 561 : : atermpp::aterm_appl(core::detail::function_symbol_StructCons(), core::identifier_string(name), structured_sort_constructor_argument_list(), core::identifier_string(recogniser))
109 561 : {}
110 :
111 : /// \brief Constructor.
112 : template <typename Container>
113 : structured_sort_constructor(const std::string& name, const structured_sort_constructor_argument_list& arguments, typename atermpp::enable_if_container<Container, structured_sort_constructor_argument>::type* = 0)
114 : : atermpp::aterm_appl(core::detail::function_symbol_StructCons(), core::identifier_string(name), arguments, core::empty_identifier_string())
115 : {}
116 :
117 : /// \brief Constructor.
118 : template <typename Container>
119 341 : structured_sort_constructor(const std::string& name, const Container& arguments, typename atermpp::enable_if_container<Container, structured_sort_constructor_argument>::type* = nullptr)
120 341 : : atermpp::aterm_appl(core::detail::function_symbol_StructCons(), core::identifier_string(name), structured_sort_constructor_argument_list(arguments.begin(), arguments.end()), core::empty_identifier_string())
121 341 : {}
122 :
123 : /// \brief Constructor
124 : structured_sort_constructor(const core::identifier_string& name)
125 : : atermpp::aterm_appl(core::detail::function_symbol_StructCons(), name, structured_sort_constructor_argument_list(), core::empty_identifier_string())
126 : {}
127 :
128 : /// \brief Constructor.
129 6 : structured_sort_constructor(const std::string& name)
130 6 : : atermpp::aterm_appl(core::detail::function_symbol_StructCons(), core::identifier_string(name), structured_sort_constructor_argument_list(), core::empty_identifier_string())
131 6 : {}
132 :
133 : /// \brief Constructor
134 : ///
135 : /// \overload to work around problem that MSVC reinterprets char* or char[] as core::identifier_string
136 : template < typename Container, std::size_t S, std::size_t S0 >
137 3 : structured_sort_constructor(const char(&name)[S],
138 : const Container& arguments,
139 : const char(&recogniser)[S0],
140 : typename atermpp::enable_if_container< Container, structured_sort_constructor_argument >::type* = nullptr)
141 3 : : atermpp::aterm_appl(core::detail::function_symbol_StructCons(), core::identifier_string(name), structured_sort_constructor_argument_list(arguments.begin(), arguments.end()), core::identifier_string(recogniser))
142 3 : {}
143 :
144 : /// \brief Returns the constructor function for this constructor,
145 : /// assuming it is internally represented with sort s.
146 : /// \param s Sort expression this sort is internally represented as.
147 : ///
148 : /// In general, constructor_function is used with s the structured
149 : /// sort of which this constructor is a part.
150 : /// Consider for example struct c|d, be a structured sort, where
151 : /// this constructor is c, then this.constructor_function(struct c|d)
152 : /// returns the fuction symbol c : struct c|d, i.e. the function c of
153 : /// sort struct c|d.
154 63176 : function_symbol constructor_function(const sort_expression& s) const
155 : {
156 63176 : sort_expression_vector arguments;
157 63176 : std::back_insert_iterator<sort_expression_vector> inserter(arguments);
158 63176 : argument_sorts(inserter);
159 :
160 189528 : return function_symbol(name(), (arguments.empty()) ? s : function_sort(arguments, s));
161 63176 : }
162 :
163 : /// \brief Returns the projection functions for this constructor.
164 : /// \param s The sort as which the structured sort this constructor corresponds
165 : /// to is treated internally.
166 7377 : function_symbol_vector projection_functions(const sort_expression& s) const
167 : {
168 7377 : function_symbol_vector result;
169 10179 : for (const auto & i : arguments())
170 : {
171 2802 : if (i.name() != core::empty_identifier_string())
172 : {
173 2597 : result.push_back(function_symbol(i.name(), make_function_sort_(s, i.sort())));
174 : }
175 : }
176 7377 : return result;
177 0 : }
178 :
179 : /// \brief Returns the function corresponding to the recogniser of this
180 : /// constructor, such that it is usable in the rewriter.
181 : /// \param s The sort as which the structured sort this constructor
182 : /// corresponds to is treated internally.
183 2804 : function_symbol recogniser_function(const sort_expression& s) const
184 : {
185 5608 : return function_symbol(recogniser(), make_function_sort_(s, sort_bool::bool_()));
186 : }
187 : //--- end user section structured_sort_constructor ---//
188 : };
189 :
190 : /// \\brief Make_structured_sort_constructor constructs a new term into a given address.
191 : /// \\ \param t The reference into which the new structured_sort_constructor is constructed.
192 : template <class... ARGUMENTS>
193 17153 : inline void make_structured_sort_constructor(atermpp::aterm_appl& t, const ARGUMENTS&... args)
194 : {
195 17153 : atermpp::make_term_appl(t, core::detail::function_symbol_StructCons(), args...);
196 17153 : }
197 :
198 : /// \\brief list of structured_sort_constructors
199 : typedef atermpp::term_list<structured_sort_constructor> structured_sort_constructor_list;
200 :
201 : /// \\brief vector of structured_sort_constructors
202 : typedef std::vector<structured_sort_constructor> structured_sort_constructor_vector;
203 :
204 : /// \\brief Test for a structured_sort_constructor expression
205 : /// \\param x A term
206 : /// \\return True if \\a x is a structured_sort_constructor expression
207 : inline
208 : bool is_structured_sort_constructor(const atermpp::aterm_appl& x)
209 : {
210 : return x.function() == core::detail::function_symbols::StructCons;
211 : }
212 :
213 : // prototype declaration
214 : std::string pp(const structured_sort_constructor& x);
215 :
216 : /// \\brief Outputs the object to a stream
217 : /// \\param out An output stream
218 : /// \\param x Object x
219 : /// \\return The output stream
220 : inline
221 0 : std::ostream& operator<<(std::ostream& out, const structured_sort_constructor& x)
222 : {
223 0 : return out << data::pp(x);
224 : }
225 :
226 : /// \\brief swap overload
227 : inline void swap(structured_sort_constructor& t1, structured_sort_constructor& t2)
228 : {
229 : t1.swap(t2);
230 : }
231 : //--- end generated class structured_sort_constructor ---//
232 :
233 : // template function overloads
234 : std::string pp(const structured_sort_constructor_list& x);
235 : std::string pp(const structured_sort_constructor_vector& x);
236 :
237 : } // namespace data
238 :
239 : } // namespace mcrl2
240 :
241 : #endif // MCRL2_DATA_STRUCTURED_SORT_CONSTRUCTOR_H
|
