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.

1 files changed, 13 insertions, 1 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 7b51fb5e..1710be05 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -299,6 +299,9 @@ bool IsGenericInstantiation() {
       return false;

   }

 }

+/* Returns true if the next thing is of the form:

+ *     "<" Type { "," Type } ">"

+ */

 bool IsTypeList(ref IToken pt) {

   if (pt.kind != _openAngleBracket) {

     return false;

@@ -306,6 +309,10 @@ bool IsTypeList(ref IToken pt) {
   pt = scanner.Peek();

   return IsTypeSequence(ref pt, _closeAngleBracket);

 }

+/* Returns true if the next thing is of the form:

+ *     Type { "," Type }

+ * followed by an endBracketKind.

+ */

 bool IsTypeSequence(ref IToken pt, int endBracketKind) {

   while (true) {

     if (!IsType(ref pt)) {

@@ -343,7 +350,7 @@ bool IsType(ref IToken pt) {
     case _map:

     case _imap:

       pt = scanner.Peek();

-      return IsTypeList(ref pt);

+      return pt.kind != _openAngleBracket || IsTypeList(ref pt);

     case _ident:

       while (true) {

         // invariant: next token is an ident

@@ -362,6 +369,11 @@ bool IsType(ref IToken pt) {
       }

     case _openparen:

       pt = scanner.Peek();

+      if (pt.kind == _closeparen) {

+        // end of type list

+        pt = scanner.Peek();

+        return true;

+      }

       return IsTypeSequence(ref pt, _closeparen);

     default:

       return false;