Changed computation of ghosts until pass 2 of resolution.

Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.

1 files changed, 11 insertions, 3 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index dd2eed69..032e30a0 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -550,13 +550,21 @@ namespace Microsoft.Dafny
         r = new ForallStmt(Tok(s.Tok), Tok(s.EndTok), 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), Tok(s.EndTok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));

+        var s = (CalcStmt)stmt;

+        // calc statements have the unusual property that the last line is duplicated.  If that is the case (which

+        // we expect it to be here), we share the clone of that line as well.

+        var lineCount = s.Lines.Count;

+        var lines = new List<Expression>(lineCount);

+        for (int i = 0; i < lineCount; i++) {

+          lines.Add(i == lineCount - 1 && 2 <= lineCount && s.Lines[i] == s.Lines[i - 1] ? lines[i - 1] : CloneExpr(s.Lines[i]));

+        }

+        Contract.Assert(lines.Count == lineCount);

+        r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), lines, s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));

 

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

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

-          s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);

+        s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);

 

       } else if (stmt is AssignSuchThatStmt) {

         var s = (AssignSuchThatStmt)stmt;