Removed the remaining pure collections.

5 files changed, 26 insertions, 932 deletions

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index f3db4f9a..6d5b7bd9 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -167,7 +167,6 @@
     <Compile Include="OOLongUtil.cs" />

     <Compile Include="OwickiGries.cs" />

     <Compile Include="Parser.cs" />

-    <Compile Include="PureCollections.cs" />

     <Compile Include="ResolutionContext.cs" />

     <Compile Include="Scanner.cs" />

     <Compile Include="StandardVisitor.cs" />

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 356ff272..9d20c15e 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -1,7 +1,6 @@
 using System;

 using System.Collections.Generic;

 using Microsoft.Boogie.GraphUtil;

-using PureCollections;

 using System.Diagnostics.Contracts;

 

 

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index fa15b100..310e3cc0 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1,4 +1,3 @@
-using PureCollections;

 using System.Collections;

 using System.Collections.Generic;

 using System.IO;

diff --git a/Source/Core/PureCollections.cs b/Source/Core/PureCollections.cs
deleted file mode 100644
index 8eafd73f..00000000
--- a/Source/Core/PureCollections.cs
+++ /dev/null
@@ -1,923 +0,0 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-

-//---------------------------------------------------------------------

-// PureCollections.cs

-//       - Mostly pure functions for tuples, sets, maps, Sequences

-// Version 1.0, WS, 3/23/2002 

-//---------------------------------------------------------------------

-

-

-using System;

-using System.Collections;

-using System.Diagnostics.Contracts;

-

-namespace PureCollections {

-  //-------------------------------------------------------------------

-  // General types

-  //-------------------------------------------------------------------

-

-  public class MissingCase : Exception {

-  }

-

-  public struct Capacity {

-    public int capacity;

-    public Capacity(int i) {

-      capacity = i;

-    }

-  }

-

-  abstract public class Coll {

-    public object[] elems;      // null is used to show empty spots!

-    protected int card;

-    protected Coll() {

-    }

-    protected Coll(object[] elems, int card) {

-      this.elems = elems;

-      this.card = card;

-    }

-    protected Coll(Coll c) {

-      Contract.Requires(c != null);

-      Contract.Requires(c.elems != null);

-      this.elems = (object[])c.elems.Clone();

-      this.card = c.card;

-    }

-  }

-

-

-  // ------------------------------------------------------------------

-  // Tuple

-  // ------------------------------------------------------------------

-

-  public class Tuple : Coll, IComparable {

-    //public object[] elems;

-

-    //invariant this.elems != null;

-

-    // Constructor - - - - - - - - - - - - - - - - - - - - - - - - - - 

-    public Tuple(params object[] ts) {

-      Contract.Requires(ts != null);

-      elems = ts;

-      card = ts.Length;

-    }

-    public Tuple(Capacity c) {

-      elems = new object[c.capacity];

-      card = c.capacity;

-    }

-

-    //Equality - - - - - - - - - - - - - - - - - - - - - - - - - - - - 

-

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]

-    public override bool Equals(object o) {

-      Contract.Assert(this.elems != null);

-      if (o == null || !(o is Tuple) || elems.Length != (cce.NonNull((Tuple)o).elems).Length)

-        return false;

-

-      Tuple s = (Tuple)o;

-      for (int i = 0; i < elems.Length; i++)

-        if (!Equals(this.elems[i], s.elems[i]))

-          return false;

-      return true;

-    }

-

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]  // ugh, is this right?  --KRML

-    public static bool operator ==(Tuple s, Tuple t) {

-      return s == null ? t == null : s.Equals(t);

-    }

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]  // ugh, is this right?  --KRML

-    public static bool operator !=(Tuple s, Tuple t) {

-      return !(t == s);

-    }

-

-    [Pure]

-    public override int GetHashCode() {

-      int h = 0;

-      Contract.Assume(this.elems != null);

-      for (int i = 0; i < elems.Length; i++) {

-        object elem = elems[i];

-        if (elem != null)

-          h += elem.GetHashCode();

-      }

-      return h;

-    }

