Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: reintroduce match constraint syntax #328

Merged
merged 2 commits into from
Jul 1, 2023
Merged

Conversation

bitwalker
Copy link
Contributor

This PR brings back the syntax for match constraints, modified to remove grammar ambiguities discovered with the previous syntax.

An example of the syntax is shown below:

integrity_constraints:
    enf match:
        case s[0] & s[1]: clk' = clk
        case !s[0] & !s[1]: clk' = 1

The choice of enf match vs match enf is intentional, and is intended to make the declaration of a constraint uniform, i.e. a constraint statement always begins with enf whether it is a simple constraint, a constraint comprehension, or a match constraint.

The implementation of this syntax simply compiles to a flat set of constraints for now, as if every branch of the match was a separate constraint conditioned on the selector for the match. This is handled directly in the parser for now, since we don't actually do anything meaningful with match constraints yet. Once we do, we'll update the parser accordingly and introduce distinct AST nodes to represent the construct.


I think we should still plan on eventually switching to block syntax for all "blocks" in the language, which was also discussed alongside the match syntax changes, but we were able to implement the latter without the former, so it is strictly speaking not necessary, but would make the grammar more regular (beneficial for any future syntax changes) and would improve the clarity of the language (IMO). In any case, that's a topic for a different discussion, but I wanted to make a note about it here for future reference.

The current implementation of this syntax simply compiles to a flat set
of constraints, as if every branch of the match was a separate
constraint conditioned on the selector for the match.

Since this does not yet introduce a separate internal statement type for
match constraints, we are using a temporary hack in the parser which
parses match constraints directly into the representation described
above. When we actually implement the correct semantics for match
constraints, we'll update the parser accordingly.
@bitwalker bitwalker requested review from bobbinth and grjte June 29, 2023 19:02
@bitwalker bitwalker self-assigned this Jun 29, 2023
@bitwalker
Copy link
Contributor Author

Looks like there is an issue with miden-vm causing the build to fail

@bobbinth
Copy link
Contributor

Yep - will fix later today.

Copy link
Contributor

@bobbinth bobbinth left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks great! Thank you!

The choice of enf match vs match enf is intentional, and is intended to make the declaration of a constraint uniform, i.e. a constraint statement always begins with enf whether it is a simple constraint, a constraint comprehension, or a match constraint.

Agreed! I like this approach.

The implementation of this syntax simply compiles to a flat set of constraints for now, as if every branch of the match was a separate constraint conditioned on the selector for the match. This is handled directly in the parser for now, since we don't actually do anything meaningful with match constraints yet. Once we do, we'll update the parser accordingly and introduce distinct AST nodes to represent the construct.

Yes, agreed. I think with this PR we can probably close #125 and create a separate issue to address improvements I mentioned in #125 (comment).

I think we should still plan on eventually switching to block syntax for all "blocks" in the language, which was also discussed alongside the match syntax changes, but we were able to implement the latter without the former, so it is strictly speaking not necessary, but would make the grammar more regular (beneficial for any future syntax changes) and would improve the clarity of the language (IMO). In any case, that's a topic for a different discussion, but I wanted to make a note about it here for future reference.

I've been thinking about this as well, but as you said, this would be a separate discussion. Could you create an issue for this?

@bobbinth bobbinth merged commit 982d38e into next Jul 1, 2023
@bobbinth bobbinth deleted the bitwalker/match-syntax branch July 1, 2023 05:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants