Skip to content
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

Standard library: MutableCollections #4648

Open
robin-aws opened this issue Oct 11, 2023 · 1 comment
Open

Standard library: MutableCollections #4648

robin-aws opened this issue Oct 11, 2023 · 1 comment
Assignees
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: standard libraries Standard libraries packaged in the Dafny distribution

Comments

@robin-aws
Copy link
Member

robin-aws commented Oct 11, 2023

Mutable versions of common collection types.

Depends on #4640, since the current approach is using {:extern} to use efficient native implementations.

Update: starting with Vector from the existing JSON library, since it is pure Dafny that doesn't need extern code

Existing source:

dafny-lang/libraries/src/MutableMap (partial) - Paused since the Go and JS backends don't support hashcodes on all Dafny types, so it's not possible to implement efficiently yet
dafny-lang/libraries/src/JSON/Utils/Vectors.dfy

@robin-aws robin-aws added this to the Dafny Standard Libraries milestone Oct 11, 2023
@robin-aws robin-aws added part: standard libraries Standard libraries packaged in the Dafny distribution kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny labels Oct 11, 2023
@robin-aws robin-aws assigned fabiomadge and unassigned fabiomadge Oct 16, 2023
@stefan-aws stefan-aws assigned stefan-aws and unassigned stefan-aws Oct 17, 2023
@robin-aws
Copy link
Member Author

Note that the current implementation's example makes use of a generic AssertAndExpect utility that should be promoted somewhere more central.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: standard libraries Standard libraries packaged in the Dafny distribution
Projects
None yet
Development

No branches or pull requests

4 participants