Add MapWithResult for maps

[MikaelMayer]

Here is sample code that could be integrated, need to test if it's fast enough and relevant.

datatype Option<W> = None | Some(value: W)

function MapWithFailure<U, V, W>(oldmap: map<U, V>, f: V -> Option<W>): (result: Option<map<U, W>>) {
  if forall k <- oldmap :: f(oldmap[k]).Some? then
    Some(map k <- oldmap :: k := f(oldmap[k]).value)
  else
    None
} by method {
  var keySet := oldmap.Keys;
  ghost var keySetcomplement := {};
  var tmp := map[];
  while |keySet| > 0
    invariant keySet !! keySetcomplement
    invariant keySet + keySetcomplement == oldmap.Keys
    invariant forall k <- keySetcomplement :: f(oldmap[k]).Some?
    invariant Some(tmp) == MapWithFailure(map k <- oldmap | k in keySetcomplement :: k := oldmap[k], f)
  {
    var x :| x in keySet;
    keySet := keySet - {x};
    var t := f(oldmap[x]);
    if t.None? {
      return None;
    }
    ghost var oldTmp := tmp;
    tmp := tmp[x := t.value];
    calc {
      tmp;
      oldTmp[x := t.value];
      MapWithFailure(map k <- oldmap | k in keySetcomplement :: k := oldmap[k], f).value[x := t.value];
      MapWithFailure(map k <- oldmap | k in keySetcomplement + {x} :: k := oldmap[k], f).value;
    }
    keySetcomplement := keySetcomplement + {x};
  }
  result := Some(tmp);
  assert keySetcomplement == oldmap.Keys;
  assert oldmap == map k <- oldmap | k in keySetcomplement :: k := oldmap[k];
}