Added a sequence update expression in Dafny.

6 files changed, 124 insertions, 14 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 022dc912..5da2b44b 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -847,14 +847,20 @@ SelectOrCallSuffix<ref Expression! e>
         [ ".."                                 (. anyDots = true; .)

           [ Expression<out ee>                 (. e1 = ee; .)

           ]

+        | ":="

+          Expression<out ee>                   (. e1 = ee; .)

         ]

       | ".." Expression<out ee>                (. anyDots = true;  e1 = ee; .)

-      )                                        (. if (!anyDots) {

-                                                    assert e1 == null;

-                                                    e = new SeqSelectExpr(x, true, e, e0, null);

-                                                  } else {

+      )                                        (. assert !anyDots ==> e0 != null;

+                                                  if (anyDots) {

                                                     assert e0 != null || e1 != null;

                                                     e = new SeqSelectExpr(x, false, e, e0, e1);

+                                                  } else if (e1 == null) {

+                                                    assert e0 != null;

+                                                    e = new SeqSelectExpr(x, true, e, e0, null);

+                                                  } else {

+                                                    assert e0 != null;

+                                                    e = new SeqUpdateExpr(x, e, e0, e1);

                                                   }

                                                .)

     "]"

diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index 4b97edbd..f50ded86 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -871,6 +871,20 @@ namespace Microsoft.Dafny
     }

   }

 

+  public class SeqUpdateExpr : Expression {

+    public readonly Expression! Seq;

+    public readonly Expression! Index;

+    public readonly Expression! Value;

+    

+    public SeqUpdateExpr(Token! tok, Expression! seq, Expression! index, Expression! val)

+    {

+      Seq = seq;

+      Index = index;

+      Value = val;

+      base(tok);

+    }

+  }

