Dafny: deal with equality-support issues in refinements

Dafny: a small amount of refactoring and bug fixes

6 files changed, 147 insertions, 58 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 6da3138c..1f3326da 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -539,7 +539,16 @@ namespace Microsoft.Dafny {
         } else if (ResolvedClass is CoDatatypeDecl) {

           return false;

         } else if (ResolvedClass is IndDatatypeDecl) {

+          var dt = (IndDatatypeDecl)ResolvedClass;

           // TODO

+          // For now, say 'no' if some constructor takes a parameter that is a codatatype.  This is BOGUS.

+          foreach (var ctor in dt.Ctors) {

+            foreach (var arg in ctor.Formals) {

+              if (arg.Type.IsCoDatatype) {

+                return false;

+              }

+            }

+          }

           return true;

         } else if (ResolvedParam != null) {

           return ResolvedParam.MustSupportEquality;

diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index b7866bfd..5afe1ba7 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -50,7 +50,7 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class RefinementTransformer

+  public class RefinementTransformer : Rewriter

   {

     ResolutionErrorReporter reporter;

     public RefinementTransformer(ResolutionErrorReporter reporter) {

@@ -59,12 +59,18 @@ namespace Microsoft.Dafny {
     }

 

     private ModuleDecl moduleUnderConstruction;  // non-null for the duration of Construct calls

+    private Queue<Action> postTasks = new Queue<Action>();  // empty whenever moduleUnderConstruction==null, these tasks are for the post-resolve phase of module moduleUnderConstruction

 

-    public void Construct(ModuleDecl m) {

+    public void PreResolve(ModuleDecl m) {

       Contract.Requires(m != null);

-      Contract.Requires(m.RefinementBase != null);

+      if (m.RefinementBase == null) {

+        // This Rewriter doesn't do anything

+        return;

+      }

 

-      Contract.Assert(moduleUnderConstruction == null);

+      if (moduleUnderConstruction != null) {

+        postTasks.Clear();

+      }

       moduleUnderConstruction = m;

       var prev = m.RefinementBase;

 

@@ -99,7 +105,35 @@ namespace Microsoft.Dafny {
         } else {

           var nw = m.TopLevelDecls[index];

           if (d is ArbitraryTypeDecl) {

-            // this is allowed to be refined by any type declaration, so just keep the new one

+            bool dDemandsEqualitySupport = ((ArbitraryTypeDecl)d).MustSupportEquality;

+            if (nw is ArbitraryTypeDecl) {

+              if (dDemandsEqualitySupport != ((ArbitraryTypeDecl)nw).MustSupportEquality) {

+                reporter.Error(nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name);

+              }

+            } else if (dDemandsEqualitySupport) {

+              if (nw is ClassDecl) {

+                // fine, as long as "nw" does not take any type parameters

+                if (nw.TypeArgs.Count != 0) {

+                  reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a class that takes type parameters", nw.Name);

+                }

+              } else if (nw is CoDatatypeDecl) {

+                reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");

+              } else {

+                Contract.Assert(nw is IndDatatypeDecl);

+                if (nw.TypeArgs.Count != 0) {

+                  reporter.Error(nw, "arbitrary type '{0}' is not allowed to be replaced by a datatype that takes type parameters", nw.Name);

+                } else {

+                  // Here, we need to figure out if the new type supports equality.  But we won't know about that until resolution has

+                  // taken place, so we defer it until the PostResolve phase.

+                  var udt = new UserDefinedType(nw.tok, nw.Name, nw, new List<Type>());

+                  postTasks.Enqueue(delegate() {

+                    if (!udt.SupportsEquality) {

+                      reporter.Error(udt.tok, "datatype '{0}' is used to refine an arbitrary type with equality support, but '{0}' does not support equality", udt.Name);

+                    }

+                  });

+                }

+              }

+            }

           } else if (nw is ArbitraryTypeDecl) {

             reporter.Error(nw, "an arbitrary type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name);

           } else if (nw is DatatypeDecl) {

@@ -115,7 +149,20 @@ namespace Microsoft.Dafny {
         }

       }

 

-      Contract.Assert(moduleUnderConstruction == m);

+      Contract.Assert(moduleUnderConstruction == m);  // this should be as it was set earlier in this method

+    }

+

+    public void PostResolve(ModuleDecl m) {

+      Contract.Requires(m != null);

+

+      if (m == moduleUnderConstruction) {

+        while (this.postTasks.Count != 0) {

+          var a = postTasks.Dequeue();

+          a();

+        }

+      } else {

+        postTasks.Clear();

+      }

       moduleUnderConstruction = null;

     }

 

@@ -598,6 +645,8 @@ namespace Microsoft.Dafny {
     // -------------------------------------------------- Merging ---------------------------------------------------------------

 

     ClassDecl MergeClass(ClassDecl nw, ClassDecl prev) {

+      CheckAgreement_TypeParameters(nw.tok, prev.TypeArgs, nw.TypeArgs, nw.Name, "class");

+

       // Create a simple name-to-member dictionary.  Ignore any duplicates at this time.

       var declaredNames = new Dictionary<string, int>();

       for (int i = 0; i < nw.Members.Count; i++) {

@@ -731,6 +780,27 @@ namespace Microsoft.Dafny {
           var n = nw[i];

           if (o.Name != n.Name) {

             reporter.Error(n.tok, "type parameters are not allowed to be renamed from the names given in the {0} in the module being refined (expected '{1}', found '{2}')", thing, o.Name, n.Name);

+          } else {

+            // This explains what we want to do and why:

+            // switch (o.EqualitySupport) {

+            //   case TypeParameter.EqualitySupportValue.Required:

+            //     // here, we will insist that the new type-parameter also explicitly requires equality support (because we don't want

+            //     // to wait for the inference to run on the new module)

+            //     good = n.EqualitySupport == TypeParameter.EqualitySupportValue.Required;

+            //     break;

+            //   case TypeParameter.EqualitySupportValue.InferredRequired:

+            //     // here, we can allow anything, because even with an Unspecified value, the inference will come up with InferredRequired, like before

+            //     good = true;

+            //     break;

+            //   case TypeParameter.EqualitySupportValue.Unspecified:

+            //     // inference didn't come up with anything on the previous module, so the only value we'll allow here is Unspecified as well

+            //     good = n.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified;

+            //     break;

+            // }

+            // Here's how we actually compute it:

+            if (o.EqualitySupport != TypeParameter.EqualitySupportValue.InferredRequired && o.EqualitySupport != n.EqualitySupport) {

+              reporter.Error(n.tok, "type parameter '{0}' is not allowed to change the requirement of supporting equality", n.Name);

+            }

           }

         }

       }

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 74e401a7..ca7a0c69 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -170,15 +170,17 @@ namespace Microsoft.Dafny {
       }

 

       // register top-level declarations

-      Rewriter rewriter = new AutoContractsRewriter();

+      var rewriters = new List<Rewriter>();

+      // The following line could be generalized to allow rewriter plug-ins; to support such, just add command-line

+      // switches and .Add to "rewriters" here.

+      rewriters.Add(new AutoContractsRewriter());

+      rewriters.Add(new RefinementTransformer(this));

+

       var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls);

       var moduleNameInfo = new ModuleNameInformation[h];

       foreach (var m in mm) {

-        rewriter.PreResolve(m);

-        if (m.RefinementBase != null) {

-          var transformer = new RefinementTransformer(this);

-          transformer.Construct(m);

-        }

+        rewriters.Iter(r => r.PreResolve(m));

+

         moduleNameInfo[m.Height] = RegisterTopLevelDecls(m.TopLevelDecls);

 

         // set up environment

@@ -187,13 +189,16 @@ namespace Microsoft.Dafny {
         allDatatypeCtors = info.Ctors;

         // resolve

         var datatypeDependencies = new Graph<IndDatatypeDecl>();

+        int prevErrorCount = ErrorCount;

         ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);

-        ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);

+        if (prevErrorCount == ErrorCount) {

+          ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);

+        }

         // tear down

         classes = null;

         allDatatypeCtors = null;

-        // give rewriter a chance to do processing

-        rewriter.PostResolve(m);

+        // give rewriters a chance to do processing

+        rewriters.Iter(r => r.PostResolve(m));

       }

 

       // compute IsRecursive bit for mutually recursive functions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5f80df86..c8cca5d3 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -58,7 +58,6 @@ class C {
 Dafny program verifier finished with 0 verified, 0 errors

 

 -------------------- TypeTests.dfy --------------------

-TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type

 TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)

 TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)

 TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)

@@ -88,11 +87,12 @@ TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the
 TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)

 TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

 TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type

-TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(90,6): Error: sorry, cannot instantiate collection type with a subrange type

+TypeTests.dfy(91,9): Error: sorry, cannot instantiate type parameter with a subrange type

 TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(116,4): Error: cannot assign to non-ghost variable in a ghost context

-TypeTests.dfy(117,7): Error: cannot assign to non-ghost variable in a ghost context

+TypeTests.dfy(93,8): Error: sorry, cannot instantiate 'array' type with a subrange type

+TypeTests.dfy(117,4): Error: cannot assign to non-ghost variable in a ghost context

+TypeTests.dfy(118,7): Error: cannot assign to non-ghost variable in a ghost context

 TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

 36 resolution/type errors detected in TypeTests.dfy

 

@@ -719,33 +719,32 @@ Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of th
 Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

 Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

 Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

-Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)

-Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

-Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)

-Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)

-Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)

-Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

-Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

-Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)

-Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)

-Modules0.dfy(250,15): Error: unresolved identifier: X

-Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X

-Modules0.dfy(294,16): Error: member R does not exist in class B

-Modules0.dfy(294,6): Error: expected method call, found expression

-Modules0.dfy(317,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)

-Modules0.dfy(321,13): Error: arguments must have the same type (got Q_Imp.Node and Node)

-Modules0.dfy(322,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)

-Modules0.dfy(323,11): Error: Undeclared module name: Wazzup (did you forget a module import?)

-Modules0.dfy(324,17): Error: Undeclared class name Edon in module Q_Imp

-Modules0.dfy(326,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)

-Modules0.dfy(327,30): Error: member Create does not exist in class Klassy

-Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts

-Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts

-Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts

-Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts

-Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context

-Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context

-37 resolution/type errors detected in Modules0.dfy

+Modules0.dfy(52,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)

+Modules0.dfy(52,12): Error: new can be applied only to reference types (got T)

+Modules0.dfy(57,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)

+Modules0.dfy(73,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)

+Modules0.dfy(74,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

+Modules0.dfy(84,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

+Modules0.dfy(108,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)

+Modules0.dfy(247,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)

+Modules0.dfy(256,13): Error: unresolved identifier: X

+Modules0.dfy(257,15): Error: member DoesNotExist does not exist in class X

+Modules0.dfy(299,16): Error: member R does not exist in class B

+Modules0.dfy(299,6): Error: expected method call, found expression

+Modules0.dfy(322,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)

+Modules0.dfy(326,13): Error: arguments must have the same type (got Q_Imp.Node and Node)

+Modules0.dfy(327,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)

+Modules0.dfy(328,11): Error: Undeclared module name: Wazzup (did you forget a module import?)

+Modules0.dfy(329,17): Error: Undeclared class name Edon in module Q_Imp

+Modules0.dfy(331,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)

+Modules0.dfy(332,30): Error: member Create does not exist in class Klassy

+Modules0.dfy(143,11): Error: ghost variables are allowed only in specification contexts

+Modules0.dfy(157,11): Error: old expressions are allowed only in specification and ghost contexts

+Modules0.dfy(158,11): Error: fresh expressions are allowed only in specification and ghost contexts

+Modules0.dfy(159,11): Error: allocated expressions are allowed only in specification and ghost contexts

+Modules0.dfy(175,10): Error: match source expression 'tree' has already been used as a match source expression in this context

+Modules0.dfy(214,12): Error: match source expression 'l' has already been used as a match source expression in this context

+36 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

 Modules1.dfy(74,16): Error: assertion violation

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index cc66c3c1..80ac7eef 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -45,9 +45,12 @@ module A imports N, M {  // Note, this has the effect of importing two different
     { x }

     method M(x: T)  // error: use of the ambiguous name T

       returns (y: T)  // error: use of the ambiguous name T

-    { var g := new T; }  // error: use of the ambiguous name T

   }

 }

+module A' imports N, M {

+  method M()

+    { var g := new T; }  // error: use of the ambiguous name T

+}

 

 module B0 imports A {

   class BadUse {

@@ -241,15 +244,17 @@ module BTr imports ATr {
 module CTr imports BTr {

   class Z {

     var b: Y;  // fine

-    var a: X;  // error: imports don't reach name name X explicitly

-    method P() {

-      var y := new Y;

-      var x := y.N();  // this is allowed and will correctly infer the type of x to

-                       // be X, but X could not have been mentioned explicitly

-      var q := x.M();

-      var r := X.Q();  // error: X is not in scope

-      var s := x.DoesNotExist();  // error: method not declared in class X

-    }

+    var a: X;  // error: imports don't reach name X explicitly

+  }

+}

+module CTs imports BTr {

+  method P() {

+    var y := new Y;

+    var x := y.N();  // this is allowed and will correctly infer the type of x to

+                     // be X, but X could not have been mentioned explicitly

+    var q := x.M();

+    var r := X.Q();  // error: X is not in scope

+    var s := x.DoesNotExist();  // error: method not declared in class X

   }

 }

 

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 8434f06c..2dea7a52 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -86,7 +86,8 @@ method ArrayRangeAssignments(a: array<C>, c: C)
 

 // --------------------- tests of restrictions on subranges (nat)

 

-method K(s: set<nat>) {  // error: not allowed to instantiate 'set' with 'nat'

+method K() {

+  var s: set<nat>;  // error: not allowed to instantiate 'set' with 'nat'

   var d: MutuallyRecursiveDataType<nat>;  // error: not allowed to instantiate with 'nat'

   var a := new nat[100];  // error: not allowed the type array<nat>

   var b := new nat[100,200];  // error: not allowed the type array2<nat>