feat: Compute triggers for such-that operations

Source/DafnyCore/AST/Cloner.cs

@@ -282,7 +282,7 @@ public virtual BoundVar CloneBoundVar(BoundVar bv, bool isReference) {
           return bv;
         }
 
-        var bvNew = new BoundVar(Origin(bv.Origin), new Name(this, bv.NameNode), CloneType(bv.SyntacticType));
+        var bvNew = new BoundVar(Origin(bv.Origin), new Name(this, bv.NameNode), CloneType(bv.SyntacticType), bv.IsGhost);
         bvNew.IsGhost = bv.IsGhost;
         return bvNew;
       });

Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs

@@ -40,29 +40,27 @@ public Expression AlphaRename(string prefix) {
     Contract.Requires(this != null);
     Contract.Requires(prefix != null);
 
-    if (SplitQuantifier != null) {
-      // TODO: what to do?  Substitute(exists.SplitQuantifierExpression);
+    if (SplitQuantifierExpression is ExistsExpr splitQuantifierExpression) {
+      return splitQuantifierExpression.AlphaRename(prefix);
     }
 
     var substMap = new Dictionary<IVariable, Expression>();
-    var var4var = new Dictionary<BoundVar, BoundVar>();
     var bvars = new List<BoundVar>();
     foreach (var bv in BoundVars) {
       var newBv = new BoundVar(bv.Origin, prefix + bv.Name, bv.Type);
       bvars.Add(newBv);
-      var4var.Add(bv, newBv);
-      var ie = new IdentifierExpr(newBv.Origin, newBv.Name);
-      ie.Var = newBv;  // resolve here
-      ie.Type = newBv.Type;  // resolve here
+      var ie = new IdentifierExpr(newBv.Origin, newBv);
       substMap.Add(bv, ie);
     }
     var s = new Substituter(null, substMap, new Dictionary<TypeParameter, Type>());
     var range = Range == null ? null : s.Substitute(Range);
     var term = s.Substitute(Term);
     var attrs = s.SubstAttributes(Attributes);
-    var ex = new ExistsExpr(Origin, bvars, range, term, attrs);
-    ex.Type = Type.Bool;
-    ex.Bounds = s.SubstituteBoundedPoolList(Bounds);
+
+    var ex = new ExistsExpr(Origin, bvars, range, term, attrs) {
+      Type = Type.Bool,
+      Bounds = s.SubstituteBoundedPoolList(Bounds),
+    };
     return ex;
   }
-}
+}

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -248,10 +248,10 @@ public static Expression CreateAdd(Expression e0, Expression e1) {
       (e0.Type.IsNumericBased(Type.NumericPersuasion.Int) && e1.Type.IsNumericBased(Type.NumericPersuasion.Int)) ||
       (e0.Type.IsNumericBased(Type.NumericPersuasion.Real) && e1.Type.IsNumericBased(Type.NumericPersuasion.Real)));
     Contract.Ensures(Contract.Result<Expression>() != null);
-    var s = new BinaryExpr(e0.Origin, BinaryExpr.Opcode.Add, e0, e1);
-    s.ResolvedOp = BinaryExpr.ResolvedOpcode.Add;  // resolve here
-    s.Type = e0.Type.NormalizeExpand();  // resolve here
-    return s;
+    return new BinaryExpr(e0.Origin, BinaryExpr.Opcode.Add, e0, e1) {
+      ResolvedOp = BinaryExpr.ResolvedOpcode.Add,
+      Type = e0.Type.NormalizeExpand()
+    };
   }
 
   /// <summary>
@@ -264,10 +264,10 @@ public static Expression CreateMul(Expression e0, Expression e1) {
       (e0.Type.IsNumericBased(Type.NumericPersuasion.Int) && e1.Type.IsNumericBased(Type.NumericPersuasion.Int)) ||
       (e0.Type.IsNumericBased(Type.NumericPersuasion.Real) && e1.Type.IsNumericBased(Type.NumericPersuasion.Real)));
     Contract.Ensures(Contract.Result<Expression>() != null);
-    var s = new BinaryExpr(e0.Origin, BinaryExpr.Opcode.Mul, e0, e1);
-    s.ResolvedOp = BinaryExpr.ResolvedOpcode.Mul;  // resolve here
-    s.Type = e0.Type.NormalizeExpand();  // resolve here
-    return s;
+    return new BinaryExpr(e0.Origin, BinaryExpr.Opcode.Mul, e0, e1) {
+      ResolvedOp = BinaryExpr.ResolvedOpcode.Mul,
+      Type = e0.Type.NormalizeExpand()
+    };
   }
 
   /// <summary>
