From f09fb9edbd4e6dfb064359887c17dd3dc1630302 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 12 Aug 2014 15:30:56 -0700
Subject: Forget the extra copy of DafnyRuntime.cs that gets copied into
 DafnyExtension

---
 Source/DafnyExtension/DafnyRuntime.cs | 751 ----------------------------------
 1 file changed, 751 deletions(-)
 delete mode 100644 Source/DafnyExtension/DafnyRuntime.cs

(limited to 'Source/DafnyExtension')

diff --git a/Source/DafnyExtension/DafnyRuntime.cs b/Source/DafnyExtension/DafnyRuntime.cs
deleted file mode 100644
index d6bd895a..00000000
--- a/Source/DafnyExtension/DafnyRuntime.cs
+++ /dev/null
@@ -1,751 +0,0 @@
-using System.Numerics;
-
-namespace Dafny
-{
-  using System.Collections.Generic;
-
-  public class Set<T>
-  {
-    Dictionary<T, bool> dict;
-    Set(Dictionary<T, bool> d) {
-      dict = d;
-    }
-    public static Set<T> Empty {
-      get {
-        return new Set<T>(new Dictionary<T, bool>(0));
-      }
-    }
-    public static Set<T> FromElements(params T[] values) {
-      Dictionary<T, bool> d = new Dictionary<T, bool>(values.Length);
-      foreach (T t in values)
-        d[t] = true;
-      return new Set<T>(d);
-    }
-    public static Set<T> FromCollection(ICollection<T> values) {
-      Dictionary<T, bool> d = new Dictionary<T, bool>();
-      foreach (T t in values)
-        d[t] = true;
-      return new Set<T>(d);
-    }
-    
-    public IEnumerable<T> Elements {
-      get {
-        return dict.Keys;
-      }
-    }
-    /// <summary>
-    /// This is an inefficient iterator for producing all subsets of "this".  Each set returned is the same
-    /// Set<T> object (but this Set<T> object is fresh; in particular, it is not "this").
-    /// </summary>
-    public IEnumerable<Set<T>> AllSubsets {
-      get {
-        // Start by putting all set elements into a list
-        var elmts = new List<T>();
-        elmts.AddRange(dict.Keys);
-        var n = elmts.Count;
-        var which = new bool[n];
-        var s = new Set<T>(new Dictionary<T, bool>(0));
-        while (true) {
-          yield return s;
-          // "add 1" to "which", as if doing a carry chain.  For every digit changed, change the membership of the corresponding element in "s".
-          int i = 0;
-          for (; i < n && which[i]; i++) {
-            which[i] = false;
-            s.dict.Remove(elmts[i]);
-          }
-          if (i == n) {
-            // we have cycled through all the subsets
-            break;
-          }
-          which[i] = true;
-          s.dict.Add(elmts[i], true);
-        }
-      }
-    }
-    public bool Equals(Set<T> other) {
-      return dict.Count == other.dict.Count && IsSubsetOf(other);
-    }
-    public override bool Equals(object other) {
-      return other is Set<T> && Equals((Set<T>)other);
-    }
-    public override int GetHashCode() {
-      return dict.GetHashCode();
-    }
-    public override string ToString() {
-      var s = "{";
-      var sep = "";
-      foreach (var t in dict.Keys) {
-        s += sep + t.ToString();
-        sep = ", ";
-      }
-      return s + "}";
-    }
-    public bool IsProperSubsetOf(Set<T> other) {
-      return dict.Count < other.dict.Count && IsSubsetOf(other);
-    }
-    public bool IsSubsetOf(Set<T> other) {
-      if (other.dict.Count < dict.Count)
-        return false;
-      foreach (T t in dict.Keys) {
-        if (!other.dict.ContainsKey(t))
-          return false;
-      }
-      return true;
-    }
-    public bool IsSupersetOf(Set<T> other) {
-      return other.IsSubsetOf(this);
-    }
-    public bool IsProperSupersetOf(Set<T> other) {
-      return other.IsProperSubsetOf(this);
-    }
-    public bool IsDisjointFrom(Set<T> other) {
-      Dictionary<T, bool> a, b;
-      if (dict.Count < other.dict.Count) {
-        a = dict; b = other.dict;
-      } else {
-        a = other.dict; b = dict;
-      }
-      foreach (T t in a.Keys) {
-        if (b.ContainsKey(t))
-          return false;
-      }
-      return true;
-    }
-    public bool Contains(T t) {
-      return dict.ContainsKey(t);
-    }
-    public Set<T> Union(Set<T> other) {
-      if (dict.Count == 0)
-        return other;
-      else if (other.dict.Count == 0)
-        return this;
-      Dictionary<T, bool> a, b;
-      if (dict.Count < other.dict.Count) {
-        a = dict; b = other.dict;
-      } else {
-        a = other.dict; b = dict;
-      }
-      Dictionary<T, bool> r = new Dictionary<T, bool>();
-      foreach (T t in b.Keys)
-        r[t] = true;
-      foreach (T t in a.Keys)
-        r[t] = true;
-      return new Set<T>(r);
-    }
-    public Set<T> Intersect(Set<T> other) {
-      if (dict.Count == 0)
-        return this;
-      else if (other.dict.Count == 0)
-        return other;
-      Dictionary<T, bool> a, b;
-      if (dict.Count < other.dict.Count) {
-        a = dict; b = other.dict;
-      } else {
-        a = other.dict; b = dict;
-      }
-      var r = new Dictionary<T, bool>();
-      foreach (T t in a.Keys) {
-        if (b.ContainsKey(t))
-          r.Add(t, true);
-      }
-      return new Set<T>(r);
-    }
-    public Set<T> Difference(Set<T> other) {
-      if (dict.Count == 0)
-        return this;
-      else if (other.dict.Count == 0)
-        return this;
-      var r = new Dictionary<T, bool>();
-      foreach (T t in dict.Keys) {
-        if (!other.dict.ContainsKey(t))
-          r.Add(t, true);
-      }
-      return new Set<T>(r);
-    }
-  }
-  public class MultiSet<T>
-  {
-    Dictionary<T, int> dict;
-    MultiSet(Dictionary<T, int> d) {
-      dict = d;
-    }
-    public static MultiSet<T> Empty {
-      get {
-        return new MultiSet<T>(new Dictionary<T, int>(0));
-      }
-    }
-    public static MultiSet<T> FromElements(params T[] values) {
-      Dictionary<T, int> d = new Dictionary<T, int>(values.Length);
-      foreach (T t in values) {
-        var i = 0;
-        if (!d.TryGetValue(t, out i)) {
-          i = 0;
-        }
-        d[t] = i + 1;
-      }
-      return new MultiSet<T>(d);
-    }
-    public static MultiSet<T> FromCollection(ICollection<T> values) {
-      Dictionary<T, int> d = new Dictionary<T, int>();
-      foreach (T t in values) {
-        var i = 0;
-        if (!d.TryGetValue(t, out i)) {
-          i = 0;
-        }
-        d[t] = i + 1;
-      }
-      return new MultiSet<T>(d);
-    }
-    public static MultiSet<T> FromSeq(Sequence<T> values) {
-      Dictionary<T, int> d = new Dictionary<T, int>();
-      foreach (T t in values.Elements) {
-        var i = 0;
-        if (!d.TryGetValue(t, out i)) {
-          i = 0;
-        }
-        d[t] = i + 1;
-      }
-      return new MultiSet<T>(d);
-    }
-    public static MultiSet<T> FromSet(Set<T> values) {
-      Dictionary<T, int> d = new Dictionary<T, int>();
-      foreach (T t in values.Elements) {
-        d[t] = 1;
-      }
-      return new MultiSet<T>(d);
-    }
-
-    public bool Equals(MultiSet<T> other) {
-      return other.IsSubsetOf(this) && this.IsSubsetOf(other);
-    }
-    public override bool Equals(object other) {
-      return other is MultiSet<T> && Equals((MultiSet<T>)other);
-    }
-    public override int GetHashCode() {
-      return dict.GetHashCode();
-    }
-    public override string ToString() {
-      var s = "multiset{";
-      var sep = "";
-      foreach (var kv in dict) {
-        var t = kv.Key.ToString();
-        for (int i = 0; i < kv.Value; i++) {
-          s += sep + t.ToString();
-          sep = ", ";
-        }
-      }
-      return s + "}";
-    }
-    public bool IsProperSubsetOf(MultiSet<T> other) {
-      return !Equals(other) && IsSubsetOf(other);
-    }
-    public bool IsSubsetOf(MultiSet<T> other) {
-      foreach (T t in dict.Keys) {
-        if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])
-          return false;
-      }
-      return true;
-    }
-    public bool IsSupersetOf(MultiSet<T> other) {
-      return other.IsSubsetOf(this);
-    }
-    public bool IsProperSupersetOf(MultiSet<T> other) {
-      return other.IsProperSubsetOf(this);
-    }
-    public bool IsDisjointFrom(MultiSet<T> other) {
-      foreach (T t in dict.Keys) {
-        if (other.dict.ContainsKey(t))
-          return false;
-      }
-      foreach (T t in other.dict.Keys) {
-        if (dict.ContainsKey(t))
-          return false;
-      }
-      return true;
-    }
-    public bool Contains(T t) {
-      return dict.ContainsKey(t);
-    }
-    public MultiSet<T> Union(MultiSet<T> other) {
-      if (dict.Count == 0)
-        return other;
-      else if (other.dict.Count == 0)
-        return this;
-      var r = new Dictionary<T, int>();
-      foreach (T t in dict.Keys) {
-        var i = 0;
-        if (!r.TryGetValue(t, out i)) {
-          i = 0;
-        }
-        r[t] = i + dict[t];
-      }
-      foreach (T t in other.dict.Keys) {
-        var i = 0;
-        if (!r.TryGetValue(t, out i)) {
-          i = 0;
-        }
-        r[t] = i + other.dict[t];
-      }
-      return new MultiSet<T>(r);
-    }
-    public MultiSet<T> Intersect(MultiSet<T> other) {
-      if (dict.Count == 0)
-        return this;
-      else if (other.dict.Count == 0)
-        return other;
-      var r = new Dictionary<T, int>();
-      foreach (T t in dict.Keys) {
-        if (other.dict.ContainsKey(t)) {
-          r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);
-        }
-      }
-      return new MultiSet<T>(r);
-    }
-    public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other
-      if (dict.Count == 0)
-        return this;
-      else if (other.dict.Count == 0)
-        return this;
-      var r = new Dictionary<T, int>();
-      foreach (T t in dict.Keys) {
-        if (!other.dict.ContainsKey(t)) {
-          r.Add(t, dict[t]);
-        } else if (other.dict[t] < dict[t]) {
-          r.Add(t, dict[t] - other.dict[t]);
-        }
-      }
-      return new MultiSet<T>(r);
-    }
-    public IEnumerable<T> Elements {
-      get {
-        List<T> l = new List<T>();
-        foreach (T t in dict.Keys) {
-          int n;
-          dict.TryGetValue(t, out n);
-          for (int i = 0; i < n; i ++) {
-            l.Add(t);
-          }
-        }
-        return l;
-      }
-    }
-  }
-
-  public class Map<U, V>
-  {
-    Dictionary<U, V> dict;
-    Map(Dictionary<U, V> d) {
-      dict = d;
-    }
-    public static Map<U, V> Empty {
-      get {
-        return new Map<U, V>(new Dictionary<U,V>());
-      }
-    }
-    public static Map<U, V> FromElements(params Pair<U, V>[] values) {
-      Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
-      foreach (Pair<U, V> p in values) {
-        d[p.Car] = p.Cdr;
-      }
-      return new Map<U, V>(d);
-    }
-    public static Map<U, V> FromCollection(List<Pair<U, V>> values) {
-      Dictionary<U, V> d = new Dictionary<U, V>(values.Count);
-      foreach (Pair<U, V> p in values) {
-        d[p.Car] = p.Cdr;
-      }
-      return new Map<U, V>(d);
-    }
-    public bool Equals(Map<U, V> other) {
-      foreach (U u in dict.Keys) {
-        V v1, v2;
-        if (!dict.TryGetValue(u, out v1)) {
-          return false; // this shouldn't happen
-        }
-        if (!other.dict.TryGetValue(u, out v2)) {
-          return false; // other dictionary does not contain this element
-        }
-        if (!v1.Equals(v2)) {
-          return false;
-        }
-      }
-      foreach (U u in other.dict.Keys) {
-        if (!dict.ContainsKey(u)) {
-          return false; // this shouldn't happen
-        }
-      }
-      return true;
-    }
-    public override bool Equals(object other) {
-      return other is Map<U, V> && Equals((Map<U, V>)other);
-    }
-    public override int GetHashCode() {
-      return dict.GetHashCode();
-    }
-    public override string ToString() {
-      var s = "map[";
-      var sep = "";
-      foreach (var kv in dict) {
-        s += sep + kv.Key.ToString() + " := " + kv.Value.ToString();
-        sep = ", ";
-      }
-      return s + "]";
-    }
-    public bool IsDisjointFrom(Map<U, V> other) {
-      foreach (U u in dict.Keys) {
-        if (other.dict.ContainsKey(u))
-          return false;
-      }
-      foreach (U u in other.dict.Keys) {
-        if (dict.ContainsKey(u))
-          return false;
-      }
-      return true;
-    }
-    public bool Contains(U u) {
-      return dict.ContainsKey(u);
-    }
-    public V Select(U index) {
-      return dict[index];
-    }
-    public Map<U, V> Update(U index, V val) {
-      Dictionary<U, V> d = new Dictionary<U, V>(dict);
-      d[index] = val;
-      return new Map<U, V>(d);
-    }
-    public IEnumerable<U> Domain {
-      get {
-        return dict.Keys;
-      }
-    }
-  }
-  public class Sequence<T>
-  {
-    T[] elmts;
-    public Sequence(T[] ee) {
-      elmts = ee;
-    }
-    public static Sequence<T> Empty {
-      get {
-        return new Sequence<T>(new T[0]);
-      }
-    }
-    public static Sequence<T> FromElements(params T[] values) {
-      return new Sequence<T>(values);
-    }
-    public BigInteger Length {
-      get { return new BigInteger(elmts.Length); }
-    }
-    public T[] Elements {
-      get {
-        return elmts;
-      }
-    }
-    public IEnumerable<T> UniqueElements {
-      get {
-        var st = Set<T>.FromElements(elmts);
-        return st.Elements;
-      }
-    }
-    public T Select(BigInteger index) {
-      return elmts[(int)index];
-    }
-    public Sequence<T> Update(BigInteger index, T t) {
-      T[] a = (T[])elmts.Clone();
-      a[(int)index] = t;
-      return new Sequence<T>(a);
-    }
-    public bool Equals(Sequence<T> other) {
-      int n = elmts.Length;
-      return n == other.elmts.Length && EqualUntil(other, n);
-    }
-    public override bool Equals(object other) {
-      return other is Sequence<T> && Equals((Sequence<T>)other);
-    }
-    public override int GetHashCode() {
-      return elmts.GetHashCode();
-    }
-    public override string ToString() {
-      var s = "[";
-      var sep = "";
-      foreach (var t in elmts) {
-        s += sep + t.ToString();
-        sep = ", ";
-      }
-      return s + "]";
-    }
-    bool EqualUntil(Sequence<T> other, int n) {
-      for (int i = 0; i < n; i++) {
-        if (!elmts[i].Equals(other.elmts[i]))
-          return false;
-      }
-      return true;
-    }
-    public bool IsProperPrefixOf(Sequence<T> other) {
-      int n = elmts.Length;
-      return n < other.elmts.Length && EqualUntil(other, n);
-    }
-    public bool IsPrefixOf(Sequence<T> other) {
-      int n = elmts.Length;
-      return n <= other.elmts.Length && EqualUntil(other, n);
-    }
-    public Sequence<T> Concat(Sequence<T> other) {
-      if (elmts.Length == 0)
-        return other;
-      else if (other.elmts.Length == 0)
-        return this;
-      T[] a = new T[elmts.Length + other.elmts.Length];
-      System.Array.Copy(elmts, 0, a, 0, elmts.Length);
-      System.Array.Copy(other.elmts, 0, a, elmts.Length, other.elmts.Length);
-      return new Sequence<T>(a);
-    }
-    public bool Contains(T t) {
-      int n = elmts.Length;
-      for (int i = 0; i < n; i++) {
-        if (t.Equals(elmts[i]))
-          return true;
-      }
-      return false;
-    }
-    public Sequence<T> Take(BigInteger n) {
-      int m = (int)n;
-      if (elmts.Length == m)
-        return this;
-      T[] a = new T[m];
-      System.Array.Copy(elmts, a, m);
-      return new Sequence<T>(a);
-    }
-    public Sequence<T> Drop(BigInteger n) {
-      if (n.IsZero)
-        return this;
-      int m = (int)n;
-      T[] a = new T[elmts.Length - m];
-      System.Array.Copy(elmts, m, a, 0, elmts.Length - m);
-      return new Sequence<T>(a);
-    }
-  }
-  public struct Pair<A, B>
-  {
-    public readonly A Car;
-    public readonly B Cdr;
-    public Pair(A a, B b) {
-      this.Car = a;
-      this.Cdr = b;
-    }
-  }
-  public partial class Helpers {
-    // Computing forall/exists quantifiers
-    public static bool QuantBool(bool frall, System.Predicate<bool> pred) {
-      if (frall) {
-        return pred(false) && pred(true);
-      } else {
-        return pred(false) || pred(true);
-      }
-    }
-    public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
-      for (BigInteger i = lo; i < hi; i++) {
-        if (pred(i) != frall) { return !frall; }
-      }
-      return frall;
-    }
-    public static bool QuantSet<U>(Dafny.Set<U> set, bool frall, System.Predicate<U> pred) {
-      foreach (var u in set.Elements) {
-        if (pred(u) != frall) { return !frall; }
-      }
-      return frall;
-    }
-    public static bool QuantMap<U,V>(Dafny.Map<U,V> map, bool frall, System.Predicate<U> pred) {
-      foreach (var u in map.Domain) {
-        if (pred(u) != frall) { return !frall; }
-      }
-      return frall;
-    }
-    public static bool QuantSeq<U>(Dafny.Sequence<U> seq, bool frall, System.Predicate<U> pred) {
-      foreach (var u in seq.Elements) {
-        if (pred(u) != frall) { return !frall; }
-      }
-      return frall;
-    }
-    public static bool QuantDatatype<U>(IEnumerable<U> set, bool frall, System.Predicate<U> pred) {
-      foreach (var u in set) {
-        if (pred(u) != frall) { return !frall; }
-      }
-      return frall;
-    }
-    // Enumerating other collections
-    public delegate Dafny.Set<T> ComprehensionDelegate<T>();
-    public delegate Dafny.Map<U, V> MapComprehensionDelegate<U, V>();
-    public static IEnumerable<bool> AllBooleans {
-      get {
-        yield return false;
-        yield return true;
-      }
-    }
-    public static IEnumerable<BigInteger> AllIntegers {
-      get {
-        yield return new BigInteger(0);
-        for (var j = new BigInteger(1);; j++) {
-          yield return j;
-          yield return -j;
-        }
-      }
-    }
-    // pre: b != 0
-    // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
-    public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {
-      if (0 <= a.Sign) {
-        if (0 <= b.Sign) {
-          // +a +b: a/b
-          return BigInteger.Divide(a, b);
-        } else {
-          // +a -b: -(a/(-b))
-          return BigInteger.Negate(BigInteger.Divide(a, BigInteger.Negate(b)));
-        }
-      } else {
-        if (0 <= b.Sign) {
-          // -a +b: -((-a-1)/b) - 1
-          return BigInteger.Negate(BigInteger.Divide(BigInteger.Negate(a) - 1, b)) - 1;
-        } else {
-          // -a -b: ((-a-1)/(-b)) + 1
-          return BigInteger.Divide(BigInteger.Negate(a) - 1, BigInteger.Negate(b)) + 1;
-        }
-      }
-    }
-    // pre: b != 0
-    // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)
-    public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {
-      var bp = BigInteger.Abs(b);
-      if (0 <= a.Sign) {
-        // +a: a % b'
-        return BigInteger.Remainder(a, bp);
-      } else {
-        // c = ((-a) % b')
-        // -a: b' - c if c > 0
-        // -a: 0 if c == 0
-        var c = BigInteger.Remainder(BigInteger.Negate(a), bp);
-        return c.IsZero ? c : BigInteger.Subtract(bp, c);
-      }
-    }
-    public static Sequence<T> SeqFromArray<T>(T[] array) {
-      return new Sequence<T>(array);
-    }
-    // In .NET version 4.5, it it possible to mark a method with "AggressiveInlining", which says to inline the
-    // method if possible.  Method "ExpressionSequence" would be a good candidate for it:
-    // [System.Runtime.CompilerServices.MethodImpl(System.Runtime.CompilerServices.MethodImplOptions.AggressiveInlining)]
-    public static U ExpressionSequence<T, U>(T t, U u)
-    {
-      return u;
-    }
-    public delegate Result Function<Input,Result>(Input input);
-  }
-
-  public struct BigRational
-  {
-    public static readonly BigRational ZERO = new BigRational(0);
-
-    BigInteger num, den;  // invariant 1 <= den
-    public override string ToString() {
-      return string.Format("({0}.0 / {1}.0)", num, den);
-    }
-    public BigRational(int n) {
-      num = new BigInteger(n);
-      den = BigInteger.One;
-    }
-    public BigRational(BigInteger n, BigInteger d) {
-      // requires 1 <= d
-      num = n;
-      den = d;
-    }
-    public BigInteger ToBigInteger() {
-      if (0 <= num) {
-        return num / den;
-      } else {
-        return (num - den + 1) / den;
-      }
-    }
-    /// <summary>
-    /// Returns values such that aa/dd == a and bb/dd == b.
-    /// </summary>
-    private static void Normalize(BigRational a, BigRational b, out BigInteger aa, out BigInteger bb, out BigInteger dd) {
-      var gcd = BigInteger.GreatestCommonDivisor(a.den, b.den);
-      var xx = a.den / gcd;
-      var yy = b.den / gcd;
-      // We now have a == a.num / (xx * gcd) and b == b.num / (yy * gcd).
-      aa = a.num * yy;
-      bb = b.num * xx;
-      dd = a.den * yy;
-    }
-    public int CompareTo(BigRational that) {
-      // simple things first
-      int asign = this.num.Sign;
-      int bsign = that.num.Sign;
-      if (asign < 0 && 0 <= bsign) {
-        return 1;
-      } else if (asign <= 0 && 0 < bsign) {
-        return 1;
-      } else if (bsign < 0 && 0 <= asign) {
-        return -1;
-      } else if (bsign <= 0 && 0 < asign) {
-        return -1;
-      }
-      BigInteger aa, bb, dd;
-      Normalize(this, that, out aa, out bb, out dd);
-      return aa.CompareTo(bb);
-    }
-    public override int GetHashCode() {
-      return num.GetHashCode() + 29 * den.GetHashCode();
-    }
-    public override bool Equals(object obj) {
-      if (obj is BigRational) {
-        return this == (BigRational)obj;
-      } else {
-        return false;
-      }
-    }
-    public static bool operator ==(BigRational a, BigRational b) {
-      return a.CompareTo(b) == 0;
-    }
-    public static bool operator !=(BigRational a, BigRational b) {
-      return a.CompareTo(b) != 0;
-    }
-    public static bool operator >(BigRational a, BigRational b) {
-      return 0 < a.CompareTo(b);
-    }
-    public static bool operator >=(BigRational a, BigRational b) {
-      return 0 <= a.CompareTo(b);
-    }
-    public static bool operator <(BigRational a, BigRational b) {
-      return a.CompareTo(b) < 0;
-    }
-    public static bool operator <=(BigRational a, BigRational b) {
-      return a.CompareTo(b) <= 0;
-    }
-    public static BigRational operator +(BigRational a, BigRational b) {
-      BigInteger aa, bb, dd;
-      Normalize(a, b, out aa, out bb, out dd);
-      return new BigRational(aa + bb, dd);
-    }
-    public static BigRational operator -(BigRational a, BigRational b) {
-      BigInteger aa, bb, dd;
-      Normalize(a, b, out aa, out bb, out dd);
-      return new BigRational(aa - bb, dd);
-    }
-    public static BigRational operator -(BigRational a) {
-      return new BigRational(-a.num, a.den);
-    }
-    public static BigRational operator *(BigRational a, BigRational b) {
-      return new BigRational(a.num * b.num, a.den * b.den);
-    }
-    public static BigRational operator /(BigRational a, BigRational b) {
-      // Compute the reciprocal of b
-      BigRational bReciprocal;
-      if (0 < b.num) {
-        bReciprocal = new BigRational(b.den, b.num);
-      } else {
-        // this is the case b.num < 0
-        bReciprocal = new BigRational(-b.den, -b.num);
-      }
-      return a * bReciprocal;
-    }
-  }
-}
-- 
cgit v1.2.3