mCRL2
Loading...
Searching...
No Matches
mcrl2::data::sort_specification Class Reference

#include <sort_specification.h>

Inheritance diagram for mcrl2::data::sort_specification:
mcrl2::data::data_specification

Public Member Functions

 sort_specification ()
 Default constructor.
 
 sort_specification (const basic_sort_vector &sorts, const alias_vector &aliases)
 
void add_sort (const basic_sort &s)
 Adds a sort to this specification.
 
void add_system_defined_sort (const sort_expression &s)
 Adds a sort to this specification, and marks it as system defined.
 
void add_context_sort (const sort_expression &s)
 Adds the sort s to the context sorts.
 
template<typename Container >
void add_context_sorts (const Container &c, typename atermpp::enable_if_container< Container >::type *=nullptr)
 Adds the sorts in c to the context sorts.
 
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.
 
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.
 
const std::set< sort_expression > & context_sorts () const
 Return the user defined context sorts of the current specification.
 
const basic_sort_vectoruser_defined_sorts () const
 Gets all sorts defined by a user (excluding the system defined sorts).
 
void add_alias (const alias &a)
 Adds an alias (new name for a sort) to this specification.
 
void remove_alias (const alias &a)
 Removes a user defined //alias from specification.
 
const alias_vectoruser_defined_aliases () const
 Gets the user defined aliases.
 
const std::map< sort_expression, sort_expression > & sort_alias_map () const
 Gets a normalisation mapping that maps each sort to its unique normalised sort.
 
bool operator== (const sort_specification &other) const
 

Protected Member Functions

void sorts_are_not_necessarily_normalised_anymore () const
 
void data_is_not_necessarily_normalised_anymore () const
 
void normalise_sort_specification_if_required () const
 
void add_predefined_basic_sorts ()
 
template<class CONTAINER >
void import_system_defined_sorts (const CONTAINER &sorts)
 
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.
 
void reconstruct_m_normalised_aliases () const
 
void check_for_alias_loop (const sort_expression &s, std::set< sort_expression > sorts_already_seen, const bool toplevel=true) const
 

Protected Attributes

bool 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.
 
bool 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.
 
basic_sort_vector m_user_defined_sorts
 The basic sorts and structured sorts in the specification.
 
std::set< sort_expressionm_normalised_sorts
 Set containing all the sorts, including the system defined ones.
 
std::set< sort_expressionm_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 m_user_defined_aliases
 The basic sorts and structured sorts in the specification.
 
std::map< sort_expression, sort_expressionm_normalised_aliases
 Table containing how sorts should be mapped to normalised sorts.
 

Detailed Description

Definition at line 45 of file sort_specification.h.

Constructor & Destructor Documentation

◆ sort_specification() [1/2]

mcrl2::data::sort_specification::sort_specification ( )
inline

Default constructor.

Definition at line 82 of file sort_specification.h.

◆ sort_specification() [2/2]

mcrl2::data::sort_specification::sort_specification ( const basic_sort_vector sorts,
const alias_vector aliases 
)
inline

Definition at line 89 of file sort_specification.h.

Member Function Documentation

◆ add_alias()

void mcrl2::data::sort_specification::add_alias ( const alias a)
inline

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

Parameters
[in]aan alias

Definition at line 206 of file sort_specification.h.

◆ add_context_sort()

void mcrl2::data::sort_specification::add_context_sort ( const sort_expression s)
inline

Adds the sort s to the context sorts.

Parameters
[in]sa 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.

Definition at line 135 of file sort_specification.h.

◆ add_context_sorts()

template<typename Container >
void mcrl2::data::sort_specification::add_context_sorts ( const Container &  c,
typename atermpp::enable_if_container< Container >::type *  = nullptr 
)
inline

Adds the sorts in c to the context sorts.

Parameters
[in]ca 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.

Definition at line 147 of file sort_specification.h.

◆ add_predefined_basic_sorts()

void mcrl2::data::sort_specification::add_predefined_basic_sorts ( )
protected

Definition at line 286 of file data_specification.cpp.

◆ add_sort()

void mcrl2::data::sort_specification::add_sort ( const basic_sort s)
inline

Adds a sort to this specification.

Parameters
[in]sA sort expression.

Definition at line 108 of file sort_specification.h.

◆ add_system_defined_sort()

void mcrl2::data::sort_specification::add_system_defined_sort ( const sort_expression s)
inline

Adds a sort to this specification, and marks it as system defined.

Parameters
[in]sA sort expression.
Precondition
s does not yet occur in this specification.
Postcondition
is_system_defined(s) = true
Note
this operation does not invalidate iterators of sorts_const_range