+

   public class FunctionCallExpr : Expression {

     public readonly string! Name;

     [Peer] public readonly Expression! Receiver;

diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc
index 0fd3e612..6b12d796 100644
--- a/Source/Dafny/Parser.ssc
+++ b/Source/Dafny/Parser.ssc
@@ -1312,10 +1312,16 @@ public static int Parse (List<ClassDecl!>! classes) {
 			if (StartOf(5)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (t.kind == 78) {

-					Get();

-					anyDots = true; 

-					if (StartOf(5)) {

+				if (t.kind == 35 || t.kind == 78) {

+					if (t.kind == 78) {

+						Get();

+						anyDots = true; 

+						if (StartOf(5)) {

+							Expression(out ee);

+							e1 = ee; 

+						}

+					} else {

+						Get();

 						Expression(out ee);

 						e1 = ee; 

 					}

@@ -1325,12 +1331,16 @@ public static int Parse (List<ClassDecl!>! classes) {
 				Expression(out ee);

 				anyDots = true;  e1 = ee; 

 			} else Error(118);

-			if (!anyDots) {

-			 assert e1 == null;

-			 e = new SeqSelectExpr(x, true, e, e0, null);

-			} else {

+			assert !anyDots ==> e0 != null;

+			if (anyDots) {

 			  assert e0 != null || e1 != null;

 			  e = new SeqSelectExpr(x, false, e, e0, e1);

+			} else if (e1 == null) {

+			  assert e0 != null;

+			  e = new SeqSelectExpr(x, true, e, e0, null);

+			} else {

+			  assert e0 != null;

+			  e = new SeqUpdateExpr(x, e, e0, e1);

 			}

 			

 			Expect(76);

diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc
index ba44f9a9..68b9e132 100644
--- a/Source/Dafny/Printer.ssc
+++ b/Source/Dafny/Printer.ssc
@@ -495,6 +495,22 @@ namespace Microsoft.Dafny {
         wr.Write("]");

         if (parensNeeded) { wr.Write(")"); }

       

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr e = (SeqUpdateExpr)expr;

+        // determine if parens are needed

+        int opBindingStrength = 0x70;

+        bool parensNeeded = opBindingStrength < contextBindingStrength ||

+          (fragileContext && opBindingStrength == contextBindingStrength);

+        

+        if (parensNeeded) { wr.Write("("); }

+        PrintExpr(e.Seq, 00, false, indent);  // BOGUS: fix me

+        wr.Write("[");

+        PrintExpression(e.Index);

+        wr.Write(" := ");

+        PrintExpression(e.Value);

+        wr.Write("]");

+        if (parensNeeded) { wr.Write(")"); }

+      

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         // determine if parens are needed

diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc
index 47727562..7f1342f1 100644
--- a/Source/Dafny/Resolver.ssc
+++ b/Source/Dafny/Resolver.ssc
@@ -1020,14 +1020,14 @@ namespace Microsoft.Dafny {
           ResolveExpression(e.E0, twoState);

           assert e.E0.Type != null;  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(e.E0.Type, Type.Int)) {

-            Error(e.E0, "sequence selections requires integer indices (got {0})", e.E0.Type);

+            Error(e.E0, "sequence selection requires integer indices (got {0})", e.E0.Type);

           }

         }

         if (e.E1 != null) {

           ResolveExpression(e.E1, twoState);

           assert e.E1.Type != null;  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(e.E1.Type, Type.Int)) {

-            Error(e.E1, "sequence selections requires integer indices (got {0})", e.E1.Type);

+            Error(e.E1, "sequence selection requires integer indices (got {0})", e.E1.Type);

           }

         }

         if (!seqErr) {

@@ -1038,6 +1038,30 @@ namespace Microsoft.Dafny {
           }

         }

         

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr e = (SeqUpdateExpr)expr;

+        bool seqErr = false;

+        ResolveExpression(e.Seq, twoState);

+        assert e.Seq.Type != null;  // follows from postcondition of ResolveExpression

+        Type elementType = new InferredTypeProxy();

+        if (!UnifyTypes(e.Seq.Type, new SeqType(elementType))) {

+          Error(expr, "sequence update requires a sequence (got {0})", e.Seq.Type);

+          seqErr = true;

+        }

+        ResolveExpression(e.Index, twoState);

+        assert e.Index.Type != null;  // follows from postcondition of ResolveExpression

+        if (!UnifyTypes(e.Index.Type, Type.Int)) {

+          Error(e.Index, "sequence update requires integer index (got {0})", e.Index.Type);

+        }

+        ResolveExpression(e.Value, twoState);

+        assert e.Value.Type != null;  // follows from postcondition of ResolveExpression

+        if (!UnifyTypes(e.Value.Type, elementType)) {

+          Error(e.Value, "sequence update requires the value to have the element type of the sequence (got {0})", e.Value.Type);

+        }

+        if (!seqErr) {

+          expr.Type = e.Seq.Type;

+        }

+        

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         ResolveExpression(e.Receiver, twoState);

diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 33002065..ae8f03a5 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -695,6 +695,15 @@ namespace Microsoft.Dafny {
           total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true));

         }

         return total;

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr e = (SeqUpdateExpr)expr;

+        Bpl.Expr total = IsTotal(e.Seq, etran);

+        Bpl.Expr seq = etran.TrExpr(e.Seq);

+        Bpl.Expr index = etran.TrExpr(e.Index);

+        total = BplAnd(total, IsTotal(e.Index, etran));

+        total = BplAnd(total, InSeqRange(expr.tok, index, seq, null, false));

+        total = BplAnd(total, IsTotal(e.Value, etran));

+        return total;

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         Bpl.Expr r = IsTotal(e.Receiver, etran);

@@ -825,6 +834,14 @@ namespace Microsoft.Dafny {
           CheckWellformed(e.E1, func, Position.Neither, builder, etran);

           builder.Add(new Bpl.AssertCmd(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true)));

         }

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr e = (SeqUpdateExpr)expr;

+        CheckWellformed(e.Seq, func, Position.Neither, builder, etran);

+        Bpl.Expr seq = etran.TrExpr(e.Seq);

+        Bpl.Expr index = etran.TrExpr(e.Index);

+        CheckWellformed(e.Index, func, Position.Neither, builder, etran);

+        builder.Add(new Bpl.AssertCmd(expr.tok, InSeqRange(expr.tok, index, seq, null, false)));

+        CheckWellformed(e.Value, func, Position.Neither, builder, etran);

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         CheckWellformed(e.Receiver, func, Position.Neither, builder, etran);

@@ -1891,6 +1908,15 @@ namespace Microsoft.Dafny {
             return seq;

           }

         

+        } else if (expr is SeqUpdateExpr) {

+          SeqUpdateExpr e = (SeqUpdateExpr)expr;

+          Bpl.Expr seq = TrExpr(e.Seq);

+          Type elmtType = ((SeqType!)e.Seq.Type).Arg;

+          Bpl.Type elType = translator.TrType(elmtType);

+          Bpl.Expr index = TrExpr(e.Index);

+          Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType);

+          return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val);

+        

         } else if (expr is FunctionCallExpr) {

           FunctionCallExpr e = (FunctionCallExpr)expr;

           string nm = ((!)e.Function).FullName + (e is UseExpr ? "#use" : "");

@@ -2308,6 +2334,7 @@ namespace Microsoft.Dafny {
       SeqBuild,

       SeqAppend,

       SeqIndex,

+      SeqUpdate,

       SeqContains,

       SeqDrop,

       SeqTake,

@@ -2395,6 +2422,10 @@ namespace Microsoft.Dafny {
           assert args.Length == 2;

           assert typeInstantiation != null;

           return FunctionCall(tok, "Seq#Index", typeInstantiation, args);

+        case BuiltinFunction.SeqUpdate:

+          assert args.Length == 3;

+          assert typeInstantiation != null;

+          return FunctionCall(tok, "Seq#Update", predef.SeqType(tok, typeInstantiation), args);

         case BuiltinFunction.SeqContains:

           assert args.Length == 2;

           assert typeInstantiation == null;

@@ -2616,6 +2647,15 @@ namespace Microsoft.Dafny {
           newExpr = new SeqSelectExpr(sse.tok, sse.SelectOne, seq, e0, e1);

         }

         

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr sse = (SeqUpdateExpr)expr;

+        Expression seq = Substitute(sse.Seq, receiverReplacement, substMap);

+        Expression index = Substitute(sse.Index, receiverReplacement, substMap);

+        Expression val = Substitute(sse.Value, receiverReplacement, substMap);

+        if (seq != sse.Seq || index != sse.Index || val != sse.Value) {

+          newExpr = new SeqUpdateExpr(sse.tok, seq, index, val);

+        }

+        

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

         Expression receiver = Substitute(e.Receiver, receiverReplacement, substMap);