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

Eliminate Operator Precedence #506

Closed
DavePearce opened this Issue Jul 16, 2015 · 3 comments

Comments

Projects
None yet
1 participant
@DavePearce
Member

DavePearce commented Jul 16, 2015

Whiley currently supports the usual concepts of operator precedence. However, this is unsatisfactory for a few reasons. Firstly, it complicates the language specification itself. Secondly we have to choose precedence for some operators and it seems arbitrary. Finally if we want to support operator overloading, this will be a problem.

I think there are two good options:

  1. Require braces for all non-commutative operators. For example, "1+2+3" is ok but not "1-2-3". This still doesnt work for operator overloading, though.
  2. Prohibit mixed operator expressions without braces. For example "1+2+3" is ok but not "1+2×3". Within a group left-to-right evaluation is assumed. This does work with operator overloading.

DavePearce added a commit that referenced this issue Jul 31, 2015

WyCS: Removed ListUpdate syntax #506
The list update syntax did not work correctly, and so I've removed it.
instead, I've introduced a new macro for describing array updates and
this needs to be used in place.  This will require updating Whiley's
verification condition generator to utilise this.  At the moment,
however, there is a bug with macro expansion from the standard library
or similar.

DavePearce added a commit that referenced this issue Jul 31, 2015

Update VcGenerator to remove ListUpdate #506
The VcGenerator now generates verification conditions using the new
Array update macro.  This is working, though it doesn't handle nested
updates (e.g. to multi-dimensional arrays or combinations of
fields/array updates.)

DavePearce added a commit that referenced this issue Jul 31, 2015

WyCS: Update WyCS to use new Rewriter API #506
The new rewriter API is not yet fully figure out, but it's slowly
starting to take shape.

DavePearce added a commit that referenced this issue Aug 1, 2015

WyCS: Removed ListUpdate syntax #506
The list update syntax did not work correctly, and so I've removed it.
instead, I've introduced a new macro for describing array updates and
this needs to be used in place.  This will require updating Whiley's
verification condition generator to utilise this.  At the moment,
however, there is a bug with macro expansion from the standard library
or similar.

The VcGenerator now generates verification conditions using the new
Array update macro.  This is working, though it doesn't handle nested
updates (e.g. to multi-dimensional arrays or combinations of
fields/array updates.)
@DavePearce

This comment has been minimized.

Show comment
Hide comment
@DavePearce

DavePearce Aug 2, 2015

Member

See also #499

Member

DavePearce commented Aug 2, 2015

See also #499

@DavePearce DavePearce removed the WYC label Oct 19, 2016

@DavePearce

This comment has been minimized.

Show comment
Hide comment
@DavePearce

DavePearce May 13, 2017

Member

Am now developing an RFC for this.

Member

DavePearce commented May 13, 2017

Am now developing an RFC for this.

@DavePearce

This comment has been minimized.

Show comment
Hide comment
@DavePearce

DavePearce May 17, 2017

Member

This is now an RFC here: Whiley/RFCs#1

Member

DavePearce commented May 17, 2017

This is now an RFC here: Whiley/RFCs#1

@DavePearce DavePearce closed this May 17, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment