Removed specContextOnly parameter from ResolveStatement.

Moved all bounds discovery to resolution pass 1.

2 files changed, 34 insertions, 19 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 49e6efa0..e935c83d 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -586,16 +586,16 @@ method LetSuchThat(ghost z: int, n: nat)
 module NonInferredType {

   predicate P<T>(x: T)

 

-  method NonInferredType0(x: int)

+  method InferredType(x: int)

   {

     var t;

-    assume forall z :: P(z) && z == t;  // It would be nice to allow the following example, but the implementation calls DiscoverBounds before CheckInference for quantifiers.

+    assume forall z :: P(z) && z == t;

     assume t == x;  // this statement determines the type of t and z

   }

 

-  method NonInferredType1(x: int)

+  method NonInferredType(x: int)

   {

-    var t;

+    var t;  // error: the type of t is not determined

     assume forall z :: P(z) && z == t;  // error: the type of z is not determined

   }

 }

@@ -1126,15 +1126,15 @@ method TraitSynonym()
 // ----- set comprehensions where the term type is finite -----

 

 module ObjectSetComprehensions {

-  // allowed in non-ghost context:

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

+  // the following set comprehensions are known to be finite

+  function A() : set<object> { set o : object | true :: o }  // error: a function is not allowed to depend on the allocated state

 

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

+  function method B() : set<object> { set o : object | true :: o }  // error: a function is not allowed to depend on the allocated state

 

-  // not allowed in non-ghost context:

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

+  // outside functions, the comprehension is permitted, but it cannot be compiled

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

 

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

+  method D() { var x := set o : object | true :: o; }  // error: not (easily) compilable

 }

 

 // ------ regression test for type checking of integer division -----

@@ -1228,9 +1228,9 @@ module NonInferredTypeVariables {
   method BadClient(n: nat)

   {

     var p := P(n);  // error: cannot infer the type argument for P

-    ghost var q := Q(n);  // error: cannot infer the type argument for Q

+    ghost var q := Q(n);  // error: cannot infer the type argument for Q (and thus q's type cannot be determined either)

     M(n);  // error: cannot infer the type argument for M

-    var x := N(n);  // error: cannot infer the type argument for N

+    var x := N(n);  // error: cannot infer the type argument for N (and thus x's type cannot be determined either)

     var a := new array;  // error: cannot infer the type argument for 'array'

     var c := new C;  // error: cannot infer the type argument for 'C'

     var s: set;  // type argument for 'set' 

@@ -1248,7 +1248,7 @@ module NonInferredTypeVariables {
     ghost var d0 := forall s :: s == {7} ==> s != {};

     var d1 := forall s: set :: s in S ==> s == {};

     var ggcc0: C;

-    var ggcc1: C;

+    var ggcc1: C;  // error: full type cannot be determined

     ghost var d2 := forall c: C :: c != null ==> c.f == 10;

     ghost var d2' := forall c :: c == ggcc0 && c != null ==> c.f == 10;

     ghost var d2'' := forall c :: c == ggcc1 && c != null ==> c.f == c.f; // error: here, type of c is not determined

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index edf61b33..be19eeac 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -20,10 +20,9 @@ ResolutionErrors.dfy(535,7): Error: RHS (of type List<A>) not assignable to LHS
 ResolutionErrors.dfy(540,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)

 ResolutionErrors.dfy(554,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

 ResolutionErrors.dfy(566,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree

-ResolutionErrors.dfy(592,25): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(592,23): Error: type variable 'T' in the function call to 'P' could not be determined

-ResolutionErrors.dfy(599,25): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(598,8): Error: the type of this local variable is underspecified

 ResolutionErrors.dfy(599,23): Error: type variable 'T' in the function call to 'P' could not be determined

+ResolutionErrors.dfy(599,18): Error: type of bound variable 'z' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(612,13): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(613,9): Error: 'new' is not allowed in ghost contexts

 ResolutionErrors.dfy(622,23): Error: 'new' is not allowed in ghost contexts

@@ -81,12 +80,28 @@ ResolutionErrors.dfy(1105,6): Error: RHS (of type P<int>) not assignable to LHS
 ResolutionErrors.dfy(1110,13): Error: arguments must have the same type (got P<int> and P<X>)

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

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

-ResolutionErrors.dfy(1135,38): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

+ResolutionErrors.dfy(1130,31): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

+ResolutionErrors.dfy(1132,38): Error: a set comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'o'

 ResolutionErrors.dfy(1137,24): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'

+ResolutionErrors.dfy(1230,13): Error: type variable 'PT' in the function call to 'P' could not be determined

+ResolutionErrors.dfy(1231,14): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1231,19): Error: type variable 'QT' in the function call to 'Q' could not be determined

+ResolutionErrors.dfy(1232,4): Error: type '?' to the method 'M' is not determined

+ResolutionErrors.dfy(1233,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1233,13): Error: type '?' to the method 'N' is not determined

+ResolutionErrors.dfy(1234,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1235,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1236,8): Error: the type of this local variable is underspecified

+ResolutionErrors.dfy(1237,8): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1238,8): Error: the type of this local variable is underspecified

 ResolutionErrors.dfy(1242,26): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1242,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(1243,31): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1243,21): Error: type of bound variable 's' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(1244,29): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1254,34): Error: the type of this variable is underspecified

+ResolutionErrors.dfy(1244,21): Error: type of bound variable 'c' could not be determined; please specify the type explicitly

+ResolutionErrors.dfy(1251,8): Error: the type of this local variable is underspecified

+ResolutionErrors.dfy(1254,29): Error: type of bound variable 'c' could not be determined; please specify the type explicitly

 ResolutionErrors.dfy(1270,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

 ResolutionErrors.dfy(1271,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')

 ResolutionErrors.dfy(1308,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)

@@ -209,4 +224,4 @@ ResolutionErrors.dfy(1123,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1144,13): Error: first argument to / must be of numeric type (instead got set<bool>)

 ResolutionErrors.dfy(1151,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating

 ResolutionErrors.dfy(1166,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

-211 resolution/type errors detected in ResolutionErrors.dfy

+226 resolution/type errors detected in ResolutionErrors.dfy