Get rid of F# dependencies - use System.Numerics and a custom Rational structure instead

6 files changed, 73 insertions, 107 deletions

diff --git a/Source/AIFramework/Polyhedra/LinearConstraint.cs b/Source/AIFramework/Polyhedra/LinearConstraint.cs
index ce5c23a2..5d1cabd5 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraint.cs
+++ b/Source/AIFramework/Polyhedra/LinearConstraint.cs
@@ -429,14 +429,14 @@ namespace Microsoft.AbstractInterpretationFramework {
       foreach (DictionaryEntry /*IVarianble->Rational*/ e in coefficients) {

         Rational r = (Rational)(cce.NonNull(e.Value));

         if (r.IsNonZero) {

-          newCoefficients.Add(e.Key, new Rational(r.Numerator / gcd.Numerator, r.Denominator / gcd.Denominator));

+          newCoefficients.Add(e.Key, Rational.FromBignums(r.Numerator / gcd.Numerator, r.Denominator / gcd.Denominator));

         } else {

           newCoefficients.Add(e.Key, r);

         }

       }

 

       coefficients = newCoefficients;

-      rhs = rhs.IsNonZero ? (Rational)new Rational(rhs.Numerator / gcd.Numerator, rhs.Denominator / gcd.Denominator) : rhs;

+      rhs = rhs.IsNonZero ? Rational.FromBignums(rhs.Numerator / gcd.Numerator, rhs.Denominator / gcd.Denominator) : rhs;

     }

   }

 

diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj
index 23edd35d..4dabe875 100644
--- a/Source/Basetypes/Basetypes.csproj
+++ b/Source/Basetypes/Basetypes.csproj
@@ -99,16 +99,9 @@
     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

   </PropertyGroup>

   <ItemGroup>

-    <Reference Include="FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\FSharp.Core.dll</HintPath>

-    </Reference>

-    <Reference Include="FSharp.PowerPack, Version=1.9.9.9, Culture=neutral, PublicKeyToken=a19089b1c74d0809, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\FSharp.PowerPack.dll</HintPath>

-    </Reference>

     <Reference Include="System" />

     <Reference Include="System.Data" />

+    <Reference Include="System.Numerics" />

     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

diff --git a/Source/Basetypes/BigNum.cs b/Source/Basetypes/BigNum.cs
index 2e56fd1a..31fcf482 100644
--- a/Source/Basetypes/BigNum.cs
+++ b/Source/Basetypes/BigNum.cs
@@ -85,7 +85,7 @@ namespace Microsoft.Basetypes {
 

     public Rational ToRational {

       get {

-        return new Rational(this, BigNum.ONE);

+        return Rational.FromBignum(this);

       }

     }

 

diff --git a/Source/Basetypes/Rational.cs b/Source/Basetypes/Rational.cs
index 609970a2..cd0eddce 100644
--- a/Source/Basetypes/Rational.cs
+++ b/Source/Basetypes/Rational.cs
@@ -7,28 +7,15 @@ using System;
 using System.Diagnostics.Contracts;

 

 namespace Microsoft.Basetypes {

-  using BNM = Microsoft.FSharp.Math.BigRational;

-

   /// <summary>

   /// The representation of a rational number.

   /// </summary>

   public struct Rational {

-    public static readonly Rational ZERO = new Rational(cce.NonNull(BNM.Zero));

-    public static readonly Rational ONE = new Rational(cce.NonNull(BNM.One));

-    public static readonly Rational MINUS_ONE = new Rational(cce.NonNull(-BNM.One));

-

-    private readonly Microsoft.FSharp.Math.BigRational _val;

-

-    private Microsoft.FSharp.Math.BigRational val {

-      get {

-        Contract.Ensures(Contract.Result<FSharp.Math.BigRational>() != null);

-        if ((object)_val == null)

-          return cce.NonNull(BNM.Zero);

-        else

-          return _val;

-      }

-    }

+    public static readonly Rational ZERO = Rational.FromInts(0, 1);

+    public static readonly Rational ONE = Rational.FromInts(1, 1);

+    public static readonly Rational MINUS_ONE = Rational.FromInts(-1, 1);

 

+    private BigNum numerator, denominator;

 

     //    int numerator;

     //    int denominator;

@@ -38,27 +25,41 @@ namespace Microsoft.Basetypes {
     // invariant: numerator != 0 ==> gcd(abs(numerator),denominator) == 1;

     // invariant: numerator == 0 ==> denominator == 1 || denominator == 0;

 

-    private Rational(int x) {

-      this._val = BNM.FromInt(x);

-    }

-

     public static Rational FromInt(int x) {

-      return new Rational(x);

+      return FromBignum(BigNum.FromInt(x));

     }

 

-    private Rational(Microsoft.FSharp.Math.BigRational/*!*/ val) {

-      Contract.Requires(val != null);

-      this._val = val;

+    public static Rational FromBignum(BigNum n)       

+    {

+      return new Rational(n, BigNum.ONE);

     }

 

-    public Rational(BigNum num, BigNum den) {

-      System.Diagnostics.Debug.Assert(!den.IsZero);

+    private Rational(BigNum num, BigNum den)

+    {

+      Contract.Assert(den.Signum > 0);

+      Contract.Assert(num == BigNum.ZERO || num.Gcd(den) == BigNum.ONE);

+      numerator = num;

+      denominator = den;

+    }

 

-      this._val = BNM.FromBigInt(num.val) / BNM.FromBigInt(den.val);

+    public static Rational FromBignums(BigNum num, BigNum den) {

+      Contract.Assert(!den.IsZero);

+      if (num == BigNum.ZERO)

+        return ZERO;

+      if (den.Signum < 0) {

+        den = -den;

+        num = -num;

+      }

+      if (den == BigNum.ONE)

+        return new Rational(num, den);

+      var gcd = num.Gcd(den);

+      if (gcd == BigNum.ONE)

+        return new Rational(num, den);

+      return new Rational(num / gcd, den / gcd);

     }

 

     public static Rational FromInts(int num, int den) {

-      return new Rational(BigNum.FromInt(num), BigNum.FromInt(den));

+      return FromBignums(BigNum.FromInt(num), BigNum.FromInt(den));

     }

 

     /// <summary>

@@ -94,31 +95,8 @@ namespace Microsoft.Basetypes {
       }

     }

 

-    public BigNum Numerator {

-      get {

-        // Better way to obtain the numerator?

-        // The FSharp library does not seem to offer any methods for this

-        string/*!*/ lin = cce.NonNull(val.ToString());

-        int i = lin.IndexOf('/');

-        if (i == -1)

-          return new BigNum(BNM.ToBigInt(this.val));

-        else

-          return BigNum.FromString(lin.Substring(0, i));

-      }

-    }

-

-    public BigNum Denominator {

-      get {

-        // Better way to obtain the numerator?

-        // The FSharp library does not seem to offer any methods for this

-        string/*!*/ lin = cce.NonNull(val.ToString());

-        int i = lin.IndexOf('/');

-        if (i == -1)

-          return BigNum.ONE;

-        else

-          return BigNum.FromString(lin.Substring(i + 1));

-      }

-    }

+    public BigNum Numerator { get { return numerator; } }

+    public BigNum Denominator { get { return denominator == BigNum.ZERO ? BigNum.ONE : denominator; } }

 

     public override string/*!*/ ToString() {

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

@@ -127,11 +105,11 @@ namespace Microsoft.Basetypes {
 

 

     public static bool operator ==(Rational r, Rational s) {

-      return (r.val == s.val);

+      return r.Numerator == s.Numerator && r.Denominator == s.Denominator;

     }

 

     public static bool operator !=(Rational r, Rational s) {

-      return !(r.val == s.val);

+      return !(r == s);

     }

 

     public override bool Equals(object obj) {

@@ -141,12 +119,12 @@ namespace Microsoft.Basetypes {
     }

 

     public override int GetHashCode() {

-      return this.val.GetHashCode();

+      return this.Numerator.GetHashCode() * 13 + this.Denominator.GetHashCode();

     }

 

     public int Signum {

       get {

-        return this.val.Sign;

+        return this.Numerator.Signum;

       }

     }

 

@@ -164,8 +142,7 @@ namespace Microsoft.Basetypes {
 

     public bool IsIntegral {

       get {

-        // better way?

-        return !cce.NonNull(this.val.ToString()).Contains("/");

+        return Denominator == BigNum.ONE;

       }

     }

 

@@ -173,7 +150,7 @@ namespace Microsoft.Basetypes {
     [Pure]

     [Reads(ReadsAttribute.Reads.Nothing)]

     public bool HasValue(int n) {

-      return this == new Rational(n);

+      return this == FromInt(n);

     }

 

     /// <summary>

@@ -181,15 +158,15 @@ namespace Microsoft.Basetypes {
     /// </summary>

     public int AsInteger {

       get {

-        System.Diagnostics.Debug.Assert(this.IsIntegral);

+        Contract.Assert(this.IsIntegral);

         return Numerator.ToIntSafe;

       }

     }

 

     public BigNum AsBigNum {

       get {

-        System.Diagnostics.Debug.Assert(this.IsIntegral);

-        return new BigNum(BNM.ToBigInt(this.val));

+        Contract.Assert(this.IsIntegral);

+        return Numerator;

       }

     }

 

@@ -225,42 +202,47 @@ namespace Microsoft.Basetypes {
       }

     }

 

-

-    public static Rational operator -(Rational r) {

-      return new Rational(cce.NonNull(BNM.Zero - r.val)); // for whatever reason, the Spec# compiler refuses to accept -r.val (unary negation)

+    public static Rational operator -(Rational r)

+    {

+      return new Rational(-r.Numerator, r.Denominator);

     }

 

-

-    public static Rational operator +(Rational r, Rational s) {

-      return new Rational(cce.NonNull(r.val + s.val));

+    public static Rational operator /(Rational r, Rational s)

+    {

+      return FromBignums(r.Numerator * s.Denominator, r.Denominator * s.Numerator);

     }

 

-    public static Rational operator -(Rational r, Rational s) {

-      return new Rational(cce.NonNull((r.val - s.val)));

+    public static Rational operator -(Rational r, Rational s)

+    {

+      return r + (-s);

     }

 

-    public static Rational operator *(Rational r, Rational s) {

-      return new Rational(cce.NonNull(r.val * s.val));

+    public static Rational operator +(Rational r, Rational s)

+    {

+      return FromBignums(r.Numerator * s.Denominator + s.Numerator * r.Denominator, r.Denominator * s.Denominator);

     }

 

-    public static Rational operator /(Rational r, Rational s) {

-      return new Rational(cce.NonNull(r.val / s.val));

+    public static Rational operator *(Rational r, Rational s)

+    {

+      return FromBignums(r.Numerator * s.Numerator, r.Denominator * s.Denominator);

     }

 

-    public static bool operator <=(Rational r, Rational s) {

-      return (r.val <= s.val);

+    public static bool operator <(Rational r, Rational s)

+    {

+      return (r - s).Signum < 0;

     }

 

-    public static bool operator >=(Rational r, Rational s) {

-      return (r.val >= s.val);

+    public static bool operator <=(Rational r, Rational s)

+    {

+      return !(r > s);

     }

 

-    public static bool operator <(Rational r, Rational s) {

-      return (r.val < s.val);

+    public static bool operator >=(Rational r, Rational s) {

+      return !(r < s);

     }

 

     public static bool operator >(Rational r, Rational s) {

-      return (r.val > s.val);

+      return s < r;

     }

   }

 }

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index 6cea383c..625ab9b6 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -99,11 +99,8 @@
     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

   </PropertyGroup>

   <ItemGroup>

-    <Reference Include="FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\FSharp.Core.dll</HintPath>

-    </Reference>

     <Reference Include="System" />

+    <Reference Include="System.Numerics" />

     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index a93dffe1..a4206998 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -34,7 +34,8 @@
     <IsWebBootstrapper>false</IsWebBootstrapper>

     <UseApplicationTrust>false</UseApplicationTrust>

     <BootstrapperEnabled>true</BootstrapperEnabled>

-    <TargetFrameworkProfile />

+    <TargetFrameworkProfile>

+    </TargetFrameworkProfile>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

     <DebugSymbols>true</DebugSymbols>

@@ -97,19 +98,12 @@
       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\Binaries\Core.dll</HintPath>

     </Reference>

-    <Reference Include="FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\FSharp.Core.dll</HintPath>

-    </Reference>

-    <Reference Include="FSharp.PowerPack, Version=1.9.9.9, Culture=neutral, PublicKeyToken=a19089b1c74d0809, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\Binaries\FSharp.PowerPack.dll</HintPath>

-    </Reference>

     <Reference Include="System" />

     <Reference Include="System.Core">

       <RequiredTargetFramework>3.5</RequiredTargetFramework>

     </Reference>

     <Reference Include="System.Data" />

+    <Reference Include="System.Numerics" />

     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>