//----------------------------------------------------------------------------- // // 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 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; } } }