'union' syntax support - #332
Merged
Merged
Conversation
Smattr
force-pushed
the
smattr/github-331
branch
from
August 12, 2026 07:06
b4ac715 to
2662c93
Compare
Smattr
added a commit
that referenced
this pull request
Aug 12, 2026
Commits CI-ed in an intermediate state of #332.
Smattr
added a commit
that referenced
this pull request
Aug 12, 2026
Commits CI-ed in an intermediate state of #332.
Smattr
force-pushed
the
smattr/github-331
branch
from
August 12, 2026 09:47
2662c93 to
35f35d0
Compare
Smattr
added a commit
that referenced
this pull request
Aug 12, 2026
Commit CI-ed in an intermediate state of #332.
Smattr
force-pushed
the
smattr/github-331
branch
from
August 13, 2026 07:06
35f35d0 to
2cb9376
Compare
Smattr
added a commit
that referenced
this pull request
Aug 13, 2026
Commits CI-ed in an intermediate state of #332.
Smattr
force-pushed
the
smattr/github-331
branch
3 times, most recently
from
August 14, 2026 07:03
fe67f4b to
26502ed
Compare
Smattr
added a commit
that referenced
this pull request
Aug 14, 2026
Commits CI-ed in an intermediate state of #332.
Smattr
force-pushed
the
smattr/github-331
branch
2 times, most recently
from
August 15, 2026 21:37
965b1d9 to
824d5e3
Compare
Smattr
marked this pull request as ready for review
August 15, 2026 21:39
Owner
Author
|
This is in a state where we could now merge it if it passes CI. |
This support is extremely limited. The intent is to allow parsing
`union` with librumur so users can build union-supporting tools on top,
but not to support `union` within `rumur`. Despite this, some partial
handling of `union` is added within `rumur`. The intent of this is to
avoid anything slipping through the cracks if/when `union` support is
added to `rumur` in future. I.e. any attempt to do this should result in
visible errors surfacing from these locations that need to be updated.
This change does not include changes to the parser itself, which will
arrive in an upcoming commit.
There are a number of notable divergences from CMurphi semantics:
1. As discussed in an added comment, unions with 0 or 1 members are
supported in contrast to CMurphi.
2. Differing unions within other types make the containing types
non-equal. E.g. CMurphi appears to consider variables of types
`record a: union {foo, bar}; endrecord` and
`record a: union {foo, baz}; endrecord` to be
comparable/assignable/etc because they have at least one equivalent
type interpretation. In Rumur, we do not consider these variables
compatible in this way.
Gitlab: #331 “MultiSet support within scope?”
This still has no effect because `union` is not yet supported during parsing. Github: #331 “MultiSet support within scope?”
At this point, it is possible to parse and process a model using `union` types. Doing this on real world models is still challenging because there is no support for `ismember` that most real world `union`-using models also use. Github: #331 “MultiSet support within scope?”
This is still rejected by most Rumur tools. The intent is to just allow librumur users to successfully parse models using `ismember`. Gitlab: #331 “MultiSet support within scope?”
There is still no parser support. Github: #331 “MultiSet support within scope?”
At this point, `ismember` support is complete, in the sense we can parse and manipulate it. This allows ingesting models like sci.m from CMurphi’s examples. There is still no support for producing a checker from a model that uses `union` types or `ismember`, and none is planned right now. Gitlab: #331 “MultiSet support within scope?”
Smattr
force-pushed
the
smattr/github-331
branch
from
August 16, 2026 01:18
824d5e3 to
c89bd8a
Compare
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
1 participant
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.
This is in a preliminary state and needs a lot of work, but worth getting some CI.