#include <sort_specification.h>
Definition at line 45 of file sort_specification.h.
◆ sort_specification() [1/2]
| mcrl2::data::sort_specification::sort_specification |
( |
| ) |
|
|
inline |
◆ sort_specification() [2/2]
◆ 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
-
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] | 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. |
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] | 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. |
Definition at line 147 of file sort_specification.h.
◆ add_predefined_basic_sorts()
| void mcrl2::data::sort_specification::add_predefined_basic_sorts |
( |
| ) |
|
|
protected |
◆ add_sort()
| void mcrl2::data::sort_specification::add_sort |
( |
const basic_sort & |
s | ) |
|
|
inline |
◆ 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
-
- 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 |
◆ 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 |
◆ 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 |
◆ normalise_sort_specification_if_required()
| void mcrl2::data::sort_specification::normalise_sort_specification_if_required |
( |
| ) |
const |
|
inlineprotected |
◆ operator==()
| bool mcrl2::data::sort_specification::operator== |
( |
const sort_specification & |
other | ) |
const |
|
inline |
◆ reconstruct_m_normalised_aliases()
| void mcrl2::data::sort_specification::reconstruct_m_normalised_aliases |
( |
| ) |
const |
|
protected |
◆ 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
-
- Postcondition
- s does not occur in this specification.
Definition at line 161 of file sort_specification.h.
◆ sort_alias_map()
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 |
◆ 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.
◆ m_normalised_aliases
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
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:
