Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, so use the new name resolution machinery that handles modules and type parameters

Included some inadvertently left-out test cases in dafny0/Modules0.dfy
Fixed comparable-types tests

1 files changed, 11 insertions, 5 deletions

diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect
index 0d9d44de..5d11f9c9 100644
--- a/Test/dafny0/Modules0.dfy.expect
+++ b/Test/dafny0/Modules0.dfy.expect
@@ -1,5 +1,5 @@
-Modules0.dfy(332,3): warning: module-level functions are always non-instance, so the 'static' keyword is not allowed here

-Modules0.dfy(334,3): warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here

+Modules0.dfy(333,3): warning: module-level functions are always non-instance, so the 'static' keyword is not allowed here

+Modules0.dfy(335,3): warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here

 Modules0.dfy(8,8): Error: Duplicate name of top-level declaration: WazzupA

 Modules0.dfy(9,11): Error: Duplicate name of top-level declaration: WazzupA

 Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupA

@@ -18,7 +18,7 @@ Modules0.dfy(84,9): Error: expected method call, found expression
 Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)

 Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

 Modules0.dfy(226,8): Error: new can be applied only to reference types (got X)

-Modules0.dfy(235,13): Error: Undeclared type X in module B

+Modules0.dfy(235,13): Error: module 'B' does not declare a type 'X'

 Modules0.dfy(245,13): Error: unresolved identifier: X

 Modules0.dfy(246,15): Error: member DoesNotExist does not exist in class X

 Modules0.dfy(285,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)

@@ -28,7 +28,13 @@ Modules0.dfy(289,16): Error: type of the receiver is not fully determined at thi
 Modules0.dfy(289,17): Error: expected method call, found expression

 Modules0.dfy(290,16): Error: type of the receiver is not fully determined at this program point

 Modules0.dfy(290,17): Error: expected method call, found expression

-Modules0.dfy(312,24): Error: module Q_Imp does not exist

+Modules0.dfy(314,18): Error: second argument to "in" must be a set, multiset, or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)

+Modules0.dfy(318,13): Error: arguments must have the same type (got Q_Imp.Node and Node)

+Modules0.dfy(319,11): Error: Undeclared top-level type or type parameter: LongLostModule (did you forget to qualify a name?)

+Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup (did you forget to qualify a name?)

+Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'

+Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)

+Modules0.dfy(324,30): Error: member Create does not exist in class Klassy

 Modules0.dfy(102,6): Error: type MyClassY does not have a member M

 Modules0.dfy(102,7): Error: expected method call, found expression

 Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts

@@ -36,4 +42,4 @@ Modules0.dfy(142,13): Error: old expressions are allowed only in specification a
 Modules0.dfy(143,13): Error: fresh expressions are allowed only in specification and ghost contexts

 Modules0.dfy(144,13): Error: unresolved identifier: allocated

 Modules0.dfy(147,21): Error: unresolved identifier: allocated

-36 resolution/type errors detected in Modules0.dfy

+42 resolution/type errors detected in Modules0.dfy