summaryrefslogtreecommitdiff
path: root/Source/Core/PureCollections.cs
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-08-20 22:29:44 +0000
committerGravatar tabarbe <unknown>2010-08-20 22:29:44 +0000
commitb617dda87871573b826dada4af73fc48dce94f15 (patch)
tree453088d59b99376c0b14035e76463a4561d6ec1c /Source/Core/PureCollections.cs
parent0d77cf304b9bd2b2152fe1a733e4533536c883c0 (diff)
Boogie: Renaming core sources in preparation for port commit
Diffstat (limited to 'Source/Core/PureCollections.cs')
-rw-r--r--Source/Core/PureCollections.cs785
1 files changed, 785 insertions, 0 deletions
diff --git a/Source/Core/PureCollections.cs b/Source/Core/PureCollections.cs
new file mode 100644
index 00000000..e6d68a34
--- /dev/null
+++ b/Source/Core/PureCollections.cs
@@ -0,0 +1,785 @@
+//-----------------------------------------------------------------------------
+//
+// 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 Microsoft.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)
+ 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) {
+ 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){
+ assert this.elems != null;
+ if (o == null || !(o is Tuple) || elems.Length != ((!)((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;
+ 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) {
+ assert this.elems != null;
+ if (o == null || !(o is Tuple) || elems.Length != ((!)((Tuple)o).elems).Length)
+ throw new MissingCase();
+
+ Tuple t = (Tuple) o;
+ for(int i = 0; i < elems.Length; i ++) {
+ int c = ((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{assert this.elems != null; return elems[index];}
+ set{assert this.elems != null; elems[index] = value;}
+ }
+
+ //ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+ [Pure]
+ public override string! ToString() {
+ assert this.elems != null;
+ if (elems.Length==0)
+ return "()";
+
+ string s = "(";
+ for (int i= 0; i< elems.Length-1; i++)
+ s += ((!)elems[i]).ToString() + ", ";
+ return s + ((!)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{assert this.elems != null; return elems[0];}
+ set{assert this.elems != null; elems[0]=value;}
+ }
+ public object Second{
+ get{assert this.elems != null; return elems[1];}
+ set{assert this.elems != null; elems[1]=value;}
+ }
+ }
+
+ // --------------------------------------------------------------------
+ // Map
+ // --------------------------------------------------------------------
+
+ public class MapEnumerator: IEnumerator{
+ private Map! map;
+ private int index = -1;
+ public MapEnumerator(Map! m) { map = m;}
+ public bool MoveNext() {
+ do{
+ index++;
+ assert map.elems != null;
+ } while (index < map.elems.Length && map.elems[index] == null);
+ return index < map.elems.Length;
+ }
+ public object Current{ get { 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;
+
+ //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){
+ elems = new Object[ps.Length*2];
+ vals = new Object[ps.Length*2];
+ base();
+ card = 0;
+ for(int i = 0; i < ps.Length; i++)
+ Insert( ((!)ps[i]).First, ((!)ps[i]).Second);
+ }
+
+ // iterators - - - - - - - - - - - - - - - - - - - - - - - - - - -
+ [Pure] [GlobalAccess(false)] [Escapes(true,false)]
+ public IEnumerator! GetEnumerator() {
+ return new MapEnumerator(this);
+ }
+ public Pair[] ToArray() {
+ Pair [] n = new Pair[card];
+ int ct = 0;
+ 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));
+ 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) {
+ 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();
+
+ 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() {
+ if (card ==0)
+ return "{|->}";
+ else {
+ string s = "{"; int ct = 0;
+ assert this.elems != null;
+ for(int i =0; i < elems.Length ; i++) {
+ object elem = elems[i];
+ if (elem != null){
+ s += elem.ToString() +"|->" + ((!)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;
+ 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;
+ assert this.elems != null;
+ for(int i = 0; i < elems.Length; i++)
+ {
+ object elem = elems[i];
+ if (elem != null)
+ {
+ h += elem.GetHashCode() + ((!)vals[i]).GetHashCode();
+ }
+ }
+ return h;
+ }
+
+ //Ordinary map operations- - - - - - - - - - - - - - - - - - - - - - - -
+
+ [Pure]
+ public bool Has(Object x) {
+ if (x == null)
+ throw new MissingCase();
+
+ 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();
+ 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) {
+ Map m = new Map(new Capacity(s.card+t.card));
+ 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]);
+ 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;
+ private int index = -1;
+ [Captured]
+ public SequenceEnumerator(Sequence! s) { seq = s;}
+ public bool MoveNext() {
+ index++;
+ //while (index < seq.elems.Length); // Sequences allow nils ... && seq.elems[index] == null);
+ return index < seq.Length;
+ }
+ public object Current{ get { 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){card = ds.Length; elems = ds; }
+ public Sequence(Sequence! seq) {
+ base(seq);
+ }
+ public Sequence(Capacity c){elems = new object [c.capacity];}
+
+ // Iterators - - - - - - - - - - - - - - - - - - - - - - - - - - -
+ [Pure] [GlobalAccess(false)] [Escapes(true,false)]
+ public IEnumerator! GetEnumerator()
+ ensures Owner.Same(result, this);
+ ensures result.IsNew;
+ {
+ return new SequenceEnumerator(this);
+ }
+
+ public object[] ToArray() {
+ object [] n = new object[card];
+ int ct = 0;
+ assert this.elems != null;
+ for(int i =0; i < elems.Length ; i++)
+ n[ct++] = elems[i];
+ return n;
+ }
+
+ //ASM Update - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+ public Sequence Update(int i, object v) {
+ Sequence n = new Sequence(new Capacity(card+1));
+ assert this.elems != null;
+ 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 Length {
+ get{return this.card;}
+ }
+
+ public object this[int index]{
+ get{assert this.elems != null; return this.elems[index];}
+ set{assert this.elems != null; this.elems[index] = value;}
+ }
+
+ public void Add(object o){
+ 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){
+ foreach (object o in seq) {
+ Add(o);
+ }
+ }
+
+ public void Remove(){
+ if (card == 0)
+ return;
+ card--;
+ }
+
+ // remove the first occurrence of o from this sequence
+ public void Remove(Object x) {
+ if (x == null)
+ throw new MissingCase();
+ assert this.elems != null;
+ for (int i = 0; i < card; i++) {
+ if (x.Equals(elems[i])) {
+ ++i;
+ while (i < card) {
+ elems[i-1] = elems[i];
+ ++i;
+ }
+ card--;
+ elems[card] = null;
+ return;
+ }
+ }
+ }
+
+ public void Truncate(int newLen)
+ requires 0 <= newLen && newLen <= Length;
+ {
+ assert elems != null;
+ for (int i = newLen; i < card; i++) {
+ elems[i] = null;
+ }
+ card = newLen;
+ }
+
+ //ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -
+ [Pure]
+ public override string! ToString() {
+ string s ="";
+ 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;
+ assert s.elems != null;
+ 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++)
+ {
+ 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;
+ assert s.elems != null;
+ 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;
+ assert s.elems != null;
+ 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 Has(object x) { // WS translate to tailrecursion
+ if (x == null)
+ throw new MissingCase();
+ 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();
+ 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();
+ assert this.elems != null;
+ for (int i = card - 1; i >= 0; i--)
+ if (x.Equals(elems[i]))
+ return i;
+ return -1;
+ }
+
+ public object Head() {assert this.elems != null; return elems[0]; }
+ public object Last() {assert this.elems != null; return elems[card-1]; }
+
+ public static Sequence Tail(Sequence! s) {
+ Sequence n = new Sequence(new Capacity(s.card-1));
+ assert n.elems != null;
+ 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) {
+ Sequence n = new Sequence(new Capacity(s.card-1));
+ assert n.elems != null;
+ 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) {
+ Sequence n = new Sequence(new Capacity(s.card));
+ assert n.elems != null;
+ assert s.elems != null;
+ for (int i = 0; i< s.card; i++) {
+ Sequence t = (Sequence!) s.elems[i];
+ 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) {
+ Sequence n = new Sequence(new Capacity(s.card));
+ assert n.elems != null;
+ 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) {
+ Sequence! n = new Sequence(new Capacity(s.card + t.card));
+ assert n.elems != null;
+ assert s.elems != null;
+ 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) {
+ int min = s.card<t.card ? s.card : t.card;
+ Sequence n = new Sequence(new Capacity(min));
+ assert n.elems != null;
+ assert s.elems != null;
+ 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) {
+ Sequence n0 = new Sequence(new Capacity(s.card));
+ Sequence n1 = new Sequence(new Capacity(s.card));
+ assert s.elems != null;
+ assert n0.elems != null;
+ assert n1.elems != null;
+ for (int i = 0; i< s.card; i++) {
+ n0.elems[n0.card++] = ((!)((Tuple!)s.elems[i]).elems)[0];
+ n1.elems[n1.card++] = ((!)((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));
+ 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;
+ }
+
+ }
+
+}