-

-    //Compare - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

-    int IComparable.CompareTo(object o) {

-      Contract.Assert(this.elems != null);

-      if (o == null || !(o is Tuple) || elems.Length != (cce.NonNull((Tuple)o).elems).Length)

-        throw new MissingCase();

-

-      Tuple t = (Tuple)o;

-      for (int i = 0; i < elems.Length; i++) {

-        int c = cce.NonNull((IComparable)elems[i]).CompareTo(t.elems[i]);

-        if (c < 0)

-          return -1;

-        else if (c > 0)

-          return +1;

-      }

-      return 0;

-    }

-

-    public static bool operator <=(Tuple s, Tuple t) {

-      return s == null ? t == null : ((IComparable)s).CompareTo(t) <= 0;

-    }

-    public static bool operator <(Tuple s, Tuple t) {

-      return s == null ? false : ((IComparable)s).CompareTo(t) < 0;

-    }

-    public static bool operator >=(Tuple s, Tuple t) {

-      return t <= s;

-    }

-    public static bool operator >(Tuple s, Tuple t) {

-      return t < s;

-    }

-

-    //Select and Update - - - - - - - - - - - - - - - - - - - - - - - -

-    public object this[int index] {

-      get {

-        Contract.Assert(this.elems != null);

-        return elems[index];

-      }

-      set {

-        Contract.Assert(this.elems != null);

-        elems[index] = value;

-      }

-    }

-

-    //ToString - - - -  - - - - - - - - - - - - - - - - - - - - - - - -

-    [Pure]

-    public override string ToString() {

-      Contract.Ensures(Contract.Result<string>() != null);

-      Contract.Assert(this.elems != null);

-      if (elems.Length == 0)

-        return "()";

-

-      string s = "(";

-      for (int i = 0; i < elems.Length - 1; i++)

-        s += cce.NonNull(elems[i]).ToString() + ", ";

-      return s + cce.NonNull(elems[elems.Length - 1]).ToString() + ")";

-    }

-  }

-

-  // ------------------------------------------------------------------

-  // Pair

-  public class Pair : Tuple {

-    protected Pair() {

-    }

-    public Pair(object first, object second) {

-      elems = new object[] { first, second };

-    }

-    public object First {

-      get {

-        Contract.Assert(this.elems != null);

-        return elems[0];

-      }

-      set {

-        Contract.Assert(this.elems != null);

-        elems[0] = value;

-      }

-    }

-    public object Second {

-      get {

-        Contract.Assert(this.elems != null);

-        return elems[1];

-      }

-      set {

-        Contract.Assert(this.elems != null);

-        elems[1] = value;

-      }

-    }

-  }

-

-  // --------------------------------------------------------------------

-  // Map

-  // --------------------------------------------------------------------

-

-  public class MapEnumerator : IEnumerator {

-    private Map/*!*/ map;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(map != null);

-    }

-

-    private int index = -1;

-    public MapEnumerator(Map m) {

-      Contract.Requires(m != null);

-      map = m;

-    }

-    public bool MoveNext() {

-      do {

-        index++;

-        Contract.Assert(map.elems != null);

-      } while (index < map.elems.Length && map.elems[index] == null);

-      return index < map.elems.Length;

-    }

-    public object Current {

-      get {

-        Contract.Assert(map.elems != null);

-        return new Pair(map.elems[index], map.vals[index]);

-      }

-    }

-    public void Reset() {

-      index = -1;

-    }

-  }

-

-  public class Map : Coll, IEnumerable, IComparable {

-    public Object[]/*!*/ vals;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(vals != null);

-    }

-

-

-    //invariant this.elems != null;

-

-    // constructors - - - - - - - - - - - - - - - - - - - - - - - - - - - 

-    public Map(Capacity c) {

-      elems = new Object[c.capacity * 2];

-      vals = new Object[c.capacity * 2];

-      card = 0;

-    }

-

-    [NotDelayed]

