Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Feat rust operators #5380

Merged
merged 4 commits into from
Apr 29, 2024
Merged

Feat rust operators #5380

merged 4 commits into from
Apr 29, 2024

Commits on Apr 29, 2024

  1. Feat: Rust operators and immutable collections (#5081) 

    ### 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>
    @MikaelMayer @robin-aws
    MikaelMayer and robin-aws committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    6418399 View commit details
    Browse the repository at this point in the history

  2. Fixed CI

    @MikaelMayer
    MikaelMayer committed Apr 29, 2024
    Configuration menu
    Copy the full SHA
    a6bf008 View commit details
    Browse the repository at this point in the history

  3. Update Source/TestDafny/MultiBackendTest.cs

    @MikaelMayer
    MikaelMayer authored Apr 29, 2024
    Configuration menu
    Copy the full SHA
    9c8242f View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into feat-rust-operators

    @MikaelMayer
    MikaelMayer authored Apr 29, 2024
    Configuration menu
    Copy the full SHA
    e2e9907 View commit details
    Browse the repository at this point in the history