fix: Always parse parentheses for predicates (#5069)

A loooong time ago, Dafny supported `predicate` definitions without parentheses. Apparently, the parser still allowed that, which is wrong. This PR changes the parser to make sure that a predicate definition always includes parentheses. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
dafny-lang · Feb 20, 2024 · e49dec6 · e49dec6
1 parent ab33478
commit e49dec6
Show file tree

Hide file tree

Showing 5 changed files with 28 additions and 5 deletions.
diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg
@@ -1771,8 +1771,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
                   "a formal [ ] declaration is only allowed for least and greatest predicates");
         .)
       ]
-      [ Formals<true, true, isTwoState, true, formals>
-      ]
+      Formals<true, true, isTwoState, true, formals>
       [ PredicateResult<"predicate", out result> ]
     | ellipsis   (. signatureEllipsis = t; .)
     )

diff --git a/Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs b/Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs
@@ -65,7 +65,7 @@ method TestMethod() returns (x: int) {
 
 trait TestTrait {}
 
-predicate TestPredicate { false }", "test-workspace-symbols.dfy", false);
+predicate TestPredicate() { false }", "test-workspace-symbols.dfy", false);
 
       await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
 

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy
@@ -273,6 +273,26 @@ module ArrowTypes {
   }
 }
 
+// ---------------------- missing parentheses for `predicate` -----------------------------------
+
+module MissingPredicateParens0 {
+  predicate P<A>
+} // error: expecting open paren
+
+module MissingPredicateParens1 {
+  predicate P<A> { // error: expecting open paren
+    true
+  }
+}
+
+module MissingPredicateParens2 {
+  predicate P<A> { // error: expecting open paren
+    true
+  } by method {
+    return true;
+  }
+}
+
 // ---------------------- invalid newtype definition -----------------------------------
 
 newtype T {} // error: newtype is expected to have an '='
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParseErrors.dfy.expect
@@ -79,5 +79,8 @@ ParseErrors.dfy(261,28): Error: formal cannot be declared 'older' in this contex
 ParseErrors.dfy(267,12): Error: arrow-type arguments may not be declared as 'ghost'
 ParseErrors.dfy(272,18): Error: arrow-type arguments may not be declared as 'ghost'
 ParseErrors.dfy(272,35): Error: arrow-type arguments may not be declared as 'ghost'
-ParseErrors.dfy(278,10): Error: invalid NewtypeDecl
-77 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(280,0): Error: openparen expected
+ParseErrors.dfy(283,17): Error: openparen expected
+ParseErrors.dfy(289,17): Error: openparen expected
+ParseErrors.dfy(298,10): Error: invalid NewtypeDecl
+80 parse errors detected in ParseErrors.dfy
diff --git a/docs/dev/news/5069.fix b/docs/dev/news/5069.fix
@@ -0,0 +1 @@
+The syntax of a predicate definition must always include parentheses.