-    public Map(params Pair[] ps)

-      : base() {

-      Contract.Requires(ps != null);

-      elems = new Object[ps.Length * 2];

-      vals = new Object[ps.Length * 2];

-      card = 0;

-      for (int i = 0; i < ps.Length; i++)

-        Insert(cce.NonNull(ps[i]).First, cce.NonNull(ps[i]).Second);

-    }

-

-    // iterators - - - - - - - - - - - - - - - - - - - - - - - - - - - 

-    [Pure]

-    [GlobalAccess(false)]

-    [Escapes(true, false)]

-    public IEnumerator GetEnumerator() {

-      Contract.Ensures(Contract.Result<IEnumerator>() != null);

-      return new MapEnumerator(this);

-    }

-    public Pair[] ToArray() {

-      Pair[] n = new Pair[card];

-      int ct = 0;

-      Contract.Assert(this.elems != null);

-      for (int i = 0; i < elems.Length; i++)

-        if (elems[i] != null)

-          n[ct++] = new Pair(elems[i], vals[i]);

-      return n;

-    }

-

-    //(ASM) Update- - - - - - - - - - - - - - - - - - - - - - - - - - -

-    public Map Update(object k, object v) {

-      Map n = new Map(new Capacity(card + 1));

-      Contract.Assert(this.elems != null);

-      for (int i = 0; i < elems.Length; i++)

-        if (elems[i] != null && !Equals(elems[i], k))

-          n.Insert(elems[i], vals[i]);

-      n.Insert(k, v);

-      return n;

-    }

-

-    //In place Update (and Remove)- - - - - - - - - - - - - - - - - - -

-    public object this[object index] {

-      get {

-        return this.Apply(index);

-      }

-      set {

-        this.Insert(index, value);

-      }

-    }

-

-    public void Remove(object o) {

-      Contract.Requires(o != null);

-      Contract.Assert(this.elems != null);

-      int h = Math.Abs(o.GetHashCode()) % elems.Length;

-      for (int i = 0; i < elems.Length; i++) {

-        int j = (i + h) % elems.Length;

-        if (elems[j] == null) {

-          break;

-        } else if (Equals(elems[j], o)) {

-          elems[j] = null;

-          vals[j] = null;

-          break;

-        }

-      }

-    }

-

-    public void Insert(Object key, Object val) {

-      if (key == null)

-        throw new MissingCase();

-

-      Contract.Assert(this.elems != null);

-      if (elems.Length == 0 || 2 * card >= elems.Length) {

-        int m = card * 2;

-        if (m < 4)

-          m = 4;

-        object[] newElems = new object[m];

-        object[] newVals = new object[m];

-        for (int k = 0; k < elems.Length; k++) {

-          object elem = elems[k];

-          if (elem != null) {

-            int newHash = Math.Abs(elem.GetHashCode()) % newElems.Length;

-            for (int i = 0; i < newElems.Length; i++) {

-              int j = (i + newHash) % newElems.Length;

-              if (newElems[j] == null) {

-                newElems[j] = elem;

-                newVals[j] = vals[k];

-                break;

-              }

-            }

-          }

-        }

-        elems = newElems;

-        vals = newVals;

-      }

-      int h = Math.Abs(key.GetHashCode()) % elems.Length;

-      for (int i = 0; i < elems.Length; i++) {

-        int j = (i + h) % elems.Length;

-        if (elems[j] == null) {

-          elems[j] = key;

-          vals[j] = val;

-          card++;

-          return;

-        } else if (key.Equals(elems[j])) {

-          vals[j] = val;

-          return;

-        }

-      }

-    }

-

-    //ToString - - - - - - - - - - - - - - - - - - - - - - - - -

-    [Pure]

