Added s[..] syntax in anticipation of sequence forming operation. (also updated regression tests.)

4 files changed, 38 insertions, 35 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index f6e40722..bcd23618 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1354,7 +1354,9 @@ Suffix<ref Expression/*!*/ e>
                                                .)

           }

         )

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

+      | ".."                                   (. anyDots = true; .)

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

+	    ]

       )

       (. if (multipleIndices != null) {

            e = new MultiSelectExpr(x, e, multipleIndices);

@@ -1367,7 +1369,7 @@ Suffix<ref Expression/*!*/ e>
            }

            Contract.Assert(anyDots || e0 != null);

            if (anyDots) {

-             Contract.Assert(e0 != null || e1 != null);

+             //Contract.Assert(e0 != null || e1 != null);

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

            } else if (e1 == null) {

              Contract.Assert(e0 != null);

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 4868be10..ce3e479e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2113,7 +2113,6 @@ namespace Microsoft.Dafny {
     void ObjectInvariant() {

       Contract.Invariant(Seq != null);

       Contract.Invariant(!SelectOne || E1 == null);

-      Contract.Invariant(E0 != null || E1 != null);

     }

 

     public SeqSelectExpr(IToken tok, bool selectOne, Expression seq, Expression e0, Expression e1)

@@ -2121,7 +2120,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Requires(seq != null);

       Contract.Requires(!selectOne || e1 == null);

-      Contract.Requires(e0 != null || e1 != null);

 

       SelectOne = selectOne;

       Seq = seq;

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index e12ab7e3..4041ad45 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1570,7 +1570,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Term(out e1);

 			e = new BinaryExpr(x, op, e0, e1);

 			if (op == BinaryExpr.Opcode.Disjoint)

-			acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

+			  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

 			

 			while (StartOf(16)) {

 				if (chain == null) {

@@ -1603,36 +1603,35 @@ List<Expression/*!*/>/*!*/ decreases) {
 				   break;

 				 case BinaryExpr.Opcode.Neq:

 				   if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); }

-				if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }

-				                              hasSeenNeq = true;  break;

-				                            case BinaryExpr.Opcode.Lt:

-				                            case BinaryExpr.Opcode.Le:

-				                              if (kind == 0) { kind = 1; }

-				                              else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }

-				                              break;

-				                            case BinaryExpr.Opcode.Gt:

-				                            case BinaryExpr.Opcode.Ge:

-				                              if (kind == 0) { kind = 2; }

-				                              else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }

-				                              break;

-				                            case BinaryExpr.Opcode.Disjoint:

-				                              if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }

-				break;

-				                            default:

-				                              SemErr(x, "this operator cannot be part of a chain");

-				                              kind = 3;  break;

-				                          }

-				                       

+				   if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }

+				   hasSeenNeq = true;  break;

+				 case BinaryExpr.Opcode.Lt:

+				 case BinaryExpr.Opcode.Le:

+				   if (kind == 0) { kind = 1; }

+				   else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }

+				   break;

+				 case BinaryExpr.Opcode.Gt:

+				 case BinaryExpr.Opcode.Ge:

+				   if (kind == 0) { kind = 2; }

+				   else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }

+				   break;

+				 case BinaryExpr.Opcode.Disjoint:

+				   if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }

+				   break;

+				 default:

+				   SemErr(x, "this operator cannot be part of a chain");

+				   kind = 3;  break;

+				}

+				

 				Term(out e1);

 				ops.Add(op); chain.Add(e1);

-				if (op == BinaryExpr.Opcode.Disjoint)

-				{

+				if (op == BinaryExpr.Opcode.Disjoint) {

 				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

-				acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

-				    }

-				 else

-				   e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

-				                         

+				  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

+				}

+				else

+				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

+				

 			}

 		}

 		if (chain != null) {

@@ -1916,8 +1915,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 				} else SynErr(136);

 			} else if (la.kind == 97) {

 				Get();

-				Expression(out ee);

-				anyDots = true;  e1 = ee; 

+				anyDots = true; 

+				if (StartOf(8)) {

+					Expression(out ee);

+					e1 = ee; 

+				}

 			} else SynErr(137);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

@@ -1930,7 +1932,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			  }

 			  Contract.Assert(anyDots || e0 != null);

 			  if (anyDots) {

-			    Contract.Assert(e0 != null || e1 != null);

+			    //Contract.Assert(e0 != null || e1 != null);

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

 			  } else if (e1 == null) {

 			    Contract.Assert(e0 != null);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index d1c77122..6b77ca71 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4674,6 +4674,7 @@ namespace Microsoft.Dafny {
             if (e0 != null) {

               seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqDrop, elType, seq, e0);

             }

+            // if e0 == null && e1 == null, then we have the identity operation seq[..];

             return seq;

           }