Removed some old code for the defunct array-range assignments

2 files changed, 40 insertions, 68 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2486f337..a30ff65d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3328,11 +3328,7 @@ namespace Microsoft.Dafny
       } else if (stmt is AssignStmt) {

         AssignStmt s = (AssignStmt)stmt;

         int prevErrorCount = ErrorCount;

-        if (s.Lhs is SeqSelectExpr) {

-          ResolveSeqSelectExpr((SeqSelectExpr)s.Lhs, true, false);  // allow ghosts for now, tighted up below

-        } else {

-          ResolveExpression(s.Lhs, true);  // allow ghosts for now, tighted up below

-        }

+        ResolveExpression(s.Lhs, true);  // allow ghosts for now, tighted up below

         bool lhsResolvedSuccessfully = ErrorCount == prevErrorCount;

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

         // check that LHS denotes a mutable variable or a field

@@ -3397,43 +3393,38 @@ namespace Microsoft.Dafny
 

         s.IsGhost = lvalueIsGhost;

         Type lhsType = s.Lhs.Type;

-        if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {

-          Error(stmt, "cannot assign to a range of array elements (try the 'parallel' statement)");

-          //lhsType = UserDefinedType.ArrayElementType(lhsType);

-        } else {

-          if (s.Rhs is ExprRhs) {

-            ExprRhs rr = (ExprRhs)s.Rhs;

-            ResolveExpression(rr.Expr, true);

-            if (!lvalueIsGhost) {

-              CheckIsNonGhost(rr.Expr);

-            }

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

-            if (!UnifyTypes(lhsType, rr.Expr.Type)) {

-              Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType);

-            }

-          } else if (s.Rhs is TypeRhs) {

-            TypeRhs rr = (TypeRhs)s.Rhs;

-            Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, codeContext);

-            if (!lvalueIsGhost) {

-              if (rr.ArrayDimensions != null) {

-                foreach (var dim in rr.ArrayDimensions) {

-                  CheckIsNonGhost(dim);

-                }

-              }

-              if (rr.InitCall != null) {

-                foreach (var arg in rr.InitCall.Args) {

-                  CheckIsNonGhost(arg);

-                }

+        if (s.Rhs is ExprRhs) {

+          ExprRhs rr = (ExprRhs)s.Rhs;

+          ResolveExpression(rr.Expr, true);

+          if (!lvalueIsGhost) {

+            CheckIsNonGhost(rr.Expr);

+          }

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

+          if (!UnifyTypes(lhsType, rr.Expr.Type)) {

+            Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType);

+          }

+        } else if (s.Rhs is TypeRhs) {

+          TypeRhs rr = (TypeRhs)s.Rhs;

+          Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, codeContext);

+          if (!lvalueIsGhost) {

+            if (rr.ArrayDimensions != null) {

+              foreach (var dim in rr.ArrayDimensions) {

+                CheckIsNonGhost(dim);

               }

             }

-            if (!UnifyTypes(lhsType, t)) {

-              Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType);

+            if (rr.InitCall != null) {

+              foreach (var arg in rr.InitCall.Args) {

+                CheckIsNonGhost(arg);

+              }

             }

-          } else if (s.Rhs is HavocRhs) {

-            // nothing else to do

-          } else {

-            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS

           }

+          if (!UnifyTypes(lhsType, t)) {

+            Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType);

+          }

+        } else if (s.Rhs is HavocRhs) {

+          // nothing else to do

+        } else {

+          Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS

         }

       } else if (stmt is VarDecl) {

         VarDecl s = (VarDecl)stmt;

@@ -3771,23 +3762,17 @@ namespace Microsoft.Dafny
 

       int prevErrorCount = ErrorCount;

       // First, resolve all LHS's and expression-looking RHS's.

-      SeqSelectExpr arrayRangeLhs = null;

       var update = s as UpdateStmt;

 

       foreach (var lhs in s.Lhss) {

         var ec = ErrorCount;

-        if (lhs is SeqSelectExpr) {

-          var sse = (SeqSelectExpr)lhs;

-          ResolveSeqSelectExpr(sse, true, true);

-          if (arrayRangeLhs == null && !sse.SelectOne) {

-            arrayRangeLhs = sse;

-          }

-        } else {

-          ResolveExpression(lhs, true);

-        }

+        ResolveExpression(lhs, true);

         if (update == null && ec == ErrorCount && specContextOnly && !AssignStmt.LhsIsToGhost(lhs)) {

           Error(lhs, "cannot assign to non-ghost variable in a ghost context");

         }

+        if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {

+          Error(lhs, "cannot assign to a range of array elements (try the 'parallel' statement)");

+        }

       }

       // Resolve RHSs

       if (update == null) {

@@ -3848,8 +3833,6 @@ namespace Microsoft.Dafny
           Error(s, "expected method call, found expression");

         } else if (s.Lhss.Count != update.Rhss.Count) {

           Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count);

-        } else if (arrayRangeLhs != null && s.Lhss.Count != 1) {

-          Error(arrayRangeLhs, "array-range may not be used as LHS of multi-assignment; use separate assignment statements for each array-range assignment");

         } else if (ErrorCount == prevErrorCount) {

           // add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)

           for (int i = 0; i < s.Lhss.Count; i++) {

@@ -3882,8 +3865,6 @@ namespace Microsoft.Dafny
         // if there was an effectful RHS, that must be the only RHS

         if (update.Rhss.Count != 1) {

           Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");

-        } else if (arrayRangeLhs != null) {

-          Error(arrayRangeLhs, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");

         } else if (callRhs == null) {

           // must be a single TypeRhs

           if (s.Lhss.Count != 1) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0dd78b1e..008ca31f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -72,21 +72,12 @@ TypeTests.dfy(58,8): Error: Duplicate local-variable name: x
 TypeTests.dfy(61,6): Error: Duplicate local-variable name: y

 TypeTests.dfy(68,17): Error: member F in type C does not refer to a method

 TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments

-TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(82,2): Error: LHS of array assignment must denote an array element (found seq<C>)

-TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(83,2): Error: LHS of array assignment must denote an array element (found seq<C>)

-TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)

-TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(78,3): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(79,3): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(80,3): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(82,3): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(83,3): Error: cannot assign to a range of array elements (try the 'parallel' statement)

+TypeTests.dfy(84,3): Error: cannot assign to a range of array elements (try the 'parallel' statement)

 TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a subrange type

 TypeTests.dfy(91,9): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type

@@ -95,7 +86,7 @@ TypeTests.dfy(105,15): Error: ghost variables are allowed only in specification
 TypeTests.dfy(115,4): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(116,7): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-37 resolution/type errors detected in TypeTests.dfy

+28 resolution/type errors detected in TypeTests.dfy

 

 -------------------- NatTypes.dfy --------------------

 NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative