Mutable maps via Java extern #87
Conversation
src/MutableMap/MutableMap.dfy
Outdated
| reads this | ||
| ensures keys == this.content().Keys | ||
|
|
||
| function {:extern "values"} Values(): (values: set<V>) |
There was a problem hiding this comment.
Could we leave off Values() and Items() for now, so that we don't force V to be equality-supporting unnecessarily?
Alternatively, you could make those methods instead of functions and have them return non-deterministically ordered sequences instead of sets.
There was a problem hiding this comment.
I'm especially inclined to leave these out given dafny-lang/dafny#1373
There was a problem hiding this comment.
Keep them functions if they are there. But perhaps then we need two types, because equality supporting types for the parameters are going to be by far the most common.
There was a problem hiding this comment.
From what I've seen, at least Values() is used frequently by our customers. It would be good if we could find a way to support it.
|
Oh one other thing for later: users might expect more to find this under "Collections". We may want to consider that when we make a copy for this under DafnyCore as well. |
| * NOTE: Only here because of #2500; once resolved import "../../examples/MutableMap/ | ||
| * MutableMapTrait.dfy". |
There was a problem hiding this comment.
nit for later: it seems useful to have the trait for consumers too, so my preference would be to remove the example copy instead. But this is fine for now.
robin-aws
dismissed
davidcok’s stale review
Feedback addressed and reviewer is not available for a while
Per request, adds support for mutable maps by interfacing with Java. Partly follows https://github.com/dafny-lang/dafny/wiki/Modeling-External-State-Correctly and https://github.com/dafny-lang/libraries/tree/master/src/FileIO.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.