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

Allow non-reference-type traits #4137

Merged
merged 47 commits into from
Jul 3, 2023
Merged

Allow non-reference-type traits #4137

merged 47 commits into from
Jul 3, 2023

Commits on Jun 5, 2023

  1. Parsing and resolution

    @RustanLeino
    RustanLeino committed Jun 5, 2023
    Configuration menu
    Copy the full SHA
    e861001 View commit details
    Browse the repository at this point in the history

  2. Add verification support

    @RustanLeino
    RustanLeino committed Jun 5, 2023
    Configuration menu
    Copy the full SHA
    73b6431 View commit details
    Browse the repository at this point in the history

  3. Adjust error message wording in .expect files

    @RustanLeino
    RustanLeino committed Jun 5, 2023
    Configuration menu
    Copy the full SHA
    952a34b View commit details
    Browse the repository at this point in the history

  4. Adjust .expect files for verification messages

    @RustanLeino
    RustanLeino committed Jun 5, 2023
    Configuration menu
    Copy the full SHA
    b0d07f2 View commit details
    Browse the repository at this point in the history

  5. Add compilation support

    @RustanLeino
    RustanLeino committed Jun 5, 2023
    Configuration menu
    Copy the full SHA
    d990ba9 View commit details
    Browse the repository at this point in the history

Commits on Jun 6, 2023

  1. Fix up recently added coersions

    @RustanLeino
    RustanLeino committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    f961c73 View commit details
    Browse the repository at this point in the history

  2. Add new tests

    @RustanLeino
    RustanLeino committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    23e9172 View commit details
    Browse the repository at this point in the history

  3. Add tests for issue 4046

    @RustanLeino
    RustanLeino committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    21438a7 View commit details
    Browse the repository at this point in the history

  4. Fix whitespace

    @RustanLeino
    RustanLeino committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    b9f4f39 View commit details
    Browse the repository at this point in the history

  5. Update options doc

    @RustanLeino
    RustanLeino committed Jun 6, 2023
    Configuration menu
    Copy the full SHA
    3e484c0 View commit details
    Browse the repository at this point in the history

Commits on Jun 8, 2023

  1. Adjust wording in expected error in tutorial

    @RustanLeino
    RustanLeino committed Jun 8, 2023
    Configuration menu
    Copy the full SHA
    b91ffee View commit details
    Browse the repository at this point in the history

  2. Update Go runtime with new generated code

    @RustanLeino
    RustanLeino committed Jun 8, 2023
    Configuration menu
    Copy the full SHA
    3e688c9 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into non-reference-traits

    @RustanLeino
    RustanLeino committed Jun 8, 2023
    Configuration menu
    Copy the full SHA
    cefc6de View commit details
    Browse the repository at this point in the history

  4. Correct spelling

    @RustanLeino
    RustanLeino committed Jun 8, 2023
    Configuration menu
    Copy the full SHA
    4883fb3 View commit details
    Browse the repository at this point in the history

  5. Remove p_no_mutable_fields_in_value_types

    @RustanLeino
    RustanLeino committed Jun 8, 2023
    Configuration menu
    Copy the full SHA
    1c15a01 View commit details
    Browse the repository at this point in the history

  6. Add test for p_general_traits_beta

    @RustanLeino
    RustanLeino committed Jun 8, 2023
    Configuration menu
    Copy the full SHA
    3482ada View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' into non-reference-traits

    @RustanLeino
    RustanLeino committed Jun 8, 2023
    Configuration menu
    Copy the full SHA
    43ef4ff View commit details
    Browse the repository at this point in the history

  8. Fix error-catalog template

    @RustanLeino
    RustanLeino committed Jun 8, 2023
    Configuration menu
    Copy the full SHA
    832ee5e View commit details
    Browse the repository at this point in the history

  9. Merge branch 'master' into non-reference-traits 

    # Conflicts:
#	Source/DafnyCore/Resolver/Resolver.cs
#	Source/DafnyCore/Resolver/TypeInferenceChecker.cs
    @RustanLeino
    RustanLeino committed Jun 8, 2023
    Configuration menu
    Copy the full SHA
    6cc241d View commit details
    Browse the repository at this point in the history

  10. Fix merge

    @RustanLeino
    RustanLeino committed Jun 8, 2023
    Configuration menu
    Copy the full SHA
    6a4bac2 View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2023

  1. Fix newtype-with-trait printing in Python, per reveiw comments

    @RustanLeino
    RustanLeino committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    9687c6f View commit details
    Browse the repository at this point in the history

  2. chore: Parameter renaming to simplify merge

    @RustanLeino
    RustanLeino committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    b8de6e0 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into non-reference-traits 

    # Conflicts:
#	Source/DafnyCore/AST/Cloner.cs
#	Source/DafnyCore/AST/Modules/ScopeCloner.cs
#	Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs
#	Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs
#	Source/DafnyCore/Dafny.atg
#	Source/DafnyCore/Resolver/Resolver.cs
#	Source/DafnyCore/Verifier/Translator.ClassMembers.cs
#	Test/dafny0/DividedConstructors.dfy.expect
#	Test/dafny0/MiscTypeInferenceTests.dfy.expect
    @RustanLeino
    RustanLeino committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    11d65c2 View commit details
    Browse the repository at this point in the history

  4. Fix merge

    @RustanLeino
    RustanLeino committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    60af01f View commit details
    Browse the repository at this point in the history

  5. Fix testDafnyForEachCompiler violations

    @RustanLeino
    RustanLeino committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    6279117 View commit details
    Browse the repository at this point in the history

  6. Find moduleInfo elsewhere

    @RustanLeino
    RustanLeino committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    cd341cf View commit details
    Browse the repository at this point in the history

