diff --git a/src/MutableMap/MutableMap.cs b/src/MutableMap/MutableMap.cs new file mode 100644 index 00000000..ff5358b1 --- /dev/null +++ b/src/MutableMap/MutableMap.cs @@ -0,0 +1,78 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ +using System.Collections; +using System.Collections.Concurrent; +using System.Collections.Immutable; +using System.Numerics; +using _System; +using Dafny; + + +namespace DafnyLibraries { + public partial class MutableMap + { + private ConcurrentDictionary m; + public MutableMap() { + m = new ConcurrentDictionary(); + } + + public IMap content() { + var keyPairs = new List>(); + foreach (var k in m.Keys) { + keyPairs.Add(new Pair(k, m[k])); + } + return Map.FromCollection(keyPairs); + } + + public void Put(K k, V v) + { + m[k] = v; + } + + public Dafny.ISet Keys() + { + var keys = m.Keys; + return Set.FromCollection(keys); + } + + public bool HasKey(K k) + { + return m.ContainsKey(k); + } + + public Dafny.ISet Values() + { + var values= m.Values; + return Set.FromCollection(values); + } + + public Dafny.ISet<_ITuple2> Items() + { + var keyPairs = new List<_ITuple2>(); + foreach (var k in m.Keys) { + keyPairs.Add(new Tuple2(k, m[k])); + } + return Set<_ITuple2>.FromCollection(keyPairs); + } + + public V Select(K k) + { + return m[k]; + } + + public void Remove(K k) + { + if (HasKey(k)) { + var keypair = new KeyValuePair(k, m[k]); + m.TryRemove(keypair); + } + } + + public BigInteger Size() + { + return new BigInteger(m.Count); + } + } +}