Fixed bug in resolution of illegal programs.

Fixed comments in some test cases.

2 files changed, 18 insertions, 37 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index aabaf320..825fb5bf 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2563,8 +2563,8 @@ namespace Microsoft.Dafny {
         //    LamLet(G, tmp =>

         //      LamLet(dtorX(tmp), x =>

         //      LamLet(dtorY(tmp), y => E)))

-        Contract.Assert(e.LHSs.Count == e.RHSs.Count);  // checked by resolution

         Contract.Assert(e.Exact);  // because !Exact is ghost only

+        Contract.Assert(e.LHSs.Count == e.RHSs.Count);  // checked by resolution

         var neededCloseParens = 0;

         for (int i = 0; i < e.LHSs.Count; i++) {

           var lhs = e.LHSs[i];

@@ -2586,32 +2586,6 @@ namespace Microsoft.Dafny {
           wr.Write(")");

         }

 

-        /*

-        int i = 0;

-        for (int i = 0; i < e.LHSs.Count; ++i) {

-          var lhs = e.LHSs[i];

-          if (Contract.Exists(lhs.Vars, bv => !bv.IsGhost)) {

-            var rhsName = string.Format("_pat_let{0}_{1}", GetUniqueAstNumber(e), i);

-

-            wr.Write("Dafny.Helpers.Id<");

-            wr.Write(TypeName(new ArrowType(e.RHSs[i], bodyType)));

-            wr.Write(">(");

-            wr.Write(rhsName);

-            wr.Write(" => ");

-            neededCloseParens++;

-

-            c = TrCasePattern(lhs, rhsName));

-            Contract.Assert(c != 0);  // we already checked that there's at least one non-ghost

-            neededCloseParens += c;

-          }

-        }

-

-        TrExpr(e.Body);

-        for (int i = 0; i < neededCloseParens; i++) {

-          wr.Write(")");

-        }

-        */

-

       } else  if (expr is MatchExpr) {

         var e = (MatchExpr)expr;

         // new Dafny.Helpers.Function<SourceType, TargetType>(delegate (SourceType _source) {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index c16b8710..98fcb0ee 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -8263,18 +8263,25 @@ namespace Microsoft.Dafny
         }

       } else if (expr is LetExpr) {

         var e = (LetExpr)expr;

-        if (!e.Exact) {

-          Error(expr, "let-such-that expressions are allowed only in ghost contexts");

-        }

-        Contract.Assert(e.LHSs.Count == e.RHSs.Count);

-        var i = 0;

-        foreach (var ee in e.RHSs) {

-          if (!e.LHSs[i].Vars.All(bv => bv.IsGhost)) {

-            CheckIsNonGhost(ee);

+        if (e.Exact) {

+          Contract.Assert(e.LHSs.Count == e.RHSs.Count);

+          var i = 0;

+          foreach (var ee in e.RHSs) {

+            if (!e.LHSs[i].Vars.All(bv => bv.IsGhost)) {

+              CheckIsNonGhost(ee);

+            }

+            i++;

           }

-          i++;

+          CheckIsNonGhost(e.Body);

+        } else {

+          Contract.Assert(e.RHSs.Count == 1);

+          var lhsVarsAreAllGhost = e.LHSs.All(casePat => casePat.Vars.All(bv => bv.IsGhost));

+          if (!lhsVarsAreAllGhost) {

+            CheckIsNonGhost(e.RHSs[0]);

+          }

+          CheckIsNonGhost(e.Body);

+          Error(expr, "let-such-that expressions are allowed only in ghost contexts");

         }

-        CheckIsNonGhost(e.Body);

         return;

       } else if (expr is QuantifierExpr) {

         var e = (QuantifierExpr)expr;