mcrl2::data::sort_specification

Include file:

#include "mcrl2/data/sort_specification.h

class mcrl2::data::sort_specification

Protected attributes

std::map<sort_expression, sort_expression> mcrl2::data::sort_specification::m_normalised_aliases

Table containing how sorts should be mapped to normalised sorts.

bool 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.

std::set<sort_expression> mcrl2::data::sort_specification::m_normalised_sorts

Set containing all the sorts, including the system defined ones.

bool 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.

std::set<sort_expression> 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.

alias_vector mcrl2::data::sort_specification::m_user_defined_aliases

The basic sorts and structured sorts in the specification.

basic_sort_vector mcrl2::data::sort_specification::m_user_defined_sorts

The basic sorts and structured sorts in the specification.

Public member functions

void add_alias(const alias &a)

Adds an alias (new name for a sort) to this specification.

Parameters:

• a an alias

void 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.

void 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.

void add_sort(const basic_sort &s)

Adds a sort to this specification.

Parameters:

• s A sort expression.

void 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

const std::set<sort_expression> &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.

bool operator==(const sort_specification &other) const

void 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.

void 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.

const std::map<sort_expression, sort_expression> &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)

const std::set<sort_expression> &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.

const alias_vector &user_defined_aliases() const

Gets the user defined aliases.

The time complexity is constant.

const basic_sort_vector &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.

Protected member functions

void add_predefined_basic_sorts()

void check_for_alias_loop(const sort_expression &s, std::set<sort_expression> sorts_already_seen, const bool toplevel = true) const

void data_is_not_necessarily_normalised_anymore() const

void import_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.

void import_system_defined_sorts(const CONTAINER &sorts)

void normalise_sort_specification_if_required() const

void reconstruct_m_normalised_aliases() const

void sorts_are_not_necessarily_normalised_anymore() const