diff options
| author |  Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-25 14:13:09 -0700 |
|---|---|---|
| committer | Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-25 14:13:09 -0700 |
| commit | aa6921029400e5dfa4186e0eff420c46d9b68f1d (patch) | |
| tree | 16895335104372dbe97ee85480e2136777ced42b /Binaries | |
| parent | 2b6114bab22c9d6fc99fc90c34be1f5b22f07da7 (diff) | |
Dafny: Added compilation of finite maps
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 2f8d2764..67669245 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -275,6 +275,75 @@ namespace Dafny return new MultiSet<T>(r);
}
}
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U,V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U,V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ }
public class Sequence<T>
{
T[] elmts;
|