From 095d07e15c506f78e2b76346b19900ab0fa45229 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Tue, 20 Aug 2024 14:12:09 -0700
Subject: [PATCH] Remove SetToSeq

The method makes it difficult to use the libraries in a project that
enables `--enforce-determinism`.
---
 src/Collections/Sequences/Seq.dfy | 62 -------------------------------
 src/dafny/Collections/Seqs.dfy    | 62 -------------------------------
 2 files changed, 124 deletions(-)

diff --git a/src/Collections/Sequences/Seq.dfy b/src/Collections/Sequences/Seq.dfy
index 756102fc..9aff3f6b 100644
--- a/src/Collections/Sequences/Seq.dfy
+++ b/src/Collections/Sequences/Seq.dfy
@@ -846,65 +846,3 @@ module {:options "-functionSyntax:4"} Seq {
       result := next + result;
     }
   }
-
-  /**********************************************************
-   *
-   *  Sets to Ordered Sequences
-   *
-   ***********************************************************/
-
-  /* Converts a set to a sequence (ghost). */
-  ghost function SetToSeqSpec<T>(s: set<T>): (xs: seq<T>)
-    ensures multiset(s) == multiset(xs)
-  {
-    if s == {} then [] else var x :| x in s; [x] + SetToSeqSpec(s - {x})
-  }
-
-  /* Converts a set to a sequence (compiled). */
-  method SetToSeq<T>(s: set<T>) returns (xs: seq<T>)
-    ensures multiset(s) == multiset(xs)
-  {
-    xs := [];
-    var left: set<T> := s;
-    while left != {}
-      invariant multiset(left) + multiset(xs) == multiset(s)
-    {
-      var x :| x in left;
-      left := left - {x};
-      xs := xs + [x];
-    }
-  }
-
-  /* Proves that any two sequences that are sorted by a total order and that have the same elements are equal. */
-  lemma SortedUnique<T(!new)>(xs: seq<T>, ys: seq<T>, R: (T, T) -> bool)
-    requires SortedBy(xs, R)
-    requires SortedBy(ys, R)
-    requires TotalOrdering(R)
-    requires multiset(xs) == multiset(ys)
-    ensures xs == ys
-  {
-    assert |xs| == |multiset(xs)| == |multiset(ys)| == |ys|;
-    if xs == [] || ys == [] {
-    } else {
-      assert xs == [xs[0]] + xs[1..];
-      assert ys == [ys[0]] + ys[1..];
-      assert multiset(xs[1..]) == multiset(xs) - multiset{xs[0]};
-      assert multiset(ys[1..]) == multiset(ys) - multiset{ys[0]};
-      assert multiset(xs[1..]) == multiset(ys[1..]);
-      SortedUnique(xs[1..], ys[1..], R);
-    }
-  }
-
-  /* Converts a set to a sequence that is ordered w.r.t. a given total order. */
-  function SetToSortedSeq<T(!new)>(s: set<T>, R: (T, T) -> bool): (xs: seq<T>)
-    requires TotalOrdering(R)
-    ensures multiset(s) == multiset(xs)
-    ensures SortedBy(xs, R)
-  {
-    MergeSortBy(SetToSeqSpec(s), R)
-  } by method {
-    xs := SetToSeq(s);
-    xs := MergeSortBy(xs, R);
-    SortedUnique(xs, SetToSortedSeq(s, R), R);
-  }
-}
diff --git a/src/dafny/Collections/Seqs.dfy b/src/dafny/Collections/Seqs.dfy
index c9c7814c..d73f61b2 100644
--- a/src/dafny/Collections/Seqs.dfy
+++ b/src/dafny/Collections/Seqs.dfy
@@ -803,68 +803,6 @@ module {:options "-functionSyntax:4"} Dafny.Collections.Seq {
   }
 
 
-  /**********************************************************
-   *
-   *  Sets to Ordered Sequences
-   *
-   ***********************************************************/
-
-  /* Converts a set to a sequence (ghost). */
-  ghost function SetToSeqSpec<T>(s: set<T>): (xs: seq<T>)
-    ensures multiset(s) == multiset(xs)
-  {
-    if s == {} then [] else var x :| x in s; [x] + SetToSeqSpec(s - {x})
-  }
-
-  /* Converts a set to a sequence (compiled). */
-  method SetToSeq<T>(s: set<T>) returns (xs: seq<T>)
-    ensures multiset(s) == multiset(xs)
-  {
-    xs := [];
-    var left: set<T> := s;
-    while left != {}
-      invariant multiset(left) + multiset(xs) == multiset(s)
-    {
-      var x :| x in left;
-      left := left - {x};
-      xs := xs + [x];
-    }
-  }
-
-  /* Proves that any two sequences that are sorted by a total order and that have the same elements are equal. */
-  lemma SortedUnique<T(!new)>(xs: seq<T>, ys: seq<T>, R: (T, T) -> bool)
-    requires SortedBy(xs, R)
-    requires SortedBy(ys, R)
-    requires TotalOrdering(R)
-    requires multiset(xs) == multiset(ys)
-    ensures xs == ys
-  {
-    assert |xs| == |multiset(xs)| == |multiset(ys)| == |ys|;
-    if xs == [] || ys == [] {
-    } else {
-      assert xs == [xs[0]] + xs[1..];
-      assert ys == [ys[0]] + ys[1..];
-      assert multiset(xs[1..]) == multiset(xs) - multiset{xs[0]};
-      assert multiset(ys[1..]) == multiset(ys) - multiset{ys[0]};
-      assert multiset(xs[1..]) == multiset(ys[1..]);
-      SortedUnique(xs[1..], ys[1..], R);
-    }
-  }
-
-  /* Converts a set to a sequence that is ordered w.r.t. a given total order. */
-  function SetToSortedSeq<T(!new)>(s: set<T>, R: (T, T) -> bool): (xs: seq<T>)
-    requires TotalOrdering(R)
-    ensures multiset(s) == multiset(xs)
-    ensures SortedBy(xs, R)
-  {
-    MergeSortBy(SetToSeqSpec(s), R)
-  } by method {
-    xs := SetToSeq(s);
-    xs := MergeSortBy(xs, R);
-    SortedUnique(xs, SetToSortedSeq(s, R), R);
-  }
-
-
   /****************************
    **  Sorting sequences
    ***************************** */