mCRL2
Loading...
Searching...
No Matches
data.cpp
Go to the documentation of this file.
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//
11
14#include "mcrl2/data/print.h"
17
18namespace mcrl2
19{
20
21namespace data
22{
23
24//--- start generated data overloads ---//
25std::string pp(const data::sort_expression_list& x) { return data::pp< data::sort_expression_list >(x); }
26std::string pp(const data::sort_expression_vector& x) { return data::pp< data::sort_expression_vector >(x); }
27std::string pp(const data::data_expression_list& x) { return data::pp< data::data_expression_list >(x); }
28std::string pp(const data::data_expression_vector& x) { return data::pp< data::data_expression_vector >(x); }
29std::string pp(const data::assignment_list& x) { return data::pp< data::assignment_list >(x); }
30std::string pp(const data::assignment_vector& x) { return data::pp< data::assignment_vector >(x); }
31std::string pp(const data::variable_list& x) { return data::pp< data::variable_list >(x); }
32std::string pp(const data::variable_vector& x) { return data::pp< data::variable_vector >(x); }
33std::string pp(const data::function_symbol_list& x) { return data::pp< data::function_symbol_list >(x); }
34std::string pp(const data::function_symbol_vector& x) { return data::pp< data::function_symbol_vector >(x); }
35std::string pp(const data::structured_sort_constructor_list& x) { return data::pp< data::structured_sort_constructor_list >(x); }
36std::string pp(const data::structured_sort_constructor_vector& x) { return data::pp< data::structured_sort_constructor_vector >(x); }
37std::string pp(const data::data_equation_list& x) { return data::pp< data::data_equation_list >(x); }
38std::string pp(const data::data_equation_vector& x) { return data::pp< data::data_equation_vector >(x); }
39std::string pp(const data::abstraction& x) { return data::pp< data::abstraction >(x); }
40std::string pp(const data::alias& x) { return data::pp< data::alias >(x); }
41std::string pp(const data::application& x) { return data::pp< data::application >(x); }
42std::string pp(const data::assignment& x) { return data::pp< data::assignment >(x); }
43std::string pp(const data::assignment_expression& x) { return data::pp< data::assignment_expression >(x); }
44std::string pp(const data::bag_comprehension& x) { return data::pp< data::bag_comprehension >(x); }
45std::string pp(const data::bag_comprehension_binder& x) { return data::pp< data::bag_comprehension_binder >(x); }
46std::string pp(const data::bag_container& x) { return data::pp< data::bag_container >(x); }
47std::string pp(const data::basic_sort& x) { return data::pp< data::basic_sort >(x); }
48std::string pp(const data::binder_type& x) { return data::pp< data::binder_type >(x); }
49std::string pp(const data::container_sort& x) { return data::pp< data::container_sort >(x); }
50std::string pp(const data::container_type& x) { return data::pp< data::container_type >(x); }
51std::string pp(const data::data_equation& x) { return data::pp< data::data_equation >(x); }
52std::string pp(const data::data_expression& x) { return data::pp< data::data_expression >(x); }
53std::string pp(const data::data_specification& x) { return data::pp< data::data_specification >(x); }
54std::string pp(const data::exists& x) { return data::pp< data::exists >(x); }
55std::string pp(const data::exists_binder& x) { return data::pp< data::exists_binder >(x); }
56std::string pp(const data::fbag_container& x) { return data::pp< data::fbag_container >(x); }
57std::string pp(const data::forall& x) { return data::pp< data::forall >(x); }
58std::string pp(const data::forall_binder& x) { return data::pp< data::forall_binder >(x); }
59std::string pp(const data::fset_container& x) { return data::pp< data::fset_container >(x); }
60std::string pp(const data::function_sort& x) { return data::pp< data::function_sort >(x); }
61std::string pp(const data::function_symbol& x) { return data::pp< data::function_symbol >(x); }
62std::string pp(const data::lambda& x) { return data::pp< data::lambda >(x); }
63std::string pp(const data::lambda_binder& x) { return data::pp< data::lambda_binder >(x); }
64std::string pp(const data::list_container& x) { return data::pp< data::list_container >(x); }
65std::string pp(const data::set_comprehension& x) { return data::pp< data::set_comprehension >(x); }
66std::string pp(const data::set_comprehension_binder& x) { return data::pp< data::set_comprehension_binder >(x); }
67std::string pp(const data::set_container& x) { return data::pp< data::set_container >(x); }
68std::string pp(const data::sort_expression& x) { return data::pp< data::sort_expression >(x); }
69std::string pp(const data::structured_sort& x) { return data::pp< data::structured_sort >(x); }
70std::string pp(const data::structured_sort_constructor& x) { return data::pp< data::structured_sort_constructor >(x); }
71std::string pp(const data::structured_sort_constructor_argument& x) { return data::pp< data::structured_sort_constructor_argument >(x); }
72std::string pp(const data::untyped_data_parameter& x) { return data::pp< data::untyped_data_parameter >(x); }
73std::string pp(const data::untyped_identifier& x) { return data::pp< data::untyped_identifier >(x); }
74std::string pp(const data::untyped_identifier_assignment& x) { return data::pp< data::untyped_identifier_assignment >(x); }
75std::string pp(const data::untyped_possible_sorts& x) { return data::pp< data::untyped_possible_sorts >(x); }
76std::string pp(const data::untyped_set_or_bag_comprehension& x) { return data::pp< data::untyped_set_or_bag_comprehension >(x); }
77std::string pp(const data::untyped_set_or_bag_comprehension_binder& x) { return data::pp< data::untyped_set_or_bag_comprehension_binder >(x); }
78std::string pp(const data::untyped_sort& x) { return data::pp< data::untyped_sort >(x); }
79std::string pp(const data::untyped_sort_variable& x) { return data::pp< data::untyped_sort_variable >(x); }
80std::string pp(const data::variable& x) { return data::pp< data::variable >(x); }
81std::string pp(const data::where_clause& x) { return data::pp< data::where_clause >(x); }
82data::data_equation normalize_sorts(const data::data_equation& x, const data::sort_specification& sortspec) { return data::normalize_sorts< data::data_equation >(x, sortspec); }
83data::data_equation_list normalize_sorts(const data::data_equation_list& x, const data::sort_specification& sortspec) { return data::normalize_sorts< data::data_equation_list >(x, sortspec); }
84void normalize_sorts(data::data_equation_vector& x, const data::sort_specification& sortspec) { data::normalize_sorts< data::data_equation_vector >(x, sortspec); }
85data::data_expression normalize_sorts(const data::data_expression& x, const data::sort_specification& sortspec) { return data::normalize_sorts< data::data_expression >(x, sortspec); }
86data::sort_expression normalize_sorts(const data::sort_expression& x, const data::sort_specification& sortspec) { return data::normalize_sorts< data::sort_expression >(x, sortspec); }
87data::variable_list normalize_sorts(const data::variable_list& x, const data::sort_specification& sortspec) { return data::normalize_sorts< data::variable_list >(x, sortspec); }
88data::data_expression translate_user_notation(const data::data_expression& x) { return data::translate_user_notation< data::data_expression >(x); }
89data::data_equation translate_user_notation(const data::data_equation& x) { return data::translate_user_notation< data::data_equation >(x); }
90std::set<data::sort_expression> find_sort_expressions(const data::data_equation& x) { return data::find_sort_expressions< data::data_equation >(x); }
91std::set<data::sort_expression> find_sort_expressions(const data::data_expression& x) { return data::find_sort_expressions< data::data_expression >(x); }
92std::set<data::sort_expression> find_sort_expressions(const data::sort_expression& x) { return data::find_sort_expressions< data::sort_expression >(x); }
93std::set<data::variable> find_all_variables(const data::data_expression& x) { return data::find_all_variables< data::data_expression >(x); }
94std::set<data::variable> find_all_variables(const data::data_expression_list& x) { return data::find_all_variables< data::data_expression_list >(x); }
95std::set<data::variable> find_all_variables(const data::function_symbol& x) { return data::find_all_variables< data::function_symbol >(x); }
96std::set<data::variable> find_all_variables(const data::variable& x) { return data::find_all_variables< data::variable >(x); }
97std::set<data::variable> find_all_variables(const data::variable_list& x) { return data::find_all_variables< data::variable_list >(x); }
98std::set<data::variable> find_free_variables(const data::data_expression& x) { return data::find_free_variables< data::data_expression >(x); }
99std::set<data::variable> find_free_variables(const data::data_expression_list& x) { return data::find_free_variables< data::data_expression_list >(x); }
100std::set<data::function_symbol> find_function_symbols(const data::data_equation& x) { return data::find_function_symbols< data::data_equation >(x); }
101std::set<core::identifier_string> find_identifiers(const data::variable_list& x) { return data::find_identifiers< data::variable_list >(x); }
102bool search_variable(const data::data_expression& x, const data::variable& v) { return data::search_variable< data::data_expression >(x, v); }
103//--- end generated data overloads ---//
104
105std::string pp(const std::set<variable>& x) { return data::pp< std::set<variable> >(x); }
106
108{
109 using namespace atermpp;
110 // This implementation is currently done in this class, because there
111 // is no elegant solution of distributing the implementation of the
112 // derived classes (as we need to support requesting the sort of a
113 // data_expression we do need to provide an implementation here).
114 if (is_variable(*this))
115 {
116 const auto& v = atermpp::down_cast<variable>(*this);
117 return v.sort();
118 }
119 else if (is_function_symbol(*this))
120 {
121 const auto& f = atermpp::down_cast<function_symbol>(*this);
122 return f.sort();
123 }
124 else if (is_abstraction(*this))
125 {
126 if (is_forall(*this) || is_exists(*this))
127 {
128 return sort_bool::bool_();
129 }
130 else if (is_lambda(*this))
131 {
132 const auto& v_variables = atermpp::down_cast<atermpp::term_list<aterm_appl> >((*this)[1]);
134 for (const auto & v_variable : v_variables)
135 {
136 s.push_back(down_cast<sort_expression>(v_variable[1])); // Push the sort.
137 }
138 return function_sort(sort_expression_list(s.begin(),s.end()), atermpp::down_cast<data_expression>((*this)[2]).sort());
139 }
140 else
141 {
143 const auto& v_variables = atermpp::down_cast<atermpp::term_list<aterm_appl> >((*this)[1]);
144 assert(v_variables.size() == 1);
145
146 if (is_bag_comprehension(*this))
147 {
148 return container_sort(bag_container(), atermpp::down_cast<const sort_expression>(v_variables.front()[1]));
149 }
150 else // If it is not known whether the term is a set or a bag, it returns the type of a set, as there is
151 // no setbag type. This can only occur for terms that are not propertly type checked.
152 {
153 return container_sort(set_container(), atermpp::down_cast<sort_expression>(v_variables.front()[1]));
154 }
155 }
156 }
157 else if (is_where_clause(*this))
158 {
159 return atermpp::down_cast<data_expression>((*this)[0]).sort();
160 }
161 else if (is_untyped_identifier(*this))
162 {
163 return untyped_sort();
164 }
165
166 assert(is_application(*this));
167 const auto& head = atermpp::down_cast<const data_expression>((*this)[0]);
168 sort_expression s(head.sort());
169 if (is_function_sort(s))
170 {
171 const auto& fs = atermpp::down_cast<function_sort>(s);
172 assert(fs.domain().size()+1==this->size());
173 return (fs.codomain());
174 }
175 return s;
176}
177
179{
180 std::set<data::variable> result;
181 for (const auto& i: sigma)
182 {
183 data::find_free_variables(i.second, std::inserter(result, result.end()));
184 }
185 return result;
186}
187
189{
190 std::set<variable> v = find_free_variables(x);
191 return variable_list(v.begin(), v.end());
192}
193
194namespace detail {
195
197{
199 unsigned int start_symbol_index = p.start_symbol_index("SortExpr");
200 bool partial_parses = false;
201 core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
203 return result;
204}
205
206variable_list parse_variables(const std::string& text)
207{
209 unsigned int start_symbol_index = p.start_symbol_index("VarSpec");
210 bool partial_parses = false;
211 std::string var_text("var " + text);
212 core::parse_node node = p.parse(var_text, start_symbol_index, partial_parses);
214 return result;
215}
216
218{
220 unsigned int start_symbol_index = p.start_symbol_index("DataExpr");
221 bool partial_parses = false;
222 core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
223 core::warn_and_or(node);
225 return result;
226}
227
229{
231 unsigned int start_symbol_index = p.start_symbol_index("DataSpec");
232 bool partial_parses = false;
233 core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
235 data_specification result = untyped_dataspec.construct_data_specification();
236 return result;
237}
238
240{
242 unsigned int start_symbol_index = p.start_symbol_index("VarsDeclList");
243 bool partial_parses = false;
244 core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
246 return result;
247}
248
249} // namespace detail
250
251std::pair<basic_sort_vector, alias_vector> parse_sort_specification(const std::string& text)
252{
254 unsigned int start_symbol_index = p.start_symbol_index("SortSpec");
255 bool partial_parses = false;
256 core::parse_node node = p.parse(text, start_symbol_index, partial_parses);
257 std::vector<atermpp::aterm_appl> elements = detail::data_specification_actions(p).parse_SortSpec(node);
258 basic_sort_vector sorts;
259 alias_vector aliases;
260 for (const atermpp::aterm_appl& x: elements)
261 {
262 if (is_basic_sort(x))
263 {
264 sorts.push_back(atermpp::down_cast<basic_sort>(x));
265 }
266 else if (is_alias(x))
267 {
268 aliases.push_back(atermpp::down_cast<alias>(x));
269 }
270 }
271 auto result = std::make_pair(sorts, aliases);
272 return result;
273}
274
275} // namespace data
276
277} // namespace mcrl2
278
A list of aterm objects.
Definition aterm_list.h:23
An abstraction expression.
Definition abstraction.h:26
\brief A sort alias
Definition alias.h:26
An application of a data expression to a number of arguments.
\brief Assignment expression
Definition assignment.h:27
\brief Assignment of a data expression to a variable
Definition assignment.h:91
\brief Binder for bag comprehension
universal quantification.
\brief Container type for bags
\brief A basic sort
Definition basic_sort.h:26
\brief A container sort
\brief Container type
\brief A data equation
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:107
\brief Binder for existential quantification
existential quantification.
Definition exists.h:26
\brief Container type for finite bags
\brief Binder for universal quantification
universal quantification.
Definition forall.h:26
\brief Container type for finite sets
\brief A function sort
\brief A function symbol
const sort_expression & sort() const
\brief Binder for lambda abstraction
function symbol.
Definition lambda.h:27
\brief Container type for lists
Generic substitution function. The substitution is stored as a mapping of variables to expressions....
\brief Binder for set comprehension
universal quantification.
\brief Container type for sets
\brief A sort expression
\brief An argument of a constructor of a structured sort
\brief A constructor for a structured sort
\brief Assignment of a data expression to a string
Definition assignment.h:182
\brief An untyped identifier
\brief Binder for untyped set or bag comprehension
Definition binder_type.h:77
\brief Unknown sort expression
\brief A data variable
Definition variable.h:28
\brief A where expression
D_ParserTables parser_tables_mcrl2
add your file description here.
add your file description here.
Provides utilities for pretty printing.
add your file description here.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
add your file description here.
The main namespace for the aterm++ library.
Definition algorithm.h:21
void syntax_error_fn(struct D_Parser *ap)
Custom syntax error function that prints both the line number and the column.
Definition dparser.cpp:463
struct D_ParseNode * ambiguity_fn(struct D_Parser *, int, struct D_ParseNode **)
Function for resolving ambiguities in the '_ -> _ <> _' operator for process expressions.
Definition dparser.cpp:332
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
data_expression parse_data_expression(const std::string &text)
Definition data.cpp:217
data_specification parse_data_specification_new(const std::string &text)
Definition data.cpp:228
variable_list parse_variable_declaration_list(const std::string &text)
Definition data.cpp:239
variable_list parse_variables(const std::string &text)
Definition data.cpp:206
sort_expression parse_sort_expression(const std::string &text)
Definition data.cpp:196
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
std::vector< assignment > assignment_vector
\brief vector of assignments
Definition assignment.h:149
bool is_untyped_identifier(const atermpp::aterm_appl &x)
Returns true if the term t is an identifier.
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:359
variable_list free_variables(const data_expression &x)
Definition data.cpp:188
bool is_lambda(const atermpp::aterm_appl &x)
Returns true if the term t is a lambda abstraction.
bool is_alias(const atermpp::aterm_appl &x)
Definition alias.h:81
bool is_exists(const atermpp::aterm_appl &x)
Returns true if the term t is an existential quantification.
std::vector< sort_expression > sort_expression_vector
\brief vector of sort_expressions
bool is_where_clause(const atermpp::aterm_appl &x)
Returns true if the term t is a where clause.
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:89
std::vector< alias > alias_vector
\brief vector of aliass
Definition alias.h:75
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm_appl &x)
Returns true if the term t is a set/bag comprehension.
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:93
bool is_function_symbol(const atermpp::aterm_appl &x)
Returns true if the term t is a function symbol.
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
std::set< data::variable > substitution_variables(const Substitution &)
Returns the variables appearing in the right hand sides of the substitution.
Definition replace.h:161
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
std::vector< variable > variable_vector
\brief vector of variables
Definition variable.h:89
atermpp::term_list< sort_expression > sort_expression_list
\brief list of sort_expressions
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
std::string pp(const abstraction &x)
Definition data.cpp:39
bool is_set_comprehension(const atermpp::aterm_appl &x)
Returns true if the term t is a set comprehension.
bool is_application(const atermpp::aterm_appl &x)
Returns true if the term t is an application.
std::vector< structured_sort_constructor > structured_sort_constructor_vector
\brief vector of structured_sort_constructors
bool is_forall(const atermpp::aterm_appl &x)
Returns true if the term t is a universal quantification.
bool is_basic_sort(const atermpp::aterm_appl &x)
Returns true if the term t is a basic sort.
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
Definition data.cpp:90
std::set< data::function_symbol > find_function_symbols(const data::data_equation &x)
Definition data.cpp:100
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:98
bool is_bag_comprehension(const atermpp::aterm_appl &x)
Returns true if the term t is a bag comprehension.
atermpp::term_list< variable > variable_list
\brief list of variables
std::pair< basic_sort_vector, alias_vector > parse_sort_specification(const std::string &text)
Definition data.cpp:251
bool is_function_sort(const atermpp::aterm_appl &x)
Returns true if the term t is a function sort.
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:85
std::vector< basic_sort > basic_sort_vector
vector of basic sorts
Definition basic_sort.h:94
bool search_variable(const data::data_expression &x, const data::variable &v)
Definition data.cpp:102
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Wrapper for D_ParseNode.
Definition dparser.h:86
Wrapper for D_Parser and its corresponding D_ParserTables.
Definition dparser.h:148
parse_node parse(const std::string &text, unsigned int start_symbol_index=0, bool partial_parses=false)
Parses a string. N.B. The user is responsible for destruction of the returned value by calling destro...
Definition dparser.cpp:209
unsigned int start_symbol_index(const std::string &name) const
Definition dparser.cpp:204
data::variable_list parse_VarsDeclList(const core::parse_node &node) const
Definition parse_impl.h:204
data::data_expression parse_DataExpr(const core::parse_node &node) const
Definition parse_impl.h:211
std::vector< atermpp::aterm_appl > parse_SortSpec(const core::parse_node &node) const
Definition parse_impl.h:336
data::variable_list parse_VarSpec(const core::parse_node &node) const
Definition parse_impl.h:378
untyped_data_specification parse_DataSpec(const core::parse_node &node) const
Definition parse_impl.h:461
data::sort_expression parse_SortExpr(const core::parse_node &node, data::sort_expression_list *product=nullptr) const
Definition parse_impl.h:35