From 3fd4a15c2d3158170ba40fd8bd5abce47a30d3d9 Mon Sep 17 00:00:00 2001
From: Hira Syeda <syedahir@amazon.com>
Date: Wed, 6 Oct 2021 21:38:44 +0200
Subject: [PATCH] Add mapValue

This commit adds a function `mapValue` for mapping a function over
values of a given map
---
 src/Collections/Maps/Maps.dfy        | 11 +++++++++++
 src/Collections/Maps/Maps.dfy.expect |  2 +-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/Collections/Maps/Maps.dfy b/src/Collections/Maps/Maps.dfy
index b06e65cd..fe8c5c28 100644
--- a/src/Collections/Maps/Maps.dfy
+++ b/src/Collections/Maps/Maps.dfy
@@ -48,6 +48,17 @@ module Maps {
     m'
   }
 
+  /* Map a function to the values of a map */
+  function method {:opaque} mapValue<K, V, V'>(f: V -> V', m: map<K, V>): (m':map<K, V'>)
+    requires forall k:: k in m.Keys ==> f.requires(m[k])
+    ensures m.Keys == m'.Keys
+    ensures |m| == |m'|
+  {
+    var result := map k | k in m :: f(m[k]);
+    assert |result.Keys| == |result|;
+    result
+  }
+
   /* Keep all key-value pairs corresponding to the set of keys provided. */
   function method {:opaque} Restrict<X, Y>(m: map<X, Y>, xs: set<X>): (m': map<X, Y>)
     ensures m' == RemoveKeys(m, m.Keys - xs)
diff --git a/src/Collections/Maps/Maps.dfy.expect b/src/Collections/Maps/Maps.dfy.expect
index 66ffe366..4b0fec56 100644
--- a/src/Collections/Maps/Maps.dfy.expect
+++ b/src/Collections/Maps/Maps.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 14 verified, 0 errors
+Dafny program verifier finished with 15 verified, 0 errors