Implement decreases to expressions

Source/DafnyCore/AST/Expressions/Operators/DecreasesToExpr.cs

@@ -0,0 +1,39 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+
+namespace Microsoft.Dafny;
+
+public class DecreasesToExpr : Expression, ICloneable<DecreasesToExpr> {
+  public IEnumerable<Expression> OldExpressions { get; }
+  public IEnumerable<Expression> NewExpressions { get; }
+
+  public bool AllowNoChange { get; }
+
+  public DecreasesToExpr(IToken tok, IEnumerable<Expression> oldExpressions, IEnumerable<Expression> newExpressions, bool allowNoChange) : base(tok) {
+    OldExpressions = oldExpressions;
+    NewExpressions = newExpressions;
+    AllowNoChange = allowNoChange;
+  }
+
+  public DecreasesToExpr(Cloner cloner, DecreasesToExpr original) : base(cloner, original) {
+    OldExpressions = original.OldExpressions.Select(cloner.CloneExpr);
+    NewExpressions = original.NewExpressions.Select(cloner.CloneExpr);
+    AllowNoChange = original.AllowNoChange;
+  }
+
+  public DecreasesToExpr Clone(Cloner cloner) {
+    return new DecreasesToExpr(cloner, this);
+  }
+
+  public override IEnumerable<Expression> SubExpressions {
+    get {
+      foreach (var oldExpr in OldExpressions) {
+        yield return oldExpr;
+      }
+      foreach (var newExpr in NewExpressions) {
+        yield return newExpr;
+      }
+    }
+  }
+}

Source/DafnyCore/AST/Grammar/ParseErrors.cs

@@ -139,6 +139,8 @@ public enum ErrorId {
     p_file_has_no_code,
     p_general_traits_datatype,
     p_general_traits_full,
+    p_decreases_without_to,
+    p_binding_in_decreases_to,
   }
 
   static ParseErrors() {

Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs

@@ -184,6 +184,9 @@ bool IsParenStar() {
   bool IsExpliesOp() => IsExpliesOp(la);
   bool IsAndOp() => IsAndOp(la);
   bool IsOrOp() => IsOrOp(la);
+  bool IsComma() {
+    return la.val == ",";
+  }
   static bool IsEquivOp(IToken la) {
     return la.val == "<==>";
   }
@@ -682,6 +685,39 @@ bool IsAssumeTypeKeyword(IToken la) {
     return la.kind == _assume || la.kind == _assert || la.kind == _expect;
   }
 
+  Expression ProcessTupleArgs(List<ActualBinding> args, IToken lp) {
+    if (args.Count == 1 && !args[0].IsGhost) {
+      if (args[0].FormalParameterName != null) {
+        SemErr(ErrorId.p_no_parenthesized_binding, lp, "binding not allowed in parenthesized expression");
+      }
+      return args[0].Actual;
+    } else {
+      // Compute the actual position of ghost arguments
+      var ghostness = new bool[args.Count];
+      for (var i = 0; i < args.Count; i++) {
+        ghostness[i] = false;
+      }
+      for (var i = 0; i < args.Count; i++) {
+        var arg = args[i];
+        if (arg.IsGhost) {
+          if (arg.FormalParameterName == null) {
+            ghostness[i] = true;
+          } else {
+            var success = int.TryParse(arg.FormalParameterName.val, out var index);
+            if (success && 0 <= index && index < args.Count) {
+              ghostness[index] = true;
+            }
+          }
+        }
+      }
+      var argumentGhostness = ghostness.ToList();
+      // make sure the corresponding tuple type exists
+      SystemModuleModifiers.Add(b => b.TupleType(lp, args.Count, true, argumentGhostness));
+      return new DatatypeValue(lp, SystemModuleManager.TupleTypeName(argumentGhostness), SystemModuleManager.TupleTypeCtorName(args.Count), args);
+    }
+  }
+
+
   public void ApplyOptionsFromAttributes(Attributes attrs) {
     var overrides = attrs.AsEnumerable().Where(a => a.Name == "options")
       .Reverse().Select(a =>
@@ -764,4 +800,4 @@ void CheckDeclModifiers(ref DeclModifierData dmod, string declCaption, AllowedDe
     }
   }
 
-}
+}

Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs

@@ -1193,6 +1193,28 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext,
         wr.Write("[BoogieFunctionCall]");  // this prevents debugger watch window crash
       } else if (expr is Resolver_IdentifierExpr) {
         wr.Write("[Resolver_IdentifierExpr]");  // we can get here in the middle of a debugging session
+      } else if (expr is DecreasesToExpr decreasesToExpr) {
+        var comma = false;
+        foreach (var oldExpr in decreasesToExpr.OldExpressions) {
+          if (comma) {
+            wr.Write(", ");
+          }
+          PrintExpression(oldExpr, false);
+          comma = true;
+        }
+        if (decreasesToExpr.AllowNoChange) {
+          wr.Write(" nonincreases to ");
+        } else {
+          wr.Write(" decreases to ");
+        }
+        comma = false;
+        foreach (var newExpr in decreasesToExpr.NewExpressions) {
+          if (comma) {
+            wr.Write(", ");
+          }
+          PrintExpression(newExpr, false);
+          comma = true;
+        }
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
       }

