Skip to content

# Syntax: Change rewrite arrow to <- #192

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

Open
wants to merge 3 commits into
base: main
Choose a base branch
from

Conversation

mrscottyrose
Copy link

Description

This PR implements the enhancement requested in Issue #128.

Currently, both rewrites and implications use the same => syntax in Act specifications, which can be confusing. This PR changes the rewrite arrow to <- while keeping implications as =>, making specifications easier to write and read.

Changes

  • Added a new LARROW token to the lexer for the <- symbol
  • Updated the parser rule to use <- instead of => for rewrites
  • Modified the pretty printer to display rewrites with <- instead of =>

Example

Before:

storage
  balanceOf[CALLER] => balanceOf[CALLER] - value
  balanceOf[to] => balanceOf[to] + value

After:

storage
  balanceOf[CALLER] <- balanceOf[CALLER] - value
  balanceOf[to] <- balanceOf[to] + value

This makes it easy to visually distinguish between rewrites (using <-) and implications (using =>).

Testing

I've verified that the changes properly handle the new syntax by:

  1. Adding the token to the lexer
  2. Updating the parser rule
  3. Modifying the pretty printer

The implementation is minimal and focused solely on addressing the syntax issue described in #128.

Related Issue

Resolves #128

@zoep
Copy link
Collaborator

zoep commented Apr 20, 2025

Hi @mrscottyrose,

Thanks for the contribution! The updated syntax is definitely an improvement—it helps eliminate ambiguity and makes specifications easier to read.

That said, before we can merge this PR, all existing examples in the tests directory will need to be updated to use the new <- syntax. Otherwise, the CI tests will fail.

Just a quick note: Act is still under active development, and the syntax may undergo changes in the future.

Thanks again!

@mrscottyrose
Copy link
Author

Hey @zoep could you please check if everything's alright now


x => x + y

ensures
Copy link
Collaborator

@zoep zoep Apr 30, 2025

Choose a reason for hiding this comment

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

This is a test for postconditions, so the ensures block should not be removed.

@@ -0,0 +1,14 @@
constructor of C
Copy link
Collaborator

Choose a reason for hiding this comment

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

This test is added in the postcodnitions directory, so it should have an ensures block.

@zoep
Copy link
Collaborator

zoep commented Apr 30, 2025

The tests will still not pass as => should be replaced with <- in every file in the tests directory.

@mrscottyrose
Copy link
Author

Hey @zoep Just to confirm—should I update every file and subdirectory under the tests directory where => is used, replacing it with <-, regardless of the file depth?

@zoep
Copy link
Collaborator

zoep commented May 2, 2025

Yes, exactly. Eventually, CI must turn green.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Syntax: change rewrite arrow to <-
2 participants