Commits on Jun 30, 2023

  1. Merge branch 'master' into non-reference-traits 

    # Conflicts:
#	Source/DafnyCore/Verifier/Translator.cs
    @RustanLeino
    RustanLeino committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    05f6742 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into non-reference-traits

    @RustanLeino
    RustanLeino committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    6ccf0fd View commit details
    Browse the repository at this point in the history

  3. Report C++’s lack of trait support to TestDafny

    @RustanLeino
    RustanLeino committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    9d5baf2 View commit details
    Browse the repository at this point in the history

  4. Speed up test

    @RustanLeino
    RustanLeino committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    bdad171 View commit details
    Browse the repository at this point in the history

Commits on Jul 1, 2023

  1. Merge branch 'master' into non-reference-traits

    @RustanLeino
    RustanLeino committed Jul 1, 2023
    Configuration menu
    Copy the full SHA
    408efd0 View commit details
    Browse the repository at this point in the history

  2. Fix merge

    @RustanLeino
    RustanLeino committed Jul 1, 2023
    Configuration menu
    Copy the full SHA
    086b484 View commit details
    Browse the repository at this point in the history

Commits on Jul 3, 2023

  1. Update docs/HowToFAQ/Errors-Parser.template 

    Co-authored-by: Fabio Madge <[email protected]>
    @RustanLeino @fabiomadge
    RustanLeino and fabiomadge authored Jul 3, 2023
    Configuration menu
    Copy the full SHA
    e17b252 View commit details
    Browse the repository at this point in the history

  2. Update docs/DafnyRef/Options.txt 

    Co-authored-by: Fabio Madge <[email protected]>
    @RustanLeino @fabiomadge
    RustanLeino and fabiomadge authored Jul 3, 2023
    Configuration menu
    Copy the full SHA
    a835cde View commit details
    Browse the repository at this point in the history

  3. Update Test/traits/NonReferenceTraitsCompile.dfy 

    Co-authored-by: Fabio Madge <[email protected]>
    @RustanLeino @fabiomadge
    RustanLeino and fabiomadge authored Jul 3, 2023
    Configuration menu
    Copy the full SHA
    fa2f8a4 View commit details
    Browse the repository at this point in the history

  4. Update Test/traits/NonReferenceTraits.dfy 

    Co-authored-by: Fabio Madge <[email protected]>
    @RustanLeino @fabiomadge
    RustanLeino and fabiomadge authored Jul 3, 2023
    Configuration menu
    Copy the full SHA
    ef5b66e View commit details
    Browse the repository at this point in the history

  5. Update Source/DafnyCore/AST/Modules/ModuleDefinition.cs 

    Co-authored-by: Fabio Madge <[email protected]>
    @RustanLeino @fabiomadge
    RustanLeino and fabiomadge authored Jul 3, 2023
    Configuration menu
    Copy the full SHA
    9213570 View commit details
    Browse the repository at this point in the history

  6. Update Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameR… 

    …esolutionAndTypeInference.cs

Co-authored-by: Fabio Madge <[email protected]>
    @RustanLeino @fabiomadge
    RustanLeino and fabiomadge authored Jul 3, 2023
    Configuration menu
    Copy the full SHA
    4a900e7 View commit details
    Browse the repository at this point in the history

  7. Update Source/DafnyCore/Compilers/Java/Compiler-java.cs 

    Co-authored-by: Fabio Madge <[email protected]>
    @RustanLeino @fabiomadge
    RustanLeino and fabiomadge authored Jul 3, 2023
    Configuration menu
    Copy the full SHA
    c88fb15 View commit details
    Browse the repository at this point in the history

  8. Update Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameR… 

    …esolutionAndTypeInference.cs

Co-authored-by: Fabio Madge <[email protected]>
    @RustanLeino @fabiomadge
    RustanLeino and fabiomadge authored Jul 3, 2023
    Configuration menu
    Copy the full SHA
    f21d7c1 View commit details
    Browse the repository at this point in the history

  9. Act on PR comments

    @RustanLeino
    RustanLeino committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    dc33d45 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'master' into non-reference-traits

    @RustanLeino
    RustanLeino committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    4c87084 View commit details
    Browse the repository at this point in the history

  11. Change wording in error message

    @RustanLeino
    RustanLeino committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    1efca99 View commit details
    Browse the repository at this point in the history

  12. Adjust line numbers in .expect file

    @RustanLeino
    RustanLeino committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    023f848 View commit details
    Browse the repository at this point in the history

  13. Make test what it what meant to be

    @RustanLeino
    RustanLeino committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    148f93b View commit details
    Browse the repository at this point in the history

  14. Fix message in error-message testing (parsing)

    @RustanLeino
    RustanLeino committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    5cd1185 View commit details
    Browse the repository at this point in the history

  15. Account for changed wording in error messages

    @RustanLeino
    RustanLeino committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    c0e4279 View commit details
    Browse the repository at this point in the history