Resolve and clone calc statements; fixed a small grammar bug

4 files changed, 46 insertions, 2 deletions

diff --git a/Dafny/Cloner.cs b/Dafny/Cloner.cs
index 6d99ce9b..58f16235 100644
--- a/Dafny/Cloner.cs
+++ b/Dafny/Cloner.cs
@@ -422,6 +422,10 @@ namespace Microsoft.Dafny
         var s = (ParallelStmt)stmt;

         r = new ParallelStmt(Tok(s.Tok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));

 

+      } else if (stmt is CalcStmt) {

+          var s = (CalcStmt)stmt;

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

+

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         r = new MatchStmt(Tok(s.Tok), CloneExpr(s.Source),

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index d3566685..0608fea2 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -1228,12 +1228,14 @@ CalcStmt<out Statement/*!*/ s>
   .)

   "calc"                                                (. x = t; .)

   "{"

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

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

+  ";"

   { 

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

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

     )

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

+    ";"

   }

   "}"

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

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 7d1bc666..2526ffbc 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -1630,6 +1630,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(6);

 		Expression(out e);

 		steps.Add(e); 

+		Expect(14);

 		while (StartOf(10)) {

 			if (la.kind == 6) {

 				BlockStmt(out block, out bodyStart, out bodyEnd);

@@ -1639,6 +1640,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expression(out e);

 			steps.Add(e); 

+			Expect(14);

 		}

 		Expect(7);

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

@@ -2877,7 +2879,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

-		{x,T,T,x, x,x,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,T, T,x,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,T,T,x, x,T,x,x, T,x,T,T, x,T,T,T, T,x,x,T, T,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x},

+		{x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,x,T, x,x,T,T, T,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},

 		{x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}

 

 	};

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 53449979..59b8c13e 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -7,6 +7,7 @@ using System;
 using System.Collections.Generic;

 using System.Numerics;

 using System.Diagnostics.Contracts;

+using System.Linq;

 using Microsoft.Boogie;

 

 namespace Microsoft.Dafny

@@ -1316,6 +1317,8 @@ namespace Microsoft.Dafny
           }

           return TailRecursionStatus.NotTailRecursive;

         }

+      } else if (stmt is CalcStmt) {

+          // NadiaTodo		

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         var status = TailRecursionStatus.CanBeFollowedByAnything;

@@ -1705,6 +1708,11 @@ namespace Microsoft.Dafny
         var s = (ParallelStmt)stmt;

         CheckTypeInference(s.Range);

         CheckTypeInference(s.Body);

+      } else if (stmt is CalcStmt) {

+        // NadiaToDo: what does this even do?

+        var s = (CalcStmt)stmt;

+        s.SubExpressions.Iter(e => CheckTypeInference(e));

+        s.SubStatements.Iter(CheckTypeInference);		

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         CheckTypeInference(s.Source);

@@ -3123,6 +3131,30 @@ namespace Microsoft.Dafny
           }

           CheckParallelBodyRestrictions(s.Body, s.Kind);

         }

+		

+      } else if (stmt is CalcStmt) {

+          CalcStmt s = (CalcStmt)stmt;

+          s.IsGhost = true;

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

+          var source = s.Steps[0];

+          ResolveExpression(source, true);

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

+          foreach (var e in s.Steps.Skip(1))

+          {

+              ResolveExpression(e, true);

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

+              if (!UnifyTypes(source.Type, e.Type))

+              {

+                  Error(e, "all calculation steps must have the same type (got {0} after {1})", e.Type, source.Type);

+              }

+          }

+          foreach (var h in s.Hints)

+          {

+              if (h != null)

+              {

+                  ResolveStatement(h, true, method);

+              }

+          }

 

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

@@ -3721,6 +3753,10 @@ namespace Microsoft.Dafny
             Contract.Assert(false);  // unexpected kind

             break;

         }

+		

+      } else if (stmt is CalcStmt) {

+          // cool

+          // NadiaTodo: ...I assume because it's always ghost		

 

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;