Feat: Predicates can name their return parameter

RELEASE_NOTES.md

@@ -11,6 +11,7 @@
 - fix: No more exceptions when hovering over variables without type, and types of local variabled kept under match statements (https://github.com/dafny-lang/dafny/pull/2437)
 - fix: Check extreme predicates and constants in all types, not just classes
   (https://github.com/dafny-lang/dafny/pull/2515)
+- feat: `predicate P(x: int): (y: bool) ...` is now a valid syntax (https://github.com/dafny-lang/dafny/pull/2454)
 - fix: Improve the performance of proofs involving bit vector shifts (https://github.com/dafny-lang/dafny/pull/2520)
 
 # 3.7.3

Source/Dafny/AST/DafnyAst.cs

@@ -6171,9 +6171,10 @@ public enum BodyOriginKind {
     public readonly BodyOriginKind BodyOrigin;
     public Predicate(IToken tok, string name, bool hasStaticKeyword, bool isGhost,
       List<TypeParameter> typeArgs, List<Formal> formals,
+      Formal result,
       List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens, Specification<Expression> decreases,
       Expression body, BodyOriginKind bodyOrigin, IToken/*?*/ byMethodTok, BlockStmt/*?*/ byMethodBody, Attributes attributes, IToken signatureEllipsis)
-      : base(tok, name, hasStaticKeyword, isGhost, typeArgs, formals, null, Type.Bool, req, reads, ens, decreases, body, byMethodTok, byMethodBody, attributes, signatureEllipsis) {
+      : base(tok, name, hasStaticKeyword, isGhost, typeArgs, formals, result, Type.Bool, req, reads, ens, decreases, body, byMethodTok, byMethodBody, attributes, signatureEllipsis) {
       Contract.Requires(bodyOrigin == Predicate.BodyOriginKind.OriginalOrInherited || body != null);
       BodyOrigin = bodyOrigin;
     }
@@ -6211,10 +6212,10 @@ public bool KNat {
     [FilledInDuringResolution] public PrefixPredicate PrefixPredicate;  // (name registration)
 
     public ExtremePredicate(IToken tok, string name, bool hasStaticKeyword, KType typeOfK,
-      List<TypeParameter> typeArgs, List<Formal> formals,
+      List<TypeParameter> typeArgs, List<Formal> formals, Formal result,
       List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens,
       Expression body, Attributes attributes, IToken signatureEllipsis)
-      : base(tok, name, hasStaticKeyword, true, typeArgs, formals, null, Type.Bool,
+      : base(tok, name, hasStaticKeyword, true, typeArgs, formals, result, Type.Bool,
              req, reads, ens, new Specification<Expression>(new List<Expression>(), null), body, null, null, attributes, signatureEllipsis) {
       TypeOfK = typeOfK;
     }
@@ -6244,21 +6245,21 @@ public FunctionCallExpr CreatePrefixPredicateCall(FunctionCallExpr fexp, Express
   public class LeastPredicate : ExtremePredicate {
     public override string WhatKind { get { return "least predicate"; } }
     public LeastPredicate(IToken tok, string name, bool hasStaticKeyword, KType typeOfK,
-      List<TypeParameter> typeArgs, List<Formal> formals,
+      List<TypeParameter> typeArgs, List<Formal> formals, Formal result,
       List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens,
       Expression body, Attributes attributes, IToken signatureEllipsis)
-      : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, formals,
+      : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, formals, result,
              req, reads, ens, body, attributes, signatureEllipsis) {
     }
   }
 
   public class GreatestPredicate : ExtremePredicate {
     public override string WhatKind { get { return "greatest predicate"; } }
     public GreatestPredicate(IToken tok, string name, bool hasStaticKeyword, KType typeOfK,
-      List<TypeParameter> typeArgs, List<Formal> formals,
+      List<TypeParameter> typeArgs, List<Formal> formals, Formal result,
       List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens,
       Expression body, Attributes attributes, IToken signatureEllipsis)
-      : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, formals,
+      : base(tok, name, hasStaticKeyword, typeOfK, typeArgs, formals, result,
              req, reads, ens, body, attributes, signatureEllipsis) {
     }
   }
@@ -6286,10 +6287,10 @@ public TwoStateFunction(IToken tok, string name, bool hasStaticKeyword,
   public class TwoStatePredicate : TwoStateFunction {
     public override string WhatKind { get { return "twostate predicate"; } }
     public TwoStatePredicate(IToken tok, string name, bool hasStaticKeyword,
-                     List<TypeParameter> typeArgs, List<Formal> formals,
+                     List<TypeParameter> typeArgs, List<Formal> formals, Formal result,
                      List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens, Specification<Expression> decreases,
                      Expression body, Attributes attributes, IToken signatureEllipsis)
-      : base(tok, name, hasStaticKeyword, typeArgs, formals, null, Type.Bool, req, reads, ens, decreases, body, attributes, signatureEllipsis) {
+      : base(tok, name, hasStaticKeyword, typeArgs, formals, result, Type.Bool, req, reads, ens, decreases, body, attributes, signatureEllipsis) {
       Contract.Requires(tok != null);
       Contract.Requires(name != null);
       Contract.Requires(typeArgs != null);

Source/Dafny/AST/Printer.cs

@@ -859,9 +859,7 @@ public void PrintFunction(Function f, int indent, bool printSignatureOnly) {
           PrintKTypeIndication(((ExtremePredicate)f).TypeOfK);
         }
         PrintFormals(f.Formals, f, f.Name);
-        if (f is Predicate || f is TwoStatePredicate || f is ExtremePredicate || f is PrefixPredicate) {
-          // the result type is tacitly "bool"
-        } else {
+        if (f.Result != null || (f is not Predicate && f is not ExtremePredicate && f is not TwoStatePredicate && f is not PrefixPredicate)) {
           wr.Write(": ");
           if (f.Result != null) {
             wr.Write("(");

Source/Dafny/Cloner.cs

@@ -749,6 +749,7 @@ public virtual Field CloneField(Field f) {
     public virtual Function CloneFunction(Function f, string newName = null) {
       var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
       var formals = f.Formals.ConvertAll(CloneFormal);
+      var result = f.Result != null ? CloneFormal(f.Result) : null;
       var req = f.Req.ConvertAll(CloneAttributedExpr);
       var reads = f.Reads.ConvertAll(CloneFrameExpr);
       var decreases = CloneSpecExpr(f.Decreases);
@@ -761,24 +762,24 @@ public virtual Function CloneFunction(Function f, string newName = null) {
       }
 
       if (f is Predicate) {
-        return new Predicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsGhost, tps, formals,
+        return new Predicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsGhost, tps, formals, result,
           req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited,
           f.ByMethodTok == null ? null : Tok(f.ByMethodTok), byMethodBody,
           CloneAttributes(f.Attributes), null);
       } else if (f is LeastPredicate) {
-        return new LeastPredicate(Tok(f.tok), newName, f.HasStaticKeyword, ((LeastPredicate)f).TypeOfK, tps, formals,
+        return new LeastPredicate(Tok(f.tok), newName, f.HasStaticKeyword, ((LeastPredicate)f).TypeOfK, tps, formals, result,
           req, reads, ens, body, CloneAttributes(f.Attributes), null);
       } else if (f is GreatestPredicate) {
-        return new GreatestPredicate(Tok(f.tok), newName, f.HasStaticKeyword, ((GreatestPredicate)f).TypeOfK, tps, formals,
+        return new GreatestPredicate(Tok(f.tok), newName, f.HasStaticKeyword, ((GreatestPredicate)f).TypeOfK, tps, formals, result,
           req, reads, ens, body, CloneAttributes(f.Attributes), null);
       } else if (f is TwoStatePredicate) {
-        return new TwoStatePredicate(Tok(f.tok), newName, f.HasStaticKeyword, tps, formals,
+        return new TwoStatePredicate(Tok(f.tok), newName, f.HasStaticKeyword, tps, formals, result,
           req, reads, ens, decreases, body, CloneAttributes(f.Attributes), null);
       } else if (f is TwoStateFunction) {
-        return new TwoStateFunction(Tok(f.tok), newName, f.HasStaticKeyword, tps, formals, f.Result == null ? null : CloneFormal(f.Result), CloneType(f.ResultType),
+        return new TwoStateFunction(Tok(f.tok), newName, f.HasStaticKeyword, tps, formals, result, CloneType(f.ResultType),
           req, reads, ens, decreases, body, CloneAttributes(f.Attributes), null);
       } else {
-        return new Function(Tok(f.tok), newName, f.HasStaticKeyword, f.IsGhost, tps, formals, f.Result == null ? null : CloneFormal(f.Result), CloneType(f.ResultType),
+        return new Function(Tok(f.tok), newName, f.HasStaticKeyword, f.IsGhost, tps, formals, result, CloneType(f.ResultType),
           req, reads, ens, decreases, body, f.ByMethodTok == null ? null : Tok(f.ByMethodTok), byMethodBody,
           CloneAttributes(f.Attributes), null);
       }

Source/Dafny/Dafny.atg

@@ -299,12 +299,18 @@ bool IsAlternative() {
       || la.kind == _case;
 }
 
-bool FollowedByColon() {
+bool IsParenIdentsColon() {
   IToken x = la;
-  while (IsIdentifier(x.kind) || x.kind == _openparen) {
+  if(x.kind != _openparen) {
+    return false;
+  }
+  x = scanner.Peek();
+  var oneOrMoreIdentifiers = false;
+  while(IsIdentifier(x.kind)) {
     x = scanner.Peek();
+    oneOrMoreIdentifiers = true;
   }
-  return x.kind == _colon;
+  return oneOrMoreIdentifiers && x.kind == _colon;
 }
 
 bool IsGets() {
@@ -2336,7 +2342,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
       [ GenericParameters<typeArgs, false> ]
       Formals<true, true, isTwoState, true, formals>
       ":"
-      (  IF(FollowedByColon())
+      (  IF(IsParenIdentsColon())
          "("
            GIdentType<false, false, false, false, out var resultId, out var ty, out var resultIsGhost, out var isOld, out var isNameOnly, out var isOlder>
            (. Contract.Assert(!resultIsGhost && !isOld && !isNameOnly && !isOlder);
@@ -2358,8 +2364,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
       [ GenericParameters<typeArgs, false> ]
       [ Formals<true, true, isTwoState, true, formals>
       ]
-      [ ":" Type<out returnType> (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .)
-      ]
+      [ PredicateResult<"predicate", out result> ]
     | ellipsis   (. signatureEllipsis = t; .)
     )
 
@@ -2377,8 +2382,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
       [ GenericParameters<typeArgs, false> ]
       [ KType<ref kType> ]
       Formals<true, false, false, false, formals>
-      [ ":"                    (. SemErr(t, "least predicates do not have an explicitly declared return type; it is always bool"); .)
-      ]
+      [ PredicateResult<"least predicate", out result> ]
     | ellipsis                 (. signatureEllipsis = t; .)
     )
 
@@ -2396,8 +2400,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
       [ GenericParameters<typeArgs, false> ]
       [ KType<ref kType> ]
       Formals<true, false, false, false, formals>
-      [ ":"                    (. SemErr(t, "greatest predicates do not have an explicitly declared return type; it is always bool"); .)
-      ]
+      [ PredicateResult<"greatest predicate", out result> ]
     | ellipsis                 (. signatureEllipsis = t; .)
     )
   )
@@ -2545,24 +2548,24 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
      IToken tok = id;
      if (isTwoState && isPredicate) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
-       f = new TwoStatePredicate(tok, id.val, dmod.IsStatic, typeArgs, formals,
+       f = new TwoStatePredicate(tok, id.val, dmod.IsStatic, typeArgs, formals, result,
                                  reqs, reads, ens, new Specification<Expression>(decreases, decAttrs), body, attrs, signatureEllipsis);
      } else if (isTwoState) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
        f = new TwoStateFunction(tok, id.val, dmod.IsStatic, typeArgs, formals, result, returnType,
                                 reqs, reads, ens, new Specification<Expression>(decreases, decAttrs), body, attrs, signatureEllipsis);
      } else if (isPredicate) {
        Contract.Assert(functionMethodToken == null || !dmod.IsGhost);
-       f = new Predicate(tok, id.val, dmod.IsStatic, isGhost, typeArgs, formals,
+       f = new Predicate(tok, id.val, dmod.IsStatic, isGhost, typeArgs, formals, result,
                          reqs, reads, ens, new Specification<Expression>(decreases, decAttrs), body, Predicate.BodyOriginKind.OriginalOrInherited,
                          byMethodTok, byMethodBody, attrs, signatureEllipsis);
      } else if (isLeastPredicate) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
-       f = new LeastPredicate(tok, id.val, dmod.IsStatic, kType, typeArgs, formals,
+       f = new LeastPredicate(tok, id.val, dmod.IsStatic, kType, typeArgs, formals, result,
                               reqs, reads, ens, body, attrs, signatureEllipsis);
      } else if (isGreatestPredicate) {
        Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
-       f = new GreatestPredicate(tok, id.val, dmod.IsStatic, kType, typeArgs, formals,
+       f = new GreatestPredicate(tok, id.val, dmod.IsStatic, kType, typeArgs, formals, result,
                                  reqs, reads, ens, body, attrs, signatureEllipsis);
      } else {
        Contract.Assert(functionMethodToken == null || !dmod.IsGhost);
@@ -2604,6 +2607,26 @@ FunctionSpec<.List<AttributedExpression> reqs, List<FrameExpression> reads, List
   }
   .
 
+/*------------------------------------------------------------------------*/
+PredicateResult<string name, out Formal? result>
+= (. Type/*!*/ returnType = new BoolType();
+     result = null;
+  .)
+  ":"
+  (  IF(IsParenIdentsColon())
+     "("
+       GIdentType<false, false, false, false, out var resultId, out var ty, out var resultIsGhost, out var isOld, out var isNameOnly, out var isOlder>
+       (. Contract.Assert(!resultIsGhost && !isOld && !isNameOnly && !isOlder);
+          if(ty is not BoolType) {
+            SemErr(t, $"{name} return type should be bool, got {ty}");
+          }
+          result = new Formal(resultId, resultId.val, ty, false, false, null, false);
+       .)
+     ")"
+     | Type<out returnType> (. SemErr(t, $"{name}s do not have an explicitly declared return type; it is always bool. Unless you want to name the result: ': (result: bool)'"); .)
+  )
+  .
+
 /*------------------------------------------------------------------------*/
 PossiblyWildExpression<out Expression e, bool allowLambda, bool allowWild>
 = (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null);

Source/Dafny/RefinementTransformer.cs

@@ -571,18 +571,18 @@ Function CloneFunction(IToken tok, Function f, bool isGhost, List<AttributedExpr
       var byMethodBody = refinementCloner.CloneBlockStmt(f.ByMethodBody);
 
       if (f is Predicate) {
-        return new Predicate(tok, f.Name, f.HasStaticKeyword, isGhost, tps, formals,
+        return new Predicate(tok, f.Name, f.HasStaticKeyword, isGhost, tps, formals, result,
           req, reads, ens, decreases, body, bodyOrigin,
           f.ByMethodTok == null ? null : refinementCloner.Tok(f.ByMethodTok), byMethodBody,
           refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
       } else if (f is LeastPredicate) {
-        return new LeastPredicate(tok, f.Name, f.HasStaticKeyword, ((LeastPredicate)f).TypeOfK, tps, formals,
+        return new LeastPredicate(tok, f.Name, f.HasStaticKeyword, ((LeastPredicate)f).TypeOfK, tps, formals, result,
           req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
       } else if (f is GreatestPredicate) {
-        return new GreatestPredicate(tok, f.Name, f.HasStaticKeyword, ((GreatestPredicate)f).TypeOfK, tps, formals,
+        return new GreatestPredicate(tok, f.Name, f.HasStaticKeyword, ((GreatestPredicate)f).TypeOfK, tps, formals, result,
           req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
       } else if (f is TwoStatePredicate) {
-        return new TwoStatePredicate(tok, f.Name, f.HasStaticKeyword, tps, formals,
+        return new TwoStatePredicate(tok, f.Name, f.HasStaticKeyword, tps, formals, result,
           req, reads, ens, decreases, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
       } else if (f is TwoStateFunction) {
         return new TwoStateFunction(tok, f.Name, f.HasStaticKeyword, tps, formals, result, refinementCloner.CloneType(f.ResultType),

Source/Dafny/Resolver.cs

@@ -2042,6 +2042,7 @@ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImport
           // --- here comes predicate Valid()
           var valid = new Predicate(iter.tok, "Valid", false, true, new List<TypeParameter>(),
             new List<Formal>(),
+            null,
             new List<AttributedExpression>(),
             new List<FrameExpression>(),
             new List<AttributedExpression>(),

Source/Dafny/Rewriter.cs

@@ -558,7 +558,7 @@ void ProcessClassPreResolve(ClassDecl cl) {
       // Add:  predicate Valid()
       // ...unless an instance function with that name is already present
       if (!cl.Members.Exists(member => member is Function && member.Name == "Valid" && !member.IsStatic)) {
-        var valid = new Predicate(cl.tok, "Valid", false, true, new List<TypeParameter>(), new List<Formal>(),
+        var valid = new Predicate(cl.tok, "Valid", false, true, new List<TypeParameter>(), new List<Formal>(), null,
           new List<AttributedExpression>(), new List<FrameExpression>(), new List<AttributedExpression>(), new Specification<Expression>(new List<Expression>(), null),
           null, Predicate.BodyOriginKind.OriginalOrInherited, null, null, null, null);
         cl.Members.Add(valid);

Test/dafny4/predicateReturnVariable.dfy

@@ -0,0 +1,8 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate method tautology1(x: int): (y: bool)
+  ensures x == 2 ==> y
+{
+  x >= 2
+}

Test/dafny4/predicateReturnVariable.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

Test/dafny4/predicateReturnVariableWrong.dfy

@@ -0,0 +1,26 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate tautology1(x: int): (y: int) {
+  true
+}
+
+least predicate tautology2(x: int): (y: int) {
+  true
+}
+
+greatest predicate tautology3(x: int): (y: int) {
+  true
+}
+
+type MyBoolSynonym = bool
+
+predicate tautology1(x: int): (y: MyBoolSynonym) {
+  true
+}
+
+type AlwaysTrue = x: bool | x
+
+predicate tautology1(x: int): (y: AlwaysTrue) {
+  true
+}

Test/dafny4/predicateReturnVariableWrong.dfy.expect

@@ -0,0 +1,6 @@
+predicateReturnVariableWrong.dfy(4,34): Error: predicate return type should be bool, got int
+predicateReturnVariableWrong.dfy(8,40): Error: least predicate return type should be bool, got int
+predicateReturnVariableWrong.dfy(12,43): Error: greatest predicate return type should be bool, got int
+predicateReturnVariableWrong.dfy(18,34): Error: predicate return type should be bool, got MyBoolSynonym
+predicateReturnVariableWrong.dfy(24,34): Error: predicate return type should be bool, got AlwaysTrue
+5 parse errors detected in predicateReturnVariableWrong.dfy

docs/DafnyRef/Types.md

@@ -2225,6 +2225,12 @@ PredicateSignature_(allowGhostKeyword, allowNewKeyword, allowOlderKeyword) =
   [ GenericParameters ]
   [ KType ]
   Formals(allowGhostKeyword, allowNewKeyword, allowOlderKeyword, allowDefault: true)
+  [
+    ":"
+    ( Type
+    | "(" Ident ":" "bool" ")"
+    )
+  ]
 
 FunctionBody = "{" Expression(allowLemma: true, allowLambda: true)
                "}" [ "by" "method" BlockStmt ]
@@ -2367,8 +2373,8 @@ clauses.
 ### 13.4.2. Predicates
 A function that returns a `bool` result is called a _predicate_. As an
 alternative syntax, a predicate can be declared by replacing the `function`
-keyword with the `predicate` keyword and omitting a declaration of the
-return type.
+keyword with the `predicate` keyword and possibly omitting a declaration of the
+return type (if it is not named).
 
 ### 13.4.3. Function Transparency
 A function is said to be _transparent_ in a location if the