Merge branch 'master' into assignSuchThatByBlock

.github/workflows/integration-tests-reusable.yml

@@ -72,6 +72,11 @@ jobs:
       uses: actions/setup-dotnet@v4
       with:
         dotnet-version: ${{ env.dotnet-version }}
+    #  Setup dotnet 6.0 for running Boogie. Alternatively we could try running Boogie with a roll forward policy, or updating Boogie.
+    - name: Setup dotnet
+      uses: actions/setup-dotnet@v4
+      with:
+        dotnet-version: 6.0.x
     - name: C++ for ubuntu 20.04
       if: matrix.os == 'ubuntu-20.04'
       run: |

README.md

@@ -27,7 +27,7 @@ A reference manual is available both [online](https://dafny-lang.github.io/dafny
 
 ## Community
 
-You can ask questions about Dafny on [Stack Overflow](https://stackoverflow.com/questions/tagged/dafny) or participate in general discussion on Dafny's [![Gitter](https://badges.gitter.im/dafny-lang/community.svg)](https://gitter.im/dafny-lang/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge).
+Feel free to report issues here on GitHub or to ask for questions on our :speech_balloon: [Zulip](https://dafny.zulipchat.com/) channel. 
 
 ## Try Dafny
 

Scripts/package.py

@@ -161,7 +161,6 @@ def build(self):
         if path.exists(self.buildDirectory):
             shutil.rmtree(self.buildDirectory)
         run(["make", "--quiet", "clean"])
-        self.run_publish("DafnyLanguageServer")
         self.run_publish("DafnyServer")
         self.run_publish("DafnyRuntime", "netstandard2.0")
         self.run_publish("DafnyRuntime", "net452")

Source/Dafny.sln

@@ -43,6 +43,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Scripts", "Scripts\Scripts.csproj", "{3FAB051A-1745-497B-B4C0-D49194BB5D32}"
+EndProject
 EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
@@ -130,6 +132,10 @@ Global
 		{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.Build.0 = Release|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Release|Any CPU.Build.0 = Release|Any CPU
 	EndGlobalSection
 	GlobalSection(SolutionProperties) = preSolution
 		HideSolutionNode = FALSE

Source/DafnyCore/AST/Expressions/Applications/ThisExpr.cs

@@ -66,16 +66,16 @@ public override bool IsImplicit {
 /// gives a way to distinguish this receiver from other receivers, which
 /// plays a role in checking the restrictions on divided block statements.
 /// </summary>
-public class ImplicitThisExpr_ConstructorCall : ImplicitThisExpr, ICloneable<ImplicitThisExpr_ConstructorCall> {
-  public ImplicitThisExpr_ConstructorCall(Cloner cloner, ImplicitThisExpr_ConstructorCall original) : base(cloner, original) {
+public class ImplicitThisExprConstructorCall : ImplicitThisExpr, ICloneable<ImplicitThisExprConstructorCall> {
+  public ImplicitThisExprConstructorCall(Cloner cloner, ImplicitThisExprConstructorCall original) : base(cloner, original) {
   }
 
-  public ImplicitThisExpr_ConstructorCall(IOrigin tok)
+  public ImplicitThisExprConstructorCall(IOrigin tok)
     : base(tok) {
     Contract.Requires(tok != null);
   }
 
-  public new ImplicitThisExpr_ConstructorCall Clone(Cloner cloner) {
-    return new ImplicitThisExpr_ConstructorCall(cloner, this);
+  public new ImplicitThisExprConstructorCall Clone(Cloner cloner) {
+    return new ImplicitThisExprConstructorCall(cloner, this);
   }
 }

Source/DafnyCore/AST/Expressions/Variables/Resolver_IdentifierExpr.cs → Source/DafnyCore/AST/Expressions/Variables/ResolverIdentifierExpr.cs

@@ -8,18 +8,18 @@ namespace Microsoft.Dafny;
 /// <summary>
 /// This class is used only inside the resolver itself. It gets hung in the AST in uncompleted name segments.
 /// </summary>
-class Resolver_IdentifierExpr : Expression, IHasReferences, ICloneable<Resolver_IdentifierExpr> {
+class ResolverIdentifierExpr : Expression, IHasReferences, ICloneable<ResolverIdentifierExpr> {
   public readonly TopLevelDecl Decl;
   public readonly List<Type> TypeArgs;
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(Decl != null);
     Contract.Invariant(TypeArgs != null);
     Contract.Invariant(TypeArgs.Count == Decl.TypeArgs.Count);
-    Contract.Invariant(Type is ResolverType_Module || Type is ResolverType_Type);
+    Contract.Invariant(Type is ResolverTypeModule or ResolverTypeType);
   }
 
-  public Resolver_IdentifierExpr(Cloner cloner, Resolver_IdentifierExpr original) : base(cloner, original) {
+  public ResolverIdentifierExpr(Cloner cloner, ResolverIdentifierExpr original) : base(cloner, original) {
     Decl = original.Decl;
     TypeArgs = original.TypeArgs;
   }
@@ -38,38 +38,38 @@ public override Type ReplaceTypeArguments(List<Type> arguments) {
       throw new NotSupportedException();
     }
   }
-  public class ResolverType_Module : ResolverType {
+  public class ResolverTypeModule : ResolverType {
     [System.Diagnostics.Contracts.Pure]
     public override string TypeName(DafnyOptions options, ModuleDefinition context, bool parseAble) {
       Contract.Assert(parseAble == false);
       return "#module";
     }
     public override bool Equals(Type that, bool keepConstraints = false) {
-      return that.NormalizeExpand(keepConstraints) is ResolverType_Module;
+      return that.NormalizeExpand(keepConstraints) is ResolverTypeModule;
     }
   }
-  public class ResolverType_Type : ResolverType {
+  public class ResolverTypeType : ResolverType {
     [System.Diagnostics.Contracts.Pure]
     public override string TypeName(DafnyOptions options, ModuleDefinition context, bool parseAble) {
       Contract.Assert(parseAble == false);
       return "#type";
     }
     public override bool Equals(Type that, bool keepConstraints = false) {
-      return that.NormalizeExpand(keepConstraints) is ResolverType_Type;
+      return that.NormalizeExpand(keepConstraints) is ResolverTypeType;
     }
   }
 
-  public Resolver_IdentifierExpr(IOrigin origin, TopLevelDecl decl, List<Type> typeArgs)
+  public ResolverIdentifierExpr(IOrigin origin, TopLevelDecl decl, List<Type> typeArgs)
     : base(origin) {
     Contract.Requires(origin != null);
     Contract.Requires(decl != null);
     Contract.Requires(typeArgs != null && typeArgs.Count == decl.TypeArgs.Count);
     Decl = decl;
     TypeArgs = typeArgs;
-    Type = decl is ModuleDecl ? (Type)new ResolverType_Module() : new ResolverType_Type();
+    Type = decl is ModuleDecl ? (Type)new ResolverTypeModule() : new ResolverTypeType();
     PreType = decl is ModuleDecl ? new PreTypePlaceholderModule() : new PreTypePlaceholderType();
   }
-  public Resolver_IdentifierExpr(IOrigin origin, TypeParameter tp)
+  public ResolverIdentifierExpr(IOrigin origin, TypeParameter tp)
     : this(origin, tp, new List<Type>()) {
     Contract.Requires(origin != null);
     Contract.Requires(tp != null);
@@ -79,7 +79,7 @@ public IEnumerable<Reference> GetReferences() {
     return new[] { new Reference(Center, Decl) };
   }
 
-  public Resolver_IdentifierExpr Clone(Cloner cloner) {
-    return new Resolver_IdentifierExpr(cloner, this);
+  public ResolverIdentifierExpr Clone(Cloner cloner) {
+    return new ResolverIdentifierExpr(cloner, this);
   }
 }

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

@@ -571,12 +571,12 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext,
         if (parensNeeded) { wr.Write("("); }
         if (!e.Lhs.IsImplicit) {
           PrintExpr(e.Lhs, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, -1, keyword);
-          if (e.Lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) {
+          if (e.Lhs.Type is ResolverIdentifierExpr.ResolverTypeType) {
             Contract.Assert(e.Lhs is NameSegment || e.Lhs is ExprDotName);  // these are the only expressions whose .Type can be ResolverType_Type
             if (options.DafnyPrintResolvedFile != null && options.PrintMode == PrintModes.Everything) {
               // The printing of e.Lhs printed the type arguments only if they were given explicitly in the input.
               var optionalTypeArgs = e.Lhs is NameSegment ns ? ns.OptTypeArguments : ((ExprDotName)e.Lhs).OptTypeArguments;
-              if (optionalTypeArgs == null && e.Lhs.Resolved is Resolver_IdentifierExpr ri) {
+              if (optionalTypeArgs == null && e.Lhs.Resolved is ResolverIdentifierExpr ri) {
                 PrintTypeInstantiation(ri.TypeArgs);
               }
             }
@@ -1228,7 +1228,7 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext,
         wr.Write("[BoogieWrapper]");  // this is somewhat unexpected, but we can get here if the /trace switch is used, so it seems best to cover this case here
       } else if (expr is BoogieGenerator.BoogieFunctionCall) {
         wr.Write("[BoogieFunctionCall]");  // this prevents debugger watch window crash
-      } else if (expr is Resolver_IdentifierExpr) {
+      } else if (expr is ResolverIdentifierExpr) {
         wr.Write("[Resolver_IdentifierExpr]");  // we can get here in the middle of a debugging session
       } else if (expr is DecreasesToExpr decreasesToExpr) {
         var opBindingStrength = BindingStrengthDecreasesTo;

Source/DafnyCore/AST/Types/Types.cs

@@ -1145,10 +1145,10 @@ public static bool Equal_Improved(Type a, Type b) {
           return true;
         }
       }
-    } else if (a is Resolver_IdentifierExpr.ResolverType_Module) {
-      return b is Resolver_IdentifierExpr.ResolverType_Module;
-    } else if (a is Resolver_IdentifierExpr.ResolverType_Type) {
-      return b is Resolver_IdentifierExpr.ResolverType_Type;
+    } else if (a is ResolverIdentifierExpr.ResolverTypeModule) {
+      return b is ResolverIdentifierExpr.ResolverTypeModule;
+    } else if (a is ResolverIdentifierExpr.ResolverTypeType) {
+      return b is ResolverIdentifierExpr.ResolverTypeType;
     } else {
       // this is an unexpected type; however, it may be that we get here during the resolution of an erroneous
       // program, so we'll just return false
@@ -2232,7 +2232,7 @@ public void AddSubtype(TypeConstraint c) {
   public enum Family { Unknown, Bool, Char, IntLike, RealLike, Ordinal, BitVector, ValueType, Ref, Opaque }
   public Family family = Family.Unknown;
   public static Family GetFamily(Type t) {
-    Contract.Ensures(Contract.Result<Family>() != Family.Unknown || t is TypeProxy || t is Resolver_IdentifierExpr.ResolverType);  // return Unknown ==> t is TypeProxy || t is ResolverType
+    Contract.Ensures(Contract.Result<Family>() != Family.Unknown || t is TypeProxy || t is ResolverIdentifierExpr.ResolverType);  // return Unknown ==> t is TypeProxy || t is ResolverType
     if (t.IsBoolType) {
       return Family.Bool;
     } else if (t.IsCharType) {

Source/DafnyCore/AST/Types/UserDefinedType.cs

@@ -165,7 +165,7 @@ public UserDefinedType(IOrigin origin, string name, TopLevelDecl cd, [Captured]
     this.TypeArgs = typeArgs;
     if (namePath == null) {
       var ns = new NameSegment(origin, name, typeArgs.Count == 0 ? null : typeArgs);
-      var r = new Resolver_IdentifierExpr(origin, cd, typeArgs);
+      var r = new ResolverIdentifierExpr(origin, cd, typeArgs);
       ns.ResolvedExpression = r;
       ns.Type = r.Type;
       this.NamePath = ns;
@@ -218,7 +218,7 @@ public UserDefinedType(IOrigin origin, TypeParameter tp) : base(origin) {
     this.TypeArgs = new List<Type>();
     this.ResolvedClass = tp;
     var ns = new NameSegment(origin, tp.Name, null);
-    var r = new Resolver_IdentifierExpr(origin, tp);
+    var r = new ResolverIdentifierExpr(origin, tp);
     ns.ResolvedExpression = r;
     ns.Type = r.Type;
     this.NamePath = ns;