Added a less_total function to the data types - #1968
Open
mlaveaux wants to merge 5 commits into
Open
Conversation
* This should be a total order on the arguments, used for Set, Bag and function_update to ensure a consistent ordering between the elements in the internal lists that are used within these types.
There was a problem hiding this comment.
🟢 Approval recommended
The changes consistently introduce less_total across specs, generated headers, and typechecking support, and the remaining findings are minor readability/whitespace nits.
Pull request overview
This PR introduces a new standard ordering function less_total across the mCRL2 data type ecosystem to ensure a total order where needed (notably for Set/Bag implementations that rely on sorted-list representations), and extends rewrite support for less_total on function sorts so nested container types (e.g. Set(Set(Nat))) rewrite properly.
Changes:
- Added
less_totalrewrite rules to the standard data type specifications (Bool, Nat, Int, Pos, Real, List, FSet, FBag, Set, Bag) and updated ordering-dependent rules to useless_totalinstead of<. - Extended the C++ standard library support (
standard.h, typechecker initialisation, structured sort equations) to include theless_totalsymbol and equations, including a definition for function sorts. - Updated tests that assert mapping counts to account for the new system-defined function(s).
File summaries
| File | Description |
|---|---|
| scripts/code_generation/data_types/set64.spec | Defines less_total for Set and uses it in fset-based merge rules. |
| scripts/code_generation/data_types/set1.spec | Defines less_total for Set and uses it in fset-based merge rules. |
| scripts/code_generation/data_types/real64.spec | Adds less_total for Real (delegates to <). |
| scripts/code_generation/data_types/real1.spec | Adds less_total for Real (delegates to <). |
| scripts/code_generation/data_types/pos64.spec | Adds less_total for Pos (delegates to <). |
| scripts/code_generation/data_types/pos1.spec | Adds less_total for Pos (delegates to <). |
| scripts/code_generation/data_types/nat64.spec | Adds less_total for Nat (delegates to <). |
| scripts/code_generation/data_types/nat1.spec | Adds less_total for Nat (delegates to <). |
| scripts/code_generation/data_types/list64.spec | Adds lexicographic less_total rules for List. |
| scripts/code_generation/data_types/list1.spec | Adds lexicographic less_total rules for List. |
| scripts/code_generation/data_types/int64.spec | Adds less_total for Int (delegates to <). |
| scripts/code_generation/data_types/int1.spec | Adds less_total for Int (delegates to <). |
| scripts/code_generation/data_types/fset64.spec | Adds less_total for FSet and switches ordering guards to it. |
| scripts/code_generation/data_types/fset1.spec | Adds less_total for FSet and switches ordering guards to it. |
| scripts/code_generation/data_types/fbag64.spec | Adds less_total for FBag and switches ordering guards to it. |
| scripts/code_generation/data_types/fbag1.spec | Adds less_total for FBag and switches ordering guards to it. |
| scripts/code_generation/data_types/data.py | Treats less_total as a standard function during code generation. |
| scripts/code_generation/data_types/bool.spec | Adds Bool variable + less_total rule (delegates to <). |
| scripts/code_generation/data_types/bag64.spec | Defines less_total for Bag and switches fbag merge guards to it. |
| scripts/code_generation/data_types/bag1.spec | Defines less_total for Bag and switches fbag merge guards to it. |
| libraries/data/test/parser_test.cpp | Updates expected mapping counts due to added system function(s). |
| libraries/data/test/data_specification_test.cpp | Updates expected mapping counts due to added system function(s). |
| libraries/data/source/typecheck.cpp | Registers less_total as a system-defined function. |
| libraries/data/include/mcrl2/data/structured_sort.h | Adds structured-sort equation less_total(x,y) = less(x,y). |
| libraries/data/include/mcrl2/data/standard.h | Introduces less_total symbol, constructors/recognisers, and equations incl. function-sort ordering. |
| libraries/data/include/mcrl2/data/set64.h | Adds generated less_total equation and uses it in set/fset merge equations. |
| libraries/data/include/mcrl2/data/set1.h | Adds generated less_total equation and uses it in set/fset merge equations. |
| libraries/data/include/mcrl2/data/real64.h | Adds generated less_total equation for Real. |
| libraries/data/include/mcrl2/data/real1.h | Adds generated less_total equation for Real. |
| libraries/data/include/mcrl2/data/pos64.h | Adds generated less_total equation for Pos. |
| libraries/data/include/mcrl2/data/pos1.h | Adds generated less_total equation for Pos. |
| libraries/data/include/mcrl2/data/nat64.h | Adds generated less_total equation for Nat. |
| libraries/data/include/mcrl2/data/nat1.h | Adds generated less_total equation for Nat. |
| libraries/data/include/mcrl2/data/list64.h | Adds generated lexicographic less_total equations for List. |
| libraries/data/include/mcrl2/data/list1.h | Adds generated lexicographic less_total equations for List. |
| libraries/data/include/mcrl2/data/int64.h | Adds generated less_total equation for Int. |
| libraries/data/include/mcrl2/data/int1.h | Adds generated less_total equation for Int. |
| libraries/data/include/mcrl2/data/fset64.h | Adds generated less_total equations and updates ordering guards to it. |
| libraries/data/include/mcrl2/data/fset1.h | Adds generated less_total equations and updates ordering guards to it. |
| libraries/data/include/mcrl2/data/fbag64.h | Adds generated less_total equations and updates ordering guards to it. |
| libraries/data/include/mcrl2/data/fbag1.h | Adds generated less_total equations and updates ordering guards to it. |
| libraries/data/include/mcrl2/data/bool.h | Adds generated less_total equation for Bool. |
| libraries/data/include/mcrl2/data/bag64.h | Adds generated less_total equation and updates ordering guards to it. |
| libraries/data/include/mcrl2/data/bag1.h | Adds generated less_total equation and updates ordering guards to it. |
Review details
- Files reviewed: 44/44 changed files
- Comments generated: 2
- Review effort level: Lite
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adapted the standard data types to define a less_total, to be used for the
SetandBagdefinitions, which are stored as sorted lists (and require the ordering to be total). Furthermore, added specific rewrite rules forless_totalfor function sorts as well. This should allow specifications withSet(Set(Nat))types to rewrite properly.