Add built-in Map Keys to Seq function

[lavaleri]

Maps should have a built-in function that outputs its keys in a sequence, given a way to deterministically decide ordering on input.

[robin-aws]

It would be much more natural to expose the keys as a set<T> though, and then convert to a list and sort if needed.

[robin-aws]

Note this is possible within Dafny source, if you use a datatype for which Dafny understands that <= is a total ordering such as int (full credit to @RustanLeino for coming up with this version):

function method MapToSequence<B>(m: map<int,B>): seq<(int,B)>
  ensures var qq := MapToSequence(m);
    |m.Keys| == |qq| &&
    forall i :: 0 <= i < |qq| ==> qq[i].0 in m.Keys && m[qq[i].0] == qq[i].1
{
  var keys := SetToSequence(m.Keys);
  seq(|keys|, i requires 0 <= i < |keys| => (keys[i], m[keys[i]]))
}

function method SetToSequence(s: set<int>): seq<int>
  ensures var q := SetToSequence(s);
    |s| == |q| &&
    forall i :: 0 <= i < |q| ==> q[i] in s
{
  if s == {} then
    []
  else
    ThereIsAMinimum(s);
    var a :| a in s && forall z :: z in s ==> a <= z;
    [a] + SetToSequence(s - {a})
}

lemma ThereIsAMinimum(s: set<int>)
  requires s != {}
  ensures exists a :: a in s && forall z :: z in s ==> a <= z;
{
  var a := FindMinimum(s);
}
  
lemma FindMinimum(s: set<int>) returns (a: int)
  requires s != {}
  ensures a in s && forall z :: z in s ==> a <= z;
{
  a :| a in s;
  if s == {a} {
    // done
  } else {
    var s' := s - {a};
    assert forall x :: x in s <==> x == a || x in s';
    var a' := FindMinimum(s');
    a := if a' < a then a' else a;
  }
}

Although it may be useful to have a built-in function for performance reasons, I'd love it if this could be part of the standard library, assuming there was a way to generalize over a type T for which <= is total. It might make sense to support a (<) or (<=) type parameter suffix for this.

[acioc]

Note: If the syntax changes, we should also revisit the syntax for seq to multi-set.