Merge branch 'master' into eraseGhost

dafny-lang · Jan 24, 2025 · 6825577 · 6825577
2 parents c4a4687 + 16afdc8
commit 6825577
Show file tree

Hide file tree

Showing 14 changed files with 4,055 additions and 4,010 deletions.
diff --git a/Makefile b/Makefile
@@ -114,7 +114,7 @@ update-go-module:
 update-runtime-dafny:
 	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)
 
-pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module update-rs-module
+pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module
 
 update-standard-libraries:
 	(cd "${DIR}"; cd Source/DafnyStandardLibraries; make update-binary)

diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
@@ -270,7 +270,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
     /// </summary>
     private string protectedTypeName(TopLevelDecl dt) {
       var protectedName = IdName(dt);
-      if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) {
+      if (dt.EnclosingModuleDefinition.GetCompileName(Options) == protectedName) {
         return $"_{protectedName}";
       }
       return protectedName;

diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-rast.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-rast.dfy
@@ -12,8 +12,8 @@ module RAST
   // Past that, we use Dafny system tuples (see https://www.reddit.com/r/rust/comments/11gvkda/why_rust_std_only_provides_trait_implementation/)
   const MAX_TUPLE_SIZE := 12
 
-  // Default Indentation
-  const IND := "  "
+  // Default Rust-like indentation
+  const IND := "    "
 
   datatype RASTTopDownVisitor<!T(!new)> =
     RASTTopDownVisitor(

diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
@@ -4068,6 +4068,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
     {
       s := "#![allow(warnings, unconditional_panic)]\n";
       s := s + "#![allow(nonstandard_style)]\n";
+      s := s + "#![cfg_attr(any(), rustfmt::skip)]\n"; // Because Rustfmt crashes on some generated files
 
       var externUseDecls := [];
 

diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg
@@ -2391,19 +2391,16 @@ AssignStatement<out Statement/*!*/ s>
        s = new AssignSuchThatStmt(rangeToken, lhss, suchThat, suchThatAssume, null);
      } else if (exceptionRhs != null) {
        s = new AssignOrReturnStmt(rangeToken, lhss, exceptionRhs, keywordToken, rhss);
-       if (proof != null) {
-         s = new BlockByProofStmt(rangeToken, proof, s);
-       }
      } else {
        if (lhss.Count == 0 && rhss.Count == 0) {
          s = new BlockStmt(rangeToken, new List<Statement>()); // error, give empty statement
        } else {
          s = new AssignStatement(rangeToken, lhss, rhss);
-         if (proof != null) {
-           s = new BlockByProofStmt(rangeToken, proof, s);
-         }
        }
      }
+     if (proof != null) {
+       s = new BlockByProofStmt(rangeToken, proof, s);
+     }
   .)
   .
 

diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
@@ -6764,6 +6764,7 @@ public RAST._IExpr Error(Dafny.ISequence<Dafny.Rune> message, RAST._IExpr defaul
       Dafny.ISequence<Dafny.Rune> s = Dafny.Sequence<Dafny.Rune>.Empty;
       s = Dafny.Sequence<Dafny.Rune>.UnicodeFromString("#![allow(warnings, unconditional_panic)]\n");
       s = Dafny.Sequence<Dafny.Rune>.Concat(s, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("#![allow(nonstandard_style)]\n"));
+      s = Dafny.Sequence<Dafny.Rune>.Concat(s, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("#![cfg_attr(any(), rustfmt::skip)]\n"));
       Dafny.ISequence<RAST._IModDecl> _0_externUseDecls;
       _0_externUseDecls = Dafny.Sequence<RAST._IModDecl>.FromElements();
       BigInteger _hi0 = new BigInteger((externalFiles).Count);

diff --git a/Source/DafnyCore/GeneratedFromDafny/RAST.cs b/Source/DafnyCore/GeneratedFromDafny/RAST.cs
@@ -174,7 +174,7 @@ public static RAST._IExpr IntoUsize(RAST._IExpr underlying) {
       return (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyUsize"))).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("into_usize"))).Apply1(underlying);
     }
     public static Dafny.ISequence<Dafny.Rune> IND { get {
-      return Dafny.Sequence<Dafny.Rune>.UnicodeFromString("  ");
+      return Dafny.Sequence<Dafny.Rune>.UnicodeFromString("    ");
     } }
     public static RAST._IType SelfOwned { get {
       return (RAST.Path.create_Self()).AsType();