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 :
10 : #include "mcrl2/atermpp/aterm_io_text.h"
11 :
12 : #include <fstream>
13 :
14 : namespace atermpp
15 : {
16 :
17 : // utility functions
18 :
19 211271 : static void write_string_with_escape_symbols(const std::string& s, std::ostream& os)
20 : {
21 : // Check whether the string starts with a - or a number, or contains the symbols
22 : // \, ", (, ), [, ], comma, space, \t, \n or \r. If yes, the string will be
23 : // surrounded by quotes, and the symbols \, ", \t, \n, \r
24 : // will be preceded by an escape symbol.
25 :
26 211271 : char c = s[0];
27 211271 : bool contains_special_symbols = ((c =='-') || isdigit(c));
28 :
29 1413919 : for(std::string::const_iterator i=s.begin(); !contains_special_symbols && i!=s.end(); ++i)
30 : {
31 1202648 : if (*i=='\\' || *i=='"' || *i=='(' || *i==')' || *i=='[' || *i==']' || *i==',' || *i==' ' || *i=='\n' || *i=='\t' || *i=='\r')
32 : {
33 6682 : contains_special_symbols=true;
34 : }
35 : }
36 :
37 211271 : if (contains_special_symbols)
38 : {
39 : // This function symbol needs quotes.
40 6682 : os << "\"";
41 20046 : for(std::string::const_iterator i=s.begin(); i!=s.end(); ++i)
42 : {
43 : // We need to escape special characters.
44 13364 : switch (*i)
45 : {
46 0 : case '\\':
47 : case '"':
48 0 : os << "\\" << *i;
49 0 : break;
50 0 : case '\n':
51 0 : os << "\\n";
52 0 : break;
53 0 : case '\t':
54 0 : os << "\\t";
55 0 : break;
56 0 : case '\r':
57 0 : os << "\\r";
58 0 : break;
59 13364 : default:
60 13364 : os << *i;
61 13364 : break;
62 : }
63 : }
64 6682 : os << "\"";
65 : }
66 : else
67 : {
68 204589 : os << s;
69 : }
70 211271 : }
71 :
72 : // Public functions
73 :
74 12586 : text_aterm_ostream::text_aterm_ostream(std::ostream& os, bool newline)
75 12586 : : m_stream(os),
76 12586 : m_newline(newline)
77 12586 : {}
78 :
79 12586 : void text_aterm_ostream::put(const aterm& term)
80 : {
81 12586 : write_term_line(term);
82 :
83 12586 : if (m_newline)
84 : {
85 0 : m_stream << "\n";
86 : }
87 12586 : }
88 :
89 10107 : text_aterm_istream::text_aterm_istream(std::istream& is)
90 10107 : : m_stream(is)
91 : {
92 10107 : character = next_char();
93 10107 : }
94 :
95 10107 : void text_aterm_istream::get(aterm& term)
96 : {
97 : try
98 : {
99 10107 : if (character != EOF)
100 : {
101 10107 : term = parse_aterm(character);
102 : }
103 : }
104 0 : catch (std::runtime_error& e)
105 : {
106 0 : throw std::runtime_error(e.what() + std::string("\n") + print_parse_error_position());
107 0 : }
108 :
109 : // Reset the parsing error buffers.
110 10107 : m_column = 0;
111 10107 : m_history.clear();
112 :
113 10107 : return;
114 : }
115 :
116 : // Private functions
117 :
118 222300 : void text_aterm_ostream::write_term_line(const aterm& t)
119 : {
120 222300 : if (t.type_is_int())
121 : {
122 : // Write a single integer as is.
123 2253 : m_stream << atermpp::down_cast<aterm_int>(t).value();
124 : }
125 220047 : else if (t.type_is_list())
126 : {
127 : // A list l0...ln is formatted as [l0, ..., ln].
128 8776 : m_stream << "[";
129 8776 : const aterm_list& list = down_cast<aterm_list>(t);
130 26299 : for (aterm_list::const_iterator it = list.begin(); it != list.end(); ++it)
131 : {
132 17523 : if (it!=list.begin())
133 : {
134 8750 : m_stream << ",";
135 : }
136 17523 : write_term_line(*it);
137 : }
138 :
139 8776 : m_stream << "]";
140 : }
141 : else
142 : {
143 : // An aterm_appl f(t0, ..., tn) is written as f(t0, ..., tn)
144 211271 : assert(t.type_is_appl());
145 :
146 211271 : aterm_appl appl = m_transformer(down_cast<aterm_appl>(t));
147 :
148 211271 : write_string_with_escape_symbols(appl.function().name(), m_stream);
149 :
150 211271 : if (appl.function().arity() > 0)
151 : {
152 114216 : m_stream << "(";
153 114216 : write_term_line(appl[0]);
154 192191 : for (std::size_t i = 1; i < appl.function().arity(); i++)
155 : {
156 77975 : m_stream << ",";
157 77975 : write_term_line(appl[i]);
158 : }
159 114216 : m_stream << ")";
160 : }
161 211271 : }
162 222300 : }
163 :
164 221083 : aterm text_aterm_istream::parse_aterm(int& character)
165 : {
166 : // Parse the term.
167 221083 : switch (character)
168 : {
169 6689 : case '"':
170 : {
171 6689 : std::string function_name = parse_quoted_string(character);
172 6689 : return parse_aterm_appl(function_name, character);
173 6689 : }
174 8855 : case '[':
175 : {
176 8855 : return parse_aterm_list(character, '[', ']');
177 : }
178 205539 : default:
179 : {
180 205539 : if (isdigit(character) || character == '-')
181 : {
182 204 : return parse_aterm_int(character);
183 : }
184 :
185 205335 : std::string function_symbol = parse_unquoted_string(character);
186 205335 : return parse_aterm_appl(function_symbol, character);
187 205335 : }
188 : }
189 : }
190 :
191 212024 : aterm_appl text_aterm_istream::parse_aterm_appl(const std::string& function_name, int& character)
192 : {
193 : // Parse the arguments.
194 212024 : aterm_list arguments = parse_aterm_list(character, '(', ')');
195 :
196 : // Wrap up this function application.
197 212024 : function_symbol symbol(function_name, arguments.size());
198 636072 : return m_transformer(aterm_appl(symbol, arguments.begin(), arguments.end()));
199 212024 : }
200 :
201 204 : aterm_int text_aterm_istream::parse_aterm_int(int& character)
202 : {
203 : std::array<char, 32> number;
204 204 : auto it = number.begin();
205 :
206 204 : if (character == '-')
207 : {
208 0 : *it = static_cast<char>(character);
209 0 : ++it;
210 0 : character = next_char(true, true);
211 : }
212 :
213 536 : while (isdigit(character) && it != number.end())
214 : {
215 332 : *it = static_cast<char>(character);
216 332 : ++it;
217 332 : character = next_char();
218 : }
219 :
220 204 : *it = '\0';
221 408 : return aterm_int(static_cast<std::size_t>(atol(number.data())));
222 : }
223 :
224 220879 : aterm_list text_aterm_istream::parse_aterm_list(int& character, char begin, char end)
225 : {
226 220879 : aterm_list list;
227 :
228 : // A list is [t0, ..., tn] or surrounded by ().
229 220879 : if (character == begin)
230 : {
231 123667 : character = next_char(true, true);
232 123667 : if (character != end)
233 : {
234 123656 : list.push_front(parse_aterm(character));
235 :
236 210976 : while (character == ',')
237 : {
238 87320 : character = next_char(true, true);
239 87320 : list.push_front(parse_aterm(character));
240 : }
241 :
242 123656 : if (character != end)
243 : {
244 0 : throw std::runtime_error(std::string("Missing ") + end + " while parsing a list term");
245 : }
246 : }
247 :
248 123667 : character = next_char(true);
249 : }
250 :
251 441758 : return reverse(list);
252 220879 : }
253 :
254 :
255 0 : std::string text_aterm_istream::print_parse_error_position()
256 : {
257 0 : std::stringstream s;
258 0 : s << "Error occurred at line " << m_line << ", col " << m_column << " near: ";
259 0 : for(const auto& element : m_history)
260 : {
261 0 : s << element;
262 : }
263 0 : return s.str();
264 0 : }
265 :
266 1572718 : int text_aterm_istream::next_char(bool skip_whitespace, bool required)
267 : {
268 1572718 : character = EOF;
269 :
270 : do
271 : {
272 : try
273 : {
274 : // In liblts_lts the exception bit is set, so we need to use exception to handle EOF.
275 1572718 : character = m_stream.get();
276 : }
277 0 : catch (std::ios::failure&)
278 : {
279 0 : return EOF;
280 0 : }
281 :
282 1572718 : if (character != EOF)
283 : {
284 1562611 : if (character == '\n')
285 : {
286 0 : m_line++;
287 0 : m_column = 0;
288 : }
289 : else
290 : {
291 1562611 : m_column++;
292 : }
293 :
294 1562611 : if (m_history.size() >= m_history_limit)
295 : {
296 : // If the history is full the first element must be removed.
297 1068416 : m_history.erase(m_history.begin());
298 : }
299 :
300 1562611 : m_history.emplace_back(character);
301 : }
302 10107 : else if (required)
303 : {
304 0 : throw std::runtime_error("Premature end of file while parsing.");
305 : }
306 : }
307 1572718 : while (isspace(character) && skip_whitespace);
308 :
309 : // The stream also returns a newline for the last symbol.
310 1572718 : return character == '\n' ? EOF : character;
311 : }
312 :
313 6689 : std::string text_aterm_istream::parse_quoted_string(int& character)
314 : {
315 : // We need a buffer for printing and parsing.
316 6689 : std::string string;
317 :
318 6689 : assert(character == '"');
319 :
320 : // First obtain the first symbol after ".
321 6689 : character = next_char();
322 :
323 20067 : while (character != '"')
324 : {
325 13378 : switch (character)
326 : {
327 0 : case '\\':
328 0 : character = next_char(false, true);
329 0 : switch (character)
330 : {
331 0 : case 'n':
332 0 : string += '\n';
333 0 : break;
334 0 : case 'r':
335 0 : string += '\r';
336 0 : break;
337 0 : case 't':
338 0 : string += '\t';
339 0 : break;
340 0 : default:
341 0 : string += static_cast<char>(character);
342 0 : break;
343 : }
344 0 : break;
345 13378 : default:
346 13378 : string += static_cast<char>(character);
347 13378 : break;
348 : }
349 13378 : character = next_char(false, true);
350 : }
351 :
352 6689 : character = next_char(true, false);
353 6689 : return string;
354 0 : }
355 :
356 205335 : std::string text_aterm_istream::parse_unquoted_string(int& character)
357 : {
358 205335 : std::string string;
359 :
360 205335 : if (character != '(')
361 : {
362 : // First parse the identifier
363 1611539 : while (character != '"' && character != '(' && character != ')' && character != ']'
364 1246127 : && character != ']' && character != ',' && character != ' ' && character != '\n'
365 2607092 : && character != '\t' && character != '\r' && character != EOF)
366 : {
367 1200869 : string += static_cast<char>(character);
368 1200869 : character = next_char(false);
369 : }
370 : }
371 :
372 205335 : return string;
373 0 : }
374 :
375 7 : void write_term_to_text_stream(const aterm& term, std::ostream& os)
376 : {
377 7 : text_aterm_ostream(os) << term;
378 7 : }
379 :
380 10101 : aterm read_term_from_string(const std::string& s)
381 : {
382 10101 : std::stringstream ss(s);
383 10101 : aterm t;
384 10101 : read_term_from_text_stream(ss, t);
385 20202 : return t;
386 10101 : }
387 :
388 10107 : void read_term_from_text_stream(std::istream& is, aterm& t)
389 : {
390 10107 : text_aterm_istream(is).get(t);
391 10107 : }
392 :
393 :
394 12579 : std::ostream& operator<<(std::ostream& os, const aterm& term)
395 : {
396 12579 : text_aterm_ostream(os) << term;
397 12579 : return os;
398 : }
399 :
400 : } // namespace atermpp
|
