-
Notifications
You must be signed in to change notification settings - Fork 261
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This PR is a replay of #5081 after fixing the issue with the paths too long for Windows, so it should no longer break the CI. ### Description This PR implements most immutable types in Dafny (Sequence, Set, Multiset, Map) and implements most if not all operators on them. It also sets an architecture that can now be relied on. List of features in this PR: - More comprehensive Rust AST, precedence and associativity to render parentheses - The Rust compiler no longer crash when not in /runAllTests, but emits invalid code. It makes it possible to see which features are missing by searching for `<i>` in the generated code. - Made verification of GenExpr less brittle - Previous PR review comments - Ability to use shadowed identifiers to avoid numbers in names. Rust has the same rules as Dafny for shadowing, and I will continue to monitor cases where semantics might differ. ### How has this been tested? I added an integration test for compiling Dafny to Rust, and I added unit tests for the runtime in Rust *All tests for each compiler now have a `.rs.check` if they fail.*. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
- Loading branch information
1 parent
1be1cba
commit 0b629ea
Showing
328 changed files
with
33,378 additions
and
23,491 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
using System.Collections.Concurrent; | ||
using Microsoft.Dafny; | ||
|
||
namespace DafnyCore.Test; | ||
|
||
public class GeneratedDafnyTest { | ||
[Fact] | ||
public void TestDafnyGeneratedCode() { | ||
DafnyToRustCompilerCoverage.RASTCoverage.__default.TestExpr(); | ||
} | ||
} |
162 changes: 162 additions & 0 deletions
162
Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage_RASTCoverage.cs
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.