-    public override string ToString() {

-      Contract.Ensures(Contract.Result<string>() != null);

-      if (card == 0)

-        return "{|->}";

-      else {

-        string s = "{";

-        int ct = 0;

-        Contract.Assert(this.elems != null);

-        for (int i = 0; i < elems.Length; i++) {

-          object elem = elems[i];

-          if (elem != null) {

-            s += elem.ToString() + "|->" + cce.NonNull(vals[i]).ToString();

-            s += (ct != card - 1) ? ", " : "";

-            ct++;

-          }

-        }

-        return s + "}";

-      }

-    }

-

-    // Subset operations - - - - - - - - - - - - - - - - - - - - - - -

-    // View Map as Set of Pairs

-

-    int IComparable.CompareTo(object o) {

-      if (o == null || !(o is Map))

-        throw new MissingCase();

-      // WS Improve performance!

-      Map t = (Map)o;

-      if (this < t)

-        return -1;

-      else if (this > t)

-        return +1;

-      else

-        return 0;

-    }

-    public static bool operator <=(Map s, Map t) {

-      if (s == null)

-        return t == null;

-      if (t == null)

-        return false;

-      Contract.Assert(s.elems != null);

-      for (int i = 0; i < s.elems.Length; i++)

-        if (s.elems[i] != null) {

-          object o = t.Apply(s.elems[i]);

-          if (o == null || !o.Equals(s.vals[i]))

-            return false;

-        }

-      return true;

-    }

-    public static bool operator <(Map s, Map t) {

-      return s == null || t == null ? false : s.card < t.card && s <= t;

-    }

-    public static bool operator >=(Map s, Map t) {

-      return t <= s;

-    }

-    public static bool operator >(Map s, Map t) {

-      return t < s;

-    }

-

-    // Equality - - - - - - - - - - - - - - - - - - - - - - -

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]

-    public override bool Equals(Object t) {

-      return t != null && t is Map && card == ((Map)t).card && this <= ((Map)t);

-    }

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]  // ugh, is this right?  --KRML

-    public static bool operator ==(Map s, Map t) {

-      if ((object)s == null)

-        if ((object)t == null)

-          return true;

-        else

-          return t.Equals(s);

-      else

-        return s.Equals(t);

-    }

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]  // ugh, is this right?  --KRML

-    public static bool operator !=(Map s, Map t) {

-      return !(t == s);

-    }

-    [Pure]

-    public override int GetHashCode() {

-      int h = 0;

-      Contract.Assert(this.elems != null);

-      for (int i = 0; i < elems.Length; i++) {

-        object elem = elems[i];

-        if (elem != null) {

-          h += elem.GetHashCode() + cce.NonNull(vals[i]).GetHashCode();

-        }

-      }

-      return h;

-    }

-

-    //Ordinary map operations- - - - - - - - - - - - - - - - - - - - - - - - 

-

-    [Pure]

-    public bool Has(Object x) {

-      if (x == null)

-        throw new MissingCase();

-

-      Contract.Assert(this.elems != null);

-      if (elems.Length == 0)

-        return false;

-      int h = Math.Abs(x.GetHashCode()) % elems.Length;

-      for (int i = 0; i < elems.Length; i++) {

-        int j = (i + h) % elems.Length;

-        if (x.Equals(elems[j]))

-          return true;

-      }

-      return false;

-    }

-

-    public object Apply(object x) {

-      if (x == null)

-        throw new MissingCase();

-      Contract.Assert(this.elems != null);

-      if (elems.Length == 0)

-        return null;

-      int h = Math.Abs(x.GetHashCode()) % elems.Length;

-      for (int i = 0; i < elems.Length; i++) {

-        int j = (i + h) % elems.Length;

-        if (elems[j] != null && x.Equals(elems[j]))

-          return vals[j];

-      }

-      return null;

-    }

-

-    public static Map Override(Map s, Map t) {

-      Contract.Requires(t != null);

-      Contract.Requires(s != null);

-      Map m = new Map(new Capacity(s.card + t.card));

-      Contract.Assert(s.elems != null);

-      for (int i = 0; i < s.elems.Length; i++)

-        if (s.elems[i] != null)

-          m.Insert(s.elems[i], s.vals[i]);

-      Contract.Assert(t.elems != null);

-      for (int i = 0; i < t.elems.Length; i++)

-        if (t.elems[i] != null)

-          m.Insert(t.elems[i], t.vals[i]);

-      return m;

-    }

