diff options
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 9 | ||||
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 36 |
2 files changed, 43 insertions, 2 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 09b6efcf..742fd4e4 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -371,6 +371,15 @@ axiom (forall<U, V> u: U :: { Map#Domain(Map#Empty(): Map U V)[u] }
!Map#Domain(Map#Empty(): Map U V)[u]);
+function Map#Glue<U, V>([U] bool, [U]V): Map U V;
+axiom (forall<U, V> a: [U] bool, b:[U]V ::
+ { Map#Domain(Map#Glue(a, b)) }
+ Map#Domain(Map#Glue(a, b)) == a);
+axiom (forall<U, V> a: [U] bool, b:[U]V ::
+ { Map#Elements(Map#Glue(a, b)) }
+ Map#Elements(Map#Glue(a, b)) == b);
+
+
//Build is used in displays, and for map updates
function Map#Build<U, V>(Map U V, U, V): Map U V;
/*axiom (forall<U, V> m: Map U V, u: U, v: V ::
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 67669245..f7eecfc5 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -274,6 +274,19 @@ namespace Dafny }
return new MultiSet<T>(r);
}
+ public IEnumerable<T> Elements {
+ get {
+ List<T> l = new List<T>();
+ foreach (T t in dict.Keys) {
+ int n;
+ dict.TryGetValue(t, out n);
+ for (int i = 0; i < n; i ++) {
+ l.Add(t);
+ }
+ }
+ return l;
+ }
+ }
}
public class Map<U, V>
@@ -288,9 +301,16 @@ namespace Dafny return new Map<U, V>(new Dictionary<U,V>());
}
}
- public static Map<U, V> FromElements(params Pair<U,V>[] values) {
+ 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) {
+ foreach (Pair<U, V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
+ foreach (Pair<U, V> p in values) {
d[p.Car] = p.Cdr;
}
return new Map<U, V>(d);
@@ -343,6 +363,11 @@ namespace Dafny d[index] = val;
return new Map<U, V>(d);
}
+ public IEnumerable<U> Domain {
+ get {
+ return dict.Keys;
+ }
+ }
}
public class Sequence<T>
{
@@ -471,6 +496,12 @@ namespace Dafny }
return frall;
}
+ public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
+ foreach (var u in map.Domain) {
+ if (pred(u) != frall) { return !frall; }
+ }
+ return frall;
+ }
public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
foreach (var u in seq.Elements) {
if (pred(u) != frall) { return !frall; }
@@ -479,6 +510,7 @@ namespace Dafny }
// Enumerating other collections
public delegate Dafny.Set<T> ComprehensionDelegate<T>();
+ public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
public static IEnumerable<bool> AllBooleans {
get {
yield return false;
|