mCRL2
Loading...
Searching...
No Matches
parse.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink, Jeroen Keiren, 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//
11
12#ifndef MCRL2_DATA_PARSE_H
13#define MCRL2_DATA_PARSE_H
14
16
17namespace mcrl2
18{
19
20namespace data
21{
22
23namespace detail {
24
25sort_expression parse_sort_expression(const std::string& text);
26variable_list parse_variables(const std::string& text);
27data_expression parse_data_expression(const std::string& text);
28data_specification parse_data_specification_new(const std::string& text);
29variable_list parse_variable_declaration_list(const std::string& text);
30
32{
33 static data_specification specification;
34 return specification;
35}
36
37} // namespace detail
38
39std::pair<basic_sort_vector, alias_vector> parse_sort_specification(const std::string& text);
40
61inline
63{
64 std::string text = utilities::read_text(in);
68 return result;
69}
70
78inline
80{
81 // handle empty data specification
82 if (utilities::trim_copy(text).empty())
83 {
84 return data_specification();
85 }
86 std::istringstream spec_stream(text);
87 return parse_data_specification(spec_stream);
88}
89
112
113template <typename OutputIterator, typename VariableIterator>
114void parse_variables(std::istream& in,
115 OutputIterator o,
116 VariableIterator begin,
117 VariableIterator end,
119{
120 std::string text = utilities::read_text(in);
121 utilities::trim(text);
122 variable_list data_vars;
123
124 if (!text.empty())
125 {
126 data_vars = detail::parse_variables(text);
128 // Check the variable in an empty variable context.
130
131 // Undo sort renamings for compatibility with type checker
132 // data_vars = data::detail::undo_compatibility_renamings(data_spec, data_vars);
133 data_vars = atermpp::reverse(data_vars);
134 data_vars = normalize_sorts(data_vars, data_spec);
135
136 // Check that variables do not have equal names.
137 for (const variable& v: data_vars)
138 {
139 for (VariableIterator i = begin; i != end; ++i)
140 {
141 if (v.name()==i->name())
142 {
143 throw mcrl2::runtime_error("Name conflict of variables " + data::pp(*i) + " and " + data::pp(v) + ".");
144 }
145 }
146 for (const variable& v1: data_vars)
147 {
148 if ((v1 != v) && (v1.name() == v.name()))
149 {
150 throw mcrl2::runtime_error("Name conflict of variables " + data::pp(v1) + " and " + data::pp(v) + ".");
151 }
152 }
153 }
154 }
155
156 // Output the variables read via the Output iterator.
157 std::copy(data_vars.begin(), data_vars.end(), o);
158}
159
169
170template <typename OutputIterator, typename VariableIterator>
171void parse_variables(const std::string& text,
172 OutputIterator i,
173 VariableIterator begin,
174 VariableIterator end,
176{
177 std::istringstream spec_stream(text);
178 parse_variables(spec_stream, i, begin, end, data_spec);
179}
180
186
187template <typename OutputIterator>
188void parse_variables(std::istream& text,
189 OutputIterator i,
191{
192 variable_list v_list;
193 parse_variables(text,i,v_list.begin(),v_list.end(),data_spec);
194}
195
201
202template <typename OutputIterator>
203void parse_variables(const std::string& text,
204 OutputIterator i,
206{
207 variable_list v_list;
208 parse_variables(text, i, v_list.begin(), v_list.end(), data_spec);
209}
210
217inline
218variable parse_variable(const std::string& text,
220{
221 std::vector<variable> v;
222
223 parse_variables(text + ";", std::back_inserter(v),data_spec);
224
225 if (v.empty())
226 {
227 throw mcrl2::runtime_error("Input does not contain a variable declaration.");
228 }
229 if (v.size() > 1)
230 {
231 throw mcrl2::runtime_error("Input contains more than one variable declaration.");
232 }
233
234 return v.front();
235}
236
249inline
250variable parse_variable(std::istream& text,
252{
253 std::ostringstream input;
254 input << text.rdbuf();
255 return parse_variable(input.str(),data_spec);
256}
257
275template <typename VariableContainer>
277 const VariableContainer& variables,
279 bool type_check = true,
280 bool translate_user_notation = true,
281 bool normalize_sorts = true
282 )
283{
284 std::string text = utilities::read_text(in);
286 if (type_check)
287 {
288 x = data::typecheck_data_expression(x, variables, dataspec);
289 }
291 {
293 }
294 if (normalize_sorts)
295 {
296 x = data::normalize_sorts(x, dataspec);
297 }
298 return x;
299}
300
311template <typename VariableContainer>
313 const VariableContainer& variables,
315 bool type_check = true,
316 bool translate_user_notation = true,
317 bool normalize_sorts = true
318 )
319{
320 std::istringstream spec_stream(text);
321 return parse_data_expression(spec_stream, variables, data_spec, type_check, translate_user_notation, normalize_sorts);
322}
323
333inline
336 bool type_check = true,
337 bool translate_user_notation = true,
338 bool normalize_sorts = true
339 )
340{
341 return parse_data_expression(text, variable_list(), data_spec, type_check, translate_user_notation, normalize_sorts);
342}
343
353inline
356 bool type_check = true,
357 bool translate_user_notation = true,
358 bool normalize_sorts = true
359 )
360{
361 return parse_data_expression(text, variable_list(), data_spec, type_check, translate_user_notation, normalize_sorts);
362}
363
364inline
365variable_list parse_variables(const std::string& text)
366{
367 std::vector<variable> result;
368 if (!text.empty())
369 {
370 parse_variables(text, std::back_inserter(result));
371 }
372 return variable_list(result.begin(), result.end());
373}
374
379inline
382{
383 std::string text = utilities::read_text(in);
385 typecheck_sort_expression(x, data_spec);
386 x = normalize_sorts(x, data_spec);
387 return x;
388}
389
398inline
401{
402 std::istringstream spec_stream(text);
403 return parse_sort_expression(spec_stream, data_spec);
404}
405
406// parse a string like 'tail: List(D) -> List(D)'
407//
408// TODO: replace this by a proper parse function once the current parser and type checker have been replaced
409inline
410data::function_symbol parse_function_symbol(const std::string& text, const std::string& dataspec_text = "")
411{
412 const std::string prefix = "UNIQUE_FUNCTION_SYMBOL_PREFIX";
413 std::string s = utilities::trim_copy(text);
414 std::string::size_type pos = s.find_first_of(':');
415 std::string name = utilities::trim_copy(s.substr(0, pos));
416 std::string type = prefix + s.substr(pos);
417 std::string spec_text = dataspec_text + "\nmap " + prefix + type + ";\n";
419 data::function_symbol f = dataspec.user_defined_mappings().back();
421 return result;
422}
423
428inline
430{
432 variables = normalize_sorts(variables, dataspec);
433 return variables;
434}
435
437namespace detail
438{
439
445inline
446std::pair<std::string, data_expression_list> parse_variable(std::string const& text)
447{
448 std::string name;
449 data_expression_vector variables;
450
451 std::string::size_type idx = text.find('(');
452 if (idx == std::string::npos)
453 {
454 name = text;
455 }
456 else
457 {
458 name = text.substr(0, idx);
459 assert(*text.rbegin() == ')');
460 std::string w = text.substr(idx + 1, text.size() - idx - 2);
461 std::vector<std::string> v = utilities::split(w, ",");
462 for (const std::string& s: v)
463 {
464 variables.push_back(data::parse_variable(s));
465 }
466 }
467 return std::make_pair(name, data_expression_list(variables.begin(), variables.end()));
468}
469
470} // namespace detail
472
473} // namespace data
474
475} // namespace mcrl2
476
477#endif // MCRL2_DATA_PARSE_H
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
void translate_user_notation()
Translate user notation within the equations of the data specification.
const function_symbol_vector & user_defined_mappings() const
Gets all user defined mappings in this specification.
\brief A function symbol
const sort_expression & sort() const
\brief A sort expression
\brief A data variable
Definition variable.h:28
Standard exception class for reporting runtime errors.
Definition exception.h:27
add your file description here.
term_list< Term > reverse(const term_list< Term > &l)
Returns the list with the elements in reversed order.
data_expression parse_data_expression(const std::string &text)
Definition data.cpp:224
data_specification parse_data_specification_new(const std::string &text)
Definition data.cpp:235
variable_list parse_variable_declaration_list(const std::string &text)
Definition data.cpp:246
variable_list parse_variables(const std::string &text)
Definition data.cpp:213
static data_specification const & default_specification()
Definition parse.h:31
sort_expression parse_sort_expression(const std::string &text)
Definition data.cpp:203
void parse_variables(std::istream &in, OutputIterator o, VariableIterator begin, VariableIterator end, const data_specification &data_spec=detail::default_specification())
Parses and type checks a data variable declaration list checking for double occurrences of variables ...
Definition parse.h:114
void typecheck_sort_expression(const sort_expression &sort_expr, const data_specification &data_spec)
Type check a sort expression. Throws an exception if something went wrong.
Definition typecheck.h:286
data_expression parse_data_expression(std::istream &in, const VariableContainer &variables, const data_specification &dataspec=detail::default_specification(), bool type_check=true, bool translate_user_notation=true, bool normalize_sorts=true)
Parses and type checks a data expression.
Definition parse.h:276
variable_list parse_variable_declaration_list(const std::string &text, const data_specification &dataspec=detail::default_specification())
Parses a variable declaration list.
Definition parse.h:429
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:90
sort_expression parse_sort_expression(std::istream &in, const data_specification &data_spec=detail::default_specification())
Parses and type checks a sort expression.
Definition parse.h:380
data_specification parse_data_specification(std::istream &in)
Parses a and type checks a data specification.
Definition parse.h:62
void typecheck_data_specification(data_specification &data_spec)
Type check a parsed mCRL2 data specification. Throws an exception if something went wrong.
Definition typecheck.h:344
data_expression typecheck_data_expression(const data_expression &x, const VariableContainer &variables, const data_specification &dataspec=data_specification())
Type check a data expression. Throws an exception if something went wrong.
Definition typecheck.h:308
std::vector< data_expression > data_expression_vector
\brief vector of data_expressions
data::function_symbol parse_function_symbol(const std::string &text, const std::string &dataspec_text="")
Definition parse.h:410
std::string pp(const abstraction &x)
Definition data.cpp:39
atermpp::term_list< data_expression > data_expression_list
\brief list of data_expressions
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:258
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
variable parse_variable(const std::string &text, const data_specification &data_spec=detail::default_specification())
Parses and type checks a data variable declaration.
Definition parse.h:218
void trim(std::string &text)
Remove all trailing and leading spaces from the input.
std::string read_text(const std::string &filename, bool warn=false)
Read text from a file.
std::string trim_copy(const std::string &text)
Remove all trailing and leading spaces from the input.
std::vector< std::string > split(const std::string &line, const std::string &separators)
Split the text.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72