-  }

-

-  // --------------------------------------------------------------------

-  // Sequence

-

-  public class SequenceEnumerator : IEnumerator {

-    [Peer]

-    private Sequence/*!*/ seq;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(seq != null);

-    }

-

-    private int index = -1;

-    [Captured]

-    public SequenceEnumerator(Sequence s) {

-      Contract.Requires(s != null);

-      seq = s;

-    }

-    public bool MoveNext() {

-      index++;

-      //while (index < seq.elems.Length); // Sequences allow nils ... && seq.elems[index] == null);

-      return index < seq.Count;

-    }

-    public object Current {

-      get {

-        Contract.Assert(seq.elems != null);

-        return seq.elems[index];

-      }

-    }

-    public void Reset() {

-      index = -1;

-    }

-  }

-

-  public class Sequence : Coll, IEnumerable, IComparable {

-    public Sequence() {

-      elems = new object[4];

-    }

-

-    //invariant this.elems != null;

-

-    //constructors - - - - - - - - - - - - - - - - - - - - - - - - - - - 

-    public Sequence(params object[] ds) {

-      Contract.Requires(ds != null);

-      card = ds.Length;

-      elems = ds;

-    }

-    public Sequence(Sequence seq)

-      : base(seq) {

-      Contract.Requires(seq != null);

-    }

-    public Sequence(Capacity c) {

-      elems = new object[c.capacity];

-    }

-

-    // Iterators - - - - - - - - - - - - - - - - - - - - - - - - - - - 

-    [Pure]

-    [GlobalAccess(false)]

-    [Escapes(true, false)]

-    public IEnumerator/*!*/ GetEnumerator() {

-      Contract.Ensures(cce.Owner.Same(Contract.Result<IEnumerator>(), this));

-      Contract.Ensures(Contract.Result<IEnumerator>() != null);

-      Contract.Ensures(cce.IsNew(Contract.Result<IEnumerator>()));

-      return new SequenceEnumerator(this);

-    }

-

-    public object[] ToArray() {

-      object[] n = new object[card];

-      int ct = 0;

-      Contract.Assert(this.elems != null);

-      for (int i = 0; i < card; i++)

-        n[ct++] = elems[i];

-      return n;

-    }

-

-    //ASM Update - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

-    public Sequence Update(int i, object v) {

-      Sequence n = new Sequence(new Capacity(card + 1));

-      Contract.Assert(this.elems != null);

-      Contract.Assert(n.elems != null);

-      for (int j = 0; j < elems.Length; j++)

-        n.elems[j] = elems[j];

-      if (i >= 0 && i < card) {

-        n.elems[i] = v;

-        n.card = card;

-        return n;

-      } else if (i == card) {

-        n.elems[i] = v;

-        n.card = card + 1;

-        return n;

-      } else

-        throw new Exception("Sequence Update out of range");

-    }

-

-    //In place Update (and Remove) and Length - - - - - - - - - - - - - - - 

-    public int Count {

-      get {

-        return this.card;

-      }

-    }

-

-    public object this[int index] {

-      get {

-        Contract.Assert(this.elems != null);

-        return this.elems[index];

-      }

-      set {

-        Contract.Assert(this.elems != null);

-        this.elems[index] = value;

-      }

-    }

-

-    public void Add(object o) {

-      Contract.Assert(this.elems != null);

-      int n = this.elems.Length;

-      int i = this.card++;

-      if (i == n) {

-        int m = n * 2;

-        if (m < 4)

-          m = 4;

-        object[] newElems = new object[m];

-        for (int j = 0; j < n; j++)

-          newElems[j] = elems[j];

-        elems = newElems;

-      }

-      elems[i] = o;

-    }

-

-    public void AddRange(Sequence seq) {

-      Contract.Requires(seq != null);

-      foreach (object o in seq) {

-        Add(o);

-      }

-    }

-

-    //ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -

-    [Pure]

-    public override string ToString() {

-      Contract.Ensures(Contract.Result<string>() != null);

-      string s = "";

-      if (this.elems == null)

-        return "(null)";

-      Contract.Assert(this.elems != null);

-      if (card > 0 && elems[0] is Char) {

-        for (int i = 0; i < card; i++) {

-          object elem = elems[i];

-          if (elem != null) {

-            s += elem.ToString();

-          }

-        }

-        return s;

-      } else {

-        s = "[";

-        for (int i = 0; i < card - 1; i++) {

-          object elem = elems[i];

-          if (elem != null) {

-            s += elem.ToString() + ", ";

-          }

-        }

-        if (card > 0) {

-          object last = elems[card - 1];

-          if (last != null) {

-            s += last.ToString();

-          }

-        }

-        s += "]";

-        return s;

-      }

-    }

-    //Equality- - - - - - - - - - - - - - - - - - - - - - - - - - - - - 

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]