Definition at line 125 of file sort_specification.h.

◆ check_for_alias_loop()

void mcrl2::data::sort_specification::check_for_alias_loop ( const sort_expression s,
std::set< sort_expression sorts_already_seen,
const bool  toplevel = true 
) const
protected

Definition at line 148 of file data_specification.cpp.

◆ context_sorts()

const std::set< sort_expression > & mcrl2::data::sort_specification::context_sorts ( ) const
inline

Return the user defined context sorts of the current specification.

Time complexity is constant.

Returns
The set with sorts used in the context.

Definition at line 189 of file sort_specification.h.

◆ data_is_not_necessarily_normalised_anymore()

void mcrl2::data::sort_specification::data_is_not_necessarily_normalised_anymore ( ) const
inlineprotected

Definition at line 266 of file sort_specification.h.

◆ import_system_defined_sort()

void mcrl2::data::sort_specification::import_system_defined_sort ( const sort_expression sort)
protected

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.

Definition at line 292 of file data_specification.cpp.

◆ import_system_defined_sorts()

template<class CONTAINER >
void mcrl2::data::sort_specification::import_system_defined_sorts ( const CONTAINER &  sorts)
inlineprotected

Definition at line 293 of file sort_specification.h.

◆ normalise_sort_specification_if_required()

void mcrl2::data::sort_specification::normalise_sort_specification_if_required ( ) const
inlineprotected

Definition at line 271 of file sort_specification.h.

◆ operator==()

bool mcrl2::data::sort_specification::operator== ( const sort_specification other) const
inline

Definition at line 251 of file sort_specification.h.

◆ reconstruct_m_normalised_aliases()

void mcrl2::data::sort_specification::reconstruct_m_normalised_aliases ( ) const
protected

Definition at line 381 of file data_specification.cpp.

◆ remove_alias()

void mcrl2::data::sort_specification::remove_alias ( const alias a)
inline

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.

Definition at line 221 of file sort_specification.h.

◆ remove_sort()

void mcrl2::data::sort_specification::remove_sort ( const sort_expression s)
inline

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
[in]sA sort expression.
Postcondition
s does not occur in this specification.

Definition at line 161 of file sort_specification.h.

◆ sort_alias_map()

const std::map< sort_expression, sort_expression > & mcrl2::data::sort_specification::sort_alias_map ( ) const
inline

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.

Definition at line 245 of file sort_specification.h.

◆ sorts()

const std::set< sort_expression > & mcrl2::data::sort_specification::sorts ( ) const
inline

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.

Definition at line 180 of file sort_specification.h.

◆ sorts_are_not_necessarily_normalised_anymore()

void mcrl2::data::sort_specification::sorts_are_not_necessarily_normalised_anymore ( ) const
inlineprotected

Definition at line 260 of file sort_specification.h.

◆ user_defined_aliases()

const alias_vector & mcrl2::data::sort_specification::user_defined_aliases ( ) const
inline

Gets the user defined aliases.

The time complexity is constant.

Definition at line 232 of file sort_specification.h.

◆ user_defined_sorts()

const basic_sort_vector & mcrl2::data::sort_specification::user_defined_sorts ( ) const
inline

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.

Definition at line 199 of file sort_specification.h.

Member Data Documentation

◆ m_normalised_aliases

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

Table containing how sorts should be mapped to normalised sorts.

Definition at line 77 of file sort_specification.h.

◆ m_normalised_data_is_up_to_date

bool mcrl2::data::sort_specification::m_normalised_data_is_up_to_date
mutableprotected

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.

Definition at line 58 of file sort_specification.h.

◆ m_normalised_sorts

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

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

Definition at line 64 of file sort_specification.h.

◆ m_normalised_sorts_are_up_to_date

bool mcrl2::data::sort_specification::m_normalised_sorts_are_up_to_date
mutableprotected

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.

Definition at line 52 of file sort_specification.h.

◆ m_sorts_in_context

std::set< sort_expression > mcrl2::data::sort_specification::m_sorts_in_context
protected

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.

Definition at line 71 of file sort_specification.h.

◆ m_user_defined_aliases

alias_vector mcrl2::data::sort_specification::m_user_defined_aliases
protected

The basic sorts and structured sorts in the specification.

Definition at line 74 of file sort_specification.h.

◆ m_user_defined_sorts

basic_sort_vector mcrl2::data::sort_specification::m_user_defined_sorts
protected

The basic sorts and structured sorts in the specification.

Definition at line 61 of file sort_specification.h.


The documentation for this class was generated from the following files: