Add nativeType attribute for newtype declarations. Change Compiler.cs to use native C# representation of small integer newtypes.

Examples:

newtype{:nativeType "byte"}   byte   = i:int | 0 <= i < 0x100
newtype{:nativeType "sbyte"}  sbyte  = i:int | -0x80 <= i < 0x80
newtype{:nativeType "ushort"} uint16 = i:int | 0 <= i < 0x10000
newtype{:nativeType "short"}  int16  = i:int | -0x8000 <= i < 0x8000
newtype{:nativeType "uint"}   uint32 = i:int | 0 <= i < 0x100000000
newtype{:nativeType "int"}    int32  = i:int | -0x80000000 <= i < 0x80000000
newtype{:nativeType "ulong"}  uint64 = i:int | 0 <= i < 0x10000000000000000
newtype{:nativeType "long"}   int64  = i:int | -0x8000000000000000 <= i < 0x8000000000000000

newtype month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise BigInteger
newtype{:nativeType} month = i:int | 0 <= i < 12 // same as {:nativeType true}
newtype{:nativeType true} month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise error
newtype{:nativeType false} month = i:int | 0 <= i < 12 // use BigInteger
newtype{:nativeType "uint"} month = i:int | 0 <= i < 12 // use C# uint type if possible, otherwise error

newtype{:nativeType} even20 = i:int | 0 <= i < 20 && (i % 2 == 0) // nativeTypes need not be contiguous
newtype{:nativeType} even10 = i:even20 | i < 10 // nativeTypes can inherit constraints from other nativeTypes

1 files changed, 119 insertions, 10 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 661666ef..a1d9037d 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -437,8 +437,11 @@ namespace Dafny
     public static Sequence<char> FromString(string s) {

       return new Sequence<char>(s.ToCharArray());

     }

-    public BigInteger Length {

-      get { return new BigInteger(elmts.Length); }

+    public int Length {

+      get { return elmts.Length; }

+    }

+    public long LongLength {

+      get { return elmts.LongLength; }

     }

     public T[] Elements {

       get {

@@ -451,14 +454,32 @@ namespace Dafny
         return st.Elements;

       }

     }

+    public T Select(ulong index) {

+      return elmts[index];

+    }

+    public T Select(long index) {

+      return elmts[index];

+    }

+    public T Select(uint index) {

+      return elmts[index];

+    }

+    public T Select(int index) {

+      return elmts[index];

+    }

     public T Select(BigInteger index) {

       return elmts[(int)index];

     }

-    public Sequence<T> Update(BigInteger index, T t) {

+    public Sequence<T> Update(long index, T t) {

       T[] a = (T[])elmts.Clone();

-      a[(int)index] = t;

+      a[index] = t;

       return new Sequence<T>(a);

     }

+    public Sequence<T> Update(ulong index, T t) {

+      return Update((long)index, t);

+    }

+    public Sequence<T> Update(BigInteger index, T t) {

+      return Update((long)index, t);

+    }

     public bool Equals(Sequence<T> other) {

       int n = elmts.Length;

       return n == other.elmts.Length && EqualUntil(other, n);

@@ -519,22 +540,34 @@ namespace Dafny
       }

       return false;

     }

-    public Sequence<T> Take(BigInteger n) {

-      int m = (int)n;

-      if (elmts.Length == m)

+    public Sequence<T> Take(long m) {

+      if (elmts.LongLength == 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)

+    public Sequence<T> Take(ulong n) {

+      return Take((long)n);

+    }

+    public Sequence<T> Take(BigInteger n) {

+      return Take((long)n);

+    }

+    public Sequence<T> Drop(long m) {

+      if (m == 0)

         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 Sequence<T> Drop(ulong n) {

+      return Drop((long)n);

+    }

+    public Sequence<T> Drop(BigInteger n) {

+      if (n.IsZero)

+        return this;

+      return Drop((long)n);

+    }

   }

   public struct Pair<A, B>

   {

@@ -604,6 +637,50 @@ namespace Dafny
     }

     // pre: b != 0

     // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)

+    public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) {

+      return (sbyte)EuclideanDivision(a, b);

+    }

+    public static short EuclideanDivision_short(short a, short b) {

+      return (short)EuclideanDivision(a, b);

+    }

+    public static int EuclideanDivision_int(int a, int b) {

+      if (0 <= a) {

+        if (0 <= b) {

+          // +a +b: a/b

+          return (int)(((uint)(a)) / ((uint)(b)));

+        } else {

+          // +a -b: -(a/(-b))

+          return -((int)(((uint)(a)) / ((uint)(unchecked(-b)))));

+        }

+      } else {

+        if (0 <= b) {

+          // -a +b: -((-a-1)/b) - 1

+          return -((int)(((uint)(-(a + 1))) / ((uint)(b)))) - 1;

+        } else {

+          // -a -b: ((-a-1)/(-b)) + 1

+          return ((int)(((uint)(-(a + 1))) / ((uint)(unchecked(-b))))) + 1;

+        }

+      }

+    }

+    public static long EuclideanDivision_long(long a, long b) {

+      if (0 <= a) {

+        if (0 <= b) {

+          // +a +b: a/b

+          return (long)(((ulong)(a)) / ((ulong)(b)));

+        } else {

+          // +a -b: -(a/(-b))

+          return -((long)(((ulong)(a)) / ((ulong)(unchecked(-b)))));

+        }

+      } else {

+        if (0 <= b) {

+          // -a +b: -((-a-1)/b) - 1

+          return -((long)(((ulong)(-(a + 1))) / ((ulong)(b)))) - 1;

+        } else {

+          // -a -b: ((-a-1)/(-b)) + 1

+          return ((long)(((ulong)(-(a + 1))) / ((ulong)(unchecked(-b))))) + 1;

+        }

+      }

+    }

     public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) {

       if (0 <= a.Sign) {

         if (0 <= b.Sign) {

@@ -625,6 +702,38 @@ namespace Dafny
     }

     // pre: b != 0

     // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation)

+    public static sbyte EuclideanModulus_sbyte(sbyte a, sbyte b) {

+      return (sbyte)EuclideanModulus(a, b);

+    }

+    public static short EuclideanModulus_short(short a, short b) {

+      return (short)EuclideanModulus(a, b);

+    }

+    public static int EuclideanModulus_int(int a, int b) {

+      uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b));

+      if (0 <= a) {

+        // +a: a % b'

+        return (int)(((uint)a) % bp);

+      } else {

+        // c = ((-a) % b')

+        // -a: b' - c if c > 0

+        // -a: 0 if c == 0

+        uint c = ((uint)(unchecked(-a))) % bp;

+        return (int)(c == 0 ? c : bp - c);

+      }

+    }

+    public static long EuclideanModulus_long(long a, long b) {

+      ulong bp = (0 <= b) ? (ulong)b : (ulong)(unchecked(-b));

+      if (0 <= a) {

+        // +a: a % b'

+        return (long)(((ulong)a) % bp);

+      } else {

+        // c = ((-a) % b')

+        // -a: b' - c if c > 0

+        // -a: 0 if c == 0

+        ulong c = ((ulong)(unchecked(-a))) % bp;

+        return (long)(c == 0 ? c : bp - c);

+      }

+    }

     public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) {

       var bp = BigInteger.Abs(b);

       if (0 <= a.Sign) {