Refactor resolver, and really allow reads to take fields of type A -> set<obj>

twoState and codeContext is moved to a new class ResolveOpts

4 files changed, 53 insertions, 7 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 9f6c948a..50628438 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -373,7 +373,7 @@ method TestCalc(m: int, n: int, a: bool, b: bool)
     n + m; // error: ==> operator requires boolean lines

     n + m + 1;

     n + m + 2;

-  }    

+  }

   calc {

     n + m;

     n + m + 1;

@@ -394,8 +394,8 @@ ghost method Mod(a: int)
   ensures ycalc == a;

 {

   ycalc := a;

-}  

-  

+}

+

 ghost method Bad()

   modifies this;

   ensures 0 == 1;

@@ -465,7 +465,7 @@ method AssignSuchThatFromGhost()
   ghost var g: int;

 

   x := g;  // error: ghost cannot flow into non-ghost

-  

+

   x := *;

   assume x == g;  // this mix of ghosts and non-ghosts is cool (but, of course,

                   // the compiler will complain)

@@ -509,7 +509,7 @@ module NoTypeArgs0 {
     match t

     case Leaf(_,_) => t

     case Node(x, y) => x

-  }  

+  }

 

   function FTree1(t: Tree): Tree

   {

@@ -1100,3 +1100,17 @@ method TraitSynonym()
 {

   var x := new JJ;  // error: new cannot be applied to a trait

 }

+

+// ----- set comprehensions where the term type is finite ----

+

+module ObjectSetComprehensions {

+  // allowed in non-ghost context:

+  function A() : set<object> { set o : object | true :: o }

+

+  lemma B() { var x := set o : object | true :: o; }

+

+  // not allowed in non-ghost context:

+  function method C() : set<object> { set o : object | true :: o }

+

+  method D() { var x := set o : object | true :: o; }

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index b11fa9f8..ac44375d 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -76,6 +76,8 @@ ResolutionErrors.dfy(1083,6): Error: RHS (of type P<int>) not assignable to LHS
 ResolutionErrors.dfy(1088,13): Error: arguments must have the same type (got P<int> and P<X>)

 ResolutionErrors.dfy(1089,13): Error: arguments must have the same type (got P<bool> and P<X>)

 ResolutionErrors.dfy(1090,13): Error: arguments must have the same type (got P<int> and P<bool>)

+ResolutionErrors.dfy(1113,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'

+ResolutionErrors.dfy(1115,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'

 ResolutionErrors.dfy(429,2): Error: More than one default constructor

 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts

@@ -173,4 +175,4 @@ ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from
 ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)

 ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)

 ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait

-175 resolution/type errors detected in ResolutionErrors.dfy

+177 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
index 47f7f575..d0a8b43b 100644
--- a/Test/hofs/ReadsReads.dfy
+++ b/Test/hofs/ReadsReads.dfy
@@ -101,3 +101,33 @@ module WhatWeKnowAboutReads {
     }
   }
 }
+
+module ReadsAll {
+  function A(f: int -> int) : int
+    reads set o,x | o in f.reads(x) :: o;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function method B(f: int -> int) : int
+    reads set o,x | o in f.reads(x) :: o;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function C(f: int -> int) : int
+    reads f.reads;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+
+  function method D(f: int -> int) : int
+    reads f.reads;
+    requires forall x :: f.requires(x);
+  {
+    f(0) + f(1) + f(2)
+  }
+}
diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect
index e83e017c..f1da2003 100644
--- a/Test/hofs/ReadsReads.dfy.expect
+++ b/Test/hofs/ReadsReads.dfy.expect
@@ -36,4 +36,4 @@ Execution trace:
     ReadsReads.dfy(95,16): anon15_Else

     (0,0): anon21_Then

 

-Dafny program verifier finished with 13 verified, 9 errors

+Dafny program verifier finished with 17 verified, 9 errors