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

4 files changed, 379 insertions, 23 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) {

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index a4541414..485fe661 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -953,6 +953,14 @@ namespace Microsoft.Dafny {
     readonly string DafnySeqClass = "Dafny.Sequence";

     readonly string DafnyMapClass = "Dafny.Map";

 

+    NativeType AsNativeType(Type typ) {

+      Contract.Requires(typ != null);

+      if (typ.AsNewtype != null) {

+        return typ.AsNewtype.NativeType;

+      }

+      return null;

+    }

+

     string TypeName(Type type)

     {

       Contract.Requires(type != null);

@@ -973,6 +981,10 @@ namespace Microsoft.Dafny {
       } else if (type is RealType) {

         return "Dafny.BigRational";

       } else if (type.AsNewtype != null) {

+        NativeType nativeType = type.AsNewtype.NativeType;

+        if (nativeType != null) {

+          return nativeType.Name;

+        }

         return TypeName(type.AsNewtype.BaseType);

       } else if (type is ObjectType) {

         return "object";

@@ -1070,6 +1082,9 @@ namespace Microsoft.Dafny {
       } else if (type is RealType) {

         return "Dafny.BigRational.ZERO";

       } else if (type.AsNewtype != null) {

+        if (type.AsNewtype.NativeType != null) {

+          return "0";

+        }

         return DefaultValue(type.AsNewtype.BaseType);

       } else if (type.IsRefType) {

         return string.Format("({0})null", TypeName(type));

@@ -2057,6 +2072,8 @@ namespace Microsoft.Dafny {
         } else if (e is StringLiteralExpr) {

           var str = (StringLiteralExpr)e;

           wr.Write("{0}<char>.FromString({1}\"{2}\")", DafnySeqClass, str.IsVerbatim ? "@" : "", (string)e.Value);

+        } else if (AsNativeType(e.Type) != null) {

+          wr.Write((BigInteger)e.Value + AsNativeType(e.Type).Suffix);

         } else if (e.Value is BigInteger) {

           BigInteger i = (BigInteger)e.Value;

           if (new BigInteger(int.MinValue) <= i && i <= new BigInteger(int.MaxValue)) {

@@ -2291,14 +2308,9 @@ namespace Microsoft.Dafny {
             TrParenExpr(e.E);

             break;

           case UnaryOpExpr.Opcode.Cardinality:

-            if (e.E.Type.IsArrayType) {

-              wr.Write("new BigInteger(");

-              TrParenExpr(e.E);

-              wr.Write(".Length)");

-            } else {

-              TrParenExpr(e.E);

-              wr.Write(".Length");

-            }

+            wr.Write("new BigInteger(");

+            TrParenExpr(e.E);

+            wr.Write(".Length)");

             break;

           default:

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected unary expression

@@ -2310,17 +2322,54 @@ namespace Microsoft.Dafny {
         Contract.Assert(fromInt || e.E.Type.IsNumericBased(Type.NumericPersuation.Real));

         var toInt = e.ToType.IsNumericBased(Type.NumericPersuation.Int);

         Contract.Assert(toInt || e.ToType.IsNumericBased(Type.NumericPersuation.Real));

+        Action fromIntAsBigInteger = () => {

+          Contract.Assert(fromInt);

+          if (AsNativeType(e.E.Type) != null) {

+            wr.Write("new BigInteger");

+          }

+          TrParenExpr(e.E);

+        };

+        Action toIntCast = () => {

+          Contract.Assert(toInt);

+          if (AsNativeType(e.ToType) != null) {

+            wr.Write("(" + AsNativeType(e.ToType).Name + ")");

+          }

+        };

         if (fromInt && !toInt) {

           // int -> real

           wr.Write("new Dafny.BigRational(");

-          TrExpr(e.E);

+          fromIntAsBigInteger();

           wr.Write(", BigInteger.One)");

         } else if (!fromInt && toInt) {

           // real -> int

+          toIntCast();

           TrParenExpr(e.E);

           wr.Write(".ToBigInteger()");

+        } else if (AsNativeType(e.ToType) != null) {

+          toIntCast();

+          LiteralExpr lit = e.E.Resolved as LiteralExpr;

+          UnaryOpExpr u = e.E.Resolved as UnaryOpExpr;

+          MemberSelectExpr m = e.E.Resolved as MemberSelectExpr;

+          if (lit != null && lit.Value is BigInteger) {

+            // Optimize constant to avoid intermediate BigInteger

+            wr.Write("(" + (BigInteger)lit.Value + AsNativeType(e.ToType).Suffix + ")");

+          } else if ((u != null && u.Op == UnaryOpExpr.Opcode.Cardinality) || (m != null && m.MemberName == "Length" && m.Obj.Type.IsArrayType)) {

+            // Optimize .Length to avoid intermediate BigInteger

+            TrParenExpr((u != null) ? u.E : m.Obj);

+            if (AsNativeType(e.ToType).UpperBound <= new BigInteger(0x80000000U)) {

+              wr.Write(".Length");

+            } else {

+              wr.Write(".LongLength");

+            }

+          } else {

+            TrParenExpr(e.E);

+          }

+        } else if (e.ToType.IsIntegerType && AsNativeType(e.E.Type) != null) {

+          fromIntAsBigInteger();

         } else {

           Contract.Assert(fromInt == toInt);

+          Contract.Assert(AsNativeType(e.ToType) == null);

+          Contract.Assert(AsNativeType(e.E.Type) == null);

           TrParenExpr(e.E);

         }

 

@@ -2387,8 +2436,9 @@ namespace Microsoft.Dafny {
           case BinaryExpr.ResolvedOpcode.Mul:

             opString = "*";  break;

           case BinaryExpr.ResolvedOpcode.Div:

-            if (expr.Type.IsIntegerType) {

-              wr.Write("Dafny.Helpers.EuclideanDivision(");

+            if (expr.Type.IsIntegerType || (AsNativeType(expr.Type) != null && AsNativeType(expr.Type).LowerBound < BigInteger.Zero)) {

+              string suffix = AsNativeType(expr.Type) != null ? ("_" + AsNativeType(expr.Type).Name) : "";

+              wr.Write("Dafny.Helpers.EuclideanDivision" + suffix + "(");

               TrParenExpr(e.E0);

               wr.Write(", ");

               TrExpr(e.E1);

@@ -2398,8 +2448,9 @@ namespace Microsoft.Dafny {
             }

             break;

           case BinaryExpr.ResolvedOpcode.Mod:

-            if (expr.Type.IsIntegerType) {

-              wr.Write("Dafny.Helpers.EuclideanModulus(");

+            if (expr.Type.IsIntegerType || (AsNativeType(expr.Type) != null && AsNativeType(expr.Type).LowerBound < BigInteger.Zero)) {

+              string suffix = AsNativeType(expr.Type) != null ? ("_" + AsNativeType(expr.Type).Name) : "";

+              wr.Write("Dafny.Helpers.EuclideanModulus" + suffix + "(");

               TrParenExpr(e.E0);

               wr.Write(", ");

               TrExpr(e.E1);

@@ -2485,10 +2536,18 @@ namespace Microsoft.Dafny {
             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected binary expression

         }

         if (opString != null) {

+          NativeType nativeType = AsNativeType(e.Type);

+          bool needsCast = nativeType != null && nativeType.NeedsCastAfterArithmetic;

+          if (needsCast) {

+            wr.Write("(" + nativeType.Name + ")(");

+          }

           wr.Write(preOpString);

           TrParenExpr(e.E0);

           wr.Write(" {0} ", opString);

           TrParenExpr(e.E1);

+          if (needsCast) {

+            wr.Write(")");

+          }

         } else if (callString != null) {

           wr.Write(preOpString);

           TrParenExpr(e.E0);

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 9e5c1c7f..c028fe10 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -298,6 +298,72 @@ namespace Microsoft.Dafny {
 

       return false;

     }

+

+    /// <summary>

+    /// Returns list of expressions if "nm" is a specified attribute:

+    /// - if the attribute is {:nm e1,...,en}, then returns (e1,...,en)

+    /// Otherwise, returns null.

+    /// </summary>

+    public static List<Expression> FindExpressions(Attributes attrs, string nm) {

+      Contract.Requires(nm != null);

+      for (; attrs != null; attrs = attrs.Prev) {

+        if (attrs.Name == nm) {

+          return attrs.Args;

+        }

+      }

+      return null;

+    }

+

+    /// <summary>

+    /// Returns true if "nm" is a specified attribute whose arguments match the "allowed" parameter.

+    /// - if "nm" is not found in attrs, return false and leave value unmodified.  Otherwise,

+    /// - if "allowed" contains Empty and the Args contains zero elements, return true and leave value unmodified.  Otherwise,

+    /// - if "allowed" contains Bool and Args contains one bool literal, return true and set value to the bool literal.  Otherwise,

+    /// - if "allowed" contains Int and Args contains one BigInteger literal, return true and set value to the BigInteger literal.  Otherwise,

+    /// - if "allowed" contains String and Args contains one string literal, return true and set value to the string literal.  Otherwise,

+    /// - if "allowed" contains Expression and Args contains one element, return true and set value to the one element (of type Expression).  Otherwise,

+    /// - return false, leave value unmodified, and call errorReporter with an error string.

+    /// </summary>

+    public enum MatchingValueOption { Empty, Bool, Int, String, Expression }

+    public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object value, IEnumerable<MatchingValueOption> allowed, Action<string> errorReporter) {

+      Contract.Requires(nm != null);

+      Contract.Requires(allowed != null);

+      Contract.Requires(errorReporter != null);

+      List<Expression> args = FindExpressions(attrs, nm);

+      if (args == null) {

+        return false;

+      } else if (args.Count == 0) {

+        if (allowed.Contains(MatchingValueOption.Empty)) {

+          return true;

+        } else {

+          errorReporter("Attribute " + nm + " requires one argument");

+          return false;

+        }

+      } else if (args.Count == 1) {

+        Expression arg = args[0];

+        StringLiteralExpr stringLiteral = arg as StringLiteralExpr;

+        LiteralExpr literal = arg as LiteralExpr;

+        if (literal != null && literal.Value is bool && allowed.Contains(MatchingValueOption.Bool)) {

+          value = literal.Value;

+          return true;

+        } else if (literal != null && literal.Value is BigInteger && allowed.Contains(MatchingValueOption.Int)) {

+          value = literal.Value;

+          return true;

+        } else if (stringLiteral != null && (stringLiteral.Value as string) != null && allowed.Contains(MatchingValueOption.String)) {

+          value = stringLiteral.Value;

+          return true;

+        } else if (allowed.Contains(MatchingValueOption.Expression)) {

+          value = arg;

+          return true;

+        } else {

+          errorReporter("Attribute " + nm + " expects an argument in one of the following categories: " + String.Join(", ", allowed));

+          return false;

+        }

+      } else {

+        errorReporter("Attribute " + nm + " cannot have more than one argument");

+        return false;

+      }

+    }

   }

 

   // ------------------------------------------------------------------------------------------------------

@@ -2281,11 +2347,32 @@ namespace Microsoft.Dafny {
     string Name { get; }

   }

 

+  public class NativeType

+  {

+    public readonly string Name;

+    public readonly BigInteger LowerBound;

+    public readonly BigInteger UpperBound;

+    public readonly string Suffix;

+    public readonly bool NeedsCastAfterArithmetic;

+    public NativeType(string Name, BigInteger LowerBound, BigInteger UpperBound, string Suffix, bool NeedsCastAfterArithmetic) {

+      Contract.Requires(Name != null);

+      Contract.Requires(LowerBound != null);

+      Contract.Requires(UpperBound != null);

+      Contract.Requires(Suffix != null);

+      this.Name = Name;

+      this.LowerBound = LowerBound;

+      this.UpperBound = UpperBound;

+      this.Suffix = Suffix;

+      this.NeedsCastAfterArithmetic = NeedsCastAfterArithmetic;

+    }

+  }

+

   public class NewtypeDecl : TopLevelDecl, RedirectingTypeDecl

   {

     public readonly Type BaseType;

     public readonly BoundVar Var;  // can be null (if non-null, then object.ReferenceEquals(Var.Type, BaseType))

     public readonly Expression Constraint;  // is null iff Var is

+    public NativeType NativeType; // non-null for fixed-size representations (otherwise, use BigIntegers for integers)

     public NewtypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes)

       : base(tok, name, module, new List<TypeParameter>(), attributes) {

       Contract.Requires(tok != null);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d38076fd..79421d0f 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1205,6 +1205,17 @@ namespace Microsoft.Dafny
     private readonly List<SetComprehension> needFiniteBoundsChecks = new List<SetComprehension>();

     public int NFBC_Count { get { return needFiniteBoundsChecks.Count; } } // provided just for the purpose of conveniently writing contracts for ResolveTopLevelDecl_Meat

 

+    static readonly List<NativeType> NativeTypes = new List<NativeType>() {

+      new NativeType("byte", 0, 0x100, "", true),

+      new NativeType("sbyte", -0x80, 0x80, "", true),

+      new NativeType("ushort", 0, 0x10000, "", true),

+      new NativeType("short", -0x8000, 0x8000, "", true),

+      new NativeType("uint", 0, 0x100000000, "U", false),

+      new NativeType("int", -0x80000000, 0x80000000, "", false),

+      new NativeType("ulong", 0, new BigInteger(0x100000000) * new BigInteger(0x100000000), "UL", false),

+      new NativeType("long", Int64.MinValue, 0x8000000000000000, "L", false),

+    };

+

     public void ResolveTopLevelDecls_Meat(List<TopLevelDecl/*!*/>/*!*/ declarations, Graph<IndDatatypeDecl/*!*/>/*!*/ datatypeDependencies, Graph<CoDatatypeDecl/*!*/>/*!*/ codatatypeDependencies) {

       Contract.Requires(declarations != null);

       Contract.Requires(cce.NonNullElements(datatypeDependencies));

@@ -1288,6 +1299,11 @@ namespace Microsoft.Dafny
       }

       needFiniteBoundsChecks.Clear();

 

+      Dictionary<string, NativeType> nativeTypeMap = new Dictionary<string, NativeType>();

+      foreach (var nativeType in NativeTypes) {

+        nativeTypeMap.Add(nativeType.Name, nativeType);

+      }

+

       if (ErrorCount == prevErrorCount) {

         // Check that type inference went well everywhere; this will also fill in the .ResolvedOp field in binary expressions

         foreach (TopLevelDecl d in declarations) {

@@ -1302,9 +1318,94 @@ namespace Microsoft.Dafny
             cl.Members.Iter(CheckTypeInference_Member);

           } else if (d is NewtypeDecl) {

             var dd = (NewtypeDecl)d;

+            bool? boolNativeType = null;

+            NativeType stringNativeType = null;

+            object nativeTypeAttr = true;

+            bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr,

+              new Attributes.MatchingValueOption[] {

+                Attributes.MatchingValueOption.Empty,

+                Attributes.MatchingValueOption.Bool,

+                Attributes.MatchingValueOption.String },

+              err => Error(dd, err));

+            if (hasNativeTypeAttr) {

+              if (nativeTypeAttr is bool) {

+                boolNativeType = (bool)nativeTypeAttr;

+              } else {

+                string keyString = (string)nativeTypeAttr;

+                if (nativeTypeMap.ContainsKey(keyString)) {

+                  stringNativeType = nativeTypeMap[keyString];

+                } else {

+                  Error(dd, "Unsupported nativeType {0}", keyString);

+                }

+              }

+            }

+            if (stringNativeType != null || boolNativeType == true) {

+              if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) {

+                Error(dd, "nativeType can only be used on integral types");

+              }

+              if (dd.Var == null) {

+                Error(dd, "nativeType can only be used if newtype specifies a constraint");

+              }

+            }

             if (dd.Var != null) {

               Contract.Assert(dd.Constraint != null);

               CheckTypeInference(dd.Constraint);

+

+              Func<Expression, BigInteger?> GetConst = null;

+              GetConst = (Expression e) => {

+                int m = 1;

+                BinaryExpr bin = e as BinaryExpr;

+                if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) {

+                  m = -1;

+                  e = bin.E1;

+                }

+                LiteralExpr l = e as LiteralExpr;

+                if (l != null && l.Value is BigInteger) {

+                  return m * (BigInteger)l.Value;

+                }

+                return null;

+              };

+              var missingBounds = new List<BoundVar>();

+              var bounds = DiscoverBounds(dd.Constraint.tok, new List<BoundVar> { dd.Var }, dd.Constraint,

+                true, true, missingBounds);

+              List<NativeType> potentialNativeTypes =

+                (stringNativeType != null) ? new List<NativeType> { stringNativeType } :

+                (boolNativeType == false) ? new List<NativeType>() :

+                NativeTypes;

+              foreach (var nt in potentialNativeTypes) {

+                if (missingBounds.Count == 0) {

+                  bool lowerOk = false;

+                  bool upperOk = false;

+                  foreach (var bound in bounds) {

+                    if (bound is ComprehensionExpr.IntBoundedPool) {

+                      var bnd = (ComprehensionExpr.IntBoundedPool)bound;

+                      if (bnd.LowerBound != null) {

+                        BigInteger? lower = GetConst(bnd.LowerBound);

+                        if (lower != null && nt.LowerBound <= lower) {

+                          lowerOk = true;

+                        }

+                      }

+                      if (bnd.UpperBound != null) {

+                        BigInteger? upper = GetConst(bnd.UpperBound);

+                        if (upper != null && upper <= nt.UpperBound) {

+                          upperOk = true;

+                        }

+                      }

+                    }

+                  }

+                  if (lowerOk && upperOk) {

+                    dd.NativeType = nt;

+                    break;

+                  }

+                }

+              }

+              if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) {

+                Error(dd, "Dafny's heuristics cannot find a compatible native type.  " +

+                  "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'");

+              }

+              if (dd.NativeType != null && stringNativeType == null) {

+                ReportAdditionalInformation(dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}", dd.tok.val.Length);

+              }

             }

           }

         }