Dafny:

* fixed parsing problem with a block ending a block
* replaced AssignStmt and "call" statements with UpdateStmt's
* fixed some minor printing problems
* changed implementation to check for ghost expressions in a pass separate from ResolveExpr
To-dos:
* compile and translate multi-assignments
* handle non-identifier LHSs of call statements
* change "var" statements in a similar way
* tighten up parsing of LHSs to allow only things like SelectExpr
* code and grammar clean-up to remove unused parts (e.g., "call" grammar productions and the "allowGhostFeatures" parameters)
* include the commented-out precondition of TrAssignment
* check in changes to the test suite

1 files changed, 7 insertions, 0 deletions

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 80e597e5..86fd1688 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -840,6 +840,13 @@ namespace Microsoft.Dafny {
           Indent(indent); wr.WriteLine("}");

         }

 

+      } else if (stmt is ConcreteSyntaxStatement) {

+        var s = (ConcreteSyntaxStatement)stmt;

+        // TODO: Update statements should perform multiple assignments in parallel!

+        foreach (var ss in s.ResolvedStatements) {

+          TrStmt(ss, indent);

+        }

+

       } else {

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

       }