Allow any integer-based type, not just 'int', in the following places:

 * array indices (any dimension)
 * array lengths (with new, any dimension)
 * sequence indicies
 * subsequence bounds (like sq[lo..hi])
 * the new multiplicity in multiset update (m[t := multiplicity])
 * subarray-to-sequence bounds (like a[lo..hi])
Note that for an array 'a', 'a.Length' is always an integer, so a comparison 'i < a.Length' still requires 'i' to be an integer, not any integer-based value.  Same for '|sq|' for a sequence 'sq'.

6 files changed, 168 insertions, 16 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 9a519ec1..dfd37954 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1220,12 +1220,13 @@ namespace Microsoft.Dafny {
   /// Arg is either Domain or Range, depending on what type it is.  Arg is the type

   /// one would use in an expression "x in C", whereas

   /// This proxy stands for one of:

-  ///   seq(T)       Domain,Range,Arg := int,T,T

-  ///   multiset(T)  Domain,Range,Arg := T,int,T

+  ///   seq(T)       Domain,Range,Arg := integer,T,T

+  ///   multiset(T)  Domain,Range,Arg := T,integer,T

   ///   if AllowMap, may also be:

   ///   map(T,U)     Domain,Range,Arg := T,U,T

   ///   if AllowArray, may also be:

-  ///   array(T)     Domain,Range,Arg := int,T,T

+  ///   array(T)     Domain,Range,Arg := integer,T,T

+  /// where "integer" refers to any integer-based numeric type.

   /// </summary>

   public class IndexableTypeProxy : RestrictedTypeProxy {

     public readonly bool AllowMap;

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 3bfd17b0..06e5e640 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4077,7 +4077,7 @@ namespace Microsoft.Dafny
       } else if (proxy is IndexableTypeProxy) {

         var iProxy = (IndexableTypeProxy)proxy;

         if (t is SeqType) {

-          if (!UnifyTypes(iProxy.Domain, Type.Int)) {

+          if (!UnifyTypes(iProxy.Domain, new OperationTypeProxy(true, false, false, false))) {

             return false;

           } else if (!UnifyTypes(iProxy.Range, ((SeqType)t).Arg)) {

             return false;

@@ -4086,7 +4086,7 @@ namespace Microsoft.Dafny
           }

         } else if (iProxy.AllowArray && t.IsArrayType && t.AsArrayType.Dims == 1) {

           Type elType = UserDefinedType.ArrayElementType(t);

-          if (!UnifyTypes(iProxy.Domain, Type.Int)) {

+          if (!UnifyTypes(iProxy.Domain, new OperationTypeProxy(true, false, false, false))) {

             return false;

           } else if (!UnifyTypes(iProxy.Range, elType)) {

             return false;

@@ -4104,7 +4104,7 @@ namespace Microsoft.Dafny
         } else if (t is MultiSetType) {

           if (!UnifyTypes(iProxy.Domain, ((MultiSetType)t).Arg)) {

             return false;

-          } else if (!UnifyTypes(iProxy.Range, Type.Int)) {

+          } else if (!UnifyTypes(iProxy.Range, new OperationTypeProxy(true, false, false, false))) {

             return false;

           } else if (!UnifyTypes(iProxy.Arg, iProxy.Domain)) {

             return false;

@@ -5756,8 +5756,8 @@ namespace Microsoft.Dafny
           foreach (Expression dim in rr.ArrayDimensions) {

             Contract.Assert(dim != null);

             ResolveExpression(dim, new ResolveOpts(codeContext, true));

-            if (!UnifyTypes(dim.Type, Type.Int)) {

-              Error(stmt, "new must use an integer expression for the array size (got {0} for index {1})", dim.Type, i);

+            if (!UnifyTypes(dim.Type, new OperationTypeProxy(true, false, false, false))) {

+              Error(stmt, "new must use an integer-based expression for the array size (got {0} for index {1})", dim.Type, i);

             }

             i++;

           }

@@ -6322,8 +6322,8 @@ namespace Microsoft.Dafny
           Contract.Assert(idx != null);

           ResolveExpression(idx, opts);

           Contract.Assert(idx.Type != null);  // follows from postcondition of ResolveExpression

-          if (!UnifyTypes(idx.Type, Type.Int)) {

-            Error(idx, "array selection requires integer indices (got {0} for index {1})", idx.Type, i);

+          if (!UnifyTypes(idx.Type, new OperationTypeProxy(true, false, false, false))) {

+            Error(idx, "array selection requires integer-based numeric indices (got {0} for index {1})", idx.Type, i);

           }

           i++;

         }

@@ -6364,8 +6364,8 @@ namespace Microsoft.Dafny
             Error(e.Index, "multiset update requires domain element to be of type {0} (got {1})", elementType, e.Index.Type);

           }

           ResolveExpression(e.Value, opts);

-          if (!UnifyTypes(e.Value.Type, Type.Int)) {

-            Error(e.Value, "multiset update requires integer value (got {0})", e.Value.Type);

+          if (!UnifyTypes(e.Value.Type, new OperationTypeProxy(true, false, false, false))) {

+            Error(e.Value, "multiset update requires integer-based numeric value (got {0})", e.Value.Type);

           }

           expr.Type = e.Seq.Type;

 

@@ -8381,8 +8381,9 @@ namespace Microsoft.Dafny
       if (e.E1 != null) {

         ResolveExpression(e.E1, opts);

         Contract.Assert(e.E1.Type != null);  // follows from postcondition of ResolveExpression

-        if (!UnifyTypes(e.E1.Type, domainType)) {

-          Error(e.E1, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E1.Type, domainType);

+        var domType = e.E0 == null ? domainType : new OperationTypeProxy(true, false, false, false);  // reuse 'domainType' if .E0 did not use it; otherwise, create a new proxy to allow .E1 to be any integer-based numeric type, independent of the integer-based numeric type used by .E0

+        if (!UnifyTypes(e.E1.Type, domType)) {

+          Error(e.E1, "sequence/array/multiset/map selection requires {1} indices (got {0})", e.E1.Type, domType);

         }

       }

       if (!seqErr) {

diff --git a/Test/dafny0/Newtypes.dfy b/Test/dafny0/Newtypes.dfy
index 77fbe75d..bab42378 100644
--- a/Test/dafny0/Newtypes.dfy
+++ b/Test/dafny0/Newtypes.dfy
@@ -155,3 +155,75 @@ module X {
     var y := var j := 3.0; j;

   }

 }

+

+module IntegerBasedValues {

+  // Dafny allows any integer-based type, not just 'int', in the following

+  // places:

+  //   * array indices (any dimension)

+  //   * array lengths (with new, any dimension)

+  //   * sequence indicies

+  //   * subsequence bounds (like sq[lo..hi])

+  //   * the new multiplicity in multiset update (m[t := multiplicity])

+  //   * subarray-to-sequence bounds (like a[lo..hi])

+  // Note that for an array 'a', 'a.Length' is always an integer, so a

+  // comparison 'i < a.Length' still requires 'i' to be an integer, not

+  // any integer-based value.  Same for '|sq|' for a sequence 'sq'.

+

+  type T

+

+  newtype Even = x | x % 2 == 0

+

+  method BadSpec(o: Even)

+    requires 1 < o;  // error: 1 is not of type Even

+

+  method Arrays(n: nat, o: Even, i: Even, j: Even, k: nat) returns (x: T)

+    requires 0 <= o && 0 <= i && 0 <= j;

+  {

+    var a := new T[n];

+    var b := new T[o];

+    var m := new T[o, n];

+    if {

+      case int(i) < n        =>  x := a[i];

+      case int(i) < a.Length =>  x := a[i];

+      case i < o             =>  x := b[i];

+      case int(i) < b.Length =>  x := b[i];

+      case k < m.Length0 && int(j) < m.Length1 =>  x := m[k, j];

+      case int(i) < m.Length0 && k < m.Length1 =>  x := m[i, k];

+      case int(i) < m.Length0 && int(j) < m.Length1 =>  x := m[i, j];

+      case int(i) < m.Length0 && int(j) < m.Length1 =>  x := m[j, j];  // error: bad index 0

+      case int(i) < m.Length0 && int(j) < m.Length1 =>  x := m[i, i];  // error: bad index 1

+      case true =>

+    }

+  }

+  

+  method Sequences(a: seq<T>, n: nat, i: Even, lo: Even, hi: Even) returns (x: T, b: seq<T>)

+    requires 0 <= i && 0 <= lo <= hi;

+  {

+    if {

+      case int(i) < |a|                   =>  x := a[i];

+      case |a| % 2 == 0 && i < Even(|a|)  =>  x := a[i];

+      case int(hi) <= |a|                 =>  b := a[lo..hi];

+      case int(hi) <= |a|                 =>  b := a[..hi];

+      case int(hi) <= |a|                 =>  b := a[0..hi];

+      case int(lo) <= |a|                 =>  b := a[lo..];

+      case int(lo) <= |a|                 =>  b := a[lo..|a|];

+      case int(lo) <= |a| && |a| % 2 == 0 =>  assert a[lo..|a|] == a[lo..Even(|a|)];

+      case n <= int(hi) <= |a|            =>  b := a[n..hi];

+      case int(lo) <= n <= |a|            =>  b := a[lo..n];

+      case int(hi + hi) <= |a|            =>  b := a[lo..Even(2*hi)];

+      case true =>

+    }

+  }

+

+  method MultisetUpdate<U>(m: multiset<U>, t: U, n: Even) returns (m': multiset<U>)

+  {

+    if {

+      case true   =>

+        m' := m[t := n];  // error: n may be negative

+        m' := m[t := n+n];  // fine, if the previous statement was

+      case 0 <= n =>  m' := m[t := n];

+      case 0 <= n =>  m' := m[t := n+n+1];  // error: n+n+1 is not Even (like n+n and 1 are)

+      case 0 <= n =>  m' := m[t := int(n+n)+1];

+    }

+  }

+}

diff --git a/Test/dafny0/Newtypes.dfy.expect b/Test/dafny0/Newtypes.dfy.expect
index 2678e526..7af53142 100644
--- a/Test/dafny0/Newtypes.dfy.expect
+++ b/Test/dafny0/Newtypes.dfy.expect
@@ -19,5 +19,28 @@ Execution trace:
 Newtypes.dfy(104,16): Error: result of operation might violate newtype constraint

 Execution trace:

     (0,0): anon0

+Newtypes.dfy(177,14): Error: result of operation might violate newtype constraint

+Execution trace:

+    (0,0): anon0

+Newtypes.dfy(193,64): Error: index 0 out of range

+Execution trace:

+    (0,0): anon0

+    (0,0): anon32_Then

+    (0,0): anon33_Then

+    (0,0): anon16

+Newtypes.dfy(194,67): Error: index 1 out of range

+Execution trace:

+    (0,0): anon0

+    (0,0): anon34_Then

+    (0,0): anon35_Then

+    (0,0): anon19

+Newtypes.dfy(222,16): Error: new number of occurrences might be negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon6_Then

+Newtypes.dfy(225,40): Error: result of operation might violate newtype constraint

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Then

 

-Dafny program verifier finished with 30 verified, 6 errors

+Dafny program verifier finished with 35 verified, 11 errors

diff --git a/Test/dafny0/NewtypesResolution.dfy b/Test/dafny0/NewtypesResolution.dfy
index 0fe36eec..dbf9a175 100644
--- a/Test/dafny0/NewtypesResolution.dfy
+++ b/Test/dafny0/NewtypesResolution.dfy
@@ -203,3 +203,49 @@ module QualifiedDatatypeCtor {
     var f := S.Cons(50, S.Nil);

   }

 }

+

+module IntegerBasedValues {

+  type T

+

+  newtype Even = x | x % 2 == 0

+

+  method Arrays(n: nat, o: Even, i: Even) returns (x: T)

+    requires 0 <= o;

+    requires -1 < i;  // note, -1 is not of type Even, but that's for the verifier (not type checker) to check

+  {

+    var a := new T[n];

+    var b := new T[o];

+    var m := new T[o, n];

+    var m' := new T[o, n, 3.14];  // error: 3.14 is not of an integer-based type

+    if {

+      case i < n =>  // error: i and n are of different integer-based types

+        x := a[i];

+      case i < a.Length =>  // error: i and a.Length are of different integer-based types

+        x := a[i];

+      case i < o =>

+        x := b[i];

+      case i < b.Length =>  // error: i and b.Length are of different integer-based types

+        x := b[i];

+      case i < m.Length0 =>  // error: i and m.Length0 are of different integer-based types

+      case i < m.Length1 =>  // error: i and m.Length1 are of different integer-based types

+    }

+  }

+  

+  method Sequences(a: seq<T>, i: Even) returns (x: T, b: seq<T>)

+    requires 0 <= i;

+  {

+    if {

+      case i < |a| =>  // error: i and |a| are of different integer-based types

+        x := a[i];

+      case i <= int(|a|) =>  // error: type of i is a different integer-based type than int

+        b := a[0..i];

+    }

+  }

+

+  method MultisetUpdate<U>(m: multiset<U>, t: U, n: Even)

+  {

+    var m' := m[t := n];

+    m' := m[t := 12];

+    m' := m[t := 1.1415];  // error: real is not an integer-based numeric type

+  }

+}

diff --git a/Test/dafny0/NewtypesResolution.dfy.expect b/Test/dafny0/NewtypesResolution.dfy.expect
index 81c43d35..bb1624f9 100644
--- a/Test/dafny0/NewtypesResolution.dfy.expect
+++ b/Test/dafny0/NewtypesResolution.dfy.expect
@@ -22,4 +22,13 @@ NewtypesResolution.dfy(157,11): Error: name of type ('Syn') is used as a variabl
 NewtypesResolution.dfy(162,8): Error: member U does not exist in class Klass

 NewtypesResolution.dfy(162,4): Error: expected method call, found expression

 NewtypesResolution.dfy(188,39): Error: incorrect type of datatype constructor argument (found Dt<bool>, expected S)

-24 resolution/type errors detected in NewtypesResolution.dfy

+NewtypesResolution.dfy(219,11): Error: new must use an integer-based expression for the array size (got real for index 2)

+NewtypesResolution.dfy(221,13): Error: arguments to < must have the same type (got Even and nat)

+NewtypesResolution.dfy(223,13): Error: arguments to < must have the same type (got Even and int)

+NewtypesResolution.dfy(227,13): Error: arguments to < must have the same type (got Even and int)

+NewtypesResolution.dfy(229,13): Error: arguments to < must have the same type (got Even and int)

+NewtypesResolution.dfy(230,13): Error: arguments to < must have the same type (got Even and int)

+NewtypesResolution.dfy(238,13): Error: arguments to < must have the same type (got Even and int)

+NewtypesResolution.dfy(240,13): Error: arguments to <= must have the same type (got Even and int)

+NewtypesResolution.dfy(249,17): Error: multiset update requires integer-based numeric value (got real)

+33 resolution/type errors detected in NewtypesResolution.dfy