@@ -8,15 +8,36 @@ import (
88)
99
1010// Definition of class MutableMap copied over from
11- // https://github.com/dafny-lang/dafny/blob/master /Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go
11+ // https://github.com/dafny-lang/dafny/blob/99327494b3f8b6e49b00824deb4cc2c25b375b05 /Source/DafnyStandardLibraries/src/Std/ConcurrentExterns /Std_Concurrent/Std_Concurrent.go
1212type MutableMap struct {
13- mu sync.Mutex
14-
15- Internal _dafny.Map
16- }
17-
18- func New_MutableMap_ () * MutableMap {
19- return & MutableMap {}
13+ // Default implementation - synchronized Dafny map<K, V>,
14+ // which is just a list of key-value pairs
15+ // with O(n) lookup.
16+ mu sync.Mutex
17+ dafnyInternal _dafny.Map
18+
19+ // Optimized for seq<bytes>
20+ // The Dafny byte sequences are converted to Go strings,
21+ // which can contain arbitrary bytes,
22+ // and are comparable and hence can be used as map keys,
23+ // whereas a Go byte array cannot.
24+ goInternal sync.Map
25+
26+ // Switch to control which is active
27+ bytesKeys bool
28+ }
29+
30+ // bytesKeys should be set using ctor but it does not because of Dafny bug
31+ // https://github.com/dafny-lang/dafny/issues/6333
32+ // This uses variadic parameters to make it backward compatible while adding the boolean parameter bytesKeys
33+ func New_MutableMap_ (bytesKeys ... bool ) * MutableMap {
34+ useBytes := false
35+ if len (bytesKeys ) > 0 {
36+ useBytes = bytesKeys [0 ]
37+ }
38+ return & MutableMap {
39+ bytesKeys : useBytes ,
40+ }
2041}
2142
2243type CompanionStruct_MutableMap_ struct {
@@ -31,7 +52,10 @@ func (_this *MutableMap) Equals(other *MutableMap) bool {
3152// If you use the returned value, and ALSO continue to modify the MutableMap
3253// Then things might get weird.
3354func (_this * MutableMap ) Content () _dafny.Map {
34- return _this .Internal
55+ if _this .bytesKeys == true {
56+ panic ("To maintain compatibility with other runtimes, this method does not work when bytesKeys is true." )
57+ }
58+ return _this .dafnyInternal
3559}
3660
3761func (_this * MutableMap ) EqualsGeneric (x interface {}) bool {
@@ -65,79 +89,157 @@ func (_this *MutableMap) ParentTraits_() []*_dafny.TraitID {
6589
6690var _ _dafny.TraitOffspring = & MutableMap {}
6791
68- func (_this * MutableMap ) Ctor__ () {
92+ func (_this * MutableMap ) Ctor__ (bytesKeys bool ) {
6993 {
94+ _this .bytesKeys = bytesKeys
7095 }
7196}
97+
98+ // Converts a Dafny seq<byte> to a Go string,
99+ // which can contain artibitrary bytes.
100+ func dafnyBytesToGoString (b interface {}) string {
101+ return string (_dafny .ToByteArray (b .(_dafny.Sequence )))
102+ }
103+
104+ // Converts a Dafny seq<byte> from a Go string,
105+ // which can contain artibitrary bytes.
106+ func dafnyBytesFromGoString (b interface {}) _dafny.Sequence {
107+ return _dafny .SeqOfBytes ([]byte (b .(string )))
108+ }
109+
72110func (_this * MutableMap ) Keys () _dafny.Set {
73111 {
74- _this .mu .Lock ()
75- defer _this .mu .Unlock ()
112+ if _this .bytesKeys {
113+ keys := make ([]interface {}, 0 )
114+
115+ _this .goInternal .Range (func (key , value interface {}) bool {
116+ keys = append (keys , dafnyBytesFromGoString (key ))
117+ return true
118+ })
119+
120+ return _dafny .SetOf (keys [:]... )
121+ } else {
122+ _this .mu .Lock ()
123+ defer _this .mu .Unlock ()
76124
77- return _this .Internal .Keys ()
125+ return _this .dafnyInternal .Keys ()
126+ }
78127 }
79128}
80129func (_this * MutableMap ) HasKey (k interface {}) bool {
81130 {
82- _this .mu .Lock ()
83- defer _this .mu .Unlock ()
131+ if _this .bytesKeys {
132+ _ , ok := _this .goInternal .Load (dafnyBytesToGoString (k ))
133+ return ok
134+ } else {
135+ _this .mu .Lock ()
136+ defer _this .mu .Unlock ()
84137
85- return _this .Internal .Contains (k )
138+ return _this .dafnyInternal .Contains (k )
139+ }
86140 }
87141}
88142func (_this * MutableMap ) Values () _dafny.Set {
89143 {
90- _this .mu .Lock ()
91- defer _this .mu .Unlock ()
144+ if _this .bytesKeys {
145+ values := make ([]interface {}, 0 )
146+
147+ _this .goInternal .Range (func (key , value interface {}) bool {
148+ values = append (values , value )
149+ return true
150+ })
92151
93- return _this .Internal .Values ()
152+ return _dafny .SetOf (values [:]... )
153+ } else {
154+ _this .mu .Lock ()
155+ defer _this .mu .Unlock ()
156+
157+ return _this .dafnyInternal .Values ()
158+ }
94159 }
95160}
96161func (_this * MutableMap ) Items () _dafny.Set {
97162 {
98- _this .mu .Lock ()
99- defer _this .mu .Unlock ()
163+ if _this .bytesKeys {
164+ items := make ([]interface {}, 0 )
165+
166+ _this .goInternal .Range (func (key , value interface {}) bool {
167+ items = append (items , _dafny .TupleOf (dafnyBytesFromGoString (key ), value ))
168+ return true
169+ })
100170
101- return _this .Internal .Items ()
171+ return _dafny .SetOf (items [:]... )
172+ } else {
173+ _this .mu .Lock ()
174+ defer _this .mu .Unlock ()
175+
176+ return _this .dafnyInternal .Items ()
177+ }
102178 }
103179}
104180func (_this * MutableMap ) Get (k interface {}) Std_Wrappers.Option {
105181 {
106- _this .mu .Lock ()
107- defer _this .mu .Unlock ()
108-
109- value , ok := _this .Internal .Find (k )
110- if ok {
111- return Std_Wrappers .Companion_Option_ .Create_Some_ (value )
182+ if _this .bytesKeys {
183+ value , ok := _this .goInternal .Load (dafnyBytesToGoString (k ))
184+ if ok {
185+ return Std_Wrappers .Companion_Option_ .Create_Some_ (value )
186+ } else {
187+ return Std_Wrappers .Companion_Option_ .Create_None_ ()
188+ }
112189 } else {
113- return Std_Wrappers .Companion_Option_ .Create_None_ ()
190+ _this .mu .Lock ()
191+ defer _this .mu .Unlock ()
192+
193+ value , ok := _this .dafnyInternal .Find (k )
194+ if ok {
195+ return Std_Wrappers .Companion_Option_ .Create_Some_ (value )
196+ } else {
197+ return Std_Wrappers .Companion_Option_ .Create_None_ ()
198+ }
114199 }
115200 }
116201}
117202func (_this * MutableMap ) Put (k interface {}, v interface {}) {
118- {
203+ if _this .bytesKeys {
204+ _this .goInternal .Store (dafnyBytesToGoString (k ), v )
205+ } else {
119206 _this .mu .Lock ()
120207 defer _this .mu .Unlock ()
121208
122- _this .Internal = _this .Internal .UpdateUnsafe (k , v )
209+ _this .dafnyInternal = _this .dafnyInternal .UpdateUnsafe (k , v )
123210 }
124211}
125212func (_this * MutableMap ) Remove (k interface {}) {
126213 {
127- _this .mu .Lock ()
128- defer _this .mu .Unlock ()
214+ if _this .bytesKeys {
215+ _this .goInternal .Delete (dafnyBytesToGoString (k ))
216+ } else {
217+ _this .mu .Lock ()
218+ defer _this .mu .Unlock ()
129219
130- // This could be special-cased for a single remove to be a bit faster,
131- // but it's still going to be O(n) so likely not worth it.
132- _this .Internal = _this .Internal .Subtract (_dafny .SetOf (k ))
220+ // This could be special-cased for a single remove to be a bit faster,
221+ // but it's still going to be O(n) so likely not worth it.
222+ _this .dafnyInternal = _this .dafnyInternal .Subtract (_dafny .SetOf (k ))
223+ }
133224 }
134225}
135226func (_this * MutableMap ) Size () _dafny.Int {
136227 {
137- _this .mu .Lock ()
138- defer _this .mu .Unlock ()
228+ if _this .bytesKeys {
229+ var c _dafny.Int = _dafny .Zero
230+
231+ _this .goInternal .Range (func (key , value interface {}) bool {
232+ c = c .Plus (_dafny .One )
233+ return true
234+ })
139235
140- return _this .Internal .Cardinality ()
236+ return c
237+ } else {
238+ _this .mu .Lock ()
239+ defer _this .mu .Unlock ()
240+
241+ return _this .dafnyInternal .Cardinality ()
242+ }
141243 }
142244}
143245
0 commit comments