-
Notifications
You must be signed in to change notification settings - Fork 256
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
Compiled functions #1555
Compiled functions #1555
Conversation
These replace the keyword phrases `function method` and `compiled predicate`, which are now marked as deprecated.
Note, in this commit, the tests still use the old syntax. However, this still causes a few changes in the expect test output, because of updated error messages and updated pretty printing.
except in `dafny4/RollYourOwnArrowType.dfy`, which will be completed in a separate commit
Beyond reviewing the language change itself, I think the easiest way to review this PR is to look at each individual commit. Those commits are either boring (and huge) or interesting (and small). |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just flagging that there is still some open discussion around whether we should also tweak the syntax for the function by method
feature, since it is still arguably using the method
keyword to indicate "when compiled", and we may want to align the concepts better.
Also potentially blocked on #1564 - this PR is definitely an improvement, but we may want to consider deeper changes before making this change and then potentially undoing it shortly after. |
Given the discussion on #1564, I'm retracting this PR and hope to instead follow up with one based on that discussion. |
As a result of discussion #1564, this PR implements a command-line option `/functionSyntax` that gives early access to a (syntactic) breaking change that we expect in Dafny version 4, namely changing function to be compiled (not ghost) by default. This PR does not impose any changes on existing code. When (months from now) we are ready to release Dafny version 4, we can simply change the default from `/functionSyntax:3` to `/functionSyntax:4`, as well as update the test suite and documentation. When updating the tests, `/functionSyntax:migration3to4` or other options will be useful. When updating the documentation, it may be useful to look at what had been changed in the preliminary, and since abandoned, PR #1555, which had updated the documentation in a different direction. The following table shows, for each mode of the new flag `/functionSyntax:<mode>`, what kind of declaration (ghost or compiled, or an error) you get from using the various keywords: mode | `ghost function` | `function` | `function method` -----|-----|-----|----- `3` (default) | error | ghost | compiled `4` | ghost | compiled | error `migration3to4` | ghost | error | compiled `experimentalDefaultGhost` | ghost | ghost | compiled `experimentalDefaultCompiled` | ghost | compiled | compiled `experimentalPredicateAlwaysGhost` | ghost | compiled | error The same table applies if you replace `function` with `predicate`, except in the last line, which treats `function` and `predicate` in different ways: mode | `ghost predicate` | `predicate` | `predicate method` -----|-----|-----|----- `experimentalPredicateAlwaysGhost` | error | ghost | error ## Other implementation level changes: * Remove dangling `.expect` file * Ignore generated `.py` files * chore: Code improvements * chore: Clean up some comments and formatting
This PR introduces a proposed change of syntax from the confusing keyword phrases
function method
andpredicate method
tocompiled function
andcompiled predicate
, respectively. The PR allows both pairs of keyword phrases as synonyms, but gears up toward just accepting thecompiled ...
phrases in the future. In particular, documentation and all tests are changed to the new syntax, and the old syntax gives a deprecation warning under (the non-default)/deprecation:2
.In this PR,
compiled
is not a keyword by itself. It is only looked upon specially in the two new keyword phrases.If accepted, this PR should be followed by an update of
dafny-lang/ide-vscode
to accept the new keyword, and corresponding updates indafny-lang/libraries
.