Source/DafnyCore/AST/Substituter.cs

@@ -425,6 +425,13 @@ ExtendedPattern SubstituteForPattern(ExtendedPattern pattern) {
           newExpr = new BoogieGenerator.BoogieFunctionCall(e.tok, e.FunctionName, e.UsesHeap, e.UsesOldHeap, e.HeapAtLabels, newArgs, newTyArgs);
         }
 
+      } else if (expr is DecreasesToExpr decreasesToExpr) {
+        List<Expression> oldExpressionsSubst = SubstituteExprList(decreasesToExpr.OldExpressions.ToList());
+        List<Expression> newExpressionsSubst = SubstituteExprList(decreasesToExpr.NewExpressions.ToList());
+        newExpr = new DecreasesToExpr(decreasesToExpr.tok, oldExpressionsSubst, newExpressionsSubst, decreasesToExpr.AllowNoChange) {
+          Type = decreasesToExpr.Type
+        };
+
       } else {
         Contract.Assume(false); // unexpected Expression
       }

Source/DafnyCore/Dafny.atg

@@ -144,6 +144,7 @@ TOKENS
   by = "by".
   in = "in".
   decreases = "decreases".
+  nonincreases = "nonincreases".
   invariant = "invariant".
   function = "function".
   predicate = "predicate".
@@ -2970,7 +2971,7 @@ AssumeStmt<out Statement/*!*/ s>
   .)
   "assume"                                     (. x = t; startToken = t; .)
   { Attribute<ref attrs> }
-  ( Expression<out e, false, true>
+  ( Expression<out e, false, false>
   | ellipsis                                   (. dotdotdot = t; 
                                                   errors.Deprecated(ErrorId.p_deprecated_statement_refinement, t, "the ... refinement feature in statements is deprecated");
                                                 .)
@@ -3202,6 +3203,47 @@ Forall = "forall".
 Exists = "exists".
 QSep = "::".
 
+MaybeDecreasesToExpression<out Expression e, IToken lp>
+= (. List<ActualBinding> args = new();
+     List<Expression> newExprs = new();
+     Expression tmp = null;
+     IToken x = null;
+     bool allowNoChange = false;
+  .)
+  TupleArgs<args>
+  [ ( "decreases"                                                 (. allowNoChange = false; .)
+    | "nonincreases"                                              (. allowNoChange = true; .)
+    ) (. x = t; .)
+    ident
+    (. if (t.val != "to") {
+         SemErr(ErrorId.p_decreases_without_to, t, "expected 'to'");
+       }
+    .)
+    Expression<out tmp, false, false>                             (. newExprs.Add(tmp); .)
+    { ","
+      Expression<out tmp, false, false>                           (. newExprs.Add(tmp); .)
+    }
+  ]
+  (.
+      if (newExprs.Count() == 0) {
+        e = ProcessTupleArgs(args, lp);
+      } else if (args.Count() > 0 && newExprs.Count() > 0) {
+        var formals = args.Where(arg => arg.FormalParameterName != null).ToList();
+        if (formals.Any()) {
+          SemErr(ErrorId.p_binding_in_decreases_to,
+                 formals[0].FormalParameterName,
+                 "bindings are not allowed in `decreases to` expressions.");
+        }
+        var oldExprs = args.Select(arg => arg.Actual).ToList();
+        e = new DecreasesToExpr(x, oldExprs, newExprs, allowNoChange);
+        e.RangeToken = new RangeToken(oldExprs[0].tok, newExprs[newExprs.Count() - 1].tok);
+      } else {
+        // Unreachable
+        e = null;
+      }
+  .)
+  .
+
 /* The "allowLemma" argument says whether or not the expression
  * to be parsed is allowed to have the form S;E where S is a call to a lemma.
  * "allowLemma" should be passed in as "false" whenever the expression to
@@ -3718,43 +3760,23 @@ LambdaSpec<.ref List<FrameExpression> reads, ref Attributes readsAttrs, ref Expr
 
 /*------------------------------------------------------------------------*/
 ParensExpression<out Expression e>
-= (. IToken lp; IToken rp;
+= (. IToken lp = null; IToken rp = null;
      var args = new List<ActualBinding>();
+     e = dummyExpr;
   .)
-  "("                                        (. lp = t; .)
-  [ TupleArgs<args> ]
-  ")"                                        (. rp = t; .)
-  (. if (args.Count == 1 && !args[0].IsGhost) {
-       if (args[0].FormalParameterName != null) {
-         SemErr(ErrorId.p_no_parenthesized_binding, new RangeToken(lp,rp), "binding not allowed in parenthesized expression");
-       }
-       e = new ParensExpression(lp, args[0].Actual);
-     } else {
-       // Compute the actual position of ghost arguments
-       var ghostness = new bool[args.Count];
-       for (var i = 0; i < args.Count; i++) {
-         ghostness[i] = false;
-       }
-       for (var i = 0; i < args.Count; i++) {
-         var arg = args[i];
-         if (arg.IsGhost) {
-           if (arg.FormalParameterName == null) {
-             ghostness[i] = true;
-           } else {
-             var success = int.TryParse(arg.FormalParameterName.val, out var index);
-             if (success && 0 <= index && index < args.Count) {
-               ghostness[index] = true;
-             }
-           }
-         }
-       }
-       var argumentGhostness = ghostness.ToList();
-       // make sure the corresponding tuple type exists
-       SystemModuleModifiers.Add(b => b.TupleType(lp, args.Count, true, argumentGhostness));
-       e = new DatatypeValue(lp, SystemModuleManager.TupleTypeName(argumentGhostness), SystemModuleManager.TupleTypeCtorName(args.Count), args);
-     }
-     e.RangeToken = new RangeToken(lp, rp);
-  .)
+ "("                                        (. lp = t; .)
+  (
+    MaybeDecreasesToExpression<out e, lp>
+    ")"                                     (. rp = t;
+                                               if (e is not DatatypeValue) {
+                                                 e = new ParensExpression(lp, e);
+                                               }
+                                            .)
+  |
+    ")"                                     (. rp = t;
+                                               e = ProcessTupleArgs(new List<ActualBinding>(), lp);
+                                            .)
+  )                                         (. e.RangeToken = new RangeToken(lp, rp); .)
   .
 
 /*------------------------------------------------------------------------*/

Source/DafnyCore/Pipeline/Compilation.cs

@@ -534,8 +534,19 @@ private static void AddAssertedExprToCounterExampleErrorInfo(
 
     if (boogieProofObligationDesc is ProofObligationDescription.ProofObligationDescription dafnyProofObligationDesc) {
       var expr = dafnyProofObligationDesc.GetAssertedExpr(options);
+      string? msg = null;
       if (expr != null) {
-        errorInformation.AddAuxInfo(errorInformation.Tok, expr.ToString(), ErrorReporterExtensions.AssertedExprCategory);
+        msg = expr.ToString();
+      }
+
+      var extra = dafnyProofObligationDesc.GetExtraExplanation();
+      if (extra != null) {
+        msg = (msg ?? "") + extra;
+      }
+
+      if (msg != null) {
+        errorInformation.AddAuxInfo(errorInformation.Tok, msg,
+          ErrorReporterExtensions.AssertedExprCategory);
       }
     }
   }

Source/DafnyCore/Resolver/ExpressionTester.cs

@@ -351,6 +351,11 @@ bool onlyGhostParametersChange(Expression ee) {
       // other conditions are checked below
       subexpressionsAreInsideBranchesOnlyExcept = matchExpr.Source;
 
+    } else if (expr is DecreasesToExpr _) {
+      ReportError(ErrorId.r_decreases_to_only_in_specification,
+                  expr, "a `decreases to` expression is allowed only in specification and ghost contexts");
+      return false;
+
     } else if (expr is ConcreteSyntaxExpression concreteSyntaxExpression) {
       return CheckIsCompilable(concreteSyntaxExpression.ResolvedExpression, codeContext, insideBranchesOnly);
     }

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -1165,6 +1165,12 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont
 
       } else if (expr is NestedMatchExpr nestedMatchExpr) {
         ResolveNestedMatchExpr(nestedMatchExpr, resolutionContext);
+      } else if (expr is DecreasesToExpr decreasesToExpr) {
+        foreach (var subexpr in decreasesToExpr.SubExpressions) {
+          ResolveExpression(subexpr, resolutionContext);
+        }
+
+        decreasesToExpr.Type = Type.Bool;
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
       }

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -672,6 +672,13 @@ resolutionContext.CodeContext is ConstantField ||
         var e = (NestedMatchExpr)expr;
         ResolveNestedMatchExpr(e, resolutionContext);
 
+      } else if (expr is DecreasesToExpr decreasesToExpr) {
+        foreach (var e in decreasesToExpr.SubExpressions) {
+          ResolveExpression(e, resolutionContext);
+        }
+
+        decreasesToExpr.PreType = ConstrainResultToBoolFamilyOperator(decreasesToExpr.tok, "decreasesto");
+
       } else if (expr is MatchExpr) {
         Contract.Assert(false); // this case is always handled via NestedMatchExpr
 

Source/DafnyCore/Resolver/ResolutionErrors.cs

@@ -84,7 +84,8 @@ public enum ErrorId {
     r_failure_methods_deprecated,
     r_member_only_assumes_other,
     r_member_only_has_no_before_after,
-    r_empty_cyclic_datatype
+    r_empty_cyclic_datatype,
+    r_decreases_to_only_in_specification
   }
 
   static ResolutionErrors() {

Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs

@@ -35,6 +35,7 @@ public partial class BoogieGenerator {
   void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Expression> calleeDecreases,
                             Expression allowance,
                             Expression receiverReplacement, Dictionary<IVariable, Expression> substMap,
+                            Dictionary<IVariable, Expression> directSubstMap,
                             Dictionary<TypeParameter, Type> typeMap,
                             ExpressionTranslator etranCurrent, bool oldCaller, BoogieStmtListBuilder builder, bool inferredDecreases, string hint) {
     Contract.Requires(tok != null);
@@ -69,6 +70,7 @@ void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Ex
     }
     for (int i = 0; i < N; i++) {
       Expression e0 = Substitute(calleeDecreases[i], receiverReplacement, substMap, typeMap);
+      Expression e0direct = Substitute(calleeDecreases[i], receiverReplacement, directSubstMap, typeMap);
       Expression e1 = contextDecreases[i];
       if (oldCaller) {
         e1 = new OldExpr(e1.tok, e1) {
@@ -80,7 +82,7 @@ void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Ex
         break;
       }
       oldExpressions.Add(e1);
-      newExpressions.Add(e0);
+      newExpressions.Add(e0direct);
       toks.Add(new NestedToken(tok, e1.tok));
       types0.Add(e0.Type.NormalizeExpand());
       types1.Add(e1.Type.NormalizeExpand());
@@ -94,7 +96,7 @@ void CheckCallTermination(IToken tok, List<Expression> contextDecreases, List<Ex
     }
     builder.Add(Assert(tok, decrExpr, new
       PODesc.Terminates(inferredDecreases, null, allowance,
-                        oldExpressions, newExpressions, hint)));
+                        oldExpressions, newExpressions, endsWithWinningTopComparison, hint)));
   }
 
   /// <summary>
@@ -173,7 +175,7 @@ Bpl.Expr DecreasesCheck(List<IToken> toks, List<Type> types0, List<Type> types1,
     return decrCheck;
   }
 
-  bool CompatibleDecreasesTypes(Type t, Type u) {
+  static bool CompatibleDecreasesTypes(Type t, Type u) {
     Contract.Requires(t != null);
     Contract.Requires(u != null);
     t = t.NormalizeToAncestorType();
@@ -356,5 +358,8 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out
       less = BplAnd(Bpl.Expr.Not(b0), b1);
       atmost = BplImp(b0, b1);
     }
+
+    less.tok = tok;
+    atmost.tok = tok;
   }
 }