diff options
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 129 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 85 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 87 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 101 |
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);
+ }
}
}
}
|