diff options
| author |  Rustan Leino <unknown> | 2014-07-14 19:14:30 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-07-14 19:14:30 -0700 |
| commit | fda7a92b1f8f2b1fd360aa2b52aa3ddb3c705127 (patch) | |
| tree | 2d9b0bbbfbdd4f73d5d2ba617ce9c78fec8107e0 /Test/dafny0/TypeInstantiations.dfy | |
| parent | 8041bef009e34bb3c5e81ffe7b906ae4347e85d3 (diff) | |
Support for type synonyms in refinements
Started allowing arbitrary types to have type parameters
Diffstat (limited to 'Test/dafny0/TypeInstantiations.dfy')
| -rw-r--r-- | Test/dafny0/TypeInstantiations.dfy | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/Test/dafny0/TypeInstantiations.dfy b/Test/dafny0/TypeInstantiations.dfy new file mode 100644 index 00000000..cbe6d423 --- /dev/null +++ b/Test/dafny0/TypeInstantiations.dfy @@ -0,0 +1,58 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module M0 {
+ type A
+ type B = int
+ type C(==)
+ type D(==)
+ type E(==)
+ type F(==)
+
+ type G
+ type H<X,Y>
+ type J<Z>
+
+ type K0<W(==)>
+ type K1<W(==)>
+ type L<V>
+ type M(==)<U>
+ type N(==)<U>
+ type O(==)<U>
+ type P<U>
+ type R<U>
+ type S<U>
+ type T
+
+ type TP0
+ type TP1<Y0>
+ type TP2<Y0,Y1>
+}
+module M1 refines M0 {
+ type A = int
+ type B // error: cannot change a type synonym into an opaque type
+ datatype C = MakeC(ghost x: int, y: int) // error: this type does not support equality
+ type D = C // error: this type does not support equality
+ codatatype E = More(bool, E) // error: this type does not support equality
+ datatype List<T> = Nil | Cons(T, List)
+ type F = List<real> // fine
+
+ type G<X0> = List<X0> // error: G is not allowed to take type parameters
+ type H<X1> = List<X1> // error: H needs two type parameters
+ type J = List<real> // error: J needs one type parameter
+
+ type K0<W> = List<W>
+ type K1<W>
+ type L<V(==)> = List<V> // fine
+ type M<U'> = int // fine, because M<U'> does support equality
+ type N<U'> = List<U'> // error: N<U'> does not support equality
+ type O<U'(==)> = List<U'> // fine
+ type P<U'> = List<U'> // fine
+ class R { } // error: wrong number of type arguments
+ class S<T> { }
+ class T<T> { } // error: wrong number of type arguments
+
+ type TP0<E0> // error: wrong number of type arguments
+ type TP1 // error: wrong number of type arguments
+ type TP2<E0,E1>
+}
|