Renamed terms into lines (according to the proposal), fixed some contracts

7 files changed, 41 insertions, 39 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 8a7b314c..2997b343 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -424,7 +424,7 @@ namespace Microsoft.Dafny
 

       } else if (stmt is CalcStmt) {

           var s = (CalcStmt)stmt;

-          r = new CalcStmt(Tok(s.Tok), s.Terms.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneStmt));

+          r = new CalcStmt(Tok(s.Tok), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneStmt));

 

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 2d8b9f1c..adb17fb7 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1220,7 +1220,7 @@ ParallelStmt<out Statement/*!*/ s>
 CalcStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);

      Token x;

-     List<Expression/*!*/> steps = new List<Expression/*!*/>();

+     List<Expression/*!*/> lines = new List<Expression/*!*/>();

      List<Statement> hints = new List<Statement>(); 

      Expression/*!*/ e;

      BlockStmt/*!*/ block;

@@ -1228,17 +1228,17 @@ CalcStmt<out Statement/*!*/ s>
   .)

   "calc"                                                (. x = t; .)

   "{"

-  Expression<out e>                                     (. steps.Add(e); .)

+  Expression<out e>                                     (. lines.Add(e); .)

   ";"

   { 

     ( BlockStmt<out block, out bodyStart, out bodyEnd>  (. hints.Add(block); .)

     |                                                   (. hints.Add(null); .)

     )

-    Expression<out e>                                   (. steps.Add(e); .)

+    Expression<out e>                                   (. lines.Add(e); .)

     ";"

   }

   "}"

-  (. s = new CalcStmt(x, steps, hints); .)

+  (. s = new CalcStmt(x, lines, hints); .)

   .

 /*------------------------------------------------------------------------*/

 Expression<out Expression/*!*/ e>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index f138a4d9..714d87e7 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2664,32 +2664,32 @@ namespace Microsoft.Dafny {
 

   public class CalcStmt : Statement

   {

-    public readonly List<Expression/*!*/> Terms;

+    public readonly List<Expression/*!*/> Lines;

     public readonly List<Statement> Hints;  // an empty hint is represented with null

-    public readonly List<BinaryExpr/*!*/> Steps; // expressions ti op t<i + 1>, filled in during resolution in order to get the correct op

-    public BinaryExpr Result; // expressions t0 op tn, filled in during resolution in order to get the correct op

+    public readonly List<BinaryExpr/*!*/> Steps; // expressions li op l<i + 1>, filled in during resolution in order to get the correct op

+    public BinaryExpr Result; // expressions l0 op ln, filled in during resolution in order to get the correct op

 

     [ContractInvariantMethod]

     void ObjectInvariant()

     {

-      Contract.Invariant(Terms != null);

+      Contract.Invariant(Lines != null);

       Contract.Invariant(Hints != null);

-      Contract.Invariant(Terms.Count > 0);

-      Contract.Invariant(Hints.Count == Terms.Count - 1);

-      Contract.Invariant(Steps.Count == 0 /*before resolution*/ || Steps.Count == Hints.Count /*after resolution*/);

+      Contract.Invariant(Steps != null);

+      Contract.Invariant(Lines.Count > 0);

+      Contract.Invariant(Hints.Count == Lines.Count - 1);

     }

 

-    public CalcStmt(IToken tok, List<Expression/*!*/> terms, List<Statement> hints)

+    public CalcStmt(IToken tok, List<Expression/*!*/> lines, List<Statement> hints)

       // Attributes attrs?

       : base(tok)

     {

       Contract.Requires(tok != null);

-      Contract.Requires(terms != null);

-      Contract.Requires(cce.NonNullElements(terms));

+      Contract.Requires(lines != null);

+      Contract.Requires(cce.NonNullElements(lines));

       Contract.Requires(hints != null);

-      Contract.Requires(terms.Count > 0);

-      Contract.Requires(hints.Count == terms.Count - 1);

-      this.Terms = terms;

+      Contract.Requires(lines.Count > 0);

+      Contract.Requires(hints.Count == lines.Count - 1);

+      this.Lines = lines;

       this.Hints = hints;

       this.Steps = new List<BinaryExpr>();  

       this.Result = null;

@@ -2706,8 +2706,8 @@ namespace Microsoft.Dafny {
     public override IEnumerable<Expression> SubExpressions

     {

       get {

-        foreach (var t in Terms) {

-            yield return t;

+        foreach (var l in Lines) {

+            yield return l;

         }

       }

     }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index ebde5f12..7c8cf8a2 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1619,7 +1619,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 	void CalcStmt(out Statement/*!*/ s) {

 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);

 		Token x;

-		List<Expression/*!*/> steps = new List<Expression/*!*/>();

+		List<Expression/*!*/> lines = new List<Expression/*!*/>();

 		List<Statement> hints = new List<Statement>(); 

 		Expression/*!*/ e;

 		BlockStmt/*!*/ block;

@@ -1629,7 +1629,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		x = t; 

 		Expect(6);

 		Expression(out e);

-		steps.Add(e); 

+		lines.Add(e); 

 		Expect(14);

 		while (StartOf(10)) {

 			if (la.kind == 6) {

@@ -1639,11 +1639,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				hints.Add(null); 

 			}

 			Expression(out e);

-			steps.Add(e); 

+			lines.Add(e); 

 			Expect(14);

 		}

 		Expect(7);

-		s = new CalcStmt(x, steps, hints); 

+		s = new CalcStmt(x, lines, hints); 

 	}

 

 	void ReturnStmt(out Statement/*!*/ s) {

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 8d7eb26e..f9f1f005 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -564,19 +564,19 @@ namespace Microsoft.Dafny {
         CalcStmt s = (CalcStmt)stmt;

         wr.Write("calc");

         wr.WriteLine(" {");

-        int stepInd = indent + IndentAmount;

-        Indent(stepInd);

-        PrintExpression(s.Terms[0], stepInd);

+        int lineInd = indent + IndentAmount;

+        Indent(lineInd);

+        PrintExpression(s.Lines.First(), lineInd);

         wr.WriteLine(";");

-        var pairs = s.Hints.Zip(s.Terms.Skip(1), (h, e) => Tuple.Create(h, e));

+        var pairs = s.Hints.Zip(s.Lines.Skip(1), (h, e) => Tuple.Create(h, e));

         foreach (var pair in pairs) {

           if (pair.Item1 != null) {

-            Indent(stepInd);

-            PrintStatement(pair.Item1, stepInd);

+            Indent(lineInd);

+            PrintStatement(pair.Item1, lineInd);

             wr.WriteLine();

           }

-          Indent(stepInd);

-          PrintExpression(pair.Item2, stepInd);

+          Indent(lineInd);

+          PrintExpression(pair.Item2, lineInd);

           wr.WriteLine(";");

         }

         Indent(indent);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 1c72ad31..771ea477 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3133,13 +3133,14 @@ namespace Microsoft.Dafny
         }

 		

       } else if (stmt is CalcStmt) {

+        int prevErrorCount = ErrorCount;

         CalcStmt s = (CalcStmt)stmt;

         s.IsGhost = true;

-        Contract.Assert(s.Terms.Count > 0); // follows from the invariant of CalcStatement

-        var e0 = s.Terms.First();

+        Contract.Assert(s.Lines.Count > 0); // follows from the invariant of CalcStatement

+        var e0 = s.Lines.First();

         ResolveExpression(e0, true);

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

-        foreach (var e1 in s.Terms.Skip(1))

+        foreach (var e1 in s.Lines.Skip(1))

         {

           ResolveExpression(e1, true);

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

@@ -3158,8 +3159,9 @@ namespace Microsoft.Dafny
             ResolveStatement(h, true, method);

           }

         }

-        s.Result = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Eq, s.Terms.First(), s.Terms.Last());

+        s.Result = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Eq, s.Lines.First(), s.Lines.Last());

         ResolveExpression(s.Result, true);

+        Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);

 

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b486681b..6d272c07 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3999,8 +3999,9 @@ namespace Microsoft.Dafny {
         assume t0 op tn;        

         */

         var s = (CalcStmt)stmt;

+        Contract.Assert(s.Steps.Count == s.Hints.Count); // established by the resolver

         AddComment(builder, stmt, "calc statement");

-        // NadiaTodo: check well-formedness of steps

+        // NadiaTodo: check well-formedness of lines

         if (s.Steps.Count > 0) {

           Bpl.IfCmd ifCmd = null;

           Bpl.StmtList els = null;

@@ -4011,8 +4012,7 @@ namespace Microsoft.Dafny {
             if (h != null) {

               TrStmt(h, b, locals, etran);

             }

-            // NadiaTodo: add error messages

-            b.Add(Assert(s.Terms[i + 1].tok, etran.TrExpr(s.Steps[i]), "this calculation step might not hold"));

+            b.Add(Assert(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "this calculation step might not hold"));

             b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));

             if (i == s.Steps.Count - 1) {

               // first iteration (last step)