Compiled functions #1555
Closed
Compiled functions #1555
Conversation
This file contains 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
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). |
robin-aws
requested changes
Nov 4, 2021
There was a problem hiding this comment.
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.
keyboardDrummer
approved these changes
Nov 5, 2021
|
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. |
RustanLeino
added a commit
that referenced
this pull request
Feb 22, 2022
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
# for free
to join this conversation on GitHub.
Already have an account?
# to comment
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 PR introduces a proposed change of syntax from the confusing keyword phrases
function methodandpredicate methodtocompiled functionandcompiled 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,
compiledis 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-vscodeto accept the new keyword, and corresponding updates indafny-lang/libraries.