mCRL2
Loading...
Searching...
No Matches
data_io.cpp
Go to the documentation of this file.
1// Author(s): Maurice Laveaux
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/data/data_io.h"
11
14
15using namespace mcrl2;
16using namespace mcrl2::data;
17
18static
20{
21 if (x.function() == core::detail::function_symbol_OpId())
22 {
23 return atermpp::aterm(core::detail::function_symbol_OpIdNoIndex(), x.begin(), --x.end());
24 }
25 return x;
26}
27
28static
30{
31 if (x.function() == core::detail::function_symbol_DataVarIdNoIndex()) // Obsolete. Remove in say 2025.
32 {
33 const data::variable& y = reinterpret_cast<const data::variable&>(x);
34 return variable(y.name(), y.sort());
35 }
36 else if (x.function() == core::detail::function_symbol_OpIdNoIndex())
37 {
38 const data::function_symbol& y = reinterpret_cast<const data::function_symbol&>(x);
39 return function_symbol(y.name(), y.sort());
40 }
41 return x;
42}
43
45{
46 return atermpp::aterm(core::detail::function_symbol_DataSpec(),
47 atermpp::aterm(core::detail::function_symbol_SortSpec(), atermpp::aterm_list(s.user_defined_sorts().begin(),s.user_defined_sorts().end()) +
49 atermpp::aterm(core::detail::function_symbol_ConsSpec(), atermpp::aterm_list(s.user_defined_constructors().begin(),s.user_defined_constructors().end())),
50 atermpp::aterm(core::detail::function_symbol_MapSpec(), atermpp::aterm_list(s.user_defined_mappings().begin(),s.user_defined_mappings().end())),
51 atermpp::aterm(core::detail::function_symbol_DataEqnSpec(), atermpp::aterm_list(s.user_defined_equations().begin(),s.user_defined_equations().end())));
52}
53
54inline
56{
58}
59
60inline
62{
64}
65
67{
68 atermpp::aterm_stream_state state(stream);
69 stream >> add_index_impl;
70
72 alias_vector aliases;
73 function_symbol_vector constructors;
74 function_symbol_vector user_defined_mappings;
75 data_equation_vector user_defined_equations;
76
77 stream >> sorts;
78 stream >> aliases;
79 stream >> constructors;
80 stream >> user_defined_mappings;
81 stream >> user_defined_equations;
82
83 // Store the given information in a new data specification (to ignore existing elements of spec).
84 spec = data_specification(sorts, aliases, constructors, user_defined_mappings, user_defined_equations);
85
86 return stream;
87}
88
90{
91 atermpp::aterm_stream_state state(stream);
92 stream << remove_index_impl;
93
94 stream << spec.user_defined_sorts();
95 stream << spec.user_defined_aliases();
96 stream << spec.user_defined_constructors();
97 stream << spec.user_defined_mappings();
98 stream << spec.user_defined_equations();
99 return stream;
100}
Algorithms for ATerms.
The interface for a class that reads aterm from a stream. The default constructed term aterm() indica...
Definition aterm_io.h:59
The interface for a class that writes aterm to a stream. Every written term is retrieved by the corre...
Definition aterm_io.h:48
A helper class to restore the state of the aterm_{i,o}stream objects upon destruction....
Definition aterm_io.h:84
const_iterator end() const
Returns a const_iterator pointing past the last argument.
Definition aterm.h:172
const_iterator begin() const
Returns an iterator pointing to the first argument.
Definition aterm.h:165
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
A list of aterm objects.
Definition aterm_list.h:24
const function_symbol_vector & user_defined_constructors() const
Gets the constructors defined by the user, excluding those that are system defined.
const function_symbol_vector & user_defined_mappings() const
Gets all user defined mappings in this specification.
const data_equation_vector & user_defined_equations() const
Gets all user defined equations.
\brief A function symbol
const core::identifier_string & name() const
const sort_expression & sort() const
const basic_sort_vector & user_defined_sorts() const
Gets all sorts defined by a user (excluding the system defined sorts).
const alias_vector & user_defined_aliases() const
Gets the user defined aliases.
\brief A data variable
Definition variable.h:28
const core::identifier_string & name() const
Definition variable.h:38
const sort_expression & sort() const
Definition variable.h:43
atermpp::aterm remove_index(const atermpp::aterm &x)
Definition data_io.cpp:61
static atermpp::aterm remove_index_impl(const atermpp::aterm &x)
Definition data_io.cpp:19
static atermpp::aterm add_index_impl(const atermpp::aterm &x)
Definition data_io.cpp:29
atermpp::aterm add_index(const atermpp::aterm &x)
Definition data_io.cpp:55
The class data_specification.
Term bottom_up_replace(Term t, ReplaceFunction r)
Replaces each subterm x of t by r(x). The ReplaceFunction r has the following signature: aterm x; ate...
Definition algorithm.h:276
atermpp::aterm data_specification_to_aterm(const data_specification &s)
Definition data_io.cpp:44
Namespace for all data library functionality.
Definition abstraction.h:22
std::vector< alias > alias_vector
\brief vector of aliass
Definition alias.h:75
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
std::vector< basic_sort > basic_sort_vector
vector of basic sorts
Definition basic_sort.h:94
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72