Include file:
#include "mcrl2/data/sort_specification.h
mcrl2::data::
sort_specification
¶mcrl2::data::sort_specification::
m_normalised_aliases
¶Table containing how sorts should be mapped to normalised sorts.
mcrl2::data::sort_specification::
m_normalised_data_is_up_to_date
¶The variable below indicates whether a surrounding data specification is up to data with respect to sort normalisation and available sorts. This is set to false if an alias or a new sort is added.
mcrl2::data::sort_specification::
m_normalised_sorts
¶Set containing all the sorts, including the system defined ones.
mcrl2::data::sort_specification::
m_normalised_sorts_are_up_to_date
¶This boolean indicates whether the variables m_normalised_constructors, m_mappings, m_equations, m_normalised_sorts, m_normalised_aliases are up to date with respect to changes of this sort specification.
mcrl2::data::sort_specification::
m_sorts_in_context
¶The sorts that occur are needed in this sort specification but are not explicitly defined as user defined sorts. An example is the sort Nat when declaring the use of a sort List(Nat). The normalised sorts, constructors, mappings and equations are complete with respect to these sorts.
mcrl2::data::sort_specification::
m_user_defined_aliases
¶The basic sorts and structured sorts in the specification.
mcrl2::data::sort_specification::
m_user_defined_sorts
¶The basic sorts and structured sorts in the specification.
add_alias
(const alias &a)¶Adds an alias (new name for a sort) to this specification.
Parameters:
a an alias
add_context_sort
(const sort_expression &s)¶Adds the sort s to the context sorts.
Parameters:
s a sort expression. It is added to m_sorts_in_context. For this sort standard functions are generated automatically (if, <,<=,==,!=,>=,>) and if the sort is a standard sort, the necessary constructors, mappings and equations are added to the data type.
add_context_sorts
(const Container &c, typename atermpp::enable_if_container<Container>::type * = nullptr)¶Adds the sorts in c to the context sorts.
Parameters:
c a container of sort expressions. These are added to m_sorts_in_context. For these sorts standard functions are generated automatically (if, <,<=,==,!=,>=,>) and if the sorts are standard sorts, the necessary constructors, mappings and equations are added to the data type.
add_sort
(const basic_sort &s)¶Adds a sort to this specification.
Parameters:
s A sort expression.
add_system_defined_sort
(const sort_expression &s)¶Adds a sort to this specification, and marks it as system defined.
Parameters:
s A sort expression.
Pre: s does not yet occur in this specification.
Post: is_system_defined(s) = true .. note:: this operation does not invalidate iterators of sorts_const_range
context_sorts
() const¶Return the user defined context sorts of the current specification.
Time complexity is constant.
Returns: The set with sorts used in the context.
operator==
(const sort_specification &other) const¶remove_alias
(const alias &a)¶Removes a user defined //alias from specification.
This also removes the defined sort of this alias from the set of user defined sorts. This routine does not check whether the alias, or name was in the user defined sets.
remove_sort
(const sort_expression &s)¶Removes sort from the user defined sorts in the specification. Note that this does not remove aliases for the sort, and it does not remove constructors, mappings and equations, and also keeps the sort as defined in the context.
Parameters:
s A sort expression.
Post: s does not occur in this specification.
sort_alias_map
() const¶Gets a normalisation mapping that maps each sort to its unique normalised sort.
Sorts that are mapped to itself are not include in the mapping. This map is required in functions with the name normalize_sorts. When in a specification sort aliases are used, like sort A=B or sort Tree=struct leaf | node(Tree,Tree) then there are different representations for each sort. The normalisation mapping maps each sort to a unique representant. Moreover, it is this unique sort that it provides in internal mappings.
sort_specification
()¶Default constructor.
sort_specification
(const basic_sort_vector &sorts, const alias_vector &aliases)¶sorts
() const¶Gets the normalised sort declarations including those that are system defined. This is the set with all sorts that occur in a data_specification, or that have been registered as sorts used in the context.
The time complexity of this operation is constant, except when the data specification has been changed, in which case it can be that the sorts must be renormalised. This operation is linear in the size of the specification.
Returns: The sort normalised using the aliases occurring in this specification, including the built in sorts such as Bool and Nat, and complex sorts that are used in the user defined aliases and sorts, but also that are registered as sorts used in the context of the specification.
user_defined_aliases
() const¶Gets the user defined aliases.
The time complexity is constant.
user_defined_sorts
() const¶Gets all sorts defined by a user (excluding the system defined sorts).
The time complexity of this operation is constant.
Returns: The user defined sort declaration.
add_predefined_basic_sorts
()¶check_for_alias_loop
(const sort_expression &s, std::set<sort_expression> sorts_already_seen, const bool toplevel = true) const¶data_is_not_necessarily_normalised_anymore
() constimport_system_defined_sort
(const sort_expression &sort)¶Adds the system defined sorts in a sequence. The second argument is used to check which sorts are added, to prevent useless repetitions of additions of sorts.
The function normalise_sorts imports for the given sort_expression sort all sorts, constructors, mappings and equations that belong to this sort to the `normalised’ sets in this data type. E.g. for the sort Nat of natural numbers, it is required that Pos (positive numbers) are defined.
import_system_defined_sorts
(const CONTAINER &sorts)¶normalise_sort_specification_if_required
() const¶reconstruct_m_normalised_aliases
() const¶sorts_are_not_necessarily_normalised_anymore
() const¶