-    public override bool Equals(object that) {

-      return that != null && that is Sequence && ((Sequence)this == (Sequence)that);

-    }

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]  // ugh, is this right?  --KRML

-    public static bool operator ==(Sequence s, Sequence t) {

-      if ((object)s == (object)t) {

-        return true;

-      } else if ((object)s == null || (object)t == null) {

-        return false;

-      }

-      if (s.card != t.card)

-        return false;

-      Contract.Assert(s.elems != null);

-      Contract.Assert(t.elems != null);

-      for (int i = 0; i < s.card; i++)

-        if (!Equals(s.elems[i], t.elems[i]))

-          return false;

-      return true;

-    }

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]  // ugh, is this right?  --KRML

-    public static bool operator !=(Sequence s, Sequence t) {

-      return !(s == t);

-    }

-    [Pure]

-    public override int GetHashCode() {

-      int h = 0;

-      for (int i = 0; i < card; i++) {

-        Contract.Assert(this.elems != null);

-        object elem = elems[i];

-        if (elem != null) {

-          h += elem.GetHashCode();

-        }

-      }

-      return h;

-    }

-    //Subset- - - - - - - - - - - - - - - - - - - - - - - - - - - - - 

-    // View Sequence of T as Set of (Integer,T) 

-    int IComparable.CompareTo(object o) {

-      if (o == null || !(o is Sequence))

-        throw new MissingCase();

-      // WS Improve performance!

-      Sequence t = (Sequence)o;

-      if (this < t)

-        return -1;

-      else if (this > t)

-        return +1;

-      else

-        return 0;

-    }

-

-    public static bool operator <(Sequence s, Sequence t) {

-      if (s == null)

-        throw new ArgumentNullException("s");

-      if (t == null)

-        throw new ArgumentNullException("t");

-      if (s.card >= t.card)

-        return false;

-      Contract.Assert(s.elems != null);

-      Contract.Assert(t.elems != null);

-      for (int i = 0; i < s.card; i++)

-        if (!Equals(s.elems[i], t.elems[i]))

-          return false;

-      return true;

-    }

-    public static bool operator <=(Sequence s, Sequence t) {

-      if (s == null)

-        throw new ArgumentNullException("s");

-      if (t == null)

-        throw new ArgumentNullException("t");

-      if (s.card > t.card)

-        return false;

-      Contract.Assert(s.elems != null);

-      Contract.Assert(t.elems != null);

-      for (int i = 0; i < s.card; i++)

-        if (!Equals(s.elems[i], t.elems[i]))

-          return false;

-      return true;

-    }

-    public static bool operator >(Sequence s, Sequence t) {

-      return t < s;

-    }

-    public static bool operator >=(Sequence s, Sequence t) {

-      return t <= s;

-    }

-

-    //pure---------------------------------------------------------------

-    [Pure]

