path: root/Source/Core/PureCollections.ssc

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

}