Fixed bugs in the parsing of explicit type arguments.

Fixed resolution bug where some type arguments were not checked to have been determined.
Fixed resolution bugs where checking for equality-supporting types was missing.

2 files changed, 135 insertions, 1 deletions

diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy
index b2812759..c510cfb1 100644
--- a/Test/dafny0/EqualityTypes.dfy
+++ b/Test/dafny0/EqualityTypes.dfy
@@ -241,3 +241,115 @@ module Deep {
     var m1 := map[ko := 5];  // error: bad type

   }

 }

+

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

+

+module UnderspecifiedTypeParameters {

+  method UP<T>()

+  function method UG<T>(): int

+  method Callee<T(==)>()

+  class TakesParam<U> { }

+  

+  method MPG()

+  {

+    var g := UG();  // error: type parameter underspecified

+    UP();  // error: type parameter underspecified

+  }

+  method M() {

+    var zs: set;  // error: type is underspecified

+    Callee<(int)>();

+    Callee<set>();  // error: type is underspecified

+    Callee<()>();

+    // The following 

+    Callee<TakesParam>();  // error: type is underspecified

+  }

+}

+

+module EqualitySupportingTypes {

+  method P<T>()

+  function method G<T>(): int

+  class AClass<V(==),Y> {

+    static function method H<W,X(==)>(): bool

+    static method Q<A,B(==)>()

+  }

+

+  method Callee<T(==)>()

+  function method FCallee<T>(): T

+

+  datatype Dt = Dt(f: int -> int)

+  codatatype Stream<T> = Cons(T, Stream)

+

+  method M<ArbitraryTypeArg>()

+  {

+    Callee<Dt>();  // error:  Dt is not an equality-supporting type

+    Callee<Stream<int>>();  // error: specified type does not support equality

+

+    // set<X> is allowed in a non-ghost context only if X is equality supporting.

+    // Ditto for multiset<X> and map<X,Y>.

+    var s3x: set<Dt>;  // error: this type not allowed in a non-ghost context

+    var is3x: iset<Dt>;  // error: this type not allowed in a non-ghost context

+    var mast: multiset<ArbitraryTypeArg>;  // error: this type not allowed in a non-ghost context

+    var qt: seq<Stream<int>>;  // allowed

+    var mp0: map<Dt,int>;  // error: this type not allowed in a non-ghost context

+    var mp1: map<int,Dt>;  // allowed

+    var imp0: imap<Dt,int>;  // error: this type not allowed in a non-ghost context

+    var imp1: imap<int,Dt>;  // allowed

+

+    var S := FCallee<set>();  // this gives s:set<?>

+    if 4 in S {              // this constrains the type further to be s:set<int>

+    }

+

+    var xy: set<set<int>>;

+    var xz: set<set<Stream<int>>>;  // error: set type argument must support equality

+    

+    Callee<set<Stream<int>>>();  // bogus: a set shouldn't ever be allowed to take a Stream as an argument (this check seems to be missing for explicit type arguments)  -- Note: language definition should be changed, because it doesn't make sense for it to talk about a type appearing in a ghost or non-ghost context. Instead, set/iset/multiset/map/imap should always be allowed to take any type argument, but these types may or may not support equality.

+    var xg := G<set<Stream<int>>>();

+    

+    var ac0: AClass<int,int>;

+    var ac1: AClass<Stream<int>,int>;  // error: type parameter 0 is required to support equality

+    var ac2: AClass<int,Stream<int>>;

+    var xd0 := ac0.H<real,real>();

+    var xd1 := ac1.H<Stream<real>,real>();  // error (remnant of the fact that the type of ac1 is not allowed)

+    var xd2 := ac2.H<real,Stream<real>>();  // error: type parameter 1 is required to support equality

+    var xe0 := ac0.H<real,real>;

+    var xe1 := ac1.H<Stream<real>,real>;  // error (remnant of the fact that the type of ac1 is not allowed)

+    var xe2 := ac2.H<real,Stream<real>>;  // error: type parameter 1 is required to support equality

+    var xh0 := AClass<int,int>.H<real,real>();

+    var xh1 := AClass<int,int>.H<Stream<real>,real>();

+    var xh2 := AClass<int,int>.H<real,Stream<real>>();  // error: type parameter 1 is required to support equality

+    var xk0 := AClass<real,real>.H<int,int>;

+    var xk1 := AClass<Stream<real>,real>.H<int,int>;  // error: class type param 0 wants an equality-supporting type

+    var xk2 := AClass<real,Stream<real>>.H<int,int>;

+    AClass<Stream<int>,int>.Q<real,real>();  // error: class type param 0 wants an equality-supporting type

+    AClass<int,Stream<int>>.Q<real,real>();

+    AClass<int,Stream<int>>.Q<Stream<real>,real>();

+    AClass<int,Stream<int>>.Q<real,Stream<real>>();  // error: method type param 1 wants an equality-supporting type

+  

+/*************************** TESTS YET TO COME

+    var ac8: AClass<real,real>;

+    var xd8 := (if 5/0 == 3 then ac0 else ac8).H<real,real>();  // error: this should be checked by the verifier

+

+    AClass<int,set<Stream<int>>>.Q<real,real>();  // error: cannot utter "set<Stream<int>>"   Or is that okay???

+    AClass<int,int>.Q<set<Stream<real>>,real>();  // error: cannot utter "set<Stream<real>>"   Or is that okay???

+    var xi0 := AClass<int,set<Stream<int>>>.H<real,real>();  // error: cannot utter "set<Stream<int>>"   Or is that okay???

+    var xi1 := AClass<int,int>.H<real,set<Stream<real>>>();  // error: cannot utter "set<Stream<real>>"   Or is that okay???

+

+    var x, t, s: seq<int -> int>, fii: int -> int;

+    if s == t {

+      x := 5;  // error: assigning to non-ghost variable in ghost context

+    }

+    if fii in s {

+      x := 4;  // error: assigning to non-ghost variable in ghost context

+    }

+    if !(fii in s) {

+      x := 3;  // error: assigning to non-ghost variable in ghost context

+    }

+

+    ghost var ghostset: set<Stream<int>> := {};  // fine, since this is ghost

+    forall u | 0 <= u < 100

+      ensures var lets: set<Stream<int>> := {}; lets == lets  // this is ghost, so the equality requirement doesn't apply

+    {

+    }

+*********************************************/

+  }

+}

diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect
index 9f277582..1c02f3a0 100644
--- a/Test/dafny0/EqualityTypes.dfy.expect
+++ b/Test/dafny0/EqualityTypes.dfy.expect
@@ -35,4 +35,26 @@ EqualityTypes.dfy(238,24): Error: set argument type must support equality (got C
 EqualityTypes.dfy(239,21): Error: multiset argument type must support equality (got Co)

 EqualityTypes.dfy(241,8): Error: map domain type must support equality (got Co)

 EqualityTypes.dfy(241,14): Error: map domain type must support equality (got Co)

-37 resolution/type errors detected in EqualityTypes.dfy

+EqualityTypes.dfy(255,13): Error: type variable 'T' in the function call to 'UG' could not be determined

+EqualityTypes.dfy(256,4): Error: type '?' to the method 'UP' is not determined

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

+EqualityTypes.dfy(261,4): Error: type 'set<?>' to the method 'Callee' is not determined

+EqualityTypes.dfy(264,4): Error: type 'TakesParam<?>' to the method 'Callee' is not determined

+EqualityTypes.dfy(284,14): Error: type parameter 0 (T) passed to method Callee must support equality (got Dt)

+EqualityTypes.dfy(285,23): Error: type parameter 0 (T) passed to method Callee must support equality (got Stream<int>)

+EqualityTypes.dfy(289,8): Error: set argument type must support equality (got Dt)

+EqualityTypes.dfy(290,8): Error: iset argument type must support equality (got Dt)

+EqualityTypes.dfy(291,8): Error: multiset argument type must support equality (got ArbitraryTypeArg) (perhaps try declaring type parameter 'ArbitraryTypeArg' on line 282 as 'ArbitraryTypeArg(==)', which says it can only be instantiated with a type that supports equality)

+EqualityTypes.dfy(293,8): Error: map domain type must support equality (got Dt)

+EqualityTypes.dfy(295,8): Error: imap domain type must support equality (got Dt)

+EqualityTypes.dfy(303,8): Error: set argument type must support equality (got Stream<int>)

+EqualityTypes.dfy(309,8): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)

+EqualityTypes.dfy(312,19): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)

+EqualityTypes.dfy(313,19): Error: type parameter 1 (X) passed to function H must support equality (got Stream<real>)

+EqualityTypes.dfy(315,19): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)

+EqualityTypes.dfy(316,19): Error: type parameter 1 (X) passed to function 'H' must support equality (got Stream<real>)

+EqualityTypes.dfy(319,31): Error: type parameter 1 (X) passed to function H must support equality (got Stream<real>)

+EqualityTypes.dfy(321,41): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<real>)

+EqualityTypes.dfy(323,28): Error: type parameter 0 (V) passed to type AClass must support equality (got Stream<int>)

+EqualityTypes.dfy(326,48): Error: type parameter 1 (B) passed to method Q must support equality (got Stream<real>)

+59 resolution/type errors detected in EqualityTypes.dfy