-    public bool Contains(object x) {         // WS translate to tailrecursion 

-      if (x == null)

-        throw new MissingCase();

-      Contract.Assert(this.elems != null);

-      for (int i = 0; i < card; i++)

-        if (x.Equals(elems[i]))

-          return true;

-      return false;

-    }

-

-    // the index of the first occurrence of x in this sequence,

-    // or -1 if x does not occur

-    [Pure]

-    public int IndexOf(object x) {

-      if (x == null)

-        throw new MissingCase();

-      Contract.Assert(this.elems != null);

-      for (int i = 0; i < card; i++)

-        if (x.Equals(elems[i]))

-          return i;

-      return -1;

-    }

-

-    // the index of the last occurrence of x in this sequence,

-    // or -1 if x does not occur

-    [Pure]

-    public int LastIndexOf(object x) {

-      if (x == null)

-        throw new MissingCase();

-      Contract.Assert(this.elems != null);

-      for (int i = card - 1; i >= 0; i--)

-        if (x.Equals(elems[i]))

-          return i;

-      return -1;

-    }

-

-    public object Head() {

-      Contract.Assert(this.elems != null);

-      return elems[0];

-    }

-    public object Last() {

-      Contract.Assert(this.elems != null);

-      return elems[card - 1];

-    }

-

-    public static Sequence Tail(Sequence s) {

-      Contract.Requires(s != null);

-      Sequence n = new Sequence(new Capacity(s.card - 1));

-      Contract.Assert(n.elems != null);

-      Contract.Assert(s.elems != null);

-      for (int i = 1; i < s.card; i++)

-        n.elems[n.card++] = s.elems[i];

-      return n;

-    }

-

-    public static Sequence Front(Sequence s) {

-      Contract.Requires(s != null);

-      Sequence n = new Sequence(new Capacity(s.card - 1));

-      Contract.Assert(n.elems != null);

-      Contract.Assert(s.elems != null);

-      for (int i = 0; i < s.card - 1; i++)

-        n.elems[n.card++] = s.elems[i];

-      return n;

-    }

-    public static Sequence Concat(Sequence s) {

-      Contract.Requires(s != null);

-      Sequence n = new Sequence(new Capacity(s.card));

-      Contract.Assert(n.elems != null);

-      Contract.Assert(s.elems != null);

-      for (int i = 0; i < s.card; i++) {

-        Sequence t = (Sequence)cce.NonNull(s.elems[i]);

-        Contract.Assert(t.elems != null);

-        for (int j = 0; j < t.card; j++)

-          n.Add(t.elems[j]);

-      }

-      return n;

-    }

-

-    public static Sequence Reverse(Sequence s) {

-      Contract.Requires(s != null);

-      Sequence n = new Sequence(new Capacity(s.card));

-      Contract.Assert(n.elems != null);

-      Contract.Assert(s.elems != null);

-      for (int i = s.card - 1; i >= 0; i--)

-        n.elems[n.card++] = s.elems[i];

-      return n;

-    }

-

-    public static Sequence operator +(Sequence s, Sequence t) {

-      if (s == null)

-        throw new ArgumentNullException("s");

-      if (t == null)

-        throw new ArgumentNullException("t");

-      return Append(t, s);

-    }

-

-    public static Sequence Append(Sequence s, Sequence t) {

-      Contract.Requires(t != null);

-      Contract.Requires(s != null);

-      Contract.Ensures(Contract.Result<Sequence>() != null);

-      Sequence n = new Sequence(new Capacity(s.card + t.card));

-      Contract.Assert(n != null);

-      Contract.Assert(n.elems != null);

-      Contract.Assert(s.elems != null);

-      Contract.Assert(t.elems != null);

-      for (int i = 0; i < s.card; i++)

-        n.elems[n.card++] = s.elems[i];

-      for (int i = 0; i < t.card; i++)

-        n.elems[n.card++] = t.elems[i];

-      return n;

-    }

-    public static Sequence Zip(Sequence s, Sequence t) {

-      Contract.Requires(t != null);

-      Contract.Requires(s != null);

-      int min = s.card < t.card ? s.card : t.card;

-      Sequence n = new Sequence(new Capacity(min));

-      Contract.Assert(n.elems != null);

-      Contract.Assert(s.elems != null);

-      Contract.Assert(t.elems != null);

-      for (int i = 0; i < min; i++)

-        n.elems[n.card++] = new Tuple(s.elems[i], t.elems[i]);

-      return n;

-    }

-    public static Tuple Unzip(Sequence s) {

-      Contract.Requires(s != null);

-      Sequence n0 = new Sequence(new Capacity(s.card));

-      Sequence n1 = new Sequence(new Capacity(s.card));

-      Contract.Assert(s.elems != null);

-      Contract.Assert(n0.elems != null);

-      Contract.Assert(n1.elems != null);

-      for (int i = 0; i < s.card; i++) {

-        n0.elems[n0.card++] = (cce.NonNull((Tuple)s.elems[i]).elems)[0];

-        n1.elems[n1.card++] = (cce.NonNull((Tuple)s.elems[i]).elems)[1];

-      }

-      return new Tuple(n0, n1);

-    }

-

-    public static Sequence FromTo(int from, int to) {       //WS hash the result! 

-      if (from > to)

-        return new Sequence();

-      Sequence n = new Sequence(new Capacity(to - from + 1));

-      Contract.Assert(n.elems != null);

-      for (int i = from; i <= to; i++)

-        n.elems[n.card++] = i;

-      return n;

-    }

-

-    public static Sequence FromStepTo(int from, int step, int to) {

-      Sequence n = new Sequence();

-      int incr = step - from;

-      if (incr > 0)

-        for (int i = from; i <= to; i += incr)

-          n.Add(i);

-      else if (incr < 0)

-        for (int i = to; i >= from; i -= incr)

-          n.Add(i);

-      return n;

-    }

-

-  }

-}
\ No newline at end of file
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 92d1fd14..fd7a4f72 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1120,7 +1120,7 @@ namespace VC {
             ss.Add(s0.blocks[0]);

             ss.Add(s1.blocks[0]);

             try {

-              best.SoundnessCheck(new HashSet<PureCollections.Tuple>(), best.blocks[0], ss);

+              best.SoundnessCheck(new HashSet<List<Block>>(new BlockListComparer()), best.blocks[0], ss);

             } catch (System.Exception e) {

               Console.WriteLine(e);

               best.DumpDot(-1);

@@ -1149,6 +1149,28 @@ namespace VC {
         return res;

       }

 

+      class BlockListComparer : IEqualityComparer<List<Block>>

+      {

+        public bool Equals(List<Block> x, List<Block> y)

+        {

+          return x == y || x.SequenceEqual(y);

+        }

+

+        public int GetHashCode(List<Block> obj)

+        {

+          int h = 0;

+          Contract.Assume(obj != null);

+          foreach (var b in obj)

+          {

+            if (b != null)

+            {

+              h += b.GetHashCode();

+            }

+          }

+          return h;

+        }

+      }

+

       public Checker Checker {

         get {

           Contract.Ensures(Contract.Result<Checker>() != null);

@@ -1296,17 +1318,15 @@ namespace VC {
         checker.BeginCheck(desc, vc, reporter);

       }

 

-      private void SoundnessCheck(HashSet<PureCollections.Tuple/*!*/>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {

+      private void SoundnessCheck(HashSet<List<Block>/*!*/>/*!*/ cache, Block/*!*/ orig, List<Block/*!*/>/*!*/ copies) {

         Contract.Requires(cce.NonNull(cache));

         Contract.Requires(orig != null);

         Contract.Requires(copies != null);

         {

-          PureCollections.Tuple t = new PureCollections.Tuple(new PureCollections.Capacity(1 + copies.Count));

-          int i = 0;

-          t[i++] = orig;

+          var t = new List<Block> { orig };

           foreach (Block b in copies) {

             Contract.Assert(b != null);

-            t[i++] = b;

+            t.Add(b);

           }

           if (cache.Contains(t)) {

             return;