diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/EqualityTypes.dfy | 106 | ||||
| -rw-r--r-- | Test/dafny0/EqualityTypes.dfy.expect | 28 |
2 files changed, 133 insertions, 1 deletions
diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy index a327fd1d..c04ee2c1 100644 --- a/Test/dafny0/EqualityTypes.dfy +++ b/Test/dafny0/EqualityTypes.dfy @@ -135,3 +135,109 @@ module Gh { }
}
}
+
+// ------ deeper nesting ------
+
+module Deep {
+ codatatype Co = Mo(Co) | NoMo
+ class C<T> { }
+
+ method M(a: set<C<Co>>) {
+ var s: set<C<Co>>;
+ var t: set<Co>; // error: set element type must support equality
+ var co: Co;
+ var d := G(co, NoMo); // error: actual type parameter for Y (namely, Co) does
+ // not support equality
+ d := G(t, t) + G(s, s); // fine, because all sets support equality
+ }
+
+ function method G<Y(==)>(y: Y, z: Y): int { if y == z then 5 else 7 }
+
+ method P(b: set<Co>) { // error: set element type must be a type with equality
+ }
+
+ ghost method Q(b: set<Co>) { // fine, since this is a ghost method
+ }
+
+ method R(ghost b: set<Co>) { // fine, since this is a ghost parameter
+ }
+
+ datatype Dt<T> = Bucket(T)
+ datatype Left<T,U> = Bucket(T)
+ datatype Right<T,U> = Bucket(set<U>) // note, Dafny infers that U should be U(==)
+ datatype RightExplicit<T,U(==)> = Bucket(set<U>)
+ type Syn<A,B,C> = Left<C,A>
+
+ method W<alpha(==)>()
+ {
+ var a: set<Dt<Co>>; // error: Dt<Co> does not support equality
+ var b: set<Dt<int>>;
+ var c: set<Left<int,Co>>;
+ var d: set<Left<Co,int>>; // error: Left<Co,...> does not support equality
+ var e: set<Right<Co,Co>>; // error: type parameter 1 to Right is required to support equality
+ ghost var e': set<Right<Co,Co>>; // fine, since this is a ghost field
+ var e'': set<RightExplicit<Co,Co>>; // error: cannot instantiate argument 1 with Co
+ var f: set<Syn<Co,Co,int>>;
+ var g: set<Syn<int,int,Co>>; // error: Syn<int,int,Co> does not support equality
+ ghost var h: set<Syn<int,int,Co>>; // in a ghost context, it's cool, though
+
+ var i; // error: inferred type (set<Co>) uses invalid set-element type
+ var j: set; // error: ditto
+ ghost var k: set<Co>; // type allowed here, because it's a ghost
+ assert i == k || j == k || true; // this infers the types of 'i' and 'j'
+ }
+
+ method StatementsWithVariables(a: set<C<Co>>) {
+ var s: set<C<Co>>;
+ var t: set<Co>; // error: bad type
+ ghost var u: set<Co>;
+
+ var c := new ABC;
+ forall x | x in {t} { // error: bad type for x
+ c.f := 0;
+ }
+ if t == u {
+ forall x | x in {t} // fine, because this is a ghost statement
+ ensures true;
+ {
+ }
+ }
+ }
+
+ class ABC { var f: int; }
+
+ method Expressions() {
+ var t: set<Co>; // error: bad type
+ var b := forall x | x in {t} :: x == x; // error: bad type
+ var y := var k: set<Co> := t; k <= t; // error: bad type
+ }
+
+ ghost method GhostThings0(t: set<Co>) {
+ assert forall x | x in {t} :: x == x;
+ var y := var k: set<Co> := t; k <= t;
+ assert y;
+ }
+
+ method GhostThings1(ghost t: set<Co>) {
+ assert forall x | x in {t} :: x == x;
+ ghost var y := var k: set<Co> := t; k <= t;
+ assert y;
+ }
+
+ method InferEqualitySupportIsRequired<A>(s: set<A>)
+ ghost method DontInferEqualitySupportIsRequired<A>(s: set<A>)
+ method Explicit<A(==)>(s: set<A>)
+ method TakesABoolean(b: bool)
+ method AClient(co: Co, ko: Co) {
+ Explicit({5});
+ Explicit({co}); // error: bad type
+ var b := ko in {co}; // error: bad type (argument for the set)
+ ghost var bg := ko in {co}; // fine, it's a ghost
+ InferEqualitySupportIsRequired({co}); // error: bad type
+ DontInferEqualitySupportIsRequired({co});
+ TakesABoolean(ko in {co}); // error: bad type
+ var x := multiset([co,ko,co,ko])[ko]; // error: bad type
+ var m0 := map[5 := ko]; // no prob
+ var m1 := map[ko := 5]; // error: bad type
+ }
+}
diff --git a/Test/dafny0/EqualityTypes.dfy.expect b/Test/dafny0/EqualityTypes.dfy.expect index 70e46ff0..f296ed4b 100644 --- a/Test/dafny0/EqualityTypes.dfy.expect +++ b/Test/dafny0/EqualityTypes.dfy.expect @@ -9,4 +9,30 @@ EqualityTypes.dfy(85,8): Error: type parameter 0 (T) passed to method M must sup EqualityTypes.dfy(109,7): Error: == can only be applied to expressions of types that support equality (got D)
EqualityTypes.dfy(114,13): Error: == can only be applied to expressions of types that support equality (got D)
EqualityTypes.dfy(118,16): Error: == can only be applied to expressions of types that support equality (got D)
-11 resolution/type errors detected in EqualityTypes.dfy
+EqualityTypes.dfy(147,8): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(149,13): Error: type parameter 0 (Y) passed to function G must support equality (got Co)
+EqualityTypes.dfy(156,11): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(173,8): Error: set argument type must support equality (got Dt<Co>)
+EqualityTypes.dfy(176,8): Error: set argument type must support equality (got Left<Co,int>)
+EqualityTypes.dfy(177,8): Error: type parameter 1 (U) passed to type Right must support equality (got Co)
+EqualityTypes.dfy(179,8): Error: type parameter 1 (U) passed to type RightExplicit must support equality (got Co)
+EqualityTypes.dfy(181,8): Error: set argument type must support equality (got Syn<int,int,Co>)
+EqualityTypes.dfy(184,8): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(185,8): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(192,8): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(196,11): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(196,20): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(210,8): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(211,20): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(211,29): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(212,17): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(233,4): Error: type parameter 0 (A) passed to method Explicit must support equality (got Co)
+EqualityTypes.dfy(233,13): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(234,19): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(236,4): Error: type parameter 0 (A) passed to method InferEqualitySupportIsRequired must support equality (got Co)
+EqualityTypes.dfy(236,35): Error: set argument type must support equality (got Co)
+EqualityTypes.dfy(238,24): Error: set argument type must support equality (got Co)
+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
|