@@ -300,9 +300,9 @@ public static Expression CreateSubtract_TypeConvert(Expression e0, Expression e1
 
   private static Expression CastIfNeeded(Expression expr, Type toType) {
     if (!expr.Type.Equals(toType)) {
-      var cast = new ConversionExpr(expr.Origin, expr, toType);
-      cast.Type = toType;
-      return cast;
+      return new ConversionExpr(expr.Origin, expr, toType) {
+        Type = toType
+      };
     } else {
       return expr;
     }
@@ -321,10 +321,10 @@ public static Expression CreateSubtract(Expression e0, Expression e1) {
       (e0.Type.IsNumericBased(Type.NumericPersuasion.Real) && e1.Type.IsNumericBased(Type.NumericPersuasion.Real)) ||
       (e0.Type.IsBigOrdinalType && e1.Type.IsBigOrdinalType));
     Contract.Ensures(Contract.Result<Expression>() != null);
-    var s = new BinaryExpr(e0.Origin, BinaryExpr.Opcode.Sub, e0, e1);
-    s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;  // resolve here
-    s.Type = e0.Type.NormalizeExpand();  // resolve here (and it's important to remove any constraints)
-    return s;
+    return new BinaryExpr(e0.Origin, BinaryExpr.Opcode.Sub, e0, e1) {
+      ResolvedOp = BinaryExpr.ResolvedOpcode.Sub,
+      Type = e0.Type.NormalizeExpand()
+    };
   }
 
   /// <summary>
@@ -341,11 +341,10 @@ public static Expression CreateSetDifference(Expression e0, Expression e1) {
     if (LiteralExpr.IsEmptySet(e0) || LiteralExpr.IsEmptySet(e1)) {
       return e0;
     }
-    var s = new BinaryExpr(e0.Origin, BinaryExpr.Opcode.Sub, e0, e1) {
+    return new BinaryExpr(e0.Origin, BinaryExpr.Opcode.Sub, e0, e1) {
       ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference,
       Type = e0.Type.NormalizeExpand() // important to remove any constraints
     };
-    return s;
   }
 
   /// <summary>
@@ -362,11 +361,10 @@ public static Expression CreateMultisetDifference(Expression e0, Expression e1)
     if (LiteralExpr.IsEmptyMultiset(e0) || LiteralExpr.IsEmptyMultiset(e1)) {
       return e0;
     }
-    var s = new BinaryExpr(e0.Origin, BinaryExpr.Opcode.Sub, e0, e1) {
+    return new BinaryExpr(e0.Origin, BinaryExpr.Opcode.Sub, e0, e1) {
       ResolvedOp = BinaryExpr.ResolvedOpcode.MultiSetDifference,
       Type = e0.Type.NormalizeExpand() // important to remove any constraints
     };
-    return s;
   }
 
   /// <summary>
@@ -377,10 +375,9 @@ public static Expression CreateCardinality(Expression e, SystemModuleManager sys
     Contract.Requires(e.Type != null);
     Contract.Requires(e.Type.AsSetType != null || e.Type.AsMultiSetType != null || e.Type.AsSeqType != null);
     Contract.Ensures(Contract.Result<Expression>() != null);
-    var s = new UnaryOpExpr(e.Origin, UnaryOpExpr.Opcode.Cardinality, e) {
+    return new UnaryOpExpr(e.Origin, UnaryOpExpr.Opcode.Cardinality, e) {
       Type = systemModuleManager.Nat()
     };
-    return s;
   }
 
   /// <summary>
@@ -420,9 +417,9 @@ public static Expression CreateDecrement(Expression e, int n, Type ty = null) {
   public static LiteralExpr CreateIntLiteralNonnegative(IOrigin tok, int n, Type ty = null) {
     Contract.Requires(tok != null);
     Contract.Requires(0 <= n);
-    var nn = new LiteralExpr(tok, n);
-    nn.Type = ty ?? Type.Int;
-    return nn;
+    return new LiteralExpr(tok, n) {
+      Type = ty ?? Type.Int
+    };
   }
 
   /// <summary>
@@ -443,9 +440,9 @@ public static Expression CreateIntLiteral(IOrigin tok, int n, Type ty = null) {
   /// </summary>
   public static Expression CreateRealLiteral(IOrigin tok, BaseTypes.BigDec x) {
     Contract.Requires(tok != null);
-    var nn = new LiteralExpr(tok, x);
-    nn.Type = Type.Real;
-    return nn;
+    return new LiteralExpr(tok, x) {
+      Type = Type.Real
+    };
   }
 
   /// <summary>
@@ -455,20 +452,19 @@ public static Expression CreateNatLiteral(IOrigin tok, int n, Type ty) {
     Contract.Requires(tok != null);
     Contract.Requires(0 <= n);
     Contract.Requires(ty.IsNumericBased(Type.NumericPersuasion.Int) || ty is BigOrdinalType);
-    var nn = new LiteralExpr(tok, n);
-    nn.Type = ty;
-    return nn;
+    return new LiteralExpr(tok, n) {
+      Type = ty
+    };
   }
 
   /// <summary>
   /// Create a resolved expression for a bool b
   /// </summary>
   public static LiteralExpr CreateBoolLiteral(IOrigin tok, bool b) {
     Contract.Requires(tok != null);
-    var lit = new LiteralExpr(tok, b) {
+    return new LiteralExpr(tok, b) {
       Type = Type.Bool
     };
-    return lit;
   }
 
   /// <summary>
@@ -477,10 +473,9 @@ public static LiteralExpr CreateBoolLiteral(IOrigin tok, bool b) {
   public static LiteralExpr CreateStringLiteral(IOrigin tok, string s) {
     Contract.Requires(tok != null);
     Contract.Requires(s != null);
-    var lit = new StringLiteralExpr(tok, s, true) {
+    return new StringLiteralExpr(tok, s, true) {
       Type = new SeqType(new CharType())
     };
-    return lit;
   }
 
   /// <summary>
@@ -698,16 +693,19 @@ public static Expression CreateAnd(Expression a, Expression b, bool allowSimplif
     Contract.Requires(b != null);
     Contract.Requires(a.Type.IsBoolType && b.Type.IsBoolType);
     Contract.Ensures(Contract.Result<Expression>() != null);
-    if (allowSimplification && LiteralExpr.IsTrue(a)) {
-      return b;
-    } else if (allowSimplification && LiteralExpr.IsTrue(b)) {
-      return a;
-    } else {
-      var and = new BinaryExpr(a.Origin, BinaryExpr.Opcode.And, a, b);
-      and.ResolvedOp = BinaryExpr.ResolvedOpcode.And;  // resolve here
-      and.Type = Type.Bool;  // resolve here
-      return and;
+    if (allowSimplification) {
+      if (LiteralExpr.IsTrue(a)) {
+        return b;
+      } else if (LiteralExpr.IsFalse(a) || LiteralExpr.IsTrue(b)) {
+        return a;
+      }
+      // Note, to respect evaluation order, we don't simplify "X && false" to "false".
     }
+
+    return new BinaryExpr(a.Origin, BinaryExpr.Opcode.And, a, b) {
+      ResolvedOp = BinaryExpr.ResolvedOpcode.And,
+      Type = Type.Bool
+    };
   }
 
   /// <summary>
@@ -718,14 +716,19 @@ public static Expression CreateImplies(Expression a, Expression b, bool allowSim
     Contract.Requires(b != null);
     Contract.Requires(a.Type.IsBoolType && b.Type.IsBoolType);
     Contract.Ensures(Contract.Result<Expression>() != null);
-    if (allowSimplification && (LiteralExpr.IsTrue(a) || LiteralExpr.IsTrue(b))) {
-      return b;
-    } else {
-      var imp = new BinaryExpr(a.Origin, BinaryExpr.Opcode.Imp, a, b);
-      imp.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;  // resolve here
-      imp.Type = Type.Bool;  // resolve here
-      return imp;
+    if (allowSimplification) {
+      if (LiteralExpr.IsTrue(a)) {
+        return b;
+      } else if (LiteralExpr.IsFalse(a)) {
+        return CreateBoolLiteral(a.Origin, true);
+      }
+      // Note, to respect evaluation order, we don't simplify "X ==> true" to "true".
     }
+
+    return new BinaryExpr(a.Origin, BinaryExpr.Opcode.Imp, a, b) {
+      ResolvedOp = BinaryExpr.ResolvedOpcode.Imp,
+      Type = Type.Bool
+    };
   }
 
   /// <summary>
@@ -736,16 +739,19 @@ public static Expression CreateOr(Expression a, Expression b, bool allowSimplifi
     Contract.Requires(b != null);
     Contract.Requires(a.Type.IsBoolType && b.Type.IsBoolType);
     Contract.Ensures(Contract.Result<Expression>() != null);
-    if (allowSimplification && LiteralExpr.IsTrue(a)) {
-      return a;
-    } else if (allowSimplification && LiteralExpr.IsTrue(b)) {
-      return b;
-    } else {
-      var or = new BinaryExpr(a.Origin, BinaryExpr.Opcode.Or, a, b);
-      or.ResolvedOp = BinaryExpr.ResolvedOpcode.Or;  // resolve here
-      or.Type = Type.Bool;  // resolve here
-      return or;
+    if (allowSimplification) {
+      if (LiteralExpr.IsFalse(a)) {
+        return b;
+      } else if (LiteralExpr.IsTrue(a) || LiteralExpr.IsFalse(b)) {
+        return a;
+      }
+      // Note, to respect evaluation order, we don't simplify "X || true" to "true".
     }
+
+    return new BinaryExpr(a.Origin, BinaryExpr.Opcode.Or, a, b) {
+      ResolvedOp = BinaryExpr.ResolvedOpcode.Or,
+      Type = Type.Bool
+    };
   }
 
   /// <summary>
@@ -757,9 +763,9 @@ public static Expression CreateITE(Expression test, Expression e0, Expression e1
     Contract.Requires(e1 != null);
     Contract.Requires(test.Type.IsBoolType && e0.Type.Equals(e1.Type));
     Contract.Ensures(Contract.Result<Expression>() != null);
-    var ite = new ITEExpr(test.Origin, false, test, e0, e1);
-    ite.Type = e0.type;  // resolve here
-    return ite;
+    return new ITEExpr(test.Origin, false, test, e0, e1) {
+      Type = e0.Type
+    };
   }
 
   /// <summary>

Source/DafnyCore/AST/Expressions/LiteralExpr.cs

@@ -33,6 +33,11 @@ public static bool IsTrue(Expression e) {
     return Expression.IsBoolLiteral(e, out var value) && value;
   }
 
+  public static bool IsFalse(Expression e) {
+    Contract.Requires(e != null);
+    return Expression.IsBoolLiteral(e, out var value) && !value;
+  }
+
   public static bool IsEmptySet(Expression e) {
     Contract.Requires(e != null);
     return StripParens(e) is SetDisplayExpr display && display.Elements.Count == 0;

Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs

@@ -8,11 +8,10 @@ namespace Microsoft.Dafny;
 public class BoundVar : NonglobalVariable {
   public override bool IsMutable => false;
 
-  public BoundVar(string name, Type type) : this(Token.NoToken, new Name(Token.NoToken, name), type) { }
-  public BoundVar(IOrigin origin, string name, Type type) : this(origin, new Name(origin.StartToken, name), type) { }
+  public BoundVar(IOrigin origin, string name, Type type, bool isGhost = false) : this(origin, new Name(origin.StartToken, name), type, isGhost) { }
 
-  public BoundVar(IOrigin origin, Name name, Type type)
-    : base(origin, name, type, false) {
+  public BoundVar(IOrigin origin, Name name, Type type, bool isGhost)
+    : base(origin, name, type, isGhost) {
     Contract.Requires(origin != null);
     Contract.Requires(name != null);
     Contract.Requires(type != null);

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

@@ -31,9 +31,14 @@ public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, boo
         while (true) {
           var ite = (ITEExpr)expr;
           wr.Write("if ");
-          PrintExpression(ite.Test, false);
+          if (options.DafnyPrintResolvedFile == null) {
+            PrintGuard(ite.IsBindingGuard, ite.Test);
+          } else {
+            PrintExpression(ite.Test, false);
+          }
           wr.WriteLine(" then");
-          PrintExtendedExpr(ite.Thn, indent + IndentAmount, true, false);
+          var thenBranch = options.DafnyPrintResolvedFile == null && ite.IsBindingGuard ? ((LetExpr)ite.Thn).Body : ite.Thn;
+          PrintExtendedExpr(thenBranch, indent + IndentAmount, true, false);
           expr = ite.Els;
           if (expr is ITEExpr) {
             Indent(indent); wr.Write("else ");
@@ -1150,9 +1155,14 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext,
         bool parensNeeded = !isRightmost;
         if (parensNeeded) { wr.Write("("); }
         wr.Write("if ");
-        PrintExpression(ite.Test, false);
+        if (options.DafnyPrintResolvedFile == null) {
+          PrintGuard(ite.IsBindingGuard, ite.Test);
+        } else {
+          PrintExpression(ite.Test, false);
+        }
         wr.Write(" then ");
-        PrintExpression(ite.Thn, false);
+        var thenBranch = options.DafnyPrintResolvedFile == null && ite.IsBindingGuard ? ((LetExpr)ite.Thn).Body : ite.Thn;
+        PrintExpression(thenBranch, false);
         wr.Write(" else ");
         PrintExpression(ite.Els, !parensNeeded && isFollowedBySemicolon);
         if (parensNeeded) { wr.Write(")"); }

Source/DafnyCore/AST/Statements/ControlFlow/ForallStmt.cs

@@ -81,12 +81,10 @@ public Statement S0 {
       // dig into Body to find a single statement
       Statement s = Body;
       while (true) {
-        var block = s as BlockStmt;
-        if (block != null && block.Body.Count == 1) {
+        if (s is BlockStmt { Body: { Count: 1 } } block) {
           s = block.Body[0];
           // dig further into s
-        } else if (s is AssignStatement) {
-          var update = (AssignStatement)s;
+        } else if (s is AssignStatement update) {
           if (update.ResolvedStatements?.Count == 1) {
             s = update.ResolvedStatements[0];
             // dig further into s