-
Notifications
You must be signed in to change notification settings - Fork 257
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: Default function opacity setting + autoreveal option #4342
Conversation
Fixes # <!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md --> <!-- Is this a bug fix? Remember to include a test in Test/git-issues/ --> <!-- Is this a bug fix for an issue introduced in the latest release? Mention this in the PR details and ensure a patch release is considered --> <!-- Does this PR need tests? Add them to `Test/` or to `Source/*.Test/…` and run them with `dotnet test` --> <!-- Are you moving a large amount of code? Read CONTRIBUTING.md to learn how to do that while maintaining git history --> <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Mikaël Mayer <[email protected]> Co-authored-by: Remy Willems <[email protected]> Co-authored-by: David Cok <[email protected]> Co-authored-by: davidcok <[email protected]>
…-as-arguments-causes-type' into all-opaque # Conflicts: # Source/DafnyCore/AST/Modules/ModuleDefinition.cs
…-opaque-function-causes' into all-opaque # Conflicts: # Source/DafnyCore/Verifier/Translator.cs # Test/git-issues/git-issue-4202.dfy # Test/git-issues/git-issue-4202.dfy.expect
# Conflicts: # Source/DafnyCore/Resolver/Rewriters.cs
…' into all-opaque
…' into all-opaque
…eals in a requires stmt, etc
…emmas. Implemented proper graph traversal for reveal stmt name building.
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.
Looking better! Interfaces really makes the code more maintainable, although now the code is put in different places, but that's what we do for Resolution and Formatting already anyway
…ewriter; added support for datatype constructor default values.
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.
Approved, only one small refactoring asked! Good job.
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.
Well done
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.
Very nice work!
# Conflicts: # Source/DafnyCore/AST/Members/Method.cs # docs/DafnyRef/Attributes.md
dc24bb8
…g#4342) This PR adds an additional cmdline flag `--default-function-opacity` which controls the default opacity of functions from `transparent`, `autoRevealDependencies`, or `opaque`. `transparent` is synonymous with the present behavior. `autoRevealDependencies` is a mode which makes functions opaque by default and inserts reveal stmts in each callable for each function dependency. `opaque` is a mode which makes functions opaque by default, leaving the user to insert all required function dependencies. <!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md --> <!-- Is this a bug fix? Remember to include a test in Test/git-issues/ --> <!-- Is this a bug fix for an issue introduced in the latest release? Mention this in the PR details and ensure a patch release is considered --> <!-- Does this PR need tests? Add them to `Test/` or to `Source/*.Test/…` and run them with `dotnet test` --> <!-- Are you moving a large amount of code? Read CONTRIBUTING.md to learn how to do that while maintaining git history --> <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Mikaël Mayer <[email protected]> Co-authored-by: Remy Willems <[email protected]> Co-authored-by: David Cok <[email protected]> Co-authored-by: davidcok <[email protected]> Co-authored-by: Mikael Mayer <[email protected]> Co-authored-by: Aaron Tomb <[email protected]>
This PR adds an additional cmdline flag `--default-function-opacity` which controls the default opacity of functions from `transparent`, `autoRevealDependencies`, or `opaque`. `transparent` is synonymous with the present behavior. `autoRevealDependencies` is a mode which makes functions opaque by default and inserts reveal stmts in each callable for each function dependency. `opaque` is a mode which makes functions opaque by default, leaving the user to insert all required function dependencies. <!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md --> <!-- Is this a bug fix? Remember to include a test in Test/git-issues/ --> <!-- Is this a bug fix for an issue introduced in the latest release? Mention this in the PR details and ensure a patch release is considered --> <!-- Does this PR need tests? Add them to `Test/` or to `Source/*.Test/…` and run them with `dotnet test` --> <!-- Are you moving a large amount of code? Read CONTRIBUTING.md to learn how to do that while maintaining git history --> <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Mikaël Mayer <[email protected]> Co-authored-by: Remy Willems <[email protected]> Co-authored-by: David Cok <[email protected]> Co-authored-by: davidcok <[email protected]> Co-authored-by: Mikael Mayer <[email protected]> Co-authored-by: Aaron Tomb <[email protected]>
This PR adds an additional cmdline flag `--default-function-opacity` which controls the default opacity of functions from `transparent`, `autoRevealDependencies`, or `opaque`. `transparent` is synonymous with the present behavior. `autoRevealDependencies` is a mode which makes functions opaque by default and inserts reveal stmts in each callable for each function dependency. `opaque` is a mode which makes functions opaque by default, leaving the user to insert all required function dependencies. <!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md --> <!-- Is this a bug fix? Remember to include a test in Test/git-issues/ --> <!-- Is this a bug fix for an issue introduced in the latest release? Mention this in the PR details and ensure a patch release is considered --> <!-- Does this PR need tests? Add them to `Test/` or to `Source/*.Test/…` and run them with `dotnet test` --> <!-- Are you moving a large amount of code? Read CONTRIBUTING.md to learn how to do that while maintaining git history --> <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Mikaël Mayer <[email protected]> Co-authored-by: Remy Willems <[email protected]> Co-authored-by: David Cok <[email protected]> Co-authored-by: davidcok <[email protected]> Co-authored-by: Mikael Mayer <[email protected]> Co-authored-by: Aaron Tomb <[email protected]>
This PR adds an additional cmdline flag
--default-function-opacity
which controls the default opacity of functions fromtransparent
,autoRevealDependencies
, oropaque
.transparent
is synonymous with the present behavior.autoRevealDependencies
is a mode which makes functions opaque by default and inserts reveal stmts in each callable for each function dependency.opaque
is a mode which makes functions opaque by default, leaving the user to insert all required function dependencies.By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.