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, 9 insertions, 0 deletions

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 0c750d8b..4fb42099 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3232,6 +3232,13 @@ namespace Microsoft.Dafny {
         Contract.Assert(ifCmd != null);  // follows from the fact that s.Cases.Count + s.MissingCases.Count != 0.

         builder.Add(ifCmd);

 

+      } 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, builder, locals, etran);

+        }

+

       } else {

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

       }

@@ -3905,12 +3912,14 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(tok != null);

       Contract.Requires(lhs != null);

+      // TODO:  Contract.Requires(!(lhs is ConcreteSyntaxExpression));

       Contract.Requires(rhs != null);

       Contract.Requires(builder != null);

       Contract.Requires(cce.NonNullElements(locals));

       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

 

+      lhs = lhs.Resolved;  // TODO: delete this line and instead bring in the commented-out precondition above

       TrStmt_CheckWellformed(lhs, builder, locals, etran, true);

 

       if (lhs is IdentifierExpr) {