Added type synonyms. (No support yet for these in refinements.)

4 files changed, 123 insertions, 1 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 137aa92c..823fbe29 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -983,3 +983,62 @@ module TypeArgumentCount {
     var c: C<T,int>;  // error: too many type arguments

   }

 }

+

+// --- Type synonyms ---

+

+module BadTypeSynonyms {

+  datatype List<T> = Nil | Cons(T, List)

+  type BadSyn0 = List  // error: must have at least one type parameter

+  type BadSyn1 = badName  // error: badName does not denote a type

+  type BadSyn2 = List<X>  // error: X does not denote a type

+  type BadSyn2 = int  // error: repeated name

+}

+

+// --- cycles ---

+

+module CycleError0 {

+  type A = A  // error: cycle: A -> A

+}

+module CycleError1 {

+  type A = B  // error: cycle: A -> B -> A

+  type B = A

+}

+module CycleError2 {

+  type A = B  // error: cycle: A -> B -> A

+  type B = set<A>

+}

+module Good0 {

+  type A = (B, D<bool>)

+  type B = C

+  class C {

+    var a: A;  // this is fine

+  }

+  datatype D<X> = Make(A, B, C)  // this is fine, too

+}

+module CycleError3 {

+  type A = B  // error: cycle: A -> B -> A

+  type B = C<A>

+  class C<T> { }

+}

+module CycleError4 {

+  type A = B  // error: cycle: A -> B -> A

+  type B = Dt<A>

+  datatype Dt<T> = Make(T)

+}

+

+// --- attributes in top-level declarations ---

+

+iterator {:myAttribute x} Iter() {  // error: x does not refer to anything

+}

+

+class {:myAttribute x} C {  // error: x does not refer to anything

+}

+

+datatype {:myAttribute x} Dt = Blue  // error: x does not refer to anything

+

+type {:myAttribute x} Something  // error: x does not refer to anything

+

+type {:myAttribute x} Synonym = int  // error: x does not refer to anything

+

+module {:myAttribute x} Modulette {  // error: x does not refer to anything

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 4075ff29..820465db 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -56,6 +56,16 @@ ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements (
 ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement)

 ResolutionErrors.dfy(982,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3

 ResolutionErrors.dfy(983,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C

+ResolutionErrors.dfy(994,7): Error: Duplicate name of top-level declaration: BadSyn2

+ResolutionErrors.dfy(991,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List

+ResolutionErrors.dfy(992,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)

+ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

+ResolutionErrors.dfy(1000,7): Error: Cycle among type synonyms: A -> A

+ResolutionErrors.dfy(1003,7): Error: Cycle among type synonyms: A -> B -> A

+ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A

+ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A

+ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A

+ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x

 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

@@ -84,6 +94,11 @@ ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can b
 ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

 ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)

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

+ResolutionErrors.dfy(1031,23): Error: unresolved identifier: x

+ResolutionErrors.dfy(1034,20): Error: unresolved identifier: x

+ResolutionErrors.dfy(1037,23): Error: unresolved identifier: x

+ResolutionErrors.dfy(1039,19): Error: unresolved identifier: x

+ResolutionErrors.dfy(1041,19): Error: unresolved identifier: x

 ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops

 ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)

 ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)

@@ -147,4 +162,4 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i
 ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real)

 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)

-149 resolution/type errors detected in ResolutionErrors.dfy

+164 resolution/type errors detected in ResolutionErrors.dfy

diff --git a/Test/dafny0/TypeSynonyms.dfy b/Test/dafny0/TypeSynonyms.dfy
new file mode 100644
index 00000000..4bec5253
--- /dev/null
+++ b/Test/dafny0/TypeSynonyms.dfy
@@ -0,0 +1,46 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+type MyType<A> = int

+

+type Int = int

+

+type PairaBools = (bool, bool)

+

+datatype List<T> = Nil | Cons(T, List)

+

+type Synonym0<T,U> = List<T>

+

+type Synonym1<T> = List  // type argument of List filled in automatically

+

+type Synonym2<A> = List<A>

+

+type Synonym3<B> = Synonym4

+

+type Synonym4<C> = Synonym2<C>

+

+type Synonym5<A,B> = List

+

+function Plus(x: Int, y: int): Int

+{

+  x + y

+}

+

+method Next(s: Synonym1) returns (u: Synonym1)

+{

+  match s

+  case Nil => u := Nil;

+  case Cons(_, tail) => u := tail;

+}

+

+method Add<W>(t: W, s: Synonym1) returns (u: Synonym1)

+{

+  u := Cons(t, Nil);

+}

+

+function Skip(s: Synonym3): Synonym0

+{

+  match s

+  case Nil => Nil

+  case Cons(_, tail) => tail

+}

diff --git a/Test/dafny0/TypeSynonyms.dfy.expect b/Test/dafny0/TypeSynonyms.dfy.expect
new file mode 100644
index 00000000..4ef2de53
--- /dev/null
+++ b/Test/dafny0/TypeSynonyms.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 6 verified, 0 errors