Datatypes with ghost fields (that is, with constructors with ghost parameters) do not support equality, since the ghost fields will be erased during compilation.

Allow any equalities to be passed in for ghost parameters.

4 files changed, 88 insertions, 11 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index b7ba8a72..e1305ae3 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3960,9 +3960,7 @@ namespace Microsoft.Dafny {
 

     public override IEnumerable<Expression> SubExpressions {

       get {

-        if (!Function.IsStatic) {

-          yield return Receiver;

-        }

+        yield return Receiver;

         foreach (var e in Args) {

           yield return e;

         }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 0203777c..6cf687f0 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1957,24 +1957,24 @@ namespace Microsoft.Dafny
         : base(resolver) {

         Contract.Requires(resolver != null);

       }

-      protected override bool VisitOneStmt(Statement stmt, ref bool unused) {

+      protected override bool VisitOneStmt(Statement stmt, ref bool st) {

         if (stmt.IsGhost) {

           return false;  // no need to recurse to sub-parts, since all sub-parts must be ghost as well

         } else if (stmt is WhileStmt) {

           var s = (WhileStmt)stmt;

           // don't recurse on the specification parts, which are ghost

           if (s.Guard != null) {

-            Visit(s.Guard, unused);

+            Visit(s.Guard, st);

           }

-          Visit(s.Body, unused);

+          Visit(s.Body, st);

           return false;

         } else if (stmt is AlternativeLoopStmt) {

           var s = (AlternativeLoopStmt)stmt;

           // don't recurse on the specification parts, which are ghost

           foreach (var alt in s.Alternatives) {

-            Visit(alt.Guard, unused);

+            Visit(alt.Guard, st);

             foreach (var ss in alt.Body) {

-              Visit(ss, unused);

+              Visit(ss, st);

             }

           }

           return false;

@@ -1989,6 +1989,25 @@ namespace Microsoft.Dafny
             }

             i++;

           }

+          // recursively visit all subexpressions (which are all actual parameters) passed in for non-ghost formal parameters

+          Contract.Assert(s.Lhs.Count == s.Method.Outs.Count);

+          i = 0;

+          foreach (var ee in s.Lhs) {

+            if (!s.Method.Outs[i].IsGhost) {

+              Visit(ee, st);

+            }

+            i++;

+          }

+          Visit(s.Receiver, st);

+          Contract.Assert(s.Args.Count == s.Method.Ins.Count);

+          i = 0;

+          foreach (var ee in s.Args) {

+            if (!s.Method.Ins[i].IsGhost) {

+              Visit(ee, st);

+            }

+            i++;

+          }

+          return false;  // we've done what there is to be done

         }

         return true;

       }

@@ -2058,6 +2077,17 @@ namespace Microsoft.Dafny
             }

             i++;

           }

+          // recursively visit all subexpressions (which are all actual parameters) passed in for non-ghost formal parameters

+          Visit(e.Receiver, st);

+          Contract.Assert(e.Args.Count == e.Function.Formals.Count);

+          i = 0;

+          foreach (var ee in e.Args) {

+            if (!e.Function.Formals[i].IsGhost) {

+              Visit(ee, st);

+            }

+            i++;

+          }

+          return false;  // we've done what there is to be done

         }

         return true;

       }

@@ -2456,13 +2486,14 @@ namespace Microsoft.Dafny
 

       var scc = dependencies.GetSCC(startingPoint);

       // First, the simple case:  If any parameter of any inductive datatype in the SCC is of a codatatype type, then

-      // the whole SCC is incapable of providing the equality operation.

+      // the whole SCC is incapable of providing the equality operation.  Also, if any parameter of any inductive datatype

+      // is a ghost, then the whole SCC is incapable of providing the equality operation.

       foreach (var dt in scc) {

         Contract.Assume(dt.EqualitySupport == IndDatatypeDecl.ES.NotYetComputed);

         foreach (var ctor in dt.Ctors) {

           foreach (var arg in ctor.Formals) {

             var anotherIndDt = arg.Type.AsIndDatatype;

-            if ((anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || arg.Type.IsCoDatatype) {

+            if (arg.IsGhost || (anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || arg.Type.IsCoDatatype) {

               // arg.Type is known never to support equality

               // So, go around the entire SCC and record what we learnt

               foreach (var ddtt in scc) {

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 8f138bcd..0db833a4 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1318,7 +1318,10 @@ EqualityTypes.dfy(42,11): Error: datatype 'X' is used to refine an arbitrary typ
 EqualityTypes.dfy(43,11): Error: datatype 'Y' is used to refine an arbitrary type with equality support, but 'Y' does not support equality

 EqualityTypes.dfy(63,7): Error: == can only be applied to expressions of types that support equality (got Dt<T>)

 EqualityTypes.dfy(82,8): Error: type parameter 0 (T) passed to method M must support equality (got _T0)

-8 resolution/type errors detected in EqualityTypes.dfy

+EqualityTypes.dfy(106,7): Error: == can only be applied to expressions of types that support equality (got D)

+EqualityTypes.dfy(111,13): Error: == can only be applied to expressions of types that support equality (got D)

+EqualityTypes.dfy(115,16): Error: == can only be applied to expressions of types that support equality (got D)

+11 resolution/type errors detected in EqualityTypes.dfy

 

 -------------------- SplitExpr.dfy --------------------

 

diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy
index 251b2e2f..c24e1de2 100644
--- a/Test/dafny0/EqualityTypes.dfy
+++ b/Test/dafny0/EqualityTypes.dfy
@@ -87,3 +87,48 @@ module H {
      Caller1(d);  // case in point for the error in Caller1

   }

 }

+

+// ----------------------------

+

+module Gh {

+  datatype D = Nil | Cons(head: int, tail: D, ghost x: int)

+

+  method M(n: nat, b: bool, d: D, e: D, ghost g: bool)

+    ensures b ==> d == e;  // fine, this is a ghost declaration

+  {

+    ghost var g := 0;

+    var h := 0;

+    if d == e {  // fine, this is a ghost statement

+      g := g + 1;

+    } else {

+      assert !b;

+    }

+    if d == e {  // error: not allowed to compare D's in a non-ghost context

+      h := h + 1;

+    }

+    if n != 0 {

+      M(n-1, b, d, e, d==e);  // fine

+      M(n-1, d==e, d, e, false);  // error, cannot pass in d==e like we do

+    }

+    GM(d==e, d, e);  // fine -- we're calling a ghost method

+    var y0 := F(b, d==e);

+    var y1 := F(d==e, false);  // error

+  }

+

+  function method F(b: bool, ghost g: bool): int { 6 }

+

+  ghost method GM(b: bool, d: D, e: D)  // all equalities are fine in a ghost method

+    ensures b ==> d == e;

+  {

+    ghost var g := 0;

+    var h := 0;

+    if d == e {

+      g := g + 1;

+    } else {

+      assert !b;

+    }

+    if d == e {

+      h := h + 1;

+